QLTL Model-Checking
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.
Quantified Linear-time temporal logic
Model-cheking
Verification
Automata theory
Theory of computation~Logic and verification
35:1-35:18
Regular Paper
François
Laroussinie
François Laroussinie
IRIF, Université Paris Cité, France
https://www.irif.fr/~francoisl/
Loriane
Leclercq
Loriane Leclercq
Ecole Centrale de Nantes, CNRS, LS2N, Nantes, France
https://orcid.org/0000-0002-6254-8691
ANR project ProMiS ANR-19-CE25-0015
Arnaud
Sangnier
Arnaud Sangnier
DIBRIS, Università di Genova, Italy
10.4230/LIPIcs.CSL.2024.35
B. Bednarczyk and S. Demri. Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? Logical Methods in Computer Science, 18(3):5:1-5:46, July 2022.
A. K. Chandra, D. Kozen, and L. J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981.
H. Comon and Y. Jurski. Multiple counter automata, safety analysis and PA. In CAV'98, volume 1427 of LNCS, pages 268-279. Springer, 1998.
S. Demri, A. K. Dhar, and A. Sangnier. Taming past LTL and flat counter systems. Inf. Comput., 242:306-339, 2015.
E. A. Emerson and A. P. Sistla. Deciding full branching time logic. Information and Control, 61(3):175-201, June 1984.
K. Etessami. Stutter-invariant languages, ω-automata, and temporal logic. In Nicolas Halbwachs and Doron A. Peled, editors, CAV'99), volume 1633 of LNCS, pages 236-248. Springer-Verlag, July 1999.
T. French. Decidability of quantified propositional branching time logics. In AJCAI'01, volume 2256 of LNCS, pages 165-176. Springer-Verlag, December 2001.
T. French. Quantified propositional temporal logic with repeating states. In TIME-ICTL'03, pages 155-165. IEEE Comp. Soc. Press, July 2003.
T. French and M. Reynolds. A sound and complete proof system for QPTL. In Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, editors, AIML'02, pages 127-148. King’s College Publications, 2003.
A. Hossain and F. Laroussinie. QCTL model-checking with QBF solvers. Inf. Comput., 280:104642, 2021.
Y. Kesten and A. Pnueli. Complete proof system for QPTL. Journal of Logic and Computation, 12(5):701-745, October 2002.
L. Kuhtz and B. Finkbeiner. Weak Kripke structures and LTL. In CONCUR'11, volume 6901 of LNCS, pages 419-433. Springer, 2011.
O. Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. In CAV'95, volume 939 of LNCS, pages 325-338. Springer-Verlag, July 1995.
F. Laroussinie and N. Markey. Quantified CTL: expressiveness and complexity. Logical Methods in Computer Science, 10(4), 2014.
F. Laroussinie, N. Markey, and P. Schnoebelen. Temporal logic with forgettable past. In LICS'02, pages 383-392. IEEE Computer Society, 2002.
N. Markey and P.Schnoebelen. Model checking a path. In CONCUR'03, volume 2761 of LNCS, pages 248-262. Springer, 2003.
N. Markey and P. Schnoebelen. Model checking a path. In CONCUR'03, volume 2761 of LNCS, pages 248-262. Springer, 2003.
Markey N and P. Schnoebelen. Mu-calculus path checking. Inf. Process. Lett., 97(6):225-230, 2006.
A. Pnueli. The temporal logic of programs. In FOCS'77, pages 46-57. IEEE Comp. Soc. Press, October-November 1977.
F. Schwarzentruber. The complexity of tiling problems. CoRR, abs/1907.00102, 2019.
A. P. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, Cambridge, Massachussets, USA, 1983.
A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logics. Theoretical Computer Science, 49:217-237, 1987.
M. Y. Vardi. Alternating automata and program verification. In Jan van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of LNCS, pages 471-485. Springer, 1995.
P. Wolper. Temporal logic can be more expressive. Inf. Control., 56(1/2):72-99, 1983.
François Laroussinie, Loriane Leclercq, and Arnaud Sangnier
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode