  In this paper, we resolve a longstanding open question in the probabilistic
verification of infinite-state systems. We show that model checking {\em
stateless probabilistic pushdown systems (pBPA)} against {\em probabilistic
computational tree logic (PCTL)} is generally undecidable.
