Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems
Logic in Computer Science
2025-07-02 v21 Formal Languages and Automata Theory
Logic
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.
Cite
@article{arxiv.1405.4806,
title = {Model-Checking PCTL Properties of Stateless Probabilistic Pushdown Systems},
author = {Deren Lin and Tianrong Lin},
journal= {arXiv preprint arXiv:1405.4806},
year = {2025}
}
Comments
[v21] 3 figures revised