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

Quantum Petri Nets with Event Structure semantics

Julien Saan Joachim, Marc de Visme, Stefan Haar, Glynn Winskel

Published Sep 1, 2025• 0 citations
arXivHTMLPDF

Abstract

Classical Petri nets provide a canonical model of concurrency, with unfolding semantics linking nets, occurrence nets, and event structures. No comparable framework exists for quantum concurrency: existing ''quantum Petri nets'' lack rigorous concurrent and sound quantum semantics, analysis tools, and unfolding theory. We introduce Quantum Petri Nets (QPNs), Petri nets equipped with a quantum valuation compatible with the quantum event structure semantics of Clairambault, De Visme, and Winskel (2019). Our contributions are: (i) a local definition of Quantum Occurrence Nets (LQONs) compatible with quantum event structures, (ii) a construction of QPNs with a well-defined unfolding semantics, (iii) a compositional framework for QPNs. This establishes a semantically well grounded model of quantum concurrency, bridging Petri net theory and quantum programming.

DOI
10.48550/arxiv.2509.01423

Related papers

Quantum Petri Nets with Event Structures semantics

Julien Saan Joachim, Marc de Visme, Stefan Haar

Classical Petri nets provide a canonical model of concurrency, with unfolding semantics linking nets, occurrence nets, and event structures. No comparable framework exists for quantum concurrency: existing ''quantum Petri nets'' lack rigorous concurrent and sound quantum semantics, analysis tools, and unfolding theory. We introduce Quantum Petri Nets (QPNs), Petri nets equipped with a quantum valuation compatible with the quantum event structure semantics of Clairambault, De Visme, and Winskel (2019). Our contributions are: (i) a local definition of Quantum Occurrence Nets (LQONs) compatible with quantum event structures, (ii) a construction of QPNs with a well-defined unfolding semantics, (iii) a compositional framework for QPNs. This establishes a semantically well grounded model of quantum concurrency, bridging Petri net theory and quantum programming.

arXiv:2508.14531•Aug 20, 2025•0 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

Formal verification of quantum communication protocols using Petri nets

Sheng Zhang, Yonghui Ma, Chunning Meng +1 more

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.

arXiv:1704.07031•Apr 24, 2017•2 citations

Concurrent semantics for probabilistic and quantum languages

Vítor Emanuel Gonçalves Fernandes

This thesis explores both theoretical and practical aspects of concurrent programming languages that integrate probabilistic and/or quantum computations. On the theoretical side, we investigate how event structures, a model for concurrency, can be used to furnish concurrent languages with denotational semantics. Event structures are studied in three distinct settings: non-deterministic, probabilistic, and quantum computation. Based on these three realms, we successively extend a core imperative-like concurrent language with non-deterministic choice, probabilistic choice, and standard quantum operations. For each extension, we define both operational and denotational semantics and establish their equivalence through soundness and adequacy results. Soundness ensures that every behavior obtainable through the operational semantics is reflected denotationally, showing that the denotational semantics correctly abstracts the computations. Conversely, adequacy guarantees that whenever the denotational semantics yields a value, this value can be produced by the operational semantics, demonstrating that the operational semantics explicitly realises what the denotational semantics predicts. On the practical side, motivated by the growing interplay between classical and quantum computers, we integrate non-deterministic choice, probabilistic choice, and quantum operations into a single language, further extended with a synchronization primitive. We develop an interpreter for this language and test it on several illustrative examples, including three versions of the Dining Philosophers problem: concurrentonly, probabilistic, and quantum. Using our tool, we demonstrate that a result stated in the literature about the quantum Dining Philosophers problem does not hold, leaving open the question of whether an efficient algorithm for solving it exists.

•Jun 20, 2026•0 citations

Current-State Opacity in Safe Partially Observed Quantum Petri Nets: True-Concurrency Semantics and Exact Symbolic Verification

Sichen Ding, Zhiwu Li

Classical opacity theory for discrete-event systems relies strictly on observable event sequences, fundamentally failing to capture security breaches in hybrid architectures where an attacker exploits both classical traces and localized quantum correlations. To address this gap, we formalize current-state opacity within the framework of safe partially observed quantum Petri nets by introducing a true-concurrency semantics that represents classical observations as partially ordered multisets via unfolding configurations. Building upon this, we define quantitative posterior-state leakage as the trace distance between the attacker's localized quantum states, evaluated conditionally on whether the underlying system has reached a secret or non-secret marking. This formulation strictly preserves classical opacity definitions. To achieve computational tractability, we apply the stabilizer formalism and develop an exact symbolic verification algorithm. By combining targeted unfolding exploration, state aggregation exclusively at maximal unobservable reach, and stabilizer-tableau propagation, this procedure circumvents both concurrent interleaving explosions and exponential density-matrix overhead. Finally, an entanglement-swapping case study validates the exact leakage evaluation, demonstrates substantial computational gains, and establishes a rigorous interface for counterexample-guided leakage enforcement.

cs.LOCross-listedarXiv:2604.17784•Apr 21, 2026•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
Classical Petri nets provide a canonical model of concurrency, with unfolding semantics linking nets, occurrence nets, and event structures. No comparable framework exists for quantum concurrency: existing ''quantum Petri nets'' lack rigorous concurrent and sound quantum semantics, analysis tools, and unfolding theory. We introduce Quantum Petri Nets (QPNs), Petri nets equipped with a quantum valuation compatible with the quantum event structure semantics of Clairambault, De Visme, and Winskel (2019). Our contributions are: (i) a local definition of Quantum Occurrence Nets (LQONs) compatible with quantum event structures, (ii) a construction of QPNs with a well-defined unfolding semantics, (iii) a compositional framework for QPNs. This establishes a semantically well grounded model of quantum concurrency, bridging Petri net theory and quantum programming.
Classical Petri nets provide a canonical model of concurrency, with unfolding semantics linking nets, occurrence nets, and event structures. No comparable framework exists for quantum concurrency: existing ''quantum Petri nets'' lack rigorous concurrent and sound quantum semantics, analysis tools, and unfolding theory. We introduce Quantum Petri Nets (QPNs), Petri nets equipped with a quantum valuation compatible with the quantum event structure semantics of Clairambault, De Visme, and Winskel (2019). Our contributions are: (i) a local definition of Quantum Occurrence Nets (LQONs) compatible with quantum event structures, (ii) a construction of QPNs with a well-defined unfolding semantics, (iii) a compositional framework for QPNs. This establishes a semantically well grounded model of quantum concurrency, bridging Petri net theory and quantum programming.
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.
This thesis explores both theoretical and practical aspects of concurrent programming languages that integrate probabilistic and/or quantum computations. On the theoretical side, we investigate how event structures, a model for concurrency, can be used to furnish concurrent languages with denotational semantics. Event structures are studied in three distinct settings: non-deterministic, probabilistic, and quantum computation. Based on these three realms, we successively extend a core imperative-like concurrent language with non-deterministic choice, probabilistic choice, and standard quantum operations. For each extension, we define both operational and denotational semantics and establish their equivalence through soundness and adequacy results. Soundness ensures that every behavior obtainable through the operational semantics is reflected denotationally, showing that the denotational semantics correctly abstracts the computations. Conversely, adequacy guarantees that whenever the denotational semantics yields a value, this value can be produced by the operational semantics, demonstrating that the operational semantics explicitly realises what the denotational semantics predicts. On the practical side, motivated by the growing interplay between classical and quantum computers, we integrate non-deterministic choice, probabilistic choice, and quantum operations into a single language, further extended with a synchronization primitive. We develop an interpreter for this language and test it on several illustrative examples, including three versions of the Dining Philosophers problem: concurrentonly, probabilistic, and quantum. Using our tool, we demonstrate that a result stated in the literature about the quantum Dining Philosophers problem does not hold, leaving open the question of whether an efficient algorithm for solving it exists.
Classical opacity theory for discrete-event systems relies strictly on observable event sequences, fundamentally failing to capture security breaches in hybrid architectures where an attacker exploits both classical traces and localized quantum correlations. To address this gap, we formalize current-state opacity within the framework of safe partially observed quantum Petri nets by introducing a true-concurrency semantics that represents classical observations as partially ordered multisets via unfolding configurations. Building upon this, we define quantitative posterior-state leakage as the trace distance between the attacker's localized quantum states, evaluated conditionally on whether the underlying system has reached a secret or non-secret marking. This formulation strictly preserves classical opacity definitions. To achieve computational tractability, we apply the stabilizer formalism and develop an exact symbolic verification algorithm. By combining targeted unfolding exploration, state aggregation exclusively at maximal unobservable reach, and stabilizer-tableau propagation, this procedure circumvents both concurrent interleaving explosions and exponential density-matrix overhead. Finally, an entanglement-swapping case study validates the exact leakage evaluation, demonstrates substantial computational gains, and establishes a rigorous interface for counterexample-guided leakage enforcement.