Robustness of Temporal Logic Specifications! Why?

Model checking has been proven to be a very useful tool for the verification of software and hardware systems. The tools and methodologies developed for such systems do not naturally extend to systems whose state space is some general infinite space, for example continuous and hybrid systems. In this case, the model checking problem becomes harder and in most of the cases is undecidable. In practice, the validation of such systems still relies heavily on methods that involve systematic testing. More recently, temporal logic testing has been proposed as a framework that can provide us with additional information about the properties of continuous or discrete time signals.

However, the classical approaches to the temporal logic testing involve a Boolean abstraction of the value of the signal with respect to the atomic propositions in the formula. This loss of information can be quite critical when we consider systems that model or control physical processes. For example, consider the signals s1 and s2 in Fig. 1. Both of them satisfy the same specification if the value of the signal drops below -10, then it should also raise above 10 within 2 time units. Nevertheless, a visual inspection of Fig. 1 indicates that there exists a qualitative difference between s1 and s2. The later barely satisfies the specification. Indeed as we can see in Fig. 2, adding a bounded noise on s2 renders the property unsatisfiable on s2. In order to differentiate between such trajectories of a system, in [5] we introduced the concept of robustness estimate. Informally, the robustness estimate is a bound on the perturbation that the signal can tolerate without changing the truth value of a specification expressed in the Linear or Metric Temporal Logic. For example, signal s1 in Fig. 1 has robustness estimate 5 and signal s2 has robustness estimate 0.5.

Figure 1

Figure 2

What is TaLiRo?

TaLiRo computes the robustness estimate of a temporal logic specification (LTL or MTL) over a finite timed state sequence, that is, a bounded duration discrete time signal marked with timestamps. Determining the robustness estimate of a signal is useful in cases where the system has known bounded measurement noise and bias. The robustness estimate has also been proven useful in temporal logic verification of dynamical systems [1,4] and in continuous time reasoning using discrete time methods [2,3].

Some References

The complete list of related publications can be found on the publications page.

1. MTL Robust Testing and Verification for LPV Systems (pdf, bib),
   Georgios E. Fainekos and George J. Pappas,
   In the Proceedings of the 2009 American Control Conference, St. Louis, Missouri, June 2009
   
2. Robustness of temporal logic specifications for continuous-time signals (pdf, bib),
   Georgios E. Fainekos and George J. Pappas,
   Theoretical Computer Science, Elsevier, V 410, N 42, pp 4262-4291, 2009.
3. Robust Sampling for MITL Specifications (pdf, bib),
   Georgios E. Fainekos and George J. Pappas,
   In the 5th Inter. Conference on Formal Modelling and Analysis of Timed Systems, Salzburg, Austria, October 2007
4. Temporal logic verification using simulation (pdf, bib),
   Georgios E. Fainekos, Antoine Girard and George J. Pappas,
   In the 4th Inter. Conference on Formal Modelling and Analysis of Timed Systems, Paris, France, September 2006
5. Robustness of Temporal Logic Specifications (pdf, bib),
   Georgios E. Fainekos and George J. Pappas,
   In the Workshop on Formal Approaches to Testing and Runtime Verification, Seattle, USA, August 2006
6. Robustness of Temporal Logic Specifications for Finite State Sequences in Metric Spaces (bib),
   Georgios E. Fainekos and George J. Pappas,
   Technical Report MS-CIS-06-05, Department of CIS, University of Pennsylvania, May 2006