Robustness of temporal logic specifications for continuous-time signals

Georgios Fainekos, George J. Pappas

Research output: Contribution to journalArticle

174 Citations (Scopus)

Abstract

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.

Original languageEnglish (US)
Pages (from-to)4262-4291
Number of pages30
JournalTheoretical Computer Science
Volume410
Issue number42
DOIs
StatePublished - Sep 28 2009
Externally publishedYes

Fingerprint

Temporal logic
Temporal Logic
Continuous Time
Specification
Robustness
Specifications
Metric
Discrete-time
Semantics
Boolean Satisfiability
Metric space
System Performance
Fragment
Closed
Testing
Interval

Keywords

  • Linear and metric temporal logic
  • Metric spaces
  • Robustness
  • Testing

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Robustness of temporal logic specifications for continuous-time signals. / Fainekos, Georgios; Pappas, George J.

In: Theoretical Computer Science, Vol. 410, No. 42, 28.09.2009, p. 4262-4291.

Research output: Contribution to journalArticle

@article{1787f6d24c5446d78da9ae5328ec561f,
title = "Robustness of temporal logic specifications for continuous-time signals",
abstract = "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.",
keywords = "Linear and metric temporal logic, Metric spaces, Robustness, Testing",
author = "Georgios Fainekos and Pappas, {George J.}",
year = "2009",
month = "9",
day = "28",
doi = "10.1016/j.tcs.2009.06.021",
language = "English (US)",
volume = "410",
pages = "4262--4291",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "42",

}

TY - JOUR

T1 - Robustness of temporal logic specifications for continuous-time signals

AU - Fainekos, Georgios

AU - Pappas, George J.

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

VL - 410

SP - 4262

EP - 4291

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 42

ER -