Analysis of a Quantum Error Correcting Code using Quantum Process Calculus

Timothy A. S. Davidson
(University of Warwick, UK)
Simon J. Gay
(University of Glasgow, UK)
Rajagopal Nagarajan
(University of Warwick, UK)
Ittoop Vergheese Puthoor
(University of Glasgow, UK)

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.

In Bart Jacobs, Peter Selinger and Bas Spitters: Proceedings 8th International Workshop on Quantum Physics and Logic (QPL 2011), Nijmegen, Netherlands, October 27-29, 2011, Electronic Proceedings in Theoretical Computer Science 95, pp. 67–80.
Published: 1st October 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: