一句话：提出基于 Kleene 代数的量子网络规约语言 BellKAT，并给出可靠完备的等式理论以验证网络协议。
量子网络以脆弱且难直接传输的 Bell pair 为通信基本单元，需借助中继网络及软硬件协同，资源竞争等特性使协议形式化推理困难。本文提出 BellKAT，一种基于 Kleene 代数的量子网络规约语言。为刻画量子网络需求，作者设计代数结构 BellSKA，并以其作为 BellKAT 的指称语义基础；BellKAT 的构造可模块化描述纠缠分发规则。论文给出 BellKAT 的可靠且完备的等式理论，用于验证网络协议，并实现原型工具，展示其表达力以及在实际中优化和验证网络的能力。
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.
@article{BuckleyCOSRE24,
title = {An Algebraic Language for Specifying Quantum Networks},
author = {Anita Buckley and Pavel Chuprikov and Rodrigo Otoni and Robert Soulé and Robert Rand and Patrick Eugster},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656430}
}