LQP: The Dynamic Logic of Quantum Information

TL;DR

This paper introduces LQP, a dynamic logic framework for reasoning about information flow, entanglement, and quantum protocols in composite quantum systems, enabling formal verification of quantum information processes.

Contribution

It extends previous quantum dynamic logic to composite systems, integrating quantum logic, modal logic, and quantum computation for formal reasoning about quantum protocols.

Findings

Formal semantics and proof system for LQP

Verification of teleportation and quantum secret sharing protocols

Expressiveness in representing entanglement and quantum evolutions

Abstract

The main contribution of this paper is the introduction of a dynamic logic formalism for reasoning about information flow in composite quantum systems. This builds on our previous work on a complete quantum dynamic logic for single systems. Here we extend that work to a sound (but not necessarily complete) logic for composite systems, which brings together ideas from the quantum logic tradition with concepts from (dynamic) modal logic and from quantum computation. This Logic of Quantum Programs (LQP) is capable of expressing important features of quantum measurements and unitary evolutions of multi-partite states, as well as giving logical characterisations to various forms of entanglement (for example, the Bell states, the GHZ states etc.). We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness proofs for the Teleportation protocol and for a standard Quantum Secret Sharing protocol; a whole range of other quantum circuits and programs, including other well-known protocols (for example, superdense coding, entanglement swapping, logic-gate teleportation etc.), can be similarly verified using our logic.