Paper Info
Title
From LTL to rLTL monitoring: improved monitorability through robust semantics
Abstract
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, a robust semantics for LTL was introduced to capture different degrees by wich a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring --- such as the realizability of all truth values --- can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation.
Year
DOI
Venue
2020
10.1145/3365365.3382197
arXiv: Formal Languages and Automata Theory
Keywords
DocType
Volume
Runtime Monitoring, Linear Temporal Logic, Robustness
Conference
59
Issue
ISSN
ISBN
1-3
0925-9856
978-1-4503-7018-9
Citations 
PageRank 
References 
0
0.34
2
Authors
6
Name
Order
Citations
PageRank
Corto Mascle100.34
Daniel Neider215321.97
Maximilian Schwenger320.70
Paulo Tabuada44281264.80
Alexander Weinert572.22
Martin Zimmermann 000263510.88