Verification of Quantum Protocols Adopting Physically Admissible Schedulers
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911623399079936 |
|---|---|
| author | Ceragioli, Lorenzo Gadducci, Fabio Lomurno, Giuseppe Tedeschi, Gabriele |
| author_facet | Ceragioli, Lorenzo Gadducci, Fabio Lomurno, Giuseppe Tedeschi, Gabriele |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_23756 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Verification of Quantum Protocols Adopting Physically Admissible Schedulers Ceragioli, Lorenzo Gadducci, Fabio Lomurno, Giuseppe Tedeschi, Gabriele Logic in Computer Science 68Q85 (Primary) 81P68 (Secondary) D.3.1; F.3.1; F.3.2 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. |
| title | Verification of Quantum Protocols Adopting Physically Admissible Schedulers |
| topic | Logic in Computer Science 68Q85 (Primary) 81P68 (Secondary) D.3.1; F.3.1; F.3.2 |
| url | https://arxiv.org/abs/2604.23756 |