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.
Dettaglio pubblicazione
2022, IJCAI International Joint Conference on Artificial Intelligence, Pages 2553-2560
Verification and Monitoring for First-Order LTL with Persistence-Preserving Quantification over Finite and Infinite Traces (04b Atto di convegno in volume)
Calvanese D., De Giacomo G., Montali M., Patrizi F.
keywords