Monitoring Data-aware Temporal Properties
Monitoring Data-aware Temporal Properties
Alessandro Gianola, Marco Montali, Sarah Winkler
Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence
Main Track. Pages 109-117.
https://doi.org/10.24963/ijcai.2026/13
Dynamic systems in AI are often complex and heterogeneous, so that an internal specification is not accessible and hence verification techniques like model checking are not applicable. Monitoring is in such cases an attractive alternative, as it deals with the observation of 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 (data-LTLf). Anticipatory monitoring in this setting is a highly challenging problem and undecidable in general, 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 data-LTLf properties. The framework combines automata-theoretic methods to handle the temporal aspects of reasoning 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 database. Feasibility is witnessed by a prototype implementation and preliminary evaluation.
Keywords:
Agent-based and Multi-agent Systems: Formal verification, validation and synthesis
Constraint Satisfaction and Optimization: Constraint satisfaction
Constraint Satisfaction and Optimization: Satisfiabilty
Knowledge Representation and Reasoning: Automated reasoning and theorem proving
Knowledge Representation and Reasoning: Reasoning about actions
