The principal objective of our ongoing IRF project “Programs in the wild: Uncertainties, adaptability, and verification” is to provide a formal framework and tools for modelling and verifying the behaviour of systems characterised by a close interaction of a program with an unpredictable environment, like Cyber-Physical Systems (CPSs).
In this talk we will discuss the Robustness Temporal Logic (RobTL), a novel temporal logic for the specification and analysis of distances between the behaviours of CPSs over a finite time horizon. Differently from classical temporal logic expressing properties on the behaviour of a system, we can use RobTL specifications to measure the differences in the behaviours of systems with respect to various objectives and temporal constraints, and to study how those differences evolve in time.

As the behaviour of CPSs is inevitably subject to uncertainties and approximations, we show how the unique features of RobTL allow us to specify property of robustness of systems against perturbations, i.e., their capability to function correctly even under the effect of perturbations.