On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic
Deren Lin, Tianrong Lin
TL;DR
This work introduces probabilistic ω-pushdown automata (ω-pPDS) and studies their model-checking against ω-PCTL, proving undecidability in the general ω-PCTL setting for stateless variants. It then identifies a decidable frontier by using ω-bPCTL, where the bounded until operator yields decidability and NP-hardness, via reductions from (modified) bounded PCP. The results delineate the boundary between undecidability and tractability for probabilistic infinite-state systems with ω-properties, and establish a foundation for further algorithmic development in bounded- until logics. The findings impact verification of probabilistic recursive systems by clarifying which logics allow effective model-checking and which do not.
Abstract
In this paper, we obtain the following equally important new results: We first extend the notion of {\em probabilistic pushdown automaton} to {\em probabilistic $ω$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $ω$-pushdown systems ($ω$-pBPA)} against $ω$-PCTL is generally undecidable. Our approach is to construct $ω$-PCTL formulas encoding the {\em Post Correspondence Problem}. We then study in which case there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable, and further show that this problem is in $NP$-hard.