Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Monitoring Dense-Time, Continuous-Semantics, Metric Temporal Logic
verfasst von : Kevin Baldor, Jianwei Niu
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 continuous semantics and dense time model most closely model the intuitive meaning of properties specified in metric temporal logic (
mtl
). To date, monitoring algorithms for
mtl
with dense time and continuous semantics lacked the simplicity the standard algorithms for discrete time and pointwise semantics. In this paper, we present a novel, transition-based, representation of dense-time boolean signals that lends itself to the construction of efficient monitors for safety properties defined in metric temporal logic with continuous semantics. Using this representation, we present a simple lookup-table-based algorithm for monitoring formulas consisting of arbitrarily nested
mtl
operators. We examine computational and space complexity of this monitoring algorithm for the past-only, restricted-future, and unrestricted-future temporal operators.