In this work, we first resolve a question in the probabilistic verification of infinite-state systems (specifically, the probabilistic pushdown systems). We show that model checking stateless probabilistic pushdown systems (pBPA) against probabilistic computational tree logic (PCTL) is generally undecidable. We define the quantum analogues of the probabilistic pushdown systems and Markov chains and investigate whether it is necessary to define a quantum analogue of probabilistic computational tree logic to describe the branching-time properties of the quantum Markov chain. We also study its model-checking problem and show that the model-checking of stateless quantum pushdown systems (qBPA) against probabilistic computational tree logic (PCTL) is generally undecidable, too. The immediate corollaries of the above results are summarized in the work.

翻译：在本工作中，我们首先解决了无限状态系统（具体来说，概率下推系统）概率验证中的一个问题。我们证明，针对概率计算树逻辑（PCTL）的无状态概率下推系统（pBPA）模型检测通常是不可判定的。我们定义了概率下推系统和马尔可夫链的量子模拟，并探讨了为描述量子马尔可夫链的分支时间属性而定义概率计算树逻辑的量子模拟是否必要。我们还研究了其模型检测问题，并证明针对概率计算树逻辑（PCTL）的无状态量子下推系统（qBPA）模型检测通常也是不可判定的。上述结果的直接推论在本文中进行了总结。