The PCTL satisfiability problem resolved!

The satisfiability problem for the logic PCTL is resolved.

April 2024

LICS 2024 in Tallinn

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]

More articles

All articles

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

More info