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. We have extended the quantum process calculus to describe d-dimensional quantum systems, which has not been done before. We summarise the necessary theory in the generalisation of quantum gates and Bell states and use the theory to apply the quantum process calculus CQP to quantum protocols, namely qudit teleportation and superdense coding.
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. We have extended the quantum process calculus to describe d-dimensional quantum systems, which has not been done before. We summarise the necessary theory in the generalisation of quantum gates and Bell states and use the theory to apply the quantum process calculus CQP to quantum protocols, namely qudit teleportation and superdense coding.
Formal methods have been a successful approach for modelling and verifying the correctness of complex technologies like microprocessor chip design, biological systems and others. This is the main motivation of developing quantum formal techniques which is to describe and analyse quantum information processing systems. Our previous work demonstrates the possibility of using a quantum process calculus called Communicating Quantum Processes (CQP) to model and describe higher dimensional quantum systems. By developing the theory to generalise the fundamental gates and Bell states, we have modelled quantum qudit protocols like teleportation and superdense coding in CQP. In this paper, we demonstrate the use of CQP to analyse higher dimensional quantum protocols. The main idea is to define two processes, one modelling the real protocol and the other expressing a specification, and prove that they are behaviourally equivalent. This is a work-in-progress and we present our preliminary results in extending the theory of behavioural equivalence in CQP to verify higher dimensional quantum protocols using qudits.
Formal methods is an area in theoretical computer science that provides the theories and tools for describing and verifying the correctness of computing systems. Usually, such systems comprise of concurrent and communicating components. The success of this field led to the development of quantum formal methods by transferring the ideas of formal methods to quantum systems. In particular, formal methods provides a systematic methodology for verification of systems. Quantum process calculus is a specialised field in quantum formal methods that helps to describe and analyse the behaviour of systems that combine quantum and classical elements. We focus on the theory and applications of quantum process calculus in particular to use Communicating Quantum Processes (CQP), a quantum process calculus, to model and analyse quantum information processing (QIP) systems. Previous work on CQP defined labelled transition relations for CQP in order to describe external interactions and also established the theory of behavioural equivalence in CQP based on probabilistic branching bisimilarity. This theory formalizes the idea of observational indistinguishability in order to prove or verify the correctness of a system, and an important property of the equivalence is the congruence property. We use the theory to analyse two versions of a quantum error correcting code system. We use the equational theory of CQP from the previous work and define an additional three new axioms in order to analyse quantum protocols comprising quantum secret-sharing, quantum error correction, remote-CNOT and superdense coding. We have expanded the framework of modelling in CQP from providing an abstract view of the quantum system to describe a realistic QIP system such as linear optical quantum computing (LOQC) and its associated experimental processes. By extending the theory of behavioural equivalence of CQP, we have formally verified two models of an LOQC CNOT gate using CQP. The two models use different measurement semantics in order to work at different levels of abstraction. This flexibility of the process calculus approach allows descriptions from detailed hardware implementations up to more abstract specifications. The orbital angular momentum (OAM) property of light allows us to perform experiments in studying higher dimensional quantum systems and their applications to quantum technologies. In relation to this work, we have extended CQP to model higher dimensional quantum protocols.
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.
Quantum communication is a rapidly growing area of research and development. While the successful construction of a large-scale quantum computer may be some years away, there are already commercial implementations of secure communication using quantum cryptography. The application of formal methods to classical communication and cryptographic systems has been very successful, and is now widely used in industry by organisations such as Intel, Microsoft and NASA. There is reason to believe that similar benefits can be expected for the verification of quantum systems. In this thesis, we focus on the use of process calculus, specifically Communicating Quantum Processes (CQP), for the analysis of quantum protocols. Congruence relations are an important aspect of process calculus, since they provide the foundation for equational reasoning. Previous work on congruence relations for quantum processes excluded the classical information arising from measurements, and was therefore unable to analyse many of the interesting known quantum communication protocols. Developing a congruence relation for general quantum processes is difficult because of the interaction between measurement, entanglement and parallel composition. We define a labelled transition relation for CQP in order to describe external interactions. Based on this semantics, we define a notion of observational equivalence for CQP processes, namely probabilistic branching bisimilarity. We find that this relation is not preserved by parallel composition, however we are able to gain a deeper understanding of the link between probabilistic branching and measurement. Based on this newfound understanding, we present a novel semantics for quantum processes, combining mixed quantum states with probabilistic branching. With respect to this new semantic model, we define full probabilistic branching bisimilarity and prove that it is a congruence. We use this congruence relation to discuss an axiomatic approach to the verification of quantum processes. The quantum teleportation protocol is used as a primary example throughout, and we prove that it is congruent to a quantum channel. We define a translation from CQP to the Quantum Model Checker (QMC) in order to provide automated verification techniques using CQP specifications. We prove that this translation preserves the semantics of CQP processes, thereby enabling a multifaceted approach to formal verification by enhancing the manual techniques of process calculus with the benefits of model checking.
We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.