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.
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: |
| ||||||||||||||||||||||||||||
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