The Finite Satisfiability Problem for PCTL is Undecidable
Abstract
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.
Fields of Study & Subjects
Formal Methods in Verification
Petri Nets in System Modeling
Model-Driven Software Engineering Techniques
Publication details
- Journal / source
- Journal of the ACM
- Volume
- 73
- Issue
- 1
- Pages
- 1–30
- Publication date
- 6 January 2026
- Language
- EN