The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable

2025/04/27 by Chodil, Miroslav, Kučera, Antonín · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2504.19207

Abstract

The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts, the decidability of PCTL satisfiability and validity problems remained unresolved for 30 years. We show that both problems are highly undecidable, i.e., beyond the arithmetical hierarchy. Consequently, there is no sound and complete deductive system for PCTL.

Cited by

• Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization

Related

• The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
• Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems
• Computation Tree Logic Model Checking Based on Possibility Measures
• Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization
• On Probabilistic ω-Pushdown Systems, and ω-Probabilistic Computational Tree Logic