In this paper, we study the problem of model-checking quantum pushdown systems from a computational complexity point of view. We arrive at the following equally important, interesting new results: We first extend the notions of the {\it probabilistic pushdown systems} and {\it Markov chains} to their quantum analogues and investigate the question of whether it is necessary to define a quantum analogue of {\it probabilistic computational tree logic} to describe the probabilistic and branching-time properties of the {\it quantum Markov chain}. We study its model-checking question and show that model-checking of {\it stateless quantum pushdown systems (qBPA)} against {\it probabilistic computational tree logic (PCTL)} is generally undecidable, i.e., there exists no algorithm for model-checking {\it stateless quantum pushdown systems} against {\it probabilistic computational tree logic}. We then study in which case there exists an algorithm for model-checking {\it stateless quantum pushdown systems} and show that the problem of model-checking {\it stateless quantum pushdown systems} against {\it bounded probabilistic computational tree logic} (bPCTL) is decidable, and further show that this problem is $\mathit{NP}$-hard. Our reduction is from the {\it bounded Post Correspondence Problem} for the first time, a well-known $\mathit{NP}$-complete problem. Our above results advance the field of model-checking quantum systems significantly, since all of the above important and interesting results on model-checking quantum pushdown systems are completely unknown previously.

翻译：本文从计算复杂性角度研究量子下推系统的模型检验问题。我们获得了以下同等重要且有趣的新结果：首先，我们将概率下推系统和马尔可夫链的概念推广至其量子对应形式，并探讨是否需要定义概率计算树逻辑的量子对应逻辑来描述量子马尔可夫链的概率性与分支时序性质。我们研究了其模型检验问题，证明了无状态量子下推系统（qBPA）针对概率计算树逻辑（PCTL）的模型检验在一般情况下是不可判定的，即不存在针对无状态量子下推系统验证概率计算树逻辑的通用算法。随后，我们研究了在何种情况下存在针对无状态量子下推系统的模型检验算法，证明了无状态量子下推系统针对有界概率计算树逻辑（bPCTL）的模型检验是可判定的，并进一步证明该问题是NP难的。我们的归约首次基于有界波斯特对应问题——一个著名的NP完全问题。上述结果显著推动了量子系统模型检验领域的发展，因为此前关于量子下推系统模型检验的所有重要且有趣的结果均属未知。