PI: Alexandra Silva, Co-Is: Fredrik Dahlqvist and Renato Neves, University College London

  • It is usually insufficient to tell whether two programs are equivalent or not.
  • In cyber-physical programming, particularly, it is important to tell “how close” are two programs of being equivalent to each other.
  • Our approach uses algebraic reasoning mechanisms to achieve precisely that.
  • Applications of our work include real-time and probabilistic programs.

Championed as a core ingredient of the twenty-first century technology, cyber-physical systems intertwine digital computation with continuous, physical processes and possess a wide range of application domains. They are found not only in small medical devices, such as pacemakers and insulin pumps, but also in networks of autonomous vehicles and district-wide electric grids. They are also used in the analysis of biological mechanisms such as disease propagation and personalised treatments against cancer.

The presence of physical processes, however, hinders an effective use of classical programming notions and techniques. A most basic case is the classical notion of program equivalence, which in the presence of continuous behaviour becomes too strict, for it requires that two programs behave in exactly the same way for a continuous range of possible values.

Whilst there have been recent important developments in cyber-physical program semantics there are currently no algebraic methods for telling `how close’ are two programs of being equivalent to each other. This is where our project aims to make progress.  Specifically, we aim at providing useful notions of distance between cyber-physical programs and subsequently developing corresponding axiomatisations for reasoning about approximate program equivalence.

We are targeting two specific families of cyber-physical programs: real-time and probabilistic programs. In the first case it is useful to tell how close are the execution times of two programs, for instance in the setting where time constraints and synchronisation mechanisms are a main concern (e.g. cruise control systems and platoon vehicles). In the second case it is useful to tell how close are the probabilities of two programs producing a specific output, with applications in e.g., machine learning and noise-aware quantum programming.

Our current results include a complete, generic algebraic system for reasoning about approximate equivalence that is applicable to both real-time and probabilistic programs.

PUBLICATION. Fredrik Dahlqvist and Renato Neves, “An Internal Language for Categories Enriched over Generalised Metric Spaces” (CSL’22)

IMPACT. This project proposal is concretely motivated by R. Neves’ participation in the scientific projects DaVinci and Klee, which have extensive industrial collaborations. The former concerns coordination of components in the cyber-physical domain and collaborates with the Belgian company Altreonic (specialised in the development of vehicular systems). The latter concerns synthesis and analysis of biological systems via hybrid programming techniques, and collaborates with Silicolife (a company specialised in industrial biotechnology). Notions of approximate equivalence are critical in vehicular systems (for instance to compare the speeds attained by two cruise controllers) and in biological systems due to the presence of noise in sensors and actuators.