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 (2022) From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics. Formal Methods in System Design. Springer. doi: 10.1007/s10703-022-00398-4. ISSN 0925-9856.

[img] PDF - Preprint version (submitted draft)

Official URL: https://link.springer.com/article/10.1007/s10703-022-00398-4


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 for a finite execution: the formula is already satisfied by the given execution, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions of the given execution. However, a wide range of formulas are not monitorable under this approach, meaning that there are executions 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. We show that LTL formulas with robust semantics can be monitored by deterministic automata, and provide tight bounds on the size of the constructed automaton. Lastly, we report on a prototype implementation and compare it to the LTL monitor of Bauer et al. on a sample of examples.

Item URL in elib:https://elib.dlr.de/187691/
Document Type:Article
Title:From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics
AuthorsInstitution or Email of AuthorsAuthor's ORCID iD
Mascle, Cortocorto.mascle (at) labri.frUNSPECIFIED
Neider, Danieldaniel.neider (at) uol.dehttps://orcid.org/0000-0001-9276-6342
Schwenger, Maximilianschwenger (at) react.uni-saarland.dehttps://orcid.org/0000-0002-2091-7575
Tabuada, Paulotabuada (at) ee.ucla.eduhttps://orcid.org/0000-0002-3417-0951
Weinert, Alexanderalexander.Weinert (at) dlr.dehttps://orcid.org/0000-0001-8143-246X
Zimmermann, Martinmzi (at) cs.aau.dkhttps://orcid.org/0000-0002-8038-2453
Date:21 October 2022
Journal or Publication Title:Formal Methods in System Design
Refereed publication:Yes
Open Access:Yes
Gold Open Access:No
In ISI Web of Science:Yes
Keywords:Runtime Monitoring Robust Linear Temporal Logic
HGF - Research field:other
HGF - Program:other
HGF - Program Themes:other
DLR - Research area:Digitalisation
DLR - Program:D - no assignment
DLR - Research theme (Project):D - no assignment
Location: Köln-Porz
Institutes and Institutions:Institute for Software Technology
Institute for Software Technology > Intelligent and Distributed Systems
Deposited By: Weinert, Alexander
Deposited On:06 Sep 2022 10:22
Last Modified:03 Nov 2022 08:17

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.