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:1704.07031

Formal verification of quantum communication protocols using Petri nets

Sheng Zhang, Yonghui Ma, Chunning Meng, Haiping Wang

Published Apr 24, 2017• 2 citations
arXivHTMLPDF

Abstract

This paper presents a new formal method for verification of quantum communication protocols. By extending the symbolic system of Petri nets, we can define quantum pure states in Petri-net settings. Therefore, it is possible to emerge a framework from formalizing basic quantum phenomena, which are utilized to achieve communication tasks. We also present an example of applying this framework to the modeling and analyzing quantum communication protocols to show how it works.

DOI
10.48550/arxiv.1704.07031

Related papers

Probabilistic Model--Checking of Quantum Protocols

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

We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.

arXiv:quant-ph/0504007•Apr 1, 2005•54 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

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

Modeling of Quantum Computer by using Quantum Petri Net

Ito Shinsuke, Atsushi Ohta, Kohkichi Tsuji

Petri Net that is an effective tool for concurrent systems, has been extended to Quantum Petri Net. The conventional modeling method of quantum computer using Quantum Petri Net, have several drawbacks. This paper defines new model and examines conditions to solve these drawbacks, and proposes new model from modeling quantum Turing machine, and shows that the model can simulate more general calculation processes than which the conventional model.

International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC)•Jul 1, 2008•3 citations

Symbolic Model Checking Quantum Circuits in Maude

Canh Minh Do, Kazuhiro Ogata

This paper presents a symbolic approach to model checking quantum circuits by using a set of laws from quantum mechanics and basic matrix operations with Dirac notation.We use Maude, a high-level specification/programming language based on rewriting logic, to implement our symbolic approach.As a case study, we use the approach to formally specify and verify the correctness of the quantum teleportation protocol, which is an important quantum communication protocol in the early work of quantum communications.Moreover, our implementation can be used as a general framework to formally specify and verify quantum circuits in Maude in an effortless way, where only an initial quantum state and a sequence of actions describing how a quantum circuit works in a simple way are required.

Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering•Jul 1, 2023•7 citations

Quantum Petri Nets

Tiberiu Stefan Letia, Elenita Maria Durla-Pasca, Dahlia Al-Janabi

The development of quantum software applications requires models capable to describe quantum features (superposition, entanglement, reversibility etc.) as well as the software algorithm requirements. The newly proposed Quantum Petri Nets (QPNs) have the structure of the classical Petri Nets (PNs), but their tokens represent superposed quantum states fulfilling the Hilbert space features. Instead of the integer numerical values of the PN marking, QPNs use quantum marking describing an extreme huge space. New conditions for the transition enabling and new mappings for the transition executions are conceived. A PN based language is used for the structure analysis. Replacing the classical tokens with the probability distribution of the quantum vectors, the QPN simulation is possible as well as the construction of a reachability graph.

International Conference on System Theory, Control and Computing (ICSTCC)•Oct 20, 2021•5 citations
This paper presents a new formal method for verification of quantum communication protocols. By extending the symbolic system of Petri nets, we can define quantum pure states in Petri-net settings. Therefore, it is possible to emerge a framework from formalizing basic quantum phenomena, which are utilized to achieve communication tasks. We also present an example of applying this framework to the modeling and analyzing quantum communication protocols to show how it works.
We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.
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).
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.
This paper presents a symbolic approach to model checking quantum circuits by using a set of laws from quantum mechanics and basic matrix operations with Dirac notation.We use Maude, a high-level specification/programming language based on rewriting logic, to implement our symbolic approach.As a case study, we use the approach to formally specify and verify the correctness of the quantum teleportation protocol, which is an important quantum communication protocol in the early work of quantum communications.Moreover, our implementation can be used as a general framework to formally specify and verify quantum circuits in Maude in an effortless way, where only an initial quantum state and a sequence of actions describing how a quantum circuit works in a simple way are required.
The development of quantum software applications requires models capable to describe quantum features (superposition, entanglement, reversibility etc.) as well as the software algorithm requirements. The newly proposed Quantum Petri Nets (QPNs) have the structure of the classical Petri Nets (PNs), but their tokens represent superposed quantum states fulfilling the Hilbert space features. Instead of the integer numerical values of the PN marking, QPNs use quantum marking describing an extreme huge space. New conditions for the transition enabling and new mappings for the transition executions are conceived. A PN based language is used for the structure analysis. Replacing the classical tokens with the probability distribution of the quantum vectors, the QPN simulation is possible as well as the construction of a reachability graph.