Branching-time model-checking of probabilistic pushdown automata

Varování

Publikace nespadá pod Fakultu sportovních studií, 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:	Formální metody pro analýzu a verifikaci komplexních systémů