Robust sampling for MITL specifications

Georgios Fainekos, George J. Pappas

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

21 Citations (Scopus)

Abstract

Real-time temporal logic reasoning about trajectories of physical systems necessitates models of time which are continuous. However, discrete time temporal logic reasoning is computationally more efficient than continuous time. Moreover, in a number of engineering applications only discrete time models are available for analysis. In this paper, we introduce a framework for testing MITL specifications on continuous time signals using only discrete time analysis. The motivating idea behind our approach is that if the dynamics of the signal fulfills certain conditions and the discrete time signal robustly satisfies the MITL specification, then the corresponding continuous time signal should also satisfy the same MITL specification.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages147-162
Number of pages16
Volume4763 LNCS
StatePublished - 2007
Externally publishedYes
Event5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007 - Salzburg, Austria
Duration: Oct 3 2007Oct 5 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4763 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007
CountryAustria
CitySalzburg
Period10/3/0710/5/07

Fingerprint

Temporal logic
Specification
Sampling
Specifications
Continuous Time
Discrete-time
Temporal Logic
Reasoning
Discrete-time Model
Engineering Application
Trajectories
Testing
Trajectory
Real-time
Model

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Fainekos, G., & Pappas, G. J. (2007). Robust sampling for MITL specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4763 LNCS, pp. 147-162). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4763 LNCS).

Robust sampling for MITL specifications. / Fainekos, Georgios; Pappas, George J.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4763 LNCS 2007. p. 147-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4763 LNCS).

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

Fainekos, G & Pappas, GJ 2007, Robust sampling for MITL specifications. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 4763 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4763 LNCS, pp. 147-162, 5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS 2007, Salzburg, Austria, 10/3/07.
Fainekos G, Pappas GJ. Robust sampling for MITL specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4763 LNCS. 2007. p. 147-162. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Fainekos, Georgios ; Pappas, George J. / Robust sampling for MITL specifications. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4763 LNCS 2007. pp. 147-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a4423c9a01cd4207b835342bd4b8fec4,
title = "Robust sampling for MITL specifications",
abstract = "Real-time temporal logic reasoning about trajectories of physical systems necessitates models of time which are continuous. However, discrete time temporal logic reasoning is computationally more efficient than continuous time. Moreover, in a number of engineering applications only discrete time models are available for analysis. In this paper, we introduce a framework for testing MITL specifications on continuous time signals using only discrete time analysis. The motivating idea behind our approach is that if the dynamics of the signal fulfills certain conditions and the discrete time signal robustly satisfies the MITL specification, then the corresponding continuous time signal should also satisfy the same MITL specification.",
author = "Georgios Fainekos and Pappas, {George J.}",
year = "2007",
language = "English (US)",
isbn = "9783540754534",
volume = "4763 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "147--162",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Robust sampling for MITL specifications

AU - Fainekos, Georgios

AU - Pappas, George J.

PY - 2007

Y1 - 2007

N2 - Real-time temporal logic reasoning about trajectories of physical systems necessitates models of time which are continuous. However, discrete time temporal logic reasoning is computationally more efficient than continuous time. Moreover, in a number of engineering applications only discrete time models are available for analysis. In this paper, we introduce a framework for testing MITL specifications on continuous time signals using only discrete time analysis. The motivating idea behind our approach is that if the dynamics of the signal fulfills certain conditions and the discrete time signal robustly satisfies the MITL specification, then the corresponding continuous time signal should also satisfy the same MITL specification.

AB - Real-time temporal logic reasoning about trajectories of physical systems necessitates models of time which are continuous. However, discrete time temporal logic reasoning is computationally more efficient than continuous time. Moreover, in a number of engineering applications only discrete time models are available for analysis. In this paper, we introduce a framework for testing MITL specifications on continuous time signals using only discrete time analysis. The motivating idea behind our approach is that if the dynamics of the signal fulfills certain conditions and the discrete time signal robustly satisfies the MITL specification, then the corresponding continuous time signal should also satisfy the same MITL specification.

UR - http://www.scopus.com/inward/record.url?scp=38149116993&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=38149116993&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:38149116993

SN - 9783540754534

VL - 4763 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 147

EP - 162

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -