Temporal Logic Verification Using Simulation

6 years 12 months ago
Temporal Logic Verification Using Simulation
In this paper, we consider a novel approach to the temporal logic verification problem of continuous dynamical systems. Our methodology has the distinctive feature that enables the verification of the temporal properties of a continuous system by verifying only a finite number of its (simulated) trajectories. The proposed framework comprises two main ideas. First, we take advantage of the fact that in metric spaces we can quantify how close are two different states. Based on that, we define robust, multi-valued semantics for MTL (and LTL) formulas. These capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance from unsatisfiability. Second, we use the recently developed notion of bisimulation functions to infer the behavior of a set of trajectories that lie in the neighborhood of the simulated one. If the latter set of trajectories is bounded by the tube of robustness, then we can infer that all the trajectories in the ne...
Georgios E. Fainekos, Antoine Girard, George J. Pa
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Authors Georgios E. Fainekos, Antoine Girard, George J. Pappas
Comments (0)