Monitoring Data-aware Temporal Properties

摘要

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.