Branching-time model-checking of probabilistic pushdown automata

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRÁZDIL Tomáš BROŽEK Václav FOREJT Vojtěch KUČERA Antonín

Year of publication 2014
Type Article in Periodical
Magazine / Source Journal of Computer and System Sciences
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1016/j.jcss.2013.07.001
Field Informatics
Keywords Markov chains; pushdown automata
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.