The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable
By: Miroslav Chodil, Antonín Kučera
Potential Business Impact:
Proves some computer programs can't be proven correct.
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.
Similar Papers
Possibilistic Computation Tree Logic: Decidability and Complete Axiomatization
Logic in Computer Science
Lets computers check systems with uncertain info.
Synthesis of Safety Specifications for Probabilistic Systems
Logic in Computer Science
Makes robots follow complex safety rules.
Probabilistic and Causal Satisfiability: Constraining the Model
Computational Complexity
Makes AI understand cause and effect better.