Quantum networks have capabilities that are impossible to achieve using only classical information. They connect quantum capable nodes, with their fundamental unit of communication being the Bell pair , a pair of entangled quantum bits. Due to the nature of quantum phenomena, Bell pairs are fragile and difficult to transmit over long distances, thus requiring a network of repeaters along with dedicated hardware and software to ensure the desired results. The intrinsic challenges associated with quantum networks, such as competition over shared resources and high probabilities of failure, require quantitative reasoning about quantum network protocols. This paper develops PBKAT, an expressive language for specification, verification and optimization of quantum network protocols for Bell pair distribution. Our language is equipped with primitives for expressing probabilistic and possibilistic behaviors, and with semantics modeling protocol executions. We establish the properties of PBKAT’s semantics, which we use for quantitative analysis of protocol behavior. We further implement a tool to automate PBKAT’s usage, which we evaluated on real-world protocols drawn from the literature. Our results indicate that PBKAT is well suited for both expressing real-world quantum network protocols and reasoning about their quantitative properties.
Quantum networks have capabilities that are impossible to achieve using only classical information. They connect quantum capable nodes, with their fundamental unit of communication being the Bell pair , a pair of entangled quantum bits. Due to the nature of quantum phenomena, Bell pairs are fragile and difficult to transmit over long distances, thus requiring a network of repeaters along with dedicated hardware and software to ensure the desired results. The intrinsic challenges associated with quantum networks, such as competition over shared resources and high probabilities of failure, require quantitative reasoning about quantum network protocols. This paper develops PBKAT, an expressive language for specification, verification and optimization of quantum network protocols for Bell pair distribution. Our language is equipped with primitives for expressing probabilistic and possibilistic behaviors, and with semantics modeling protocol executions. We establish the properties of PBKAT’s semantics, which we use for quantitative analysis of protocol behavior. We further implement a tool to automate PBKAT’s usage, which we evaluated on real-world protocols drawn from the literature. Our results indicate that PBKAT is well suited for both expressing real-world quantum network protocols and reasoning about their quantitative properties.
Quantum networks connect quantum capable nodes in order to achieve capabilities that are impossible only using classical information. Their fundamental unit of communication is the Bell pair , which consists of two entangled quantum bits. Unfortunately, Bell pairs are fragile and difficult to transmit directly, necessitating a network of repeaters, along with software and hardware that can ensure the desired results. Challenging intrinsic features of quantum networks, such as dealing with resource competition, motivate formal reasoning about quantum network protocols. To this end, we developed BellKAT, a novel specification language for quantum networks based upon Kleene algebra. To cater to the specific needs of quantum networks, we designed an algebraic structure, called BellSKA, which we use as the basis of BellKAT’s denotational semantics. BellKAT’s constructs describe entanglement distribution rules that allow for modular specification. We give BellKAT a sound and complete equational theory, allowing us to verify network protocols. We provide a prototype tool to showcase the expressiveness of BellKAT and how to optimize and verify networks in practice.
The distribution of high-quality entanglement over long distances remains a challenge due to losses in quantum channels. As a solution, quantum repeater protocols generate entanglement over short segments and progressively extend its range using entanglement swapping, while using distillation to compensate for entanglement degradation. Numerous studies analyze repeater protocols through tailored tools that are tied to specific protocol types and network assumptions. In this work, we propose a formal language to specify quantum repeater protocols in a unified manner, modeling the concurrent distribution of entanglement across multiple pairs of network nodes. We consider delays arising from failures and contention for resources, and account for the effects of noise and decoherence on the quality of entanglement. Furthermore, we provide a prototype tool based on our language to precisely track the rate and fidelity of the distributed entangled pairs, supporting heterogeneous hardware configurations and constraints on available quantum memories. Finally, we demonstrate the effectiveness of our approach by expressing common protocols from the literature and evaluating their performance.
The realization of the Quantum Internet promises transformative capabilities in secure communication, distributed quantum computing, and high-precision metrology. However, transitioning from laboratory experiments to a scalable, multi-tenant network utility introduces deep orchestration challenges. Current development is often siloed within physics communities, prioritizing hardware, while the classical networking community lacks architectural models to manage fragile quantum resources. This tutorial bridges this divide by providing a network-centric view of quantum networking. We dismantle idealized assumptions in current simulators to address the "simulation-reality gap," recasting them as explicit control-plane constraints. To bridge this gap, we establish Software-Defined Quantum Networking (SDQN) as a prerequisite for scale, prioritizing a symbiotic, dual-plane architecture where classical control dictates quantum data flow. Specifically, we synthesize reference models for SDQN and the Quantum Network Operating System (QNOS) for hardware abstraction, and adapt a Quantum Network Utility Maximization (Q-NUM) framework as a unifying mathematical lens for engineers to reason about trade-offs between entanglement routing, scheduling, and fidelity. Furthermore, we analyze Distributed Quantum AI (DQAI) over imperfect networks as a case study, illustrating how physical constraints such as probabilistic stragglers and decoherence dictate application-layer viability. Ultimately, this tutorial equips network engineers with the tools required to transition quantum networking from a bespoke physics experiment into a programmable, multi-tenant global infrastructure.
The main attributes of quantum networks are the utilization of quantum phenomena, security guarantees, and availability of their main quantum resource - entanglement. The fundamental differences between classical and quantum information will require joint efforts in physics, engineering and computer science to make quantum networks functional and scalable. A common language must be established between the hardware and software community. We envision a foundational model for quantum network programming languages. Such a model should contain the essential constructs for programming quantum networks, allow for specification and verification of end-to-end entanglement distribution, and provide guidelines for composing network protocols.
Quantum networks are designed to transmit quantum bits (qubits) among quantum devices to enable new network resources for the applications. Entanglement distribution and entanglement swapping are fundamental procedures that are required in several network operations. However, they are probabilistic operations, which can lead to severe network performance degradation. This article investigates the engineering problem of resource allocation in quantum networks, considering factors like entanglement distribution probability, quantum memory characteristics, and fidelity. We model this as an optimization model to obtain an optimal solution. In particular, we formulate an integer linear programming (ILP) and develop a heuristic algorithm, aiming to minimize the number of required entangled qubit pairs (Bell pairs or EPR pairs) in any adjacent pair in the quantum network. Extensive simulations are performed to compare the performance of proposed ILP and heuristic. In all the cases, the heuristic produces a comparable solution to the optimal one. Simulation results ensure that the value of maximum utilized Bell pairs in a quantum network highly depends on the value of the probability of entangled pairs established, considering the time in the quantum memory besides the number of incoming requests.
Our objective in this thesis is to perform formal specification and automated validation of the class of protocols associated with quantum cryptography. Current analyses and proofs regarding quantum cryptographic protocols and their security are information-theoretic and also require in--depth understanding of the underlying physics. The alternative approach presented here involves the use of computer modelling languages and verification software. In particular, the logical model checker SPIN and the probabilistic model checker PRISM are used to analyse quantum key distribution, entanglement and quantum teleportation. The value of our approach lies not only in the fact that it is conceptually simpler than existing proofs, but in that it allows us to disambiguate protocol definitions and to assess their properties in various circumstances. By varying the values of certain parameters, different attacks on the protocols can be attempted and implementation-specific attributes can be analysed. The quantum key distribution protocol BB84 has been proved to be unconditionally secure against all types of eavesdropping. Although a general proof of this result is extremely hard to generate automatically, it is possible to develop specific protocol attacks and validate the protocol by computer. Assuming two types of eavesdropping attack (intercept-resend and random-substitute), we have used the PRISM tool to compute exactly the probability of successful eavesdropping, and found it to diminish as the number of transmitted qubits is increased. This result is linked to Mayers' security criteria for BB84. Also, we briefly describe a new quantum protocol definition language, named qSpec. The recent CQP process algebra, due to Nagarajan and Gay, is reviewed and examples of its application are provided. Alternative formalisms and validation tools are discussed, including QPAlg, PROBMELA and probUSM, the logic of knowledge and time for quantum systems due to Van der Meyden, and the QCSim simulator.