TY - JOUR
AU - Felli, Paolo
AU - Montali, Marco
AU - Patrizi, Fabio
AU - Winkler, Sarah
PY - 2023/06/26
Y2 - 2024/04/18
TI - Monitoring Arithmetic Temporal Properties on Finite Traces
JF - Proceedings of the AAAI Conference on Artificial Intelligence
JA - AAAI
VL - 37
IS - 5
SE - AAAI Technical Track on Knowledge Representation and Reasoning
DO - 10.1609/aaai.v37i5.25781
UR - https://ojs.aaai.org/index.php/AAAI/article/view/25781
SP - 6346-6354
AB - 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.
ER -