Oxford logo
[BBFK14] T. Brázdil, V. Brožek, V. Forejt and A. Kučera. Branching-time model-checking of probabilistic pushdown automata. Journal of Computer and System Sciences, 80(1), pages 139-156, Elsevier. 2014. [pdf] [bib]
Downloads:  pdf pdf (334 KB)  bib bib
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.

QAV:

Home

People

Projects

Publications