Computational Complexity of Model-Checking Quantum Pushdown Systems

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