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)|
|Number of pages||16|
|Journal||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|State||Published - 2014|
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)