eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
35:1
35:18
10.4230/LIPIcs.CSL.2024.35
article
QLTL Model-Checking
Laroussinie, François
1
Leclercq, Loriane
2
https://orcid.org/0000-0002-6254-8691
Sangnier, Arnaud
3
IRIF, Université Paris Cité, France
Ecole Centrale de Nantes, CNRS, LS2N, Nantes, France
DIBRIS, Università di Genova, Italy
Quantified LTL (QLTL) extends the temporal logic LTL with quantifications over atomic propositions. Several semantics exist to handle these quantifications, depending on the definition of executions over which formulas are interpreted: either infinite sequences of subsets of atomic propositions (aka the "tree semantics") or infinite sequences of control states combined with a labelling function that associates atomic propositions to the control states (aka the "structure semantics"). The main difference being that in the latter different occurrences of a control state should be labelled similarly. The tree semantics has been intensively studied from the complexity and expressivity point of view (especially in the work of Sistla [Sistla, 1983; Sistla et al., 1987]) for which the satisfiability and model-checking problems are known to be TOWER-complete. For the structure semantics, French has shown that the satisfiability problem is undecidable [French, 2003]. We study here the model-checking problem for QLTL under this semantics and prove that it is EXPSPACE-complete. We also show that the complexity drops down to PSPACE-complete for two specific cases of structures, namely path and flat ones.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.35/LIPIcs.CSL.2024.35.pdf
Quantified Linear-time temporal logic
Model-cheking
Verification
Automata theory