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: 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}. 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.

翻译：本文首次定义{\em 概率ω-下推自动机}的概念，并从计算复杂性角度研究其针对ω-概率计算树逻辑（ω-PCTL）及其有界版本的模型检测问题。具体而言，我们取得以下同等重要的新成果：首次定义{\em 概率ω-下推自动机}，并研究{\em 无状态概率ω-下推系统（ω-pBPA）}针对ω-PCTL（由Chatterjee、Sen与Henzinger在\cite{CSH08}中定义）的模型检测问题，证明{\em 无状态概率ω-下推系统（ω-pBPA）}针对ω-PCTL的模型检测在一般情况下是不可判定的。我们的方法是通过构造编码{\em 波斯特对应问题}的ω-PCTL公式来实现。随后我们研究在何种情况下存在{\it 无状态概率ω-下推系统}的模型检测算法，并证明{\it 无状态概率ω-下推系统}针对ω-{\it 有界概率计算树逻辑}（ω-bPCTL）的模型检测问题是可判定的，进一步证明该问题是$\mathit{NP}$-难的。