elib
DLR-Header
DLR-Logo -> http://www.dlr.de
DLR Portal Home | Impressum | Datenschutz | Kontakt | English
Schriftgröße: [-] Text [+]

From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics

Mascle, Corto und Neider, Daniel und Schwenger, Maximilian und Tabuada, Paulo und Weinert, Alexander und 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

Kurzfassung

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.

elib-URL des Eintrags:https://elib.dlr.de/134512/
Dokumentart:Konferenzbeitrag (Vortrag)
Titel:From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics
Autoren:
AutorenInstitution oder E-Mail-AdresseAutoren-ORCID-iDORCID Put Code
Mascle, CortoENS Paris-Saclay, Cachan, FranceNICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
Neider, Danielneider (at) mpi-sws.orgNICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
Schwenger, MaximilianReactive Systems Group, Saarland University, Saarbrücken, GermanyNICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
Tabuada, PauloDepartment of Electrical and Computer Engineering, UCLA, Los Angeles, USANICHT SPEZIFIZIERTNICHT SPEZIFIZIERT
Weinert, AlexanderAlexander.Weinert (at) dlr.dehttps://orcid.org/0000-0001-8143-246XNICHT SPEZIFIZIERT
Zimmermann, Martinmartin.zimmermann (at) liverpool.ac.ukhttps://orcid.org/0000-0002-8038-2453NICHT SPEZIFIZIERT
Datum:2020
Erschienen in:HSCC 2020 - Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control ,part of CPS-IoT Week
Referierte Publikation:Nein
Open Access:Ja
Gold Open Access:Nein
In SCOPUS:Ja
In ISI Web of Science:Nein
DOI:10.1145/3365365.3382197
ISBN:978-145037018-9
Status:veröffentlicht
Stichwörter:Temporallogik, Monitoring, Robustheit
Veranstaltungstitel:23rd ACM International Conference on Hybrid Systems: Computation and Control
Veranstaltungsort:Sydney, Australien
Veranstaltungsart:internationale Konferenz
Veranstaltungsbeginn:21 April 2020
Veranstaltungsende:24 April 2020
Veranstalter :ACM
HGF - Forschungsbereich:Luftfahrt, Raumfahrt und Verkehr
HGF - Programm:Raumfahrt
HGF - Programmthema:Technik für Raumfahrtsysteme
DLR - Schwerpunkt:Raumfahrt
DLR - Forschungsgebiet:R SY - Technik für Raumfahrtsysteme
DLR - Teilgebiet (Projekt, Vorhaben):R - Vorhaben SISTEC (alt)
Standort: Köln-Porz
Institute & Einrichtungen:Institut für Simulations- und Softwaretechnik
Institut für Simulations- und Softwaretechnik > Verteilte Systeme und Komponentensoftware
Hinterlegt von: Weinert, Alexander
Hinterlegt am:20 Apr 2020 08:26
Letzte Änderung:24 Apr 2024 20:37

Nur für Mitarbeiter des Archivs: Kontrollseite des Eintrags

Blättern
Suchen
Hilfe & Kontakt
Informationen
electronic library verwendet EPrints 3.3.12
Gestaltung Webseite und Datenbank: Copyright © Deutsches Zentrum für Luft- und Raumfahrt (DLR). Alle Rechte vorbehalten.