Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Miroslav Chodil, Antonín Kučera

TL;DR

This work resolves a long-standing open problem by proving that both satisfiability and validity for Probabilistic Computational Tree Logic (PCTL) are highly undecidable, extending beyond the arithmetical hierarchy and persisting even in the $\operatorname{F},\operatorname{G}$ fragment. The authors achieve this via a reduction from the recurrent computation problem of nondeterministic two-counter machines, encoding configurations as probabilistic coordinates in $\left(0,1\right)^2$ and employing a convex-geometry argument to enforce valid step transitions. A key technical advance is the construction of a PCTL formula $\varphi_{\mathcal{M}}$ whose models correspond exactly to recurrent computations of $\mathcal{M}$, including a novel Inc/Dec encoding and polytope-based constraints to prevent spurious mass transfers. The results imply there is no sound and complete deductive system for PCTL, and even finite satisfiability for the $\operatorname{F},\operatorname{G}$-fragment is undecidable, highlighting fundamental limits of automatic reasoning for probabilistic temporal logics and impacting formal verification of probabilistic systems.

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.

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

TL;DR

This work resolves a long-standing open problem by proving that both satisfiability and validity for Probabilistic Computational Tree Logic (PCTL) are highly undecidable, extending beyond the arithmetical hierarchy and persisting even in the fragment. The authors achieve this via a reduction from the recurrent computation problem of nondeterministic two-counter machines, encoding configurations as probabilistic coordinates in and employing a convex-geometry argument to enforce valid step transitions. A key technical advance is the construction of a PCTL formula whose models correspond exactly to recurrent computations of , including a novel Inc/Dec encoding and polytope-based constraints to prevent spurious mass transfers. The results imply there is no sound and complete deductive system for PCTL, and even finite satisfiability for the -fragment is undecidable, highlighting fundamental limits of automatic reasoning for probabilistic temporal logics and impacting formal verification of probabilistic systems.

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.
Paper Structure (24 sections, 13 theorems, 42 equations, 4 figures)

This paper contains 24 sections, 13 theorems, 42 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The Logic PCTL
  4. Non-Deterministic $k$-Counter Machines
  5. Simulating Non-Deterministic Two-Counter Machines by PCTL
  6. Representing the configurations of $\mathcal{M}$
  7. Simulating a computational step of $\mathcal{M}$
  8. Constructing the formula $\varphi_\mathcal{M}$
  9. Representing Non-Negative Integers by Points in $(0,1)^2$
  10. Constructing the Formula $\varphi_\mathcal{M}$
  11. Defining the basic structure of a model
  12. Encoding the counter value
  13. The subformula $\mathit{Init}$
  14. The subformula $\mathit{Sim}_\ell$
  15. $\pmb{\mathit{Ins}_\ell}$ updates the counter by $\textit{dec}$
  16. ...and 9 more sections

Key Result

Proposition 1

The problem of whether a given non-deterministic two-counter machine $\mathcal{M}$ has a $\tau$-recurrent computation (for a given $\tau$) is $\Sigma_1^1$-hard. Furthermore, the problem of whether a given deterministic two-counter machine $\mathcal{M}$ has a bounded computation is $\Sigma_1^0$-hard.

Figures (4)

  • Figure 1: The structure of $\pmb{z}, \mathit{Inc}(\pmb{z}), \mathit{Inc}^2(\pmb{z}),\ldots$ and $\mathcal{A}(\pmb{z})$ (left); the construction proving $\mathit{Out} =\emptyset$ (right).
  • Figure 2: Illustrating the meaning of $\textit{Struct}$.
  • Figure 3: Illustrating the meaning of $\textit{Decrement}$.
  • Figure 4: Illustrating the meaning of $\textit{Update}_{i,\ell,\ell'}$ when $\mathit{Ins}_\ell$ updates the counter by $\textit{inc}$. The markers are in boldface, and '*' indicates an index $j \in \{0,1,2\}$. The colored shapes indicate the families of states used in the subformulae of $\textit{UInc}_{i,\ell,\ell'}$. Note that the probability of certain transitions is equal to $\lambda$ due to the subformula $\textit{Lambda}$.

Theorems & Definitions (14)

  • Definition 1: PCTL
  • Proposition 1
  • Lemma 1
  • Lemma 1
  • Theorem 2
  • Proposition 3
  • Proposition 4
  • Theorem 5
  • Proposition 5
  • Lemma 5
  • ...and 4 more