What is it about?
Probabilistic Computational Tree Logic (PCTL) allows quantifying the probability with which temporal properties of probabilistic systems are satisfied. For example, a PCTL formula may say "Every state of a given system can reach a configuration satisfying a property P in at most ten steps with probability at least 95%". The finite satisfiability problem for the logic PCTL, i.e., the question of whether a given PCTL formula has a finite model, has remained open for about 30 years despite numerous research attempts. This work resolves the question by demonstrating that the finite satisfiability problem is not algorithmically solvable.
Featured Image
Photo by Naser Tamimi on Unsplash
Why is it important?
The satisfiability problem is a fundamental question in logic. For non-probabilistic temporal logics such as PCTL, PCTL*, or the modal mu-calculus, the satisfiability problem is algorithmically solvable. It is even possible to construct a model for every satisfiable formula. Such a model can be seen as an abstract program satisfying the correctness property specified by the formula. Hence, the program does not require any subsequent verification because it is "correct by construction". The result shows that automatic synthesis of probabilistic programs from PCTL specifications is impossible. Furthermore, it also implies that there is no sound and complete deductive system allowing to prove all finitely valid PCTL fomulae.
Perspectives
The result is actually surprising. Due to the relative simplicity of the PCTL, one is tempted to conjecture that every finite-satisfiable PCTL formula has a model whose size can be bounded by some computable function in the length of the formula. Proving the existence of such a computable upper bound is enough to establish the decidability of the finite satisfiability problem for PCTL. Since there is no apparent way how a PCTL formula of length N can enforce the existence of "uncomputably many" states in a model, the hypothesis appears plausible and the previous research attempts concentrated on proving the decidability of the problem. To our surprise, we managed to construct a fixed PCTL formula enforcing arbitrarily many states in its model just by changing two probability constraints occurring in the formula. This observation reveals the specific power of numerical probability constraints and represents a crucial step toward the undecidability result.
Antonin Kucera
Masaryk University
Read the Original
This page is a summary of: The Finite Satisfiability Problem for PCTL is Undecidable, July 2024, ACM (Association for Computing Machinery),
DOI: 10.1145/3661814.3662145.
You can read the full text:
Contributors
The following have contributed to this page
