Publication details

Branching-time model-checking of probabilistic pushdown automata

Investor logo
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.

More info