The Finite Satisfiability Problem for PCTL is Undecidable
| Authors | |
|---|---|
| Year of publication | 2024 |
| Type | Article in Proceedings |
| Conference | Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science |
| MU Faculty or unit | |
| Citation | |
| web | https://dl.acm.org/doi/abs/10.1145/3661814.3662145 |
| Doi | http://dx.doi.org/10.1145/3661814.3662145 |
| Keywords | Markov chains; probabilistic temporal logics |
| 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 \phi_1 \wedge G=1 \phi_2 where the validity of \phi_1,\phi_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. |
| Related projects: |