In this paper, we define the notion of {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against the logic of $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity view. Specifically, we obtain the following equally important new results: (1) We define {\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}. (2) 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 $\mathit{NP}$-hard.

翻译：本文定义了"概率$ω$-下推自动机"的概念，并从计算复杂度的角度研究了针对$ω$-概率计算树逻辑（$ω$-PCTL）及其有界版本的模型检验问题。具体而言，我们获得了以下同等重要的新结果：（1）首次定义了"概率$ω$-下推自动机"，并研究了"无状态概率$ω$-下推系统（$ω$-pBPA）"对$ω$-PCTL（由Chatterjee、Sen和Henzinger在文献\cite{CSH08}中定义）的模型检验问题，结果表明无状态概率$ω$-下推系统（$ω$-pBPA）对$ω$-PCTL的模型检验在一般情况下是不可判定的。我们的方法是构造编码"Post对应问题"的$ω$-PCTL公式。（2）随后研究在何种情况下存在针对"无状态概率$ω$-下推系统"进行模型检验的算法，并证明无状态概率$ω$-下推系统对$ω$-有界概率计算树逻辑（$ω$-bPCTL）的模型检验问题是可判定的，且进一步证明该问题是$\mathit{NP}$-困难的。