arxiv: 2604.17784 · v1 · submitted 2026-04-20 · 💻 cs.LO · quant-ph

Recognition: unknown

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

Sichen Ding , Zhiwu Li

Authors on Pith no claims yet

Pith reviewed 2026-05-10 04:16 UTC · model grok-4.3

classification 💻 cs.LO quant-ph

keywords current-state opacityquantum Petri netstrue-concurrency semanticsstabilizer formalismsymbolic verificationpartially observed systemstrace distance leakage

0 comments

The pith

Current-state opacity for safe partially observed quantum Petri nets is exactly verifiable using true-concurrency unfolding configurations and stabilizer-tableau propagation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines current-state opacity in safe partially observed quantum Petri nets by treating classical observations as partially ordered multisets through unfolding configurations. It measures quantitative leakage as the trace distance between an attacker's possible quantum states, conditioned on whether the system has reached a secret or non-secret marking, while preserving the classical notion of opacity. The verification algorithm uses targeted unfolding exploration, aggregates states only at maximal unobservable reach, and propagates stabilizer tableaus to compute the leakage. This combination avoids the explosion from concurrent interleavings and the overhead of full density matrices. A sympathetic reader would care because it provides a tractable way to check security in hybrid classical-quantum discrete-event systems where attackers can exploit both event sequences and quantum correlations.

Core claim

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

What carries the argument

True-concurrency unfolding configurations for observations as partially ordered multisets, paired with state aggregation at maximal unobservable reach and stabilizer-tableau propagation for exact leakage computation.

If this is right

The definition reduces to standard current-state opacity when quantum effects are absent.
The algorithm returns exact numerical leakage values rather than over-approximations.
Counterexample paths from the unfolding can directly guide opacity enforcement.
The entanglement-swapping case study demonstrates both correctness and reduced computation time.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same aggregation points at maximal unobservable reach could be tested on other quantum discrete-event models to check whether the exactness property holds beyond Petri nets.
True-concurrency semantics might expose opacity violations in classical systems that interleaving-based checks miss, by preserving partial-order information about unobservable events.

Load-bearing premise

The stabilizer formalism together with aggregation only at maximal unobservable reach yields an exact leakage value without approximation or missing quantum correlations for arbitrary safe partially observed quantum Petri nets.

What would settle it

A concrete counterexample where the computed trace distance from the aggregated stabilizer states differs from the distance obtained by full density-matrix simulation on the same net would show the leakage is not exact.

Figures

Figures reproduced from arXiv: 2604.17784 by Sichen Ding, Zhiwu Li.

**Figure 1.** Figure 1: Representative SPO-QPN architecture for the entanglement-swapping repeater-service case study. The control layer [PITH_FULL_IMAGE:figures/full_fig_p016_1.png] view at source ↗

**Figure 2.** Figure 2: Exact secret-conditioned attacker posteriors on the [PITH_FULL_IMAGE:figures/full_fig_p019_2.png] view at source ↗

**Figure 3.** Figure 3: Analytic policy-enforcement curve for the base instance [PITH_FULL_IMAGE:figures/full_fig_p019_3.png] view at source ↗

**Figure 5.** Figure 5: In contrast to the zero-leakage equivalence established in Corollary VII.5, their role here is explicitly diagnostic: they resolve to distinct canonical normal forms that diagrammatically isolate the structural mechanism of the algebraic leakage, despite originating from the identical foreground observation pomset. G. Discussion This case study supports the main claims of the paper through a unified, caus… view at source ↗

**Figure 4.** Figure 4: Graphical algebraic derivation of the posterior state for the secret branch ( [PITH_FULL_IMAGE:figures/full_fig_p021_4.png] view at source ↗

**Figure 5.** Figure 5: Consistent canonical posterior certificates (Normal [PITH_FULL_IMAGE:figures/full_fig_p021_5.png] view at source ↗

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a workable exact method for current-state opacity in safe quantum Petri nets by pairing true-concurrency unfolding with stabilizer-tableau propagation.

read the letter

This paper's core move is to lift current-state opacity into safe partially observed quantum Petri nets while keeping the analysis exact and avoiding the usual blow-ups from interleavings or full density matrices. It replaces ordinary trace semantics with true-concurrency unfolding so that observations become partially ordered multisets, then measures leakage as the trace distance between the attacker's posterior stabilizer states conditioned on secret versus non-secret markings. The classical opacity definition is recovered as a special case when the quantum component is trivial. The verification procedure aggregates states only at maximal unobservable reach and propagates the stabilizer tableau forward; the entanglement-swapping example shows that the computed leakage matches the expected value and that run time stays manageable compared with naive enumeration. The approach is internally consistent within the stated class of safe nets and stabilizer states. The main soft spot is the scope restriction: the exactness argument depends on the nets being safe and the quantum states staying inside the stabilizer formalism. If the model were extended to unsafe nets or to states requiring full density-matrix simulation, the aggregation step could lose correlations and the claims would need re-checking. No circular reasoning appears in the definitions or the algorithm outline. This is aimed at people already working on formal methods for discrete-event systems who now need to handle localized quantum correlations in security analysis. A reader who knows Petri-net unfolding and stabilizer simulation will find the algorithm and the case study directly usable. The paper deserves peer review because the combination of semantics and the concrete verification procedure is new enough and specific enough to be worth checking in detail.

Referee Report

0 major / 2 minor

Summary. The paper formalizes current-state opacity for safe partially observed quantum Petri nets (POQPNs) via a true-concurrency semantics that models classical observations as partially ordered multisets using unfolding configurations. It defines quantitative posterior-state leakage as the trace distance between an attacker's localized quantum states conditioned on whether the system has reached a secret or non-secret marking, preserving classical opacity. An exact symbolic verification algorithm is presented that combines targeted unfolding exploration, aggregation exclusively at maximal unobservable reach, and stabilizer-tableau propagation to avoid interleaving explosion and exponential density-matrix costs. The claims are supported by an entanglement-swapping case study demonstrating exact leakage computation and computational gains.

Significance. If the exactness arguments hold, the work meaningfully extends classical opacity theory to hybrid quantum-classical systems by incorporating quantum correlations into security analysis. The stabilizer-based exact symbolic procedure, with its targeted aggregation and tableau propagation, offers a tractable alternative to full state-space exploration while maintaining precision, as illustrated by the case study. This provides a concrete foundation for counterexample-guided leakage enforcement in quantum Petri net models.

minor comments (2)

The abstract states that the leakage definition 'strictly preserves classical opacity definitions,' but a brief explicit reduction argument (e.g., when the quantum component is trivial) would strengthen the claim without altering the central contribution.
In the case-study section, the reported computational gains would be more convincing if accompanied by concrete metrics (runtime, memory, or state count) comparing the proposed algorithm against a baseline without aggregation or tableau propagation.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and accurate summary of our work on current-state opacity in safe partially observed quantum Petri nets, as well as for the favorable assessment of its significance and the recommendation for minor revision. No specific major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity detected in derivation chain

full rationale

The paper defines current-state opacity and quantitative leakage (trace distance on posterior stabilizer states) from first principles using true-concurrency unfolding configurations and maximal-unobservable-reach aggregation. The verification procedure is constructed by composing independently established techniques—Petri-net unfolding, stabilizer tableaux, and state aggregation—without any claimed prediction or uniqueness result reducing to a fitted parameter, self-defined input, or load-bearing self-citation. The exactness claim follows from the algebraic properties of the chosen aggregation points and tableau propagation rather than by re-labeling inputs. No equation or step in the provided abstract or description exhibits the self-definitional, fitted-input, or ansatz-smuggling patterns. The derivation therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on standard assumptions from Petri-net theory and quantum information, plus a newly introduced leakage measure.

axioms (2)

standard math Safe Petri net properties and unfolding semantics
Used as the base model for representing the system and observations.
domain assumption Applicability of the stabilizer formalism to the quantum states appearing in the net
Enables symbolic tableau representation instead of full density matrices.

invented entities (1)

Quantitative posterior-state leakage no independent evidence
purpose: Measure of information leakage defined as trace distance between attacker quantum states conditioned on secret versus non-secret markings
New definition introduced to quantify leakage while preserving classical opacity when quantum parts are ignored.

pith-pipeline@v0.9.0 · 5484 in / 1318 out tokens · 43502 ms · 2026-05-10T04:16:00.017364+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

45 extracted references · 3 canonical work pages · 1 internal anchor

[1]

Notions of security and opacity in discrete event systems,

A. Saboori and C. N. Hadjicostis, “Notions of security and opacity in discrete event systems,” inProc. 46th IEEE Conference on Decision and Control, 2007, pp. 5056–5061

2007
[2]

Opacity of discrete event systems and its applications,

F. Lin, “Opacity of discrete event systems and its applications,”Auto- matica, vol. 47, no. 3, pp. 496–503, 2011

2011
[3]

Current-state opacity formulations in probabilistic finite automata,

A. Saboori and C. N. Hadjicostis, “Current-state opacity formulations in probabilistic finite automata,”IEEE Transactions on Automatic Control, vol. 59, no. 1, pp. 120–133, 2014

2014
[4]

Overview of discrete event systems opacity: Models, validation, and quantification,

R. Jacob, J.-J. Lesage, and J.-M. Faure, “Overview of discrete event systems opacity: Models, validation, and quantification,”Annual Reviews in Control, vol. 41, pp. 135–146, 2016. 21 |0⟩ qM (a) 1. Initial Circuit Spider Fusion − − − − − − − → qM (b) 2. Merged Red Spiders Discard Rule− − − − − − − → qM (c) 3. Maximally Mixed State Fig. 4: Graphical algebr...

2016
[5]

On the history of diag- nosability and opacity in discrete event systems,

S. Lafortune, F. Lin, and C. N. Hadjicostis, “On the history of diag- nosability and opacity in discrete event systems,”Annual Reviews in Control, vol. 45, pp. 257–266, 2018

2018
[6]

Comparative analysis of related notions of opacity in centralized and coordinated architectures,

Y .-C. Wu and S. Lafortune, “Comparative analysis of related notions of opacity in centralized and coordinated architectures,”Discrete Event Dynamic Systems, vol. 23, no. 3, pp. 307–339, 2013

2013
[7]

Comparing the notions of opacity for discrete-event systems,

J. Balun and T. Masopust, “Comparing the notions of opacity for discrete-event systems,”Discrete Event Dynamic Systems, vol. 31, no. 4, pp. 553–582, 2021

2021
[8]

A general language-based framework for specifying and verifying notions of opacity,

A. Wintenberg, M. Blischke, S. Lafortune, and N. Ozay, “A general language-based framework for specifying and verifying notions of opacity,”Discrete Event Dynamic Systems, vol. 32, no. 2, pp. 253–289, 2022

2022
[9]

Infinite-step opacity and k-step opacity of stochastic discrete-event systems,

X. Yin, Z. Li, W. Wang, and S. Li, “Infinite-step opacity and k-step opacity of stochastic discrete-event systems,”Automatica, vol. 99, pp. 266–274, 2019

2019
[10]

Supervisory control for opacity,

J. Dubreil, P. Darondeau, and H. Marchand, “Supervisory control for opacity,”IEEE Transactions on Automatic Control, vol. 55, no. 5, pp. 1089–1100, 2010

2010
[11]

Synthesis of insertion functions for en- forcement of opacity security properties,

Y .-C. Wu and S. Lafortune, “Synthesis of insertion functions for en- forcement of opacity security properties,”Automatica, vol. 50, no. 5, pp. 1336–1348, 2014

2014
[12]

Synthesis of optimal insertion functions for opacity enforce- ment,

——, “Synthesis of optimal insertion functions for opacity enforce- ment,”IEEE Transactions on Automatic Control, vol. 61, no. 3, pp. 571–584, 2016

2016
[13]

Enforcement of opacity by public and private insertion functions,

Y . Ji, Y .-C. Wu, and S. Lafortune, “Enforcement of opacity by public and private insertion functions,”Automatica, vol. 93, pp. 369–378, 2018

2018
[14]

Synthesis of dynamic masks for infinite-step opacity,

X. Yin and S. Li, “Synthesis of dynamic masks for infinite-step opacity,” IEEE Transactions on Automatic Control, vol. 65, no. 4, pp. 1429–1441, 2020

2020
[15]

Opacity enforcement using non- deterministic publicly known edit functions,

Y . Ji, X. Yin, and S. Lafortune, “Opacity enforcement using non- deterministic publicly known edit functions,”IEEE Transactions on Automatic Control, vol. 64, no. 10, pp. 4369–4376, 2019

2019
[16]

Optimal synthesis of opacity-enforcing super- visors for qualitative and quantitative specifications,

Y . Xie, S. Li, and X. Yin, “Optimal synthesis of opacity-enforcing super- visors for qualitative and quantitative specifications,”IEEE Transactions on Automatic Control, vol. 69, no. 8, pp. 4958–4973, 2024

2024
[17]

Verification of state-based opacity using Petri nets,

Y . Tong, Z. Li, C. Seatzu, and A. Giua, “Verification of state-based opacity using Petri nets,”IEEE Transactions on Automatic Control, vol. 62, no. 6, pp. 2823–2837, 2017

2017
[18]

On-line verification of current-state opacity by Petri nets and integer linear programming,

X. Cong, M. P. Fanti, A. M. Mangini, and Z. Li, “On-line verification of current-state opacity by Petri nets and integer linear programming,” Automatica, vol. 94, pp. 205–213, 2018

2018
[19]

Current-state opacity modelling and verification in partially observed Petri nets,

I. Saadaoui, Z. Li, and N. Wu, “Current-state opacity modelling and verification in partially observed Petri nets,”Automatica, vol. 116, p. 108907, 2020

2020
[20]

Strong current-state and initial-state opacity of discrete-event systems,

X. Han, K. Zhang, J. Zhang, Z. Li, and Z. Chen, “Strong current-state and initial-state opacity of discrete-event systems,”Automatica, vol. 148, p. 110756, 2023

2023
[21]

Quantum repeaters: The role of imperfect local operations in quantum communication,

H.-J. Briegel, W. D ¨ur, J. I. Cirac, and P. Zoller, “Quantum repeaters: The role of imperfect local operations in quantum communication,”Physical Review Letters, vol. 81, no. 26, pp. 5932–5935, 1998

1998
[22]

Quantum repeaters based on entanglement purification,

W. D ¨ur, H.-J. Briegel, J. I. Cirac, and P. Zoller, “Quantum repeaters based on entanglement purification,”Physical Review A, vol. 59, no. 1, pp. 169–181, 1999

1999
[23]

The quantum internet,

H. J. Kimble, “The quantum internet,”Nature, vol. 453, no. 7198, pp. 1023–1030, 2008

2008
[24]

Inside quantum repeaters,

W. J. Munro, K. Azuma, K. Tamaki, and K. Nemoto, “Inside quantum repeaters,”IEEE Journal of Selected Topics in Quantum Electronics, vol. 21, no. 3, pp. 78–90, 2015

2015
[25]

Quantum internet: A vision for the road ahead,

S. Wehner, D. Elkouss, and R. Hanson, “Quantum internet: A vision for the road ahead,”Science, vol. 362, no. 6412, pp. 1–9, 2018

2018
[26]

Quantum internet: Networking challenges in distributed quantum computing,

A. S. Cacciapuoti, M. Caleffi, F. Tafuri, F. S. Cataliotti, S. Gherardini, and G. Bianchi, “Quantum internet: Networking challenges in distributed quantum computing,”IEEE Network, vol. 34, no. 1, pp. 137–143, 2020

2020
[27]

Quantum information-flow security: Noninterference and access control,

M. Ying, Y . Feng, and N. Yu, “Quantum information-flow security: Noninterference and access control,” inProc. 2013 IEEE 26th Computer Security Foundations Symposium. IEEE Computer Society, 2013, pp. 130–144

2013
[28]

Modeling concurrency with partial orders,

V . Pratt, “Modeling concurrency with partial orders,”International Journal of Parallel Programming, vol. 15, no. 1, pp. 33–71, 1986

1986
[29]

Event structures,

G. Winskel, “Event structures,” inAdvances in Petri Nets 1986, Part II: Proceedings of an Advanced Course, ser. Lecture Notes in Computer Science. Springer, 1987, vol. 255, pp. 325–392

1986
[30]

Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits,

K. L. McMillan, “Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits,” inComputer Aided Veri- fication, ser. Lecture Notes in Computer Science, vol. 663. Springer, 1993, pp. 164–174

1993
[31]

An improvement of mcmillan’s unfolding algorithm,

J. Esparza, S. R ¨omer, and W. V ogler, “An improvement of mcmillan’s unfolding algorithm,”Formal Methods in System Design, vol. 20, no. 3, pp. 285–310, 2002

2002
[32]

Quantum Petri nets with event structure semantics,

J. S. Joachim, M. de Visme, S. Haar, and G. Winskel, “Quantum Petri nets with event structure semantics,”arXiv preprint arXiv:2509.01423, 2025

work page arXiv 2025
[33]

Improved simulation of stabilizer circuits,

S. Aaronson and D. Gottesman, “Improved simulation of stabilizer circuits,”Physical Review A, vol. 70, no. 5, p. 052328, 2004

2004
[34]

The ZX-calculus is complete for stabilizer quantum mechanics,

M. Backens, “The ZX-calculus is complete for stabilizer quantum mechanics,”New Journal of Physics, vol. 16, no. 9, p. 093021, 2014

2014
[35]

Coecke and A

B. Coecke and A. Kissinger,Picturing quantum processes: A first course in quantum theory and diagrammatic reasoning. Cambridge University Press, 2017

2017
[36]

Completeness of graphical languages for mixed states quantum mechanics,

T. Carette, E. Jeandel, S. Perdrix, and R. Vilmart, “Completeness of graphical languages for mixed states quantum mechanics,” inProc. 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 132. Schloss Dagstuhl – Leibniz-Zentrum f ¨ur Informatik, 2019, pp. 10...

2019
[37]

ZX-calculus for the working quantum computer scientist

J. van de Wetering, “ZX-calculus for the working quantum computer scientist,”arXiv preprint arXiv:2012.13966, 2020

work page arXiv 2012
[38]

Dagger compact closed categories and completely positive maps,

P. Selinger, “Dagger compact closed categories and completely positive maps,”Electronic Notes in Theoretical Computer Science, vol. 170, pp. 139–163, 2007

2007
[39]

M. A. Nielsen and I. L. Chuang,Quantum Computation and Quantum Information. Cambridge University Press, 2010. 22

2010
[40]

Heinosaari and M

T. Heinosaari and M. Ziman,The Mathematical Language of Quantum Theory: From Uncertainty to Entanglement. Cambridge University Press, 2011

2011
[41]

M. M. Wilde,Quantum Information Theory. Cambridge University Press, 2013

2013
[42]

C. W. Helstrom,Quantum Detection and Estimation Theory. Academic Press, 1976

1976
[43]

Quantum detection and estimation theory,

——, “Quantum detection and estimation theory,”Journal of Statistical Physics, vol. 1, no. 2, pp. 231–252, 1969

1969
[44]

The Heisenberg Representation of Quantum Computers

D. Gottesman, “The heisenberg representation of quantum computers,” arXiv preprint quant-ph/9807006, 1998

work page internal anchor Pith review arXiv 1998
[45]

SPO-QPN: Current-state opacity in safe quantum Petri nets: True-concurrency semantics and symbolic verification,

S. Ding, “SPO-QPN: Current-state opacity in safe quantum Petri nets: True-concurrency semantics and symbolic verification,” https://github. com/dingsichen/SPO-QPN, 2026, accessed: Apr. 19, 2026

2026