The Finite Satisfiability Problem for PCTL is Undecidable

• Autoři: CHODIL Miroslav; KUČERA Antonín
• Rok publikování: 2026
• Druh: Recenzovaný odborný článek
• Časopis / Zdroj: JOURNAL OF THE ACM
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: DOI
• Doi: https://doi.org/10.1145/3787496
• Klíčová slova: Probabilistic temporal logics; satisfiability
• 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 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.

Související projekty

• Cyber-security Excellence Hub in Estonia and South Moravia (CHESS)
• Advanced Method for Analysis and Synthesis of Probabilistic Programs