Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems

TL;DR

This paper proves that model checking PCTL properties of stateless probabilistic pushdown systems is generally undecidable, resolving a longstanding open problem in probabilistic verification of infinite-state systems.

Contribution

It establishes the undecidability of PCTL model checking for stateless probabilistic pushdown systems, a significant theoretical result in probabilistic verification.

Findings

Model checking PCTL for pBPA is undecidable.

Addresses a longstanding open question in probabilistic verification.

Advances understanding of limitations in probabilistic model checking.

Abstract

In this communication, we resolve a longstanding open question in the probabilistic verification of infinite-state systems. We show that model checking {\it stateless probabilistic pushdown systems (pBPA)} against {\it probabilistic computational tree logic (PCTL)} is generally undecidable.