TY - GEN
T1 - Robustness of temporal logic specifications
AU - Fainekos, Georgios E.
AU - Pappas, George J.
PY - 2006
Y1 - 2006
N2 - In this paper, we consider the robust interpretation of metric temporal logic (MTL) formulas over timed sequences of states. For systems whose states are equipped with nontrivial metrics, such as continuous, hybrid, or general metric transition systems, robustness is not only natural, but also a critical measure of system performance. In this paper, we define robust, multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance, ε, from unsatisfiability. We prove that any other timed trace which remains ε-close to the initial one also satisfies the same MTL specification with the usual Boolean semantics. We derive a computational procedure for determining an under-approximation to the robustness degree ε of the specification with respect to a given finite timed state sequence. Our approach can be used for robust system simulation and testing, as well as form the basis for simulation-based verification.
AB - In this paper, we consider the robust interpretation of metric temporal logic (MTL) formulas over timed sequences of states. For systems whose states are equipped with nontrivial metrics, such as continuous, hybrid, or general metric transition systems, robustness is not only natural, but also a critical measure of system performance. In this paper, we define robust, multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance, ε, from unsatisfiability. We prove that any other timed trace which remains ε-close to the initial one also satisfies the same MTL specification with the usual Boolean semantics. We derive a computational procedure for determining an under-approximation to the robustness degree ε of the specification with respect to a given finite timed state sequence. Our approach can be used for robust system simulation and testing, as well as form the basis for simulation-based verification.
KW - Metric and linear temporal logic
KW - Metric spaces
KW - Monitoring
KW - Robustness
KW - Timed state sequences
UR - http://www.scopus.com/inward/record.url?scp=38049156042&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38049156042&partnerID=8YFLogxK
U2 - 10.1007/11940197_12
DO - 10.1007/11940197_12
M3 - Conference contribution
AN - SCOPUS:38049156042
SN - 3540496998
SN - 9783540496991
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 178
EP - 192
BT - Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers
PB - Springer Verlag
T2 - 1st Combined International Workshop on Formal Approaches to Software Testing and Runtime Verification, FATES and RV 2006
Y2 - 15 August 2006 through 16 August 2006
ER -