On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
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. 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 | 10201 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 VaV | Název: Verifikace nekonečně stavových systémů |
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 29. 9. 2024 17:21