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.

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

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

---

Anotace

V originále

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.

Č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