The Finite Satisfiability Problem for PCTL is Undecidable
We show that the problem of whether a given PCTL formula has a finite model is undecidable. The undecidability result holds even for formulae of the form \(\varphi _1 \wedge {\pmb {\mathtt {G}}}_{=1} \varphi _2\) where the validity of \(\varphi _1,\varphi _2\) depends only on the states reachable in at most two transitions. Consequently, the problem of whether a given PCTL formula is valid in all finite-state Markov chains is not even semi-decidable.
Authors
- Antonı́n Kučera (ORCID: https://orcid.org/0000-0002-6602-8028)
- Miroslav Chodil (ORCID: https://orcid.org/0000-0002-8406-0443)
Institutions
- Masaryk University (CZ)
Publication Details
- Journal
- Journal of the ACM
- Published
- 2026-01-06
- DOI
- https://doi.org/10.1145/3787496
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.00