On-line monitoring for temporal logic robustness

Adel Dokhanchi; Bardh Hoxha; Georgios Fainekos

doi:10.1007/978-3-319-11164-3_19

On-line monitoring for temporal logic robustness

Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

Research output: Contribution to journal › Article › peer-review

77 Scopus citations

Abstract

In this paper, we provide a Dynamic Programming algorithm for online monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators (MTL^<+∞_+pt) over sampled traces of Cyber-Physical Systems.We implemented our tool inMatlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL^<+∞_+pt robustness monitoring is acceptable for certain classes of practical specifications.

Original language	English (US)
Pages (from-to)	231-246
Number of pages	16
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8734
DOIs	https://doi.org/10.1007/978-3-319-11164-3_19
State	Published - 2014

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-11164-3_19

Cite this

@article{324dfed494824fe491aa5fb0716e227f,

title = "On-line monitoring for temporal logic robustness",

abstract = "In this paper, we provide a Dynamic Programming algorithm for online monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators (MTL<+∞+pt) over sampled traces of Cyber-Physical Systems.We implemented our tool inMatlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL<+∞+pt robustness monitoring is acceptable for certain classes of practical specifications.",

author = "Adel Dokhanchi and Bardh Hoxha and Georgios Fainekos",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2014.",

year = "2014",

doi = "10.1007/978-3-319-11164-3_19",

language = "English (US)",

volume = "8734",

pages = "231--246",

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

issn = "0302-9743",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - On-line monitoring for temporal logic robustness

AU - Dokhanchi, Adel

AU - Hoxha, Bardh

AU - Fainekos, Georgios

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2014.

PY - 2014

Y1 - 2014

N2 - In this paper, we provide a Dynamic Programming algorithm for online monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators (MTL<+∞+pt) over sampled traces of Cyber-Physical Systems.We implemented our tool inMatlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL<+∞+pt robustness monitoring is acceptable for certain classes of practical specifications.

AB - In this paper, we provide a Dynamic Programming algorithm for online monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators (MTL<+∞+pt) over sampled traces of Cyber-Physical Systems.We implemented our tool inMatlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL<+∞+pt robustness monitoring is acceptable for certain classes of practical specifications.

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

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

U2 - 10.1007/978-3-319-11164-3_19

DO - 10.1007/978-3-319-11164-3_19

M3 - Article

AN - SCOPUS:84921789024

SN - 0302-9743

VL - 8734

SP - 231

EP - 246

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

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

ER -

On-line monitoring for temporal logic robustness

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this