ESPARZA, Javier, Antonín KUČERA a Richard MAYR. Model Checking Probabilistic Pushdown Automata. Logical Methods in Computer Science, 2006, roč. 2, 1-2, s. 1-31. ISSN 1860-5974.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Model Checking Probabilistic Pushdown Automata
Název česky Ověřování formulí temporálních logik pro pravděpodobnostní zásobníkové automaty
Autoři ESPARZA, Javier (724 Španělsko), Antonín KUČERA (203 Česká republika, garant) a Richard MAYR (276 Německo).
Vydání Logical Methods in Computer Science, 2006, 1860-5974.
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 Německo
Utajení není předmětem státního či obchodního tajemství
WWW LMCS home page
Kód RIV RIV/00216224:14330/06:00016670
Organizační jednotka Fakulta informatiky
UT WoS 000223180900002
Klíčová slova anglicky pushdown automata; Markov chains; probabilistic model checking
Štítky Markov chains, probabilistic model checking, pushdown automata
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 22. 11. 2006 17:26.
Anotace
We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for PCTL and the subclass of stateless pPDA. Finally, we consider the class of omega-regular properties and show that both qualitative and quantitative model checking for pPDA is decidable.
Anotace česky
V článku se zkoumá problém algoritmické ověřitelnosti dané formule temporální logiky pro daný pravděpodobnostní zásobníkový automat. Nejprve jsou vyšetřeny formule, které lze specifikovat jako parametrizovanou náhodnou procházku. Pak jsou vyšetřeny obecnější formule definovatelné v logice PCTL a jejím kvalitativním fragmentu.
Návaznosti
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 22. 10. 2019 08:04