An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains

TL;DR

This paper introduces a new logical framework, QCTL, for analyzing quantum Markov chains using fidelity measures, providing an exact, decidable method for computing minimal fidelity over initial states.

Contribution

It develops a quantum logic based on fidelity, models noisy channels with super-operators, and reduces the problem to quantifier elimination, enabling exact analysis of quantum systems.

Findings

Method is exact and decidable in exponential time.

Successfully applied to a quantum IPv4 protocol.

Demonstrates effectiveness through implementation.

Abstract

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.