Monitoring Data-aware Temporal Properties (Extended Version)

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 handle the temporal aspects of the logic, with automated reasoning techniques to address the first-order dimension. Moreover, we identify for the first time decidable fragments of this monitoring problem that are practically relevant as they combine linear arithmetic with uninterpreted functions, which covers e.g. data-aware business processes and dynamic systems operating over a read-only database. Feasibility is witnessed by a prototype implementation and preliminary evaluation.