Exogenous Quantum Operator Logic Based on Density Operators

TL;DR

This paper introduces EQOL, a new exogenous quantum logic based on density operators for reasoning about open quantum systems, extending classical logic and demonstrating applications in entanglement and quantum protocols.

Contribution

The paper develops EQOL based on density operators, extending exogenous quantum logic to open systems and introducing EQMC for quantum Markov chains.

Findings

EQOL is sound and complete.

Successfully reasoned about entanglement in Bell states.

Verified eavesdropping in BB84 protocol.

Abstract

Although quantum logic by using exogenous approach has been proposed for reasoning about closed quantum systems, an improvement would be worth to study quantum logic based on density operators instead of unit vectors in the state logic point of view. In order to achieve this, we build an exogenous quantum operator logic(EQOL) based on density operators for reasoning about open quantum systems. We show that this logic is sound and complete. Just as the exogenous quantum propositional logic(EQPL), by applying exogenous approach, EQOL is extended from the classical propositional logic, and is used to describe the state logic based on density operators. As its applications, we confirm the entanglement property about Bell states by reasoning and logical argument, also verify the existence of eavesdropping about the basic BB84 protocol. As a novel type of mathematical formalism for open quantum systems, we introduce an exogenous quantum Markov chain(EQMC) where its quantum states are labelled using EQOL formulae. Then, an example is given to illustrate the termination verification problem of a generalized quantum loop program described using EQMC.