An algebraic method to fidelity-based model checking over quantum Markov chains

Fidelity is one of the most widely used quantities in quantum information that measures the distance of two quantum states through a noisy channel, a kind of quantum operations. In this paper, we consider the model of quantum Markov chain (QMC), in which transitions are weighted by super-operators to characterize quantum operations and the initial quantum state is left parametric. A quantum analogy of probabilistic computation tree logic, called QCTL, is introduced to take into account fidelity, instead of probability measure, over QMC. The key to the model checking problem lies in computing the fidelity of the super-operator valued measure specified by a path formula in QCTL. It is minimized over all initial quantum states, which is intended for analyzing the system performance in the worst case. We achieve it by a reduction to quantifier elimination in the existential theory of the reals. The method is absolutely exact, so that model checking QCTL formulas against QMCs is proved to be decidable in exponential time.(c) 2022 Elsevier B.V. All rights reserved.