From LTL to rLTL Monitoring: Improved Monitorability Through Robust Semantics

Mascle, Corto and Neider, Daniel and Schwenger, Maximilian and Tabuada, Paulo and Weinert, Alexander and Zimmermann, Martin
(2020) From LTL to rLTL Monitoring: Improved Monitorability Through Robust Semantics.
In: HSCC 2020, April 21-14 2020, Sydney, Australia.
Conference: HSCC ACM International Conference on Hybrid Systems: Computation and Control


Download (747kB) | Preview
[img] Text

Download (1kB)
Official URL:


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.


Actions (login required)

View Item View Item