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

• URL: http://arxiv.org/abs/2604.17784v1
• Date: Mon, 20 Apr 2026 04:14:26 GMT
• Title: Current-State Opacity in Safe Partially Observed Quantum Petri Nets: True-Concurrency Semantics and Exact Symbolic Verification
• Abstract summary: We formalize current-state opacity within the framework of safe partially observed quantum Petri nets.<n>We define quantitative posterior-state leakage as the trace distance between the attacker's localized quantum states.<n>An entanglement-swapping case study validates the exact leakage evaluation, demonstrates substantial computational gains.
• Score: 15.392070935885739
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Hysteretic squashed entanglement in many-body quantum systems [42.085941481155295]
  Entanglement in many-body quantum systems is distributed across spatial regions.<n>We propose hysteretic entanglement $T_sq$, a conditional entanglement that measures the genuine quantum correlations between two subregions.<n>We show that $T_sq$ can detect genuine quantum correlations across both adjacent and long-range subsystems.
  arXiv  Detail & Related papers  (2026-03-10T17:00:49Z)
• Unsupervised Anomaly Detection in Multi-Agent Trajectory Prediction via Transformer-Based Models [45.08545174556591]
  We propose an unsupervised anomaly detection framework based on a multi-agent Transformer.<n>A dual evaluation scheme has been proposed to assess both detection stability and physical alignment.<n>Our framework identifies 388 unique anomalies missed by Time-to-Collision and statistical baselines.
  arXiv  Detail & Related papers  (2026-01-28T08:33:10Z)
• Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning [52.23804865017831]
  We address the problem of verifying closed-loop contraction in nonlinear control systems whose controller and contraction metric are both parameterized by neural networks.<n>We derive a tractable and scalable sufficient condition for closed-loop contractivity that reduces to checking that the dominant eigenvalue of a symmetric Metzler matrix is nonpositive.
  arXiv  Detail & Related papers  (2025-12-01T23:06:56Z)
• Joint momenta-coordinates states as pointer states in quantum decoherence [0.0]
  We show that only in the underdamped case do joint momenta-coordinates states remain pure and robust for all times, establishing them as the true pointer states.<n>This extends Isar's earlier underdamped treatment, generalizes the concept beyond Gaussian approximations, and embeds classical robustness in the quantum phase space formalism.
  arXiv  Detail & Related papers  (2025-09-20T15:50:24Z)
• Faithful and secure distributed quantum sensing under general-coherent attacks [0.0]
  We introduce, theoretically analyze, and experimentally demonstrate single- and two-way protocols for distributed sensing.<n>We introduce a safety-threshold mechanism that allows the protocol to proceed in low-noise cases and quantifying the potential tampering with respect to the ideal estimation procedure.<n>We demonstrate our protocols in a photonic-based implementation, observing that the possibility of guaranteeing a safety threshold may come at a significant price in terms of the estimation bias.
  arXiv  Detail & Related papers  (2025-05-05T12:48:41Z)
• Bounding the Sample Fluctuation for Pure States Certification with Local Random Measurement [4.923287660970805]
  Recent advancements in randomized measurement techniques have provided fresh insights in this area. We investigate the fundamental properties of schemes that certify pure quantum states through random local Haar measurements. Our results unveil the intrinsic interplay between operator complexity and the efficiency of quantum algorithms, serving as an obstacle to local certification of pure states with long-range entanglement.
  arXiv  Detail & Related papers  (2024-10-22T02:26:44Z)
• Exploiting hidden structures in non-convex games for convergence to Nash equilibrium [62.88214569402201]
  A wide array of modern machine learning applications can be formulated as non-cooperative Nashlibria. We provide explicit convergence guarantees for both deterministic and deterministic environments.
  arXiv  Detail & Related papers  (2023-12-27T15:21:25Z)
• Noninterference Analysis of Reversible Systems: An Approach Based on Branching Bisimilarity [41.94295877935867]
  Classical equivalence-based approaches to noninterference mainly rely on weak bisimulation semantics.<n>We show that this approach is not sufficient to identify potential covert channels in the presence of reversible computations.<n>To capture the effects of back-and-forth computations, it is necessary to switch to a more expressive semantics.
  arXiv  Detail & Related papers  (2023-11-27T09:57:04Z)
• Secure and robust randomness with sequential quantum measurements [0.0]
  We prove a Tsirelson-like boundary for sequential quantum correlations, which represents a trade-off in nonlocality shared by sequential users.<n>Our simple qubit protocol reaches this boundary, and numerical analysis shows improved robustness under realistic noise.<n>This study advances understanding of sequential quantum correlations and offers insights for efficient device-independent protocols.
  arXiv  Detail & Related papers  (2023-09-21T17:50:29Z)
• Regularized Vector Quantization for Tokenized Image Synthesis [126.96880843754066]
  Quantizing images into discrete representations has been a fundamental problem in unified generative modeling. deterministic quantization suffers from severe codebook collapse and misalignment with inference stage while quantization suffers from low codebook utilization and reconstruction objective. This paper presents a regularized vector quantization framework that allows to mitigate perturbed above issues effectively by applying regularization from two perspectives.
  arXiv  Detail & Related papers  (2023-03-11T15:20:54Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Robust Control Performance for Open Quantum Systems [0.0]
  A formalism is developed to measure performance based on the transmission of a dynamic perturbation or initial state preparation error. A difficulty arising from the singularity of the closed-loop Bloch equations for the quantum state is overcome by introducing the #-inversion lemma. Additional difficulties occur when symmetry gives rise to multiple open-loop poles, which under symmetry-breaking unfold into single eigenvalues.
  arXiv  Detail & Related papers  (2020-08-31T15:51:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.