Verification of Quantum Protocols Adopting Physically Admissible Schedulers

TL;DR

This paper introduces lqCCS, a process calculus for quantum protocols that incorporates physically admissible schedulers, enabling accurate verification of quantum communication protocols through novel semantics and bisimilarity notions.

Contribution

It proposes a new process calculus with semantics constrained by physically admissible schedulers, ensuring realistic modeling and verification of quantum protocols.

Findings

Bisimilarity correctly recognizes equivalent quantum processes acting on indistinguishable states.

The semantics enable compositional reasoning about quantum protocols.

Decidability results for equivalence in certain classes of lqCCS processes.

Abstract

Reliable verification techniques for quantum communication protocols are of paramount importance, given their high implementation cost and critical contexts of application. Extensions of process calculi have been proposed, together with various notions of behavioural equivalence. However, their standard probabilistic models turn out to introduce some non-deterministic capabilities not aligned with the observational properties of physical quantum systems, leading to bisimilarity notions that distinguish physically equivalent processes. Nonetheless, 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. We introduce a novel semantics in terms of distributions, where explicit physically admissible schedulers constrain probabilistic composition and forbid ill-defined non-deterministic moves, while preserving the expressivity needed to model real-world protocols. We investigate a scheduled version of saturated bisimilarity, pairing two processes if no observer can tell them apart, and we verify its adequacy by lifting a known result from quantum mechanics to lqCCS: 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 characterizes our behavioural equivalence as 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.