Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
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).
Paper
Full text
Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
Semantic Scholar · Physics · 2015
Abstract
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).