LQP:量子信息的动态逻辑
量子物理
2021-10-05 v1 计算机科学中的逻辑
摘要
本文的主要贡献是引入一种用于推理复合量子系统中信息流的动态逻辑形式体系。这建立在我们先前关于单系统完全量子动态逻辑的工作之上。此处我们将该工作扩展为复合系统的可靠(但不一定完全)逻辑,其将量子逻辑传统的思想与(动态)模态逻辑及量子计算的概念融为一体。该量子程序逻辑 (LQP) 能够表达量子测量与多体态酉演化的重要特征,并对各种纠缠形式(例如 Bell 态、GHZ 态等)给出逻辑刻画。我们给出了该逻辑的有限语法、关系语义与可靠证明系统。作为应用,我们利用我们的系统为隐形传态协议与标准量子秘密共享协议给出形式化正确性证明;一系列其他量子电路与程序,包括其他知名协议(例如超密编码、纠缠交换、逻辑门隐形传态等),均可类似地用我们的逻辑验证。
引用
@article{arxiv.2110.01361,
title = {LQP: The Dynamic Logic of Quantum Information},
author = {Alexandru Baltag and Sonja Smets},
journal= {arXiv preprint arXiv:2110.01361},
year = {2021}
}
备注
45 pages, this paper is a revision and extension of Baltag and Smets' paper on 'The Logic of Quantum Programs'. The paper on 'The Logic of Quantum Programs' appeared in the proceedings of QPL2004, the 2nd International Workshop on Quantum Programming Languages (TUCS General Publication No 33, Turku Center for Computer Science, 2004). arXiv admin note: text overlap with arXiv:2109.06792