Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers

TL;DR

The paper tackles the challenge of providing a congruence-respecting behavioural equivalence for quantum concurrent systems. It introduces a labelled, scheduler-aware version of lqCCS (lqCCS) and proves that simple syntactic schedulers suffice to define a saturated bisimilarity $\sim_s$ that is a congruence for parallel composition and aligns with quantum observational limits. It further derives an equivalent labelled bisimilarity $\sim_l$ and shows $\sim_s$ and $\sim_l$ coincide, grounding atomic observables of quantum-capable processes. The framework is validated through canonical quantum protocols (e.g., teleportation and superdense coding) and points to future work on decidability and symbolic verification methods. Collectively, this work advances automated verification for distributed quantum systems by making observable quantum properties explicit and ensuring compatibility with quantum theory.

Abstract

The development of quantum algorithms and protocols calls for adequate modelling and verification techniques, which requires abstracting and focusing on the basic features of quantum concurrent systems, like CCS and CSP have done for their classical counterparts. So far, an equivalence relation is still missing that is a congruence for parallel composition and adheres to the limited discriminating power implied by quantum theory. In fact, defining an adequate bisimilarity for quantum-capable, concurrent systems proved a difficult task, because unconstrained non-determinism allows to spuriously discriminate indistinguishable quantum systems. We investigate this problem by enriching a linear quantum extension of CCS with simple physically admissible schedulers. We show that our approach suffices for deriving a well-behaved bisimilarity that satisfies the aforementioned desiderata.

Figures (1)

• Figure 1: Observer in parallel with indistinguishable qubit sources.