BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT a Antonín KUČERA. Branching-time model-checking of probabilistic pushdown automata. Journal of Computer and System Sciences, Academic Press, 2014, roč. 80, č. 1, s. 139-156. ISSN 0022-0000. doi:10.1016/j.jcss.2013.07.001.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Branching-time model-checking of probabilistic pushdown automata
Autoři BRÁZDIL, Tomáš (203 Česká republika, domácí), Václav BROŽEK (203 Česká republika, domácí), Vojtěch FOREJT (203 Česká republika) a Antonín KUČERA (203 Česká republika, garant, domácí).
Vydání Journal of Computer and System Sciences, Academic Press, 2014, 0022-0000.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor Computer sciences, information science, bioinformatics
Stát vydavatele Nizozemsko
Utajení není předmětem státního či obchodního tajemství
Impakt faktor Impact factor: 1.138
Kód RIV RIV/00216224:14330/14:00073430
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1016/j.jcss.2013.07.001
UT WoS 000325386500011
Klíčová slova česky Markovské procesy; zásobníkové automaty
Klíčová slova anglicky Markov chains; pushdown automata
Štítky formela-journal
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2015 03:17.
Anotace
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.
Návaznosti
GAP202/10/1469, projekt VaVNázev: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Grantová agentura ČR, Standardní projekty
VytisknoutZobrazeno: 16. 10. 2019 19:48