Publication details

The Finite Satisfiability Problem for PCTL is Undecidable

Investor logo
Authors

CHODIL Miroslav KUČERA Antonín

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info