LQP: the dynamic logic of quantum information
From MaRDI portal
Publication:5482272
DOI10.1017/S0960129506005299zbMATH Open1103.03031arXiv2110.01361OpenAlexW2138408756MaRDI QIDQ5482272FDOQ5482272
Publication date: 28 August 2006
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/2110.01361
Recommendations
- Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
- DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS
- Theoretical Aspects of Computing – ICTAC 2005
- QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
- PLQP \& Company: decidable logics for quantum algorithms
Cited In (26)
- A logical analysis of quantum voting protocols
- Logics of informational interactions
- A proof system for disjoint parallel quantum programs
- PLQP \& Company: decidable logics for quantum algorithms
- Quantum logic as a dynamic logic
- Correlated knowledge: an epistemic-logic view on quantum entanglement
- A dynamic-logical perspective on quantum behavior
- Reconstructing quantum theory from its possibilistic operational formalism
- Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
- Modeling correlated information change: from conditional beliefs to quantum conditionals
- Termination of nondeterministic quantum programs
- On definition of skew frames
- Larc: A state reduction theory of quantum measurement
- A first-order epistemic quantum computational semantics with relativistic-like epistemic effects
- QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS
- Duality for the logic of quantum actions
- A logic for quantum register measurements
- A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations
- Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect
- The dynamic turn in quantum logic
- Classical knowledge for quantum cryptographic reasoning
- Toward automatic verification of quantum programs
- Automated quantum program verification in dynamic quantum logic
- Quantum logic for observation of physical quantities
- Correlated information: a logic for multi-partite quantum systems
- DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS
This page was built for publication: LQP: the dynamic logic of quantum information
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5482272)
