Branching-time model-checking of probabilistic pushdown automata
| Autoři | |
|---|---|
| Rok publikování | 2014 |
| Druh | Článek v odborném periodiku |
| Časopis / Zdroj | Journal of Computer and System Sciences |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1016/j.jcss.2013.07.001 |
| Obor | Informatika |
| Klíčová slova | Markov chains; pushdown automata |
| Popis | 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. |
| Související projekty: |