The report FIMU-RS-2005-01
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
A full version of the paper presented at STACS 2005. February 2005, 33 pages.
Available as Postscript,
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
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.