On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic

In this paper, we define the notion of a {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity perspective. Specifically, we obtain the following important new results: (1) We first discuss the expressiveness of the logics PCTL, PCTL$^*$, $ω$-${\rm PCTL}$, and $ω$-${\rm PCTL}^*$ and study how Büchi conditions of probabilistic $ω$-pushdown systems influence $ω$-PCTL formulas. We then investigate the model-checking problem for {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (as defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}). By constructing $ω$-PCTL formulas that encode the {\em Post Correspondence Problem}, we show that this model-checking problem is generally undecidable. (2) We then study under which conditions there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-PCTL-like logic. In particular, we show that the model-checking problem for {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable and $\mathit{NP}$-hard. Currently, there is no known lower bound for this problem that is better than ours. (3) Finally, we investigate an upper bound for the model-checking problem for {\em stateless probabilistic $ω$-pushdown systems} against $ω$-bounded probabilistic computational tree logic ($ω$-bPCTL). We propose a potential approach to solving it by establishing a conditional upper bound and analyze the challenges of this method.

Paper

Similar papers

© 2026 NYSGPT2525 LLC