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. 23rd ACM International Conference on Hybrid Systems: Computation and Control, 21.-24. Apr. 2020, Sydney, Australien.
![]() |
PDF
700kB |
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.
Item URL in elib: | https://elib.dlr.de/134512/ | |||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Document Type: | Conference or Workshop Item (Speech) | |||||||||||||||||||||
Title: | From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics | |||||||||||||||||||||
Authors: |
| |||||||||||||||||||||
Date: | 2020 | |||||||||||||||||||||
Refereed publication: | No | |||||||||||||||||||||
Open Access: | Yes | |||||||||||||||||||||
Gold Open Access: | No | |||||||||||||||||||||
In SCOPUS: | No | |||||||||||||||||||||
In ISI Web of Science: | No | |||||||||||||||||||||
Status: | Published | |||||||||||||||||||||
Keywords: | Temporallogik, Monitoring, Robustheit | |||||||||||||||||||||
Event Title: | 23rd ACM International Conference on Hybrid Systems: Computation and Control | |||||||||||||||||||||
Event Location: | Sydney, Australien | |||||||||||||||||||||
Event Type: | international Conference | |||||||||||||||||||||
Event Dates: | 21.-24. Apr. 2020 | |||||||||||||||||||||
Organizer: | ACM | |||||||||||||||||||||
HGF - Research field: | Aeronautics, Space and Transport | |||||||||||||||||||||
HGF - Program: | Space | |||||||||||||||||||||
HGF - Program Themes: | Space System Technology | |||||||||||||||||||||
DLR - Research area: | Raumfahrt | |||||||||||||||||||||
DLR - Program: | R SY - Space System Technology | |||||||||||||||||||||
DLR - Research theme (Project): | R - Vorhaben SISTEC (old) | |||||||||||||||||||||
Location: | Köln-Porz | |||||||||||||||||||||
Institutes and Institutions: | Institut of Simulation and Software Technology Institut of Simulation and Software Technology > Distributed Systems and Component Software | |||||||||||||||||||||
Deposited By: | Weinert, Alexander | |||||||||||||||||||||
Deposited On: | 20 Apr 2020 08:26 | |||||||||||||||||||||
Last Modified: | 10 Dec 2020 14:10 |
Repository Staff Only: item control page