DLR-Logo -> http://www.dlr.de
DLR Portal Home | Imprint | Privacy Policy | Contact | Deutsch
Fontsize: [-] Text [+]

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. 23rd ACM International Conference on Hybrid Systems: Computation and Control, 21.-24. Apr. 2020, Sydney, Australien.

[img] PDF


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
AuthorsInstitution or Email of AuthorsAuthor's ORCID iD
Mascle, CortoENS Paris-Saclay, Cachan, FranceUNSPECIFIED
Neider, Danielneider (at) mpi-sws.orgUNSPECIFIED
Schwenger, MaximilianReactive Systems Group, Saarland University, Saarbrücken, GermanyUNSPECIFIED
Tabuada, PauloDepartment of Electrical and Computer Engineering, UCLA, Los Angeles, USAUNSPECIFIED
Weinert, AlexanderAlexander.Weinert (at) dlr.dehttps://orcid.org/0000-0001-8143-246X
Zimmermann, Martinmartin.zimmermann (at) liverpool.ac.ukhttps://orcid.org/0000-0002-8038-2453
Refereed publication:No
Open Access:Yes
Gold Open Access:No
In ISI Web of Science:No
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
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

Help & Contact
electronic library is running on EPrints 3.3.12
Website and database design: Copyright © German Aerospace Center (DLR). All rights reserved.