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.


    Access

    Download


    Export, share and cite



    Title :

    From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics



    Conference:

    2020 ; Sydney, Australien


    Publication date :

    2020


    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English




    A model-based reasoning approach to sensor placement for monitorability

    Chien, Steve / Doyle, Richard / Homemdemello, Luiz | NTRS | 1992



    Towards Robust ISO 34503 ODD Language Syntax and Semantics

    Bruce, Guild / da Costa, Antonio Bruto / Khastgir, Siddartha et al. | IEEE | 2024


    Augmenting Homeland Intelligence Through Emergent Semantics

    Monarch, Ira / Fisher, David / Nag, Pranab | AIAA | 2005


    Modeling shape and semantics through an intermediate model

    Brunetti,G. / de Martino,T. / Elter,H. et al. | Automotive engineering | 1996