On the Hardness of PCTL Satisfiability

TL;DR

This paper proves that the satisfiability problem for probabilistic CTL is undecidable in general, but identifies a fragment with an exponential-time decision procedure, highlighting the complexity landscape of PCTL satisfiability.

Contribution

It establishes undecidability of PCTL satisfiability and provides an exponential-time algorithm for a specific fragment, advancing understanding of PCTL's computational complexity.

Findings

PCTL satisfiability is undecidable.

A bounded, negation-closed fragment has an EXPTIME-hard satisfiability problem.

An exponential-time algorithm is proposed for the fragment.

Abstract

This paper shows that the satisfiability problem for probabilistic CTL (PCTL, for short) is undecidable. By a reduction from $1\frac{1}{2}$-player games with PCTL winning objectives, we establish that the PCTL satisfiability problem is ${\Sigma}_1^1$-hard. We present an exponential-time algorithm for the satisfiability of a bounded, negation-closed fragment of PCTL, and show that the satisfiability problem for this fragment is EXPTIME-hard.