Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The General and Finite Satisfiability Problems for PCTL are Undecidable

Miroslav Chodil, Antonín Kučera

TL;DR

The paper shows that the general and finite satisfiability problems for PCTL are undecidable, with finite satisfiability already failing for a simple fragment and general satisfiability being $\Sigma^1_1$-hard. The authors develop a sequence of novel constructions that encode computations of nondeterministic Minsky machines into PCTL, starting with a parameterized formula $\psi(x,y)$ that enforces arbitrarily large models and then extending the approach to simulate one-counter and two-counter machines via a synchronized product. The core technique combines geometric counter representations, area-invariant arguments, and careful formula design to ensure that any model corresponds to a machine computation, while also showing emergent finite models when the computation is periodic. These results imply there is no sound and complete deductive system for generally or finitely valid PCTL formulae, highlighting fundamental limits of axiomatization for probabilistic temporal logics and informing future work on decidable fragments.

Abstract

The general/finite PCTL satisfiability problem asks whether a given PCTL formula has a general/finite model. We show that the finite PCTL satisfiability problem is undecidable, and the general PCTL satisfiability problem is even highly undecidable (beyond the arithmetical hierarchy). Consequently, there are no sound deductive systems proving all generally/finitely valid PCTL formulae.

The General and Finite Satisfiability Problems for PCTL are Undecidable

TL;DR

The paper shows that the general and finite satisfiability problems for PCTL are undecidable, with finite satisfiability already failing for a simple fragment and general satisfiability being -hard. The authors develop a sequence of novel constructions that encode computations of nondeterministic Minsky machines into PCTL, starting with a parameterized formula that enforces arbitrarily large models and then extending the approach to simulate one-counter and two-counter machines via a synchronized product. The core technique combines geometric counter representations, area-invariant arguments, and careful formula design to ensure that any model corresponds to a machine computation, while also showing emergent finite models when the computation is periodic. These results imply there is no sound and complete deductive system for generally or finitely valid PCTL formulae, highlighting fundamental limits of axiomatization for probabilistic temporal logics and informing future work on decidable fragments.

Abstract

The general/finite PCTL satisfiability problem asks whether a given PCTL formula has a general/finite model. We show that the finite PCTL satisfiability problem is undecidable, and the general PCTL satisfiability problem is even highly undecidable (beyond the arithmetical hierarchy). Consequently, there are no sound deductive systems proving all generally/finitely valid PCTL formulae.
Paper Structure (20 sections, 15 theorems, 67 equations, 4 figures)

This paper contains 20 sections, 15 theorems, 67 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The Logic PCTL
  4. Parameterized PCTL Formulae
  5. Minsky Machines
  6. Representing a Counter
  7. A Parameterized PCTL Formula with Arbitrarily Large Models
  8. Constructing $\psi(x,y)$
  9. A Proof of Theorem \ref{['thm-paramaterized']}
  10. Simulating Minsky machines with one counter
  11. Constructing $\psi$
  12. A Proof of Theorem \ref{['thm-one-counter']}
  13. A Proof of Theorem \ref{['thm-one-counter']} (A)
  14. A Proof of Theorem \ref{['thm-one-counter']} (B)
  15. Simulating Minsky Machines with Two Counters
  16. ...and 5 more sections

Key Result

lemma 1

For every $\pmb{v} \in W$, we have the following:

Figures (4)

  • Figure 1: $\mathit{Points}(\pmb{v})$, $\mathit{LSegs}(\pmb{v})$, and $\mathit{Area}(\pmb{v})$.
  • Figure 2: The construction proving $\mathit{Out} = \emptyset$.
  • Figure 3: The structure of transient states in a model of $\psi[c,d]$
  • Figure 4: The structure of transient states satisfying $\langle\space\langle x,r_i,\ell_j \rangle\space\rangle$ where $x \in \{a,b\}$ and $\mathit{Ins}_j \equiv \textit{inc } c; \textit{ goto } u$

Theorems & Definitions (20)

  • definition 1: PCTL
  • definition 2: Markov chain
  • definition 3: characteristic vector, $\mathtt{A}_{t}$, $\mathtt{B}_{t}$, and $\mathtt{C}_{t}$ sets
  • definition 4: $\tau$, $\sigma$, and $W$
  • lemma 1
  • definition 5
  • lemma 2
  • lemma 3
  • lemma 4
  • theorem 1
  • ...and 10 more