2005
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
BRÁZDIL, Tomáš; Antonín KUČERA and Oldřich STRAŽOVSKÝBasic information
Original name
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
Name in Czech
O rozhodnutelnosti temporálních vlastností zásobníkových automatů
Authors
BRÁZDIL, Tomáš (203 Czech Republic); Antonín KUČERA (203 Czech Republic, guarantor) and Oldřich STRAŽOVSKÝ (203 Czech Republic)
V. Diekert, B. Durand (Eds.).
V. Diekert, B. Durand (Eds.).
Edition
Berlin, Proceedings of 22nd Symposium on Theoretical Aspects of Computer Science (STACS 2005), p. 145-157, 13 pp. 2005
Publisher
Springer
Other information
Language
English
Type of outcome
Proceedings paper
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Germany
Confidentiality degree
is not subject to a state or trade secret
RIV identification code
RIV/00216224:14330/05:00012349
Organization unit
Faculty of Informatics
ISBN
3-540-24998-2
UT WoS
000229009500012
Keywords in English
probabilistic pushdown automata; probabilistic temporal logics
Changed: 13/2/2006 12:42, doc. RNDr. Tomáš Brázdil, Ph.D., MBA
In the original language
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.
In Czech
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.
Links
| GA201/03/1161, research and development project |
| ||
| MSM0021622419, plan (intention) |
| ||
| 1M0545, research and development project |
|