In this paper, we define the quantum analogues of the {\em probabilistic pushdown systems} and {\em Markov chains}, and further investigate whether it is necessary to define a quantum analogue of {\em probabilistic computational tree logic} to describe the branching-time properties of the {\em quantum Markov chain} defined in this paper. We study its model-checking question and show that the model-checking of {\em stateless quantum pushdown systems (qBPA)} against {\em probabilistic computational tree logic (PCTL)} is generally undecidable, with the immediate corollaries summarized. We define the notion of {\em probabilistic $\omega$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $\omega$-pushdown system ($\omega$-pBPA)} against $\omega$-PCTL (defined by Chatterjee et al. in \cite{CSH08}) and show that the model-checking of {\em stateless probabilistic $\omega$-pushdown systems ($\omega$-pBPA)} against $\omega$-PCTL is generally undecidable, with immediate consequences summarized. Our approach is to construct formulas of $\omega$-PCTL encoding the {\em Post Correspondence Problem} indirectly.

翻译：本文定义了{\em 概率下推系统}和{\em 马尔可夫链}的量子类比，并进一步探讨是否有必要定义{\em 概率计算树逻辑}的量子类比，以描述本文所定义的{\em 量子马尔可夫链}的分支时间性质。我们研究了其模型检验问题，并证明了{\em 无状态量子下推系统（qBPA）}对{\em 概率计算树逻辑（PCTL）}的模型检验通常是不可判定的，同时总结了直接推论。我们首次定义了{\em 概率$\omega$-下推自动机}的概念，并研究了{\em 无状态概率$\omega$-下推系统（$\omega$-pBPA）}对$\omega$-PCTL（由Chatterjee等人在\cite{CSH08}中定义）的模型检验问题，证明了{\em 无状态概率$\omega$-下推系统（$\omega$-pBPA）}对$\omega$-PCTL的模型检验通常是不可判定的，同时总结了直接后果。我们的方法是通过构造$\omega$-PCTL公式间接编码{\em 波斯特对应问题}。