Document Open Access Logo

QLTL Model-Checking

Authors François Laroussinie, Loriane Leclercq , Arnaud Sangnier

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.35.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Author Details

François Laroussinie
  • IRIF, Université Paris Cité, France
Loriane Leclercq
  • Ecole Centrale de Nantes, CNRS, LS2N, Nantes, France
Arnaud Sangnier
  • DIBRIS, Università di Genova, Italy

Funding

  • Leclercq, Loriane: ANR project ProMiS ANR-19-CE25-0015

Cite AsGet BibTex

François Laroussinie, Loriane Leclercq, and Arnaud Sangnier. QLTL Model-Checking. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.35

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Quantified Linear-time temporal logic
  • Model-cheking
  • Verification
  • Automata theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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. Google Scholar
  2. A. K. Chandra, D. Kozen, and L. J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. Google Scholar
  3. H. Comon and Y. Jurski. Multiple counter automata, safety analysis and PA. In CAV'98, volume 1427 of LNCS, pages 268-279. Springer, 1998. Google Scholar
  4. S. Demri, A. K. Dhar, and A. Sangnier. Taming past LTL and flat counter systems. Inf. Comput., 242:306-339, 2015. Google Scholar
  5. E. A. Emerson and A. P. Sistla. Deciding full branching time logic. Information and Control, 61(3):175-201, June 1984. Google Scholar
  6. 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. Google Scholar
  7. T. French. Decidability of quantified propositional branching time logics. In AJCAI'01, volume 2256 of LNCS, pages 165-176. Springer-Verlag, December 2001. Google Scholar
  8. T. French. Quantified propositional temporal logic with repeating states. In TIME-ICTL'03, pages 155-165. IEEE Comp. Soc. Press, July 2003. Google Scholar
  9. 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. Google Scholar
  10. A. Hossain and F. Laroussinie. QCTL model-checking with QBF solvers. Inf. Comput., 280:104642, 2021. Google Scholar
  11. Y. Kesten and A. Pnueli. Complete proof system for QPTL. Journal of Logic and Computation, 12(5):701-745, October 2002. Google Scholar
  12. L. Kuhtz and B. Finkbeiner. Weak Kripke structures and LTL. In CONCUR'11, volume 6901 of LNCS, pages 419-433. Springer, 2011. Google Scholar
  13. 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. Google Scholar
  14. F. Laroussinie and N. Markey. Quantified CTL: expressiveness and complexity. Logical Methods in Computer Science, 10(4), 2014. Google Scholar
  15. F. Laroussinie, N. Markey, and P. Schnoebelen. Temporal logic with forgettable past. In LICS'02, pages 383-392. IEEE Computer Society, 2002. Google Scholar
  16. N. Markey and P.Schnoebelen. Model checking a path. In CONCUR'03, volume 2761 of LNCS, pages 248-262. Springer, 2003. Google Scholar
  17. N. Markey and P. Schnoebelen. Model checking a path. In CONCUR'03, volume 2761 of LNCS, pages 248-262. Springer, 2003. Google Scholar
  18. Markey N and P. Schnoebelen. Mu-calculus path checking. Inf. Process. Lett., 97(6):225-230, 2006. Google Scholar
  19. A. Pnueli. The temporal logic of programs. In FOCS'77, pages 46-57. IEEE Comp. Soc. Press, October-November 1977. Google Scholar
  20. F. Schwarzentruber. The complexity of tiling problems. CoRR, abs/1907.00102, 2019. Google Scholar
  21. A. P. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, Cambridge, Massachussets, USA, 1983. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. P. Wolper. Temporal logic can be more expressive. Inf. Control., 56(1/2):72-99, 1983. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact