Monitoring Arithmetic Temporal Properties on Finite Traces


  • Paolo Felli University of Bologna
  • Marco Montali Free University of Bozen-Bolzano
  • Fabio Patrizi Sapienza University of Rome
  • Sarah Winkler Free University of Bozen-Bolzano



KRR: Action, Change, and Causality, KRR: Geometric, Spatial, and Temporal Reasoning


We study monitoring of linear-time arithmetic properties against finite traces generated by an unknown dynamic system. The monitoring state is determined by considering at once the trace prefix seen so far, and all its possible finite-length, future continuations. This makes monitoring at least as hard as satisfiability and validity. Traces consist of finite sequences of assignments of a fixed set of variables to numerical values. Properties are specified in a logic we call ALTLf, combining LTLf (LTL on finite traces) with linear arithmetic constraints that may carry lookahead, i.e., variables may be compared over multiple instants of the trace. While the monitoring problem for this setting is undecidable in general, we show decidability for (a) properties without lookahead, and (b) properties with lookahead that satisfy the abstract, semantic condition of finite summary, studied before in the context of model checking. We then single out concrete, practically relevant classes of constraints guaranteeing finite summary. Feasibility is witnessed by a prototype implementation.




How to Cite

Felli, P., Montali, M., Patrizi, F., & Winkler, S. (2023). Monitoring Arithmetic Temporal Properties on Finite Traces. Proceedings of the AAAI Conference on Artificial Intelligence, 37(5), 6346-6354.



AAAI Technical Track on Knowledge Representation and Reasoning