TY - JOUR
T1 - Robustness of temporal logic specifications for continuous-time signals
AU - Fainekos, Georgios E.
AU - Pappas, George J.
N1 - Funding Information:
I This research has been partially supported by NSF EHS 0311123, NSF ITR 0324977 and ARO MURI DAAD 19-02-01-0383. Preliminary results of this work have appeared in [G.E. Fainekos, G.J. Pappas, Robustness of temporal logic specifications, in: Formal Approaches to Testing and Runtime Verification, in: LNCS, vol. 4262, Springer, 2006] and [G.E. Fainekos, G.J. Pappas, Robust sampling for MITL specifications, in: J.-F. Raskin, P.S. Thiagarajan (Eds.),
PY - 2009/9/28
Y1 - 2009/9/28
N2 - In this paper, we consider the 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 non-trivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we propose 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 signal that remains ε-close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. Finally, our framework is applied to the problem of testing formulas of two fragments of MTL, namely Metric Interval Temporal Logic (MITL) and closed Metric Temporal Logic (clMTL), over continuous-time signals 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 temporal logic specification, then the corresponding continuous-time signal should also satisfy the same temporal logic specification.
AB - In this paper, we consider the 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 non-trivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we propose 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 signal that remains ε-close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. Finally, our framework is applied to the problem of testing formulas of two fragments of MTL, namely Metric Interval Temporal Logic (MITL) and closed Metric Temporal Logic (clMTL), over continuous-time signals 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 temporal logic specification, then the corresponding continuous-time signal should also satisfy the same temporal logic specification.
KW - Linear and metric temporal logic
KW - Metric spaces
KW - Robustness
KW - Testing
UR - http://www.scopus.com/inward/record.url?scp=69649100075&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=69649100075&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2009.06.021
DO - 10.1016/j.tcs.2009.06.021
M3 - Article
AN - SCOPUS:69649100075
SN - 0304-3975
VL - 410
SP - 4262
EP - 4291
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 42
ER -