Verification of quantum protocols adopting physically admissible schedulers

Recent developments in the ield of quantum communication demonstrate that secure communication protocols based on quantum features are already practical. Reliable veriication techniques are of paramount importance for these technologies, given their high implementation cost and critical contexts of application. Extensions of process calculi such as CCS and �- calculus have been proposed in the literature, together with various notions of behavioural equivalence. However, their standard probabilistic models turn out to introduce some non-deterministic capabilities that are not aligned with the observational properties of physical quantum systems, leading to bisimilarity notions that distinguish processes that should be physically equivalent. Nonetheless, we argue that non-deterministic features are fundamental to account for inputs, environments and adversarial behaviour. To address this issue, we propose lqCCS, a process calculus that integrates concurrency, non-determinism and quantum capabilities. The calculus is enriched with a linear type system that enforces the no-cloning principle and resolves ambiguities in the visibility of ancillary qubits. We introduce a novel semantics in terms of distributions, where explicit physically admissible schedulers constrain probabilistic composition and forbid ill-deined non-deterministic moves, while preserving the expressivity needed to model real-world protocols. We investigate a scheduled version of saturated bisimilarity, deeming two lqCCS processes behaviourally equivalent if no observer can tell them apart. The adequacy of the approach is veriied by lifting a known result from quantum mechanics to lqCCS, i.e. that equivalent processes acting on indistinguishable mixtures of quantum states are correctly recognized as bisimilar. Finally, we give an alternative semantics and a labelled bisimilarity based on a quantum generalization of probability distributions. This provides an equivalent characterization of our behavioural equivalence that is a congruence with respect to the parallel operator, enabling compositional reasoning without the need to explicitly check all possible contexts. We describe a rich class of lqCCS processes for which equivalence is decidable using standard techniques, and we analyse real-world quantum communication protocols.