Monitoring Data-aware Temporal Properties (Extended Version)
Alessandro Gianola, Marco Montali, Sarah Winkler

TL;DR
This paper introduces a new framework for monitoring complex, data-aware temporal properties in dynamic systems where internal specifications are inaccessible, combining automata and automated reasoning techniques.
Contribution
It presents the first formal framework for anticipatory monitoring of LTLfMT properties, including decidable fragments with practical relevance.
Findings
Framework is proven correct under reasonable assumptions.
Decidable fragments combining linear arithmetic and uninterpreted functions identified.
Prototype implementation demonstrates feasibility and preliminary evaluation.
Abstract
Dynamic systems in AI are often complex and heterogeneous, so that an internal specification is not accessible and verification techniques such as model checking are not applicable. Monitoring is in such cases an attractive alternative, as it evaluates desirable properties along traces generated by an unknown dynamic system. In this work, we consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces (LTLfMT). Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations. Under reasonable assumptions on the background theory, we present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment of LTLfMT. The framework combines automata-theoretic methods to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
