Computational Complexity of Model-Checking Quantum Pushdown Systems
Deren Lin, Tianrong Lin
TL;DR
<3-5 sentence high-level summary> This work investigates the computational complexity of model-checking quantum pushdown systems (qPDS) by extending classical probabilistic models to the quantum domain and studying model-checking against probabilistic temporal logics. It establishes a precise well-formedness condition for qPDS and a construction to extend local quantum transitions to a unitary time-evolution operator, enabling a quantum-mechanical formalism for analysis. The authors prove undecidability for model-checking generalized stateless quantum pushdown systems against PCTL, and they show that model-checking stateless quantum pushdown systems against bounded PCTL is decidable but NP-hard via reductions from the bounded Post Correspondence Problem. The results illuminate the limitations and possibilities of quantum-model-checking and motivate open questions about algorithmic approaches for broader classes of quantum systems and logics.
Abstract
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 generalized stateless quantum pushdown systems (gqBPA)} against {\it probabilistic computational tree logic (PCTL)} is generally undecidable, i.e., there exists no algorithm for model-checking {\it generalized stateless quantum pushdown systems (gqBPA)} 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.