Achievements

  • Given the dynamical and unpredictable behaviour of the environment, it is crucial for programs to be robust against uncertainties and perturbations. This means that we want to measure the capability of a program to tolerate modifications in the environmental conditions and still fulfill its tasks. To this purpose, we need to compare the behaviour of the system with its behaviour under the effect of perturbations, possibly at different moments in time. In other words, whenever we require a system to be robust against perturbations, we are actually specifying a temporal property of distances between systems behaviours. Hence, we have developed the Robustness Temporal Logic (RobTL), the first ever temporal logic allowing for the specification of robustness properties.

  • We have developed the Software Tool for the Analysis of Robustness in the unKnown environment (STARK) that includes:

    • Specification language for the system (programs, environment, and their interaction)

    • Specification language for perturbations

    • Statistical algorithm for the estimation of evolution sequences and their perturbed versions

    • Statistical algorithm for the evaluation of RobTL expressions (including the evaluation of confidence intervals)

    • Model checker for RobTL formulae (with both, a classic and a three-valued semantics)

  • We have introduced the Evolution Temporal Logic (EvTL), a stochastic extension of the Signal Temporal Logic allowing us to specify properties of the probability distributions describing the transient behaviour of systems, and to include the presence of uncertainties in the specification.

We have equipped EvTL with a real-valued semantics which is sound and complete with respect to the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one.