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

**Diego Calvanese, Giuseppe De Giacomo, Marco Montali, and Fabio
Patrizi**
*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",
}

pdf
url