Undecidability of model-checking branching-time properties of stateless probabilistic pushdown process
From MaRDI portal
Abstract: In this paper, we settle a problem in probabilistic verification of infinite--state process (specifically, {it probabilistic pushdown process}). We show that model checking {it stateless probabilistic pushdown process} (pBPA) against {it probabilistic computational tree logic} (PCTL) is undecidable.
This page was built for publication: Undecidability of model-checking branching-time properties of stateless probabilistic pushdown process
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6251671)
