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

Proc. of the 31st Int. Joint Conf. on Artificial Intelligence (IJCAI 2022). 2022.

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 expressed, e.g., in the situation calculus. Recent results show that, under state-boundedness, 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 , the fragment of LTL-FO where quantification ranges only over objects that persist along traces, model checking state-bounded systems becomes decidable over infinite and finite 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.

@inproceedings{IJCAI-2022,
   title = "Verification and Monitoring for First-Order LTL with
Persistence-Preserving Quantification over Finite and Infinite Traces",
   year = "2022",
   author = "Diego Calvanese and De Giacomo, Giuseppe and Marco Montali
and Fabio Patrizi",
   booktitle = "Proc. of the 31st Int. Joint Conf. on Artificial Intelligence
(IJCAI 2022)",
   pages = "2553--2560",
   publisher = "IJCAI Org.",
   doi = "10.24963/ijcai.2022/354",
}