. "0022-0000" . . "14330" . "3"^^ . "18"^^ . "Branching-time model-checking of probabilistic pushdown automata"@en . "NL - Nizozemsko" . "P(GAP202/10/1469)" . "Forejt, Vojt\u011Bch" . "80" . "Br\u00E1zdil, Tom\u00E1\u0161" . . "RIV/00216224:14330/14:00073430!RIV15-GA0-14330___" . "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."@en . "4"^^ . "Markov chains; pushdown automata"@en . . . . . . "5763" . . "[32151210EAD0]" . . . "Journal of Computer and System Sciences" . "Branching-time model-checking of probabilistic pushdown automata" . "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." . . "10.1016/j.jcss.2013.07.001" . "Bro\u017Eek, V\u00E1clav" . . "RIV/00216224:14330/14:00073430" . "Branching-time model-checking of probabilistic pushdown automata"@en . "000325386500011" . . . "1" . "Ku\u010Dera, Anton\u00EDn" . "Branching-time model-checking of probabilistic pushdown automata" . .