Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces

Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces

Diego Calvanese, Giuseppe De Giacomo, Marco Montali, Fabio Patrizi

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 2553-2560. https://doi.org/10.24963/ijcai.2022/354

We address the problem of model checking first-order dynamic systems where new objects can be injected in the active domain during execution. Notable examples are systems induced by a first-order action theory, e.g., expressed in the Situation Calculus. Recent results have shown that, under the state-boundedness assumption, such systems, in spite of having a first-order representation of the state, admit decidable model checking for full first-order mu-calculus. However, interestingly, model checking remains undecidable in the case of first-order LTL (LTL-FO). In this paper, we show that in LTL-FOp, which is the fragment of LTL-FO in which quantification is over objects that persist along traces, model checking state-bounded systems becomes decidable over finite and infinite traces. We then employ this result to show how to handle monitoring of LTL-FOp properties against a trace stemming from an unknown state-bounded dynamic system, simultaneously considering the finite trace up to the current point, and all its possibly infinite future continuations.
Keywords:
Knowledge Representation and Reasoning: Reasoning about actions
Multidisciplinary Topics and Applications: Validation and Verification