From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics
Corto Mascle, Daniel Neider, Maximilian Schwenger, Paulo Tabuada, Alexander Weinert, Martin Zimmermann
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical systems by observing run prefixes of the system. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties, which is 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 be satisfied and violated. However, a wide range of formulas are not monitorable under this approach, meaning that every prefix is undetermined. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, robust semantics for LTL were introduced to capture degrees of violation of universal properties. Here, we define robust semantics for run prefixes and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we show that properties expressed with the robust semantics can be monitored by deterministic automata.
23rd ACM International Conference on Hybrid Systems - Computation and Control (HSCC 2020).