标题： 量子下推系统的模型检测计算复杂性 显示英文标题

标题： Computational Complexity of Model-Checking Quantum Pushdown Systems

摘要： 在本文中，我们从计算复杂性的角度研究模型检测量子下推系统的問題。 我们得出了以下同样重要且有趣的新的结果： 我们首先将{\it 概率下推系统}和{\it 马尔可夫链}的概念扩展到它们的量子对应物，并研究是否有必要定义{\it 概率计算树逻辑}的量子对应物来描述{\it 量子马尔可夫链}的概率和分支时间性质。 我们研究其模型检测问题，并表明对{\it 无状态量子下推系统 (qBPA)}与{\it 概率计算树逻辑（PCTL）}的模型检测通常是不可判定的，即不存在对{\it 无状态量子下推系统}与{\it 概率计算树逻辑}进行模型检测的算法。 我们接着研究在何种情况下存在对{\it 无状态量子下推系统}的模型检测算法，并表明对{\it 无状态量子下推系统}与{\it 有界概率计算树逻辑}（bPCTL）的模型检测问题是可判定的，进一步表明该问题属于$NP$-hard。 我们的归约首次是从{\it 有界邮递员问题 对应问题}进行的，这是一个著名的$NP$-完全问题。 显示英文摘要

摘要： 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 in $NP$-hard. Our reduction is from the {\it bounded Post Correspondence Problem} for the first time, a well-known $NP$-complete problem.