2012/10/02 by Timothy A. S. Davidson, Simon J. Gay, Rajagopal Nagarajan +1
Computer Science · Physics and Astronomy · #cs.LO #cs.PL #quant-ph
paper · pdf · doi:10.4204/eptcs.95.7
published as EPTCS 95, 2012, pp. 67-80 · In Proceedings QPL 2011, arXiv:1210.0298
arxiv created 2012/10/02 · arxiv updated 2012/10/03
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.