Branching-time model-checking of probabilistic pushdown automata

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2014
Druh Článek v odborném periodiku
Časopis / Zdroj Journal of Computer and System Sciences
Fakulta / Pracoviště MU

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.