  We propose the Robustness Temporal Logic (RobTL), a novel temporal logic for
the specification and analysis of distances between the behaviours of
Cyber-Physical Systems (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. Since 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. Given the probabilistic nature of CPSs, our model
checking algorithm for RobTL specifications is based on statistical inference.
As an example of an application of our framework, we consider a supervised,
self-coordinating engine system that is subject to attacks aimed at inflicting
overstress of equipment.
