Robustness of temporal logic specifications

Georgios E. Fainekos; George J. Pappas

doi:10.1007/11940197_12

Robustness of temporal logic specifications

Georgios E. Fainekos, George J. Pappas

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

51 Scopus citations

Abstract

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.

Original language	English (US)
Title of host publication	Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers
Publisher	Springer Verlag
Pages	178-192
Number of pages	15
ISBN (Print)	3540496998, 9783540496991
DOIs	https://doi.org/10.1007/11940197_12
State	Published - 2006
Externally published	Yes
Event	1st Combined International Workshop on Formal Approaches to Software Testing and Runtime Verification, FATES and RV 2006 - Seattle, WA, United States Duration: Aug 15 2006 → Aug 16 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4262 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	1st Combined International Workshop on Formal Approaches to Software Testing and Runtime Verification, FATES and RV 2006
Country	United States
City	Seattle, WA
Period	8/15/06 → 8/16/06

Keywords

Metric and linear temporal logic
Metric spaces
Monitoring
Robustness
Timed state sequences

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/11940197_12

Fingerprint Dive into the research topics of 'Robustness of temporal logic specifications'. Together they form a unique fingerprint.

Cite this

Fainekos, G. E., & Pappas, G. J. (2006). Robustness of temporal logic specifications. In Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers (pp. 178-192). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4262 LNCS). Springer Verlag. https://doi.org/10.1007/11940197_12

Robustness of temporal logic specifications. / Fainekos, Georgios E.; Pappas, George J.

Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers. Springer Verlag, 2006. p. 178-192 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4262 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Fainekos, GE & Pappas, GJ 2006, Robustness of temporal logic specifications. in Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4262 LNCS, Springer Verlag, pp. 178-192, 1st Combined International Workshop on Formal Approaches to Software Testing and Runtime Verification, FATES and RV 2006, Seattle, WA, United States, 8/15/06. https://doi.org/10.1007/11940197_12

Fainekos GE, Pappas GJ. Robustness of temporal logic specifications. In Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers. Springer Verlag. 2006. p. 178-192. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/11940197_12

Fainekos, Georgios E. ; Pappas, George J. / Robustness of temporal logic specifications. Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers. Springer Verlag, 2006. pp. 178-192 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{43eab15be807482d97099c9b32707926,

title = "Robustness of temporal logic specifications",

abstract = "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.",

keywords = "Metric and linear temporal logic, Metric spaces, Monitoring, Robustness, Timed state sequences",

author = "Fainekos, {Georgios E.} and Pappas, {George J.}",

note = "Copyright: Copyright 2021 Elsevier B.V., All rights reserved.; 1st Combined International Workshop on Formal Approaches to Software Testing and Runtime Verification, FATES and RV 2006 ; Conference date: 15-08-2006 Through 16-08-2006",

year = "2006",

doi = "10.1007/11940197_12",

language = "English (US)",

isbn = "3540496998",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "178--192",

booktitle = "Formal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers",

}

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 -