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 counterparts, i.e., {\em quantum pushdown system (qPDS)} and {\em quantum Markov chains}, and prove a necessary and sufficient condition for a qPDS to be well formed, also presenting a method to extend the local transition function of a well-formed qPDS to a unitary local time evolution operator. Next, we 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 (qBPA)} 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 (qBPA)} against {\it bounded probabilistic computational tree logic} (bPCTL) is decidable, and further show that this problem is in $\mathit{NP}$-hard. Our reduction is from the {\it bounded Post Correspondence Problem} for the first time, a well-known $\mathit{NP}$-complete problem.

翻译：本文从计算复杂性角度研究了量子下推系统的模型检验问题。我们取得了以下同等重要且有趣的新结果：首先，我们将**概率下推系统**和**马尔可夫链**的概念扩展至其量子对应物，即**量子下推系统（qPDS）**和**量子马尔可夫链**，并证明了qPDS良构的一个充要条件，同时提出了一种将良构qPDS的局部转移函数扩展为幺正局部时间演化算子的方法。其次，我们探讨了是否需要定义**概率计算树逻辑**的量子类比来描述**量子马尔可夫链**的概率性与分支时间性质。我们研究了其模型检验问题，并证明**无状态量子下推系统（qBPA）**对**概率计算树逻辑（PCTL）**的模型检验通常是不可判定的，即不存在针对**无状态量子下推系统（qBPA）**对**概率计算树逻辑**进行模型检验的算法。随后，我们研究了在何种情况下存在针对**无状态量子下推系统**的模型检验算法，并证明**无状态量子下推系统（qBPA）**对**有界概率计算树逻辑（bPCTL）**的模型检验问题是可判定的，进一步证明该问题是$\mathit{NP}$-难的。我们的归约首次源自**有界波斯特对应问题**，这是一个众所周知的$\mathit{NP}$-完全问题。