Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems
arXiv:1405.4806
Abstract
In this communication, we resolve a longstanding open question in the probabilistic verification of infinite-state systems. We show that model checking {\it stateless probabilistic pushdown systems (pBPA)} against {\it probabilistic computational tree logic (PCTL)} is generally undecidable.
[v21] 3 figures revised