On-line monitoring for temporal logic robustness

Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos

Research output: Contribution to journalArticle

28 Citations (Scopus)

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 languageEnglish (US)
Pages (from-to)231-246
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8734
StatePublished - 2014

Fingerprint

Temporal logic
Temporal Logic
Simulink
Monitoring
Robustness
Specifications
Dynamic programming
Specification
On-line Monitoring
Time Operator
Dynamic Programming
Trace
Metric
Operator
Demonstrate
Model
Cyber Physical System

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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",
year = "2014",
language = "English (US)",
volume = "8734",
pages = "231--246",
journal = "Lecture Notes in Computer Science",
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

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

M3 - Article

VL - 8734

SP - 231

EP - 246

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -