Quantum Network Specification and Verification

Quantum networks are slowly moving towards reality. They are envisioned as augmenting classical networks with a quantum data plane used to distribute quantum bits (qubits) in order to create end-to-end entangled qubit pairs. These pairs offer unprecedented security properties, and allow several quantum computers to be combined for increased computational power. However, due to increasing decoherence of quantum state over distance/time, and the impossibility of copying qubits, the creation of end-to-end pairs has to go through several intermediate pairs, combined step-wise through entanglement swapping and distillation. This process involves shared resources on quantum-enabled switches, requiring sophisticated protocols involving also the classical network to make best use of resources for establishing end-to-end entangled pairs exhibiting highest possible fidelity. This project aims to propose a language for specifying and verifying quantum entanglement protocols, leveraging experiences with Kleene algebras in classical networks. However, due to the significant differences to classical networks, we propose to explore a novel notion of bisynchronous Kleene algebra.