Publication details
The Finite Satisfiability Problem for PCTL is Undecidable
| Authors | |
|---|---|
| Year of publication | 2026 |
| Type | Peer-reviewed scientific article |
| Magazine / Source | JOURNAL OF THE ACM |
| MU Faculty or unit | |
| Citation | |
| web | DOI |
| Doi | https://doi.org/10.1145/3787496 |
| Keywords | Probabilistic temporal logics; satisfiability |
| Description | 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 F1 \wedge G=1 F2 where the validity of F1, F2 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. |
| Related projects: |