From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics

TL;DR

This paper introduces a robust semantics for LTL monitoring that improves monitorability, allowing all formulas to be monitored effectively and enabling deterministic automata implementation for runtime verification.

Contribution

It proposes a new robust semantics for finite strings in LTL monitoring, overcoming limitations of previous three-valued semantics and ensuring all formulas are monitorable.

Findings

All formulas from Bauer et al. are monitorable under the robust semantics.

Deterministic automata can be used to monitor LTL formulas with robust semantics.

Prototype implementation demonstrates practical applicability.

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 which 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.