分布式量子程序的验证
Verification of Distributed Quantum Programs
摘要：
分布式量子系统，特别是量子互联网，具有不断增长的潜力，可以充分展示量子计算的力量。考虑到开发通用量子计算机比连接许多小型量子设备要困难得多，这一点尤其如此。实现分布式量子系统的一个主要挑战是对其进行编程并验证其正确性。在本文中，我们提出了一个类似CSP的分布式编程语言，以方便规范和验证这样的系统。在介绍了它的操作和指称语义后，我们开发了一个分布式量子程序的Hoare式逻辑，并建立了它的部分和全部正确性方面的可靠性和（相对）完整性。该逻辑在量子隐形传态的验证和非局域CNOT门的局域实现中的应用证明了其有效性。
英文摘要：
Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
