BRÁZDIL, Tomáš, Antonín KUČERA a Oldřich STRAŽOVSKÝ. On the Decidability of Temporal Properties of Probabilistic Pushdown Automata. V. Diekert, B. Durand (Eds.). In Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005). Berlin: Springer, 2005. s. 145-157, 13 s. ISBN 3-540-24998-2.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
Název česky O rozhodnutelnosti temporálních vlastností zásobníkových automatů
Autoři BRÁZDIL, Tomáš (203 Česká republika), Antonín KUČERA (203 Česká republika, garant) a Oldřich STRAŽOVSKÝ (203 Česká republika).
V. Diekert, B. Durand (Eds.).
Vydání Berlin, Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005), od s. 145-157, 13 s. 2005.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/05:00012349
Organizační jednotka Fakulta informatiky
ISBN 3-540-24998-2
UT WoS 000229009500012
Klíčová slova anglicky probabilistic pushdown automata; probabilistic temporal logics
Štítky Probabilistic Pushdown Automata, probabilistic temporal logics
Změnil Změnil: doc. RNDr. Tomáš Brázdil, Ph.D., učo 4074. Změněno: 13. 2. 2006 12:42.
Anotace
We consider qualitative and quantitative model-checking problems for probabilistic pushdown automata (pPDA) and various temporal logics. We prove that the qualitative and quantitative model-checking problem for omega-regular properties and pPDA is in 2-EXPSPACE and 3-EXPTIME, respectively. We also prove that model-checking the qualitative fragment of the logic PECTL* for pPDA is in 2-EXPSPACE, and model-checking the qualitative fragment of PCTL for pPDA is in EXPSPACE. Furthermore, model-checking the qualitative fragment of PCTL is shown to be EXPTIME-hard even for stateless pPDA. Finally, we show that PCTL model-checking is undecidable for pPDA, and PCTL+ model-checking is undecidable even for stateless pPDA.
Anotace česky
V článku se zkoumá rozhodnutelnost a složitost problému ověření platnosti formulí kvantitativních a kvalitativních temporálních logik pro pravděpodobnostní zásobníkové automaty. Je dokázáno, že problém ověření formulí kvalitativního resp. kvantitavního fragmentu omega-regulárních vlastností patří do třídy 2-EXPSPACE resp. 3-EXPTIME. Dále je dokázáno, že problém ověření formulí kvalitativního fragmentu logiky PECTL* resp. PCTL pro pravděpodobnostní zásobníkové automaty patří do třídy 2-EXPSPACE resp. EXPSPACE. Přitom pro kvalitativní fragment PCTL je podán rovněž EXPTIME dolní složitostní odhad, který platí také pro pravděpodobnostní zásobníkové automaty s jediným kontrolním stavem. Konečně je prokázána nerozhodnutelnost problému ověření platnosti obecných formulí logiky PCTL pro pravděpodobnostní zásobníkové automaty.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Standardní projekty
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: 19. 10. 2019 17:31