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.
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.
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.
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.
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.
Quantum mechanics shows that if one is able to generate and manipulate entanglement over a distance, one is able to perform certain tasks which are impossible using only classical communication. Classical communication refers to what is used in the Internet of today. A quantum internet would therefore bring new capabilities to our highly connected world. These capabilities both involve (1) the ability to perform tasks with are provably impossible in the current Internet, such as unconditionally secure communication, and (2) the ability to perform certain tasks much more efficient, such as distributed (quantum) computing or extending the baseline of telescopes. To be able to build a quantum internet, two main components are needed: (i) hardware that can store, manipulate and entangle qubits and (ii) a software stack to control the hardware. The core task of both of these is to generate entanglement to be used by applications. In this thesis we focus on the latter, i.e. the development of software and protocols that enable entanglement generation using capable hardware. To enable a certain application, one can certainly, in theory, manually specify each operation the hardware should perform, involving micro-wave pulses, lasers etc. However, in practice this is not feasible, if not to say impossible, due to the complexity of the operations needed, especially in a distributed system such as a quantum network. What is needed is a software stack, which can help with abstracting complexity away in multiple layers. This allows for someone to program a protocol in one layer without knowing all the details of the lower layers. In particular, one can abstract away the hardware details, in order to make higher-layer protocols and applications hardware-agnostic. Therefore, to be able to build a universal, efficient and scalable quantum internet, a software stack is crucial. In chapter 2 we start discussing the networking part of a software stack. Namely, we introduce a network stack for a quantum internet, drawing parallels to the IP/TCP-suite of the classical Internet. We continue with proposing a service and interface of the lowest layer of the network stack: the link layer. The link layer is here responsible for generating entanglement between nodes in a quantum network which are directly connected by a quantum link, i.e. a fiber cable. When developing a protocol or application it is very useful to be able to run it. Both to see if the intended ideas make sense and also to check that the implementation is actually correct. Currently we do not have quantum hardware that exposes a full-fledge API that can be used to execute applications. For this reason, it is very useful to be able to instead simulate the hardware in a way that exposes the same API as the hardware being developed. In chapter 3 we introduce SimulaQron for this exact purpose. Any application of a quantum internet will need entanglement in one way or another. However, entanglement is generally hard to generate and is usually the bottleneck when executing an application. We would therefore like to make use of the generated entanglement in the most optimal way. To be able to do this we need to understand how entanglement can be transformed and distributed in a quantum network. We study the entanglement of a particular class of states called graph states in chapters 4 to 9 and how these states can be transformed in a quantum network.
A classical circuit can be represented by a circuit graph or equivalently by a Boolean expression. The advantage of a circuit graph is that it can help us to obtain an intuitive understanding of the circuit under consideration, whereas the advantage of a Boolean expression is that it is suited to various algebraic manipulations. In the literature, however, quantum circuits are mainly drawn as circuit graphs, and a formal language for quantum circuits that has a function similar to that of Boolean expressions for classical circuits is still missing. Certainly, quantum circuit graphs will become unmanageable when complicated quantum computing problems are encountered, and in particular, when they have to be solved by employing the distributed paradigm where complex quantum communication networks are involved. In this paper, we design an algebraic language for formally specifying quantum circuits in distributed quantum computing. Using this language, quantum circuits can be represented in a convenient and compact way, similar to the way in which we use Boolean expressions in dealing with classical circuits. Moreover, some fundamental algebraic laws for quantum circuits expressed in this language are established. These laws form a basis of rigorously reasoning about distributed quantum computing and quantum communication protocols.
The Quantum Internet architecture and its associated functionality are far from being standardized. Furthermore, the protocol stack that implements the abovementioned functionality is still under development. In this work, we present a framework to DEsign and Synthesize Quantum netwoRk InteroperaBle protocols for Entanglement distribution (DeSQribe), a novel iteration of the Software-Defined Networking (SDN) paradigm. DeSQribe introduces a methodology to define and implement arbitrary entanglement distribution and distillation protocols. Distinct from adaptations of existing SDN solutions to quantum networks, DeSQribe tackles quantum-specific challenges, such as the dual nature of a data plane that accommodates classical messages and quantum states. DeSQribe defines a protocol as an ordered sequence of processing units that manipulate quantum states and exchange classical messages. This high modularity encourages software reusability. A centralized controller leverages DeSQribe and dynamically orchestrates protocols on network devices. Finally, DeSQribe's technology-agnostic nature assures seamless integration across diverse quantum technologies. We showcase how to implement and combine entanglement distribution protocols of very different natures (e.g., connectionless, connection-oriented) with DeSQribe, proving its flexibility and timeliness.