Analysis of a Quantum Error Correcting Code using Quantum Process Calculus

TL;DR

This paper applies quantum process calculus to model and analyze quantum communication protocols, demonstrating behavioral equivalence between system models and specifications, with a focus on quantum error correction systems.

Contribution

It introduces the use of quantum process calculus CQP for formal analysis of quantum protocols, establishing behavioral equivalence and its preservation in various contexts.

Findings

Behavioral equivalence is a congruence in CQP.

Two quantum error correction systems are successfully analyzed.

Formal verification of quantum protocols is feasible with this approach.

Abstract

We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. The key idea is to define two systems, one modelling a protocol and one expressing a specification, and prove that they are behaviourally equivalent. We summarize the necessary theory in the process calculus CQP, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. We illustrate the approach by analyzing two versions of a quantum error correction system.