Branching-time model-checking of probabilistic pushdown automata

• We study the model-checking problem for probabilistic pushdown automata (pPDA).
• Model-checking pPDA against PCTL formulae is undecidable.
• Model-checking pPDA against qualitative PCTL* formulae is decidable.

In this paper we study the model-checking problem for probabilistic pushdown automata (pPDA) and branching-time probabilistic logics PCTL and PCTL⁎. We show that model-checking pPDA against general PCTL formulae is undecidable, but we yield positive decidability results for the qualitative fragments of PCTL and PCTL⁎. For these fragments, we also give a complete complexity classification.