2013 | OriginalPaper | Buchkapitel
From Propositional to First-Order Monitoring
verfasst von : Andreas Bauer, Jan-Christoph Küster, Gil Vegliach
Erschienen in: Runtime Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The main purpose of this paper is to introduce a first-order temporal logic, LTL
FO
, and a corresponding monitor construction based on a new type of automaton, called spawning automaton.
Specifically, we show that monitoring a specification in LTL
FO
boils down to an undecidable decision problem. The proof of this result revolves around specific ideas on what we consider a “proper” monitor. As these ideas are general, we outline them first in the setting of standard LTL, before lifting them to the setting of first-order logic and LTL
FO
. Although due to the above result one cannot hope to obtain a complete monitor for LTL
FO
, we prove the soundness of our automata-based construction and give experimental results from an implementation. These seem to substantiate our hypothesis that the automata-based construction leads to efficient runtime monitors whose size does not grow with increasing trace lengths (as is often observed in similar approaches). However, we also discuss formulae for which growth is unavoidable, irrespective of the chosen monitoring approach.