The Finite Satisfiability Problem for PCTL is Undecidable
| Autoři | |
|---|---|
| Rok publikování | 2024 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | https://dl.acm.org/doi/abs/10.1145/3661814.3662145 |
| Doi | http://dx.doi.org/10.1145/3661814.3662145 |
| Klíčová slova | Markov chains; probabilistic temporal logics |
| Popis | 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. |
| Související projekty: |