Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs

被引：6

作者：

Bergfeld, Jort Martinus ^{[1
]}

Sack, Joshua ^{[2
]}

机构：

[1] Univ Amsterdam, ILLC, POB 94242, NL-1090 GE Amsterdam, Netherlands

[2] Calif State Univ Long Beach, Dept Math & Stat, 1250 Bellflower Blvd, Long Beach, CA 90840 USA

来源：

SOFT COMPUTING | 2017年 / 21卷 / 06期

关键词：

Probability; Quantum logic; Axiomatization; Quantum computation; Quantum protocols; COMPACT CLOSED CATEGORIES; DYNAMIC LOGIC;

D O I：

10.1007/s00500-015-1802-6

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This paper presents a sound axiomatization for a probabilistic modal dynamic logic of quantum programs. The logic can express whether a state is separable or entangled, information that is local to a subsystem of the whole quantum system, and the probability of positive answers to quantum tests of certain properties. The power of this axiomatization is demonstrated with proofs of properties concerning bases of a finite-dimensional Hilbert space, composite systems, entangled and separable states, and with proofs of the correctness of two probabilistic quantum protocols (the quantum leader election protocol and the BB84 quantum key distribution protocol).

引用

页码：1421 / 1441

页数：21

共 50 条

[21] Quantum logic networks for probabilistic and controlled teleportation of unknown quantum states
Gao, T
COMMUNICATIONS IN THEORETICAL PHYSICS, 2004, 42 (02) : 223 - 228
[22] Quantum Logic Networks for Probabilistic and Controlled Teleportation of Unknown Quantum States
GAO Ting Department of Mathematics
CommunicationsinTheoreticalPhysics, 2004, 42 (08) : 223 - 228
[23] QPMC: A Model Checker for Quantum Programs and Protocols
Feng, Yuan
Hahn, Ernst Moritz
Turrini, Andrea
Zhang, Lijun
FM 2015: FORMAL METHODS, 2015, 9109 : 265 - 272
[24] A methodology for deriving probabilistic correctness measures from recognizers
Bouchaffra, D
Govindaraju, V
Srihari, S
1998 IEEE COMPUTER SOCIETY CONFERENCE ON COMPUTER VISION AND PATTERN RECOGNITION, PROCEEDINGS, 1998, : 930 - 935
[25] Partial correctness for probabilistic demonic programs
McIver, AK
Morgan, C
THEORETICAL COMPUTER SCIENCE, 2001, 266 (1-2) : 513 - 541
[26] NEW DIRECTIONS IN CATEGORICAL LOGIC, FOR CLASSICAL, PROBABILISTIC AND QUANTUM LOGIC
Jacobs, Bart
LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (03) : 1 - 76
[27] Verification of Quantum Protocols with a Probabilistic Model-Checker
Tavala, Amir M.
Nazem, Soroosh
Babaei-Brojeny, Ali A.
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 270 (01) : 175 - 182
[28] A First Step to the Categorical Logic of Quantum Programs
Sun, Xin
He, Feifei
ENTROPY, 2020, 22 (02)
[29] Floyd-Hoare Logic for Quantum Programs
Ying, Mingsheng
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2011, 33 (06):
[30] Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
Feng, Yuan
Li, Sanjiang
INFORMATION AND COMPUTATION, 2023, 294

← 1 2 3 4 5 →