Document Open Access Logo

The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable

Authors Miroslav Chodil , Antonín Kučera

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2025.151.pdf
  • Filesize: 1.17 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Satisfiability
  • temporal logics
  • probabilistic CTL

Metrics

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

Abstract

The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts, the decidability of PCTL satisfiability and validity problems remained unresolved for 30 years. We show that both problems are highly undecidable, i.e., beyond the arithmetical hierarchy. Consequently, there is no sound and complete deductive system for PCTL.

Cite As Get BibTex

Miroslav Chodil and Antonín Kučera. The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 151:1-151:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ICALP.2025.151

Author Details

Miroslav Chodil
  • Faculty of Informatics, Masaryk University, Brno, Czech Republic
Antonín Kučera
  • Faculty of Informatics, Masaryk University, Brno, Czech Republic

Funding

The presented work received funding from the European Union’s Horizon Europe program under the Grant Agreement No. 101087529.

References

  1. N. Bertrand, J. Fearnley, and S. Schewe. Bounded satisfiability for PCTL. In Proceedings of CSL 2012, volume 16 of Leibniz International Proceedings in Informatics, pages 92-106. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.CSL.2012.92.
  2. P. Billingsley. Probability and Measure. Wiley, 1995. Google Scholar
  3. T. Brázdil, V. Forejt, J. Křetínský, and A. Kučera. The satisfiability problem for probabilistic CTL. In Proceedings of LICS 2008, pages 391-402. IEEE Computer Society Press, 2008. Google Scholar
  4. J. Canny. Some algebraic and geometric computations in PSPACE. In Proceedings of STOC'88, pages 460-467. ACM Press, 1988. Google Scholar
  5. S. Chakraborty and J.P. Katoen. On the satisfiability of some simple probabilistic logics. In Proceedings of LICS 2016, pages 56-65, 2016. Google Scholar
  6. M. Chodil and A. Kučera. The finite satisfiability problem for PCTL is undecidable. In Proceedings of LICS 2024, pages Article No. 22, pages 1-14. ACM Press, 2024. Google Scholar
  7. M. Chodil and A. Kučera. The satisfiability problem for a quantitative fragment of PCTL. Journal of Computer and System Sciences, 139:103478, 2024. URL: https://doi.org/10.1016/J.JCSS.2023.103478.
  8. M. Chodil and A. Kučera. The satisfiability and validity problems for probabilistic computational tree logic are highly undecidable. arXiv, 2504.19207 [cs.LO], 2025. Google Scholar
  9. A. Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58:345-363, 1936. Google Scholar
  10. S.A. Cook. The complexity of theorem-proving procedures. In Proceedings of STOC'71, pages 151-158. ACM Press, 1971. Google Scholar
  11. E.A. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, B:995-1072, 1991. Google Scholar
  12. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512-535, 1994. URL: https://doi.org/10.1007/BF01211866.
  13. S. Hart and M. Sharir. Probabilistic temporal logic for finite and bounded models. In Proceedings of POPL'84, pages 1-13. ACM Press, 1984. Google Scholar
  14. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  15. D. Kozen. A finite-model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, 1988. URL: https://doi.org/10.1007/BF00370554.
  16. S. Kraus and D.J. Lehmann. Decision procedures for time and chance (extended abstract). In Proceedings of FOCS'83, pages 202-209. IEEE Computer Society Press, 1983. Google Scholar
  17. J. Křetínský and A. Rotar. The satisfiability problem for unbounded fragments of probabilistic CTL. In Proceedings of CONCUR 2018, volume 118 of Leibniz International Proceedings in Informatics, pages 32:1-32:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.CONCUR.2018.32.
  18. D. Lehmann and S. Shelah. Reasoning with time and chance. Information and Control, 53:165-198, 1982. URL: https://doi.org/10.1016/S0019-9958(82)91022-1.
  19. M.L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  20. C. Stirling. Modal and temporal logics. Handbook of Logic in Computer Science, 2:477-563, 1992. Google Scholar
  21. B. Trakhtenbrot. The impossibility of an algorithm for the decidability problem on finite classes. Proceedings of the USSR Academy of Sciences, 70(4):569-572, 1950. Google Scholar
  22. A.M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1):230-265, 1937. URL: https://doi.org/10.1112/PLMS/S2-42.1.230.
  23. I. Walukiewicz. On completeness of the μ-calculus. In Proceedings of LICS'93, pages 136-146. IEEE Computer Society Press, 1993. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact