Technical Reports

The report FIMU-RS-2005-01

On the Decidability of Temporal Properties of Probabilistic Pushdown Automata

by Tomá¹ Brázdil, Antonín Kuèera, Oldøich Stra¾ovský, A full version of the paper presented at STACS 2005. February 2005, 33 pages.

FIMU-RS-2005-01. Available as Postscript, PDF.

Abstract:

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.