elib
DLR-Header
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. In: HSCC 2020 - Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control ,part of CPS-IoT Week. 23rd ACM International Conference on Hybrid Systems: Computation and Control, 2020-04-21 - 2020-04-24, Sydney, Australien. doi: 10.1145/3365365.3382197. ISBN 978-145037018-9.

[img] 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:
AuthorsInstitution or Email of AuthorsAuthor's ORCID iDORCID Put Code
Mascle, CortoENS Paris-Saclay, Cachan, FranceUNSPECIFIEDUNSPECIFIED
Neider, DanielUNSPECIFIEDUNSPECIFIEDUNSPECIFIED
Schwenger, MaximilianReactive Systems Group, Saarland University, Saarbrücken, GermanyUNSPECIFIEDUNSPECIFIED
Tabuada, PauloDepartment of Electrical and Computer Engineering, UCLA, Los Angeles, USAUNSPECIFIEDUNSPECIFIED
Weinert, AlexanderUNSPECIFIEDhttps://orcid.org/0000-0001-8143-246XUNSPECIFIED
Zimmermann, MartinUNSPECIFIEDhttps://orcid.org/0000-0002-8038-2453UNSPECIFIED
Date:2020
Journal or Publication Title:HSCC 2020 - Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control ,part of CPS-IoT Week
Refereed publication:No
Open Access:Yes
Gold Open Access:No
In SCOPUS:Yes
In ISI Web of Science:No
DOI:10.1145/3365365.3382197
ISBN:978-145037018-9
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 Start Date:21 April 2020
Event End Date:24 April 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:24 Apr 2024 20:37

Repository Staff Only: item control page

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