Robustness of Temporal Logic Specifications

Temporal logic verification has been proven to be a successful tool for the analysis of software and hardware systems. For such systems, both the models and the logic are Boolean valued. In the past, similar successful results have been derived for timed and linear hybrid systems. Even though the states of these systems are real valued, temporal logics are still interpreted over Boolean signals that abstract away the actual values of the real-valued state variables. In this thesis, we advocate that in certain cases it is beneficial to define multi-valued semantics for temporal logics. That is, we consider a robust interpretation of Metric Temporal Logic (MTL) formulas over signals that take values in metric spaces. For such signals, which are generated by systems whose states are equipped with nontrivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. The proposed multi-valued semantics for MTL formulas captures not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance from unsatisfiability. This, in turn, enables the definition of robustness tubes that contain signals with the same temporal properties. The notion of robustness for MTL specifications can be applied to at least 3 important problems. The first problem is the verification of continuous time signals with respect to MTL specifications using only discrete time analysis. The motivating idea behind our approach is that if the continuous time signal fulfills certain conditions and the discrete time signal robustly satisfies the MTL specification, then the corresponding continuous time signal should also satisfy the same MTL specification. Second, the proposed robustness framework can be applied to the problem of bounded time temporal logic verification of dynamical systems. Our methodology has the distinctive feature that enables the verification of temporal properties of a dynamical system by checking only a finite number of its (simulated) trajectories. The interesting and promising feature of this approach is that the more robust the system is with respect to the temporal logic specification, the less is the number of simulations that are required in order to verify the system. Finally, the proposed definition of robustness for temporal logic specifications can be applied to the problem of automatic synthesis of hybrid systems. In particular, we address the problem of temporal logic motion planning for mobile robots that are modeled by second order dynamics. Temporal logic specifications can capture the usual control specifications such as reachability and invariance as well as more complex specifications like sequencing and obstacle avoidance. The resulting continuous time trajectory is provably guaranteed to satisfy the user specification.