Showing 1–2 of 2 results for author: Davidson, T A S

Analysis of a Quantum Error Correcting Code using Quantum Process Calculus

Authors: Timothy A. S. Davidson, Simon J. Gay, Rajagopal Nagarajan, Ittoop Vergheese Puthoor

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,… ▽ More 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. △ Less

Submitted 1 October, 2012; originally announced October 2012.

Comments: In Proceedings QPL 2011, arXiv:1210.0298

ACM Class: D.3.1; F.3.1

Journal ref: EPTCS 95, 2012, pp. 67-80

Formal Analysis of Quantum Systems using Process Calculus

Authors: Timothy A. S. Davidson, Simon J. Gay, Rajagopal Nagarajan

Abstract: Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and co… ▽ More Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11. △ Less

Submitted 1 August, 2011; originally announced August 2011.

Comments: In Proceedings ICE 2011, arXiv:1108.0144

Journal ref: EPTCS 59, 2011, pp. 104-110