Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Theory and applications of quantum process calculus

Ittoop Vergheese Puthoor

Published Dec 31, 2015• 2 citations
Publisher

Abstract

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.

DOI
10.25405/ncl.34498860

Related papers

Formal verification techniques using quantum process calculus

Timothy A. S. Davidson

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.

•Sep 12, 2026•27 citations

Formal verification of higher dimensional quantum protocols

Ittoop Vergheese Puthoor

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.

arXiv:2409.17980•Sep 26, 2024•0 citations

Analysis of a Quantum Error Correcting Code using Quantum Process Calculus

Timothy A. S. Davidson, Simon J. Gay, Rajagopal Nagarajan +1 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.

arXiv:1210.0614•Electronic Proceedings in Theoretical Computer Science•Oct 1, 2012•18 citations

Verification of Linear Optical Quantum Computing using Quantum Process Calculus

Sonja Franke‐Arnold, Simon J. Gay, Ittoop Vergheese Puthoor

We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to include multiple particles (namely photons) as information carriers, described by Fock states or number states. We summarise the theory in this paper, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. In previous work, we have used quantum process calculus to model LOQC but without verifying models against specifications. In this paper, for the first time, we are able to carry out verification. We illustrate this approach by describing and verifying two models of an LOQC CNOT gate.

arXiv:1408.1460•Electronic Proceedings in Theoretical Computer Science•Aug 6, 2014•8 citations

Application of Quantum Process Calculus to Higher Dimensional Quantum Protocols

Simon J. Gay, Ittoop Vergheese Puthoor

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.

arXiv:1303.2896•Electronic Proceedings in Theoretical Computer Science•Jul 29, 2014•7 citations

Model checking for communicating quantum processes

Tim R. Davidson, S. J. Gay, H. Mlnařík +2 more

Quantum communication is a rapidly growing area of research and development. Quantum cryptography has already been implemented for secure communication, and commercial solutions are available. The application of formal methods to classical computing and communication systems has been very successful, and is widely used by industry. We expect similar benefits for the verification of quantum systems. Communicating Quantum Processes (CQP) is a process calculus based on the π-calculus with the inclusion of primitives for quantum information. Process calculi provide an algebraic approach to system specification and behavioural analysis. The Quantum Model Checker (QMC) is a tool for the automated verification of system correctness. Through an exhaustive search of the possible executions, QMC can check that correctness properties expressed using temporal logic formulae are satisfied. In this paper we describe our approach to the verification of quantum systems using a combination of process calculus and model checking. We also define a formal translation from CQP to the modelling language used by QMC and prove that this preserves the semantics of all supported CQP processes. © 2012 Old City Publishing, Inc.

ENLIGHTEN (Jurnal Bimbingan dan Konseling Islam)•Jan 1, 2012•20 citations
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.
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.
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.
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.
We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to include multiple particles (namely photons) as information carriers, described by Fock states or number states. We summarise the theory in this paper, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. In previous work, we have used quantum process calculus to model LOQC but without verifying models against specifications. In this paper, for the first time, we are able to carry out verification. We illustrate this approach by describing and verifying two models of an LOQC CNOT gate.
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.
Quantum communication is a rapidly growing area of research and development. Quantum cryptography has already been implemented for secure communication, and commercial solutions are available. The application of formal methods to classical computing and communication systems has been very successful, and is widely used by industry. We expect similar benefits for the verification of quantum systems. Communicating Quantum Processes (CQP) is a process calculus based on the π-calculus with the inclusion of primitives for quantum information. Process calculi provide an algebraic approach to system specification and behavioural analysis. The Quantum Model Checker (QMC) is a tool for the automated verification of system correctness. Through an exhaustive search of the possible executions, QMC can check that correctness properties expressed using temporal logic formulae are satisfied. In this paper we describe our approach to the verification of quantum systems using a combination of process calculus and model checking. We also define a formal translation from CQP to the modelling language used by QMC and prove that this preserves the semantics of all supported CQP processes. © 2012 Old City Publishing, Inc.