用于量化量子网络行为的语言

《Proceedings of the ACM on Programming Languages》：A Language for Quantifying Quantum Network Behavior

量子网络利用Bell对实现量子通信，但存在脆弱性和传输难题，需中继器等支持。本文提出PBKAT语言，支持概率和可能性行为描述及协议语义建模，通过工具实现自动化验证，评估显示其适用于实际协议的规格化和量化分析。

　　

摘要

量子网络具备仅使用经典信息无法实现的功能。它们连接具有量子特性的节点，其基本的通信单位是“贝尔对”（Bell pair），即一对纠缠的量子比特。由于量子现象的特性，贝尔对非常脆弱，难以在长距离上传输，因此需要通过中继器网络以及专用硬件和软件来确保所需的结果。与量子网络相关的内在挑战，如对共享资源的竞争和高故障概率，要求对量子网络协议进行定量分析。本文提出了PBKAT，这是一种用于规范、验证和优化贝尔对分发量子网络协议的表达性语言。我们的语言配备了用于表达概率性和可能性行为的原语，并具有对协议执行进行建模的语义系统。我们确定了PBKAT语义系统的性质，并利用这些性质对协议行为进行了定量分析。此外，我们还实现了一个自动化使用PBKAT的工具，并对文献中提出的实际协议进行了测试。我们的结果表明，PBKAT非常适合用于表达实际量子网络协议及其定量属性的推理。