The PCTL satisfiability problem resolved!
The satisfiability problem for the logic PCTL is resolved.
The general/finite PCTL satisfiability problem asks whether a given PCTL formula has a general/finite model. The decidability of these problems remained open for almost 30 years. Recently, both of them have been proven undecidable.
The undecidability of finite PCTL satisfiability will be presented at LICS 2024. A follow-up paper covering also the arguments for general PCTL satisfiability is available at arXiv.
M. Chodil and A. Kučera. The General and Finite Satisfiability Problems for PCTL are Undecidable. arXiv:2404.10648 [cs.LO]
