From LTL to rLTL Monitoring: Improved Monitorability Through Robust Semantics

(2020) From LTL to rLTL Monitoring: Improved Monitorability Through Robust Semantics.

Preview	Text robustmonitoring.pdf Download (747kB) | Preview
	Text hscc.bib Download (1kB)

Abstract

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.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Bernd Finkbeiner (Reactive Systems Group, RSG)
Conference:	HSCC ACM International Conference on Hybrid Systems: Computation and Control
Depositing User:	Maximilian Schwenger
Date Deposited:	14 Sep 2020 07:23
Last Modified:	14 Sep 2020 07:23
Primary Research Area:	NRA2: Reliable Security Guarantees
URI:	https://publications.cispa.saarland/id/eprint/3171

Actions

Actions (login required)

View Item