2026-07-24T11:54:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23528 2025-10-02T12:57:52Z ddc:004 open_access

The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic Are Highly Undecidable Chodil, Miroslav Kučera, Antonín Satisfiability temporal logics probabilistic CTL 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Miroslav Chodil and Antonín Kučera 2025 Is Part Of LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2025.151 urn:nbn:de:0030-drops-235281 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.151 eng https://creativecommons.org/licenses/by/4.0/legalcode