Model-Checking PCTL Properties of Stateless Probabilistic Pushdown   Systems
  In this communication, 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. 
Deren Lin, Tianrong Lin
cs.LO cs.FL math.LO