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.