Portal de Periódicos da CAPES

On the Decidability of Temporal Properties of Probabilistic Pushdown Automata

2005; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-540-31856-9_12

1611-3349

Tomǎš Brázdil, Antonı́n Kučera, Oldřich Stražovský,

Software Testing and Debugging Techniques

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 ω-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 2-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.