Branching-time model-checking of probabilistic pushdown automata.

Abstract: 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. [Copyright &y& Elsevier]