Robustness of temporal logic specifications

Georgios E. Fainekos, George J. Pappas

Research output: Chapter in Book/Report/Conference proceedingConference contribution

45 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 languageEnglish (US)
Title of host publicationFormal Approaches to Software Testing and Runtime Verification - First Combined International Workshops FATES 2006 and RV 2006, Revised Selected Papers
Pages178-192
Number of pages15
DOIs
StatePublished - Dec 1 2006
Externally publishedYes
Event1st Combined International Workshop on Formal Approaches to Software Testing and Runtime Verification, FATES and RV 2006 - Seattle, WA, United States
Duration: Aug 15 2006Aug 16 2006

Publication series

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

Other

Other1st Combined International Workshop on Formal Approaches to Software Testing and Runtime Verification, FATES and RV 2006
CountryUnited States
CitySeattle, WA
Period8/15/068/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)

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). https://doi.org/10.1007/11940197-12