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

Automated equivalence checking of quantum information systems

Ebrahim Ardeshir-Larijani

Published Sep 11, 2026• 0 citations
Publisher

Abstract

Quantum technologies have progressed beyond the laboratory setting and are beginning to make an impact on industrial development. The construction of practical, general purpose quantum computers has been challenging, to say the least. But quantum cryptographic and communication devices have been available in the commercial marketplace for a few years. Quantum networks have been built in various cities around the world, and plans are afoot to launch a dedicated satellite for quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety and security-critical applications. In this thesis we investigate the theory and practice of equivalence checking of quantum information systems. We present a tool, Quantum Equivalence Checker (QEC), which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. For our process algebraic language CCSq, we define an operational semantics and a superoperator semantics. While in general, simulation of quantum systems using current computing technology is infeasible, we restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms and representation of quantum states. By using the stabilizer representation of quantum states we introduce various algorithms for testing equality of stabilizer states. In this thesis, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of a concurrent system. Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states. We present algorithms for the checking of functionality and equivalence of quantum protocols. Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using equivalence checking, QEC is applied to specify and verify a variety of interesting and practical quantum protocols from quantum communication and quantum cryptography to quantum error correction and quantum fault tolerant computation, where for each protocol different sequential and concurrent model are defined in CCSq. We also explain the implementation details of the QEC tool and report on the experimental results produced by using it on the verification of a number of case studies.

DOI
10.82444/warw.33648946

Related papers

Automated Equivalence Checking of Concurrent Quantum Systems

Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan

The novel field of quantum computation and quantum information has gathered significant momentum in the last few years. It has the potential to radically impact the future of information technology and influence the development of modern society. The construction of practical, general purpose quantum computers has been challenging, but quantum cryptographic and communication devices have been available in the commercial marketplace for several years. Quantum networks have been built in various cities around the world and a dedicated satellite has been launched by China to provide secure quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety- and security-critical applications. Experience with classical hardware and software systems has shown the difficulty of achieving robust and reliable implementations. We present CCS q , a concurrent language for describing quantum systems, and develop verification techniques for checking equivalence between CCS q processes. CCS q has well-defined operational and superoperator semantics for protocols that are functional , in the sense of computing a deterministic input-output relation for all interleavings arising from concurrency in the system. We have implemented QEC (Quantum Equivalence Checker), a tool that takes the specification and implementation of quantum protocols, described in CCS q , and automatically checks their equivalence. QEC is the first fully automatic equivalence checking tool for concurrent quantum systems. For efficiency purposes, we restrict ourselves to Clifford operators in the stabilizer formalism, but we are able to verify protocols over all input states. We have specified and verified a collection of interesting and practical quantum protocols, ranging from quantum communication and quantum cryptography to quantum error correction.

ACM Transactions on Computational Logic•Oct 31, 2018•17 citations

Specification and Verification of Quantum Protocols

Simon J. Gay, Rajagopal Nagarajan, Nickolas K. Papanikolaou

We describe model-checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We discuss the modeling language of QMC, the logic used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies, including quantum teleportation and the BB84 quantum coin-flipping protocol. 11.1 Introduction Model-checking is a method of computer-aided verification used widely in both academia and industry for the analysis of software and communication systems. The method essentially consists of three phases: (1) modeling the system of interest at a suitable level of abstraction, usually by describing it in a formal specification language; (2) specifying the properties that the system must satisfy – these properties are typically expressed with reference to the system model, using a logic designed specially for this purpose ( e.g. , linear or branching time temporal logic); and (3) supplying the model and the properties to a model-checking tool, which automatically constructs the state space of the model and checks whether or not the given properties are satisfied (and if not, usually providing a counterexample).

Cambridge University Press eBooks•Nov 30, 2009•20 citations

Model checking quantum protocols

Nickolas K. Papanikolaou

This thesis describes model checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We detail the syntax, semantics and type system of QMC’s modelling language, the logic QCTL which is used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies.

•Sep 9, 2026•18 citations

Automated Verification of Quantum Protocols by Equivalence Checking

Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan

In this paper we introduce a technique and a tool for formal verification of various quantum information processing protocols. The tool uses stabilizer formalism and is capable of representing concurrent quantum protocol, thus is more expressive than quantum circuits. We also report on experimental results of using our Quantum Equivalence Checker (QEC) to analyse a range of quantum information processing protocols.

arXiv:1312.5951•Dec 20, 2013•0 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 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
Quantum technologies have progressed beyond the laboratory setting and are beginning to make an impact on industrial development. The construction of practical, general purpose quantum computers has been challenging, to say the least. But quantum cryptographic and communication devices have been available in the commercial marketplace for a few years. Quantum networks have been built in various cities around the world, and plans are afoot to launch a dedicated satellite for quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety and security-critical applications. In this thesis we investigate the theory and practice of equivalence checking of quantum information systems. We present a tool, Quantum Equivalence Checker (QEC), which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. For our process algebraic language CCSq, we define an operational semantics and a superoperator semantics. While in general, simulation of quantum systems using current computing technology is infeasible, we restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms and representation of quantum states. By using the stabilizer representation of quantum states we introduce various algorithms for testing equality of stabilizer states. In this thesis, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of a concurrent system. Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states. We present algorithms for the checking of functionality and equivalence of quantum protocols. Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using equivalence checking, QEC is applied to specify and verify a variety of interesting and practical quantum protocols from quantum communication and quantum cryptography to quantum error correction and quantum fault tolerant computation, where for each protocol different sequential and concurrent model are defined in CCSq. We also explain the implementation details of the QEC tool and report on the experimental results produced by using it on the verification of a number of case studies.
The novel field of quantum computation and quantum information has gathered significant momentum in the last few years. It has the potential to radically impact the future of information technology and influence the development of modern society. The construction of practical, general purpose quantum computers has been challenging, but quantum cryptographic and communication devices have been available in the commercial marketplace for several years. Quantum networks have been built in various cities around the world and a dedicated satellite has been launched by China to provide secure quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety- and security-critical applications. Experience with classical hardware and software systems has shown the difficulty of achieving robust and reliable implementations. We present CCS q , a concurrent language for describing quantum systems, and develop verification techniques for checking equivalence between CCS q processes. CCS q has well-defined operational and superoperator semantics for protocols that are functional , in the sense of computing a deterministic input-output relation for all interleavings arising from concurrency in the system. We have implemented QEC (Quantum Equivalence Checker), a tool that takes the specification and implementation of quantum protocols, described in CCS q , and automatically checks their equivalence. QEC is the first fully automatic equivalence checking tool for concurrent quantum systems. For efficiency purposes, we restrict ourselves to Clifford operators in the stabilizer formalism, but we are able to verify protocols over all input states. We have specified and verified a collection of interesting and practical quantum protocols, ranging from quantum communication and quantum cryptography to quantum error correction.
We describe model-checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We discuss the modeling language of QMC, the logic used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies, including quantum teleportation and the BB84 quantum coin-flipping protocol. 11.1 Introduction Model-checking is a method of computer-aided verification used widely in both academia and industry for the analysis of software and communication systems. The method essentially consists of three phases: (1) modeling the system of interest at a suitable level of abstraction, usually by describing it in a formal specification language; (2) specifying the properties that the system must satisfy – these properties are typically expressed with reference to the system model, using a logic designed specially for this purpose ( e.g. , linear or branching time temporal logic); and (3) supplying the model and the properties to a model-checking tool, which automatically constructs the state space of the model and checks whether or not the given properties are satisfied (and if not, usually providing a counterexample).
This thesis describes model checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We detail the syntax, semantics and type system of QMC’s modelling language, the logic QCTL which is used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies.
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.
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.