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

arXiv:1108.0469 · Electronic Proceedings in Theoretical Computer Science

Formal Analysis of Quantum Systems using Process Calculus

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

Published Jul 31, 2011• 6 citations
arXivHTMLPDF

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 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.

DOI
10.4204/eptcs.59.9

Related papers

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

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

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

Theory and applications of quantum process calculus

Ittoop Vergheese Puthoor

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.

•Dec 31, 2015•2 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

Formal Verification of Quantum Protocols

Rajagopal Nagarajan, Gay, Simon

We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be transferable to more general quantum information processing scenarios. The example we use is the quantum key distribution protocol proposed by Bennett and Brassard, commonly referred to as BB84. We present a model of the protocol in the process calculus CCS and the results of some initial analyses using the Concurrency Workbench of the New Century (CWB-NC).

arXiv:quant-ph/0203086•Mar 18, 2002•24 citations
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.
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.
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.
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.
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 propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be transferable to more general quantum information processing scenarios. The example we use is the quantum key distribution protocol proposed by Bennett and Brassard, commonly referred to as BB84. We present a model of the protocol in the process calculus CCS and the results of some initial analyses using the Concurrency Workbench of the New Century (CWB-NC).