  Fidelity is one of the most widely used quantities in quantum information
that measure the distance of quantum states through a noisy channel. In this
paper, we introduce a quantum analogy of computation tree logic (CTL) called
QCTL, which concerns fidelity instead of probability in probabilistic CTL, over
quantum Markov chains (QMCs). Noisy channels are modelled by super-operators,
which are specified by QCTL formulas; the initial quantum states are modelled
by density operators, which are left parametric in the given QMC. The problem
is to compute the minimumfidelity over all initial states for conservation. We
achieve it by a reduction to quantifier elimination in the existential theory
of the reals. The method is absolutely exact, so that QCTL formulas are proven
to be decidable in exponential time. Finally, we implement the proposed method
and demonstrate its effectiveness via a quantum IPv4 protocol.
