J
2014
Branching-time model-checking of probabilistic pushdown automata
BRÁZDIL, Tomáš, Václav BROŽEK, Vojtěch FOREJT a Antonín KUČERA
Základní údaje
Originální název
Branching-time model-checking of probabilistic pushdown automata
Vydání
Journal of Computer and System Sciences, Academic Press, 2014, 0022-0000
Další údaje
Typ výsledku
Článek v odborném periodiku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Nizozemské království
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
Klíčová slova česky
Markovské procesy; zásobníkové automaty
Klíčová slova anglicky
Markov chains; pushdown automata
Příznaky
Mezinárodní význam, Recenzováno
V originále
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 VaV | | Název: Formální metody pro analýzu a verifikaci komplexních systémů | | Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů |
|
Zobrazeno: 28. 4. 2025 22:01