TY - GEN
T1 - Temporal logic verification using simulation
AU - Fainekos, Georgios E.
AU - Girard, Antoine
AU - Pappas, George J.
PY - 2006
Y1 - 2006
N2 - 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 neighborhood of the simulated one satisfy the same temporal specification as the simulated trajectory. The interesting and promising feature of our 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.
AB - 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 neighborhood of the simulated one satisfy the same temporal specification as the simulated trajectory. The interesting and promising feature of our 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.
UR - http://www.scopus.com/inward/record.url?scp=33750282529&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33750282529&partnerID=8YFLogxK
U2 - 10.1007/11867340_13
DO - 10.1007/11867340_13
M3 - Conference contribution
AN - SCOPUS:33750282529
SN - 3540450262
SN - 9783540450269
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 171
EP - 186
BT - Formal Modeling and Analysis of Timed Systems - 4th International Conference, FORMATS 2006, Proceedings
PB - Springer Verlag
T2 - 4th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2006
Y2 - 25 September 2006 through 27 September 2006
ER -