Exogenous Quantum Operator Logic Based on Density Operators

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.