The Finite Satisfiability Problem for PCTL is Undecidable

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	CHODIL Miroslav KUČERA Antonín
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	Fakulta informatiky
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:	Efektivní analýza a optimalizace pravděpodobnostních systémů a her Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24 Modelování, analýza a verifikace (2024)