LQP: The Dynamic Logic of Quantum Information

• URL: http://arxiv.org/abs/2110.01361v1
• Date: Mon, 4 Oct 2021 12:20:23 GMT
• Title: LQP: The Dynamic Logic of Quantum Information
• Authors: Alexandru Baltag and Sonja Smets
• Abstract summary: This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. 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 for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
• Score: 77.34726150561087
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Formal verification of higher dimensional quantum protocols [0.0]
  We present our preliminary results in extending the theory of behavioural equivalence in CQP to verify higher dimensional quantum protocols using qudits. This is a work-in-progress and we present our preliminary results in extending the theory of behavioural equivalence in CQP to verify higher dimensional quantum protocols using qudits.
  arXiv  Detail & Related papers  (2024-09-26T15:53:14Z)
• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  We demonstrate the use of coherent-state quantum process tomography (csQPT) for a bosonic-mode superconducting circuit. We show results for this method by characterizing a logical quantum gate constructed using displacement and SNAP operations on an encoded qubit.
  arXiv  Detail & Related papers  (2023-03-02T18:08:08Z)
• A Quantum Algorithm for Computing All Diagnoses of a Switching Circuit [73.70667578066775]
  Faults are by nature while most man-made systems, and especially computers, work deterministically. This paper provides such a connecting via quantum information theory which is an intuitive approach as quantum physics obeys probability laws.
  arXiv  Detail & Related papers  (2022-09-08T17:55:30Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties of quantum programs. In this paper, we introduce a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables.
  arXiv  Detail & Related papers  (2022-05-04T08:57:44Z)
• The Logic of Quantum Programs [77.34726150561087]
  We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems.
  arXiv  Detail & Related papers  (2021-09-14T16:08:37Z)
• Efficient criteria of quantumness for a large system of qubits [58.720142291102135]
  We discuss the dimensionless combinations of basic parameters of large, partially quantum coherent systems. Based on analytical and numerical calculations, we suggest one such number for a system of qubits undergoing adiabatic evolution.
  arXiv  Detail & Related papers  (2021-08-30T23:50:05Z)
• Conjugate Logic [0.0]
  We propose a conjugate logic that can capture the behavior of quantum and quantum-like systems. The proposed logic will include propositions and their relations including connectives. A key point is the addition of a transformation that allows to convert propositions about single systems into propositions about correlations between systems.
  arXiv  Detail & Related papers  (2021-02-12T15:19:11Z)
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic [22.507329566323982]
  We develop a program logic where pre- and post-conditions are BI formulas describing quantum states. We exercise the logic for proving the security of quantum one-time pad and secret sharing.
  arXiv  Detail & Related papers  (2021-01-30T22:24:36Z)
• PBS-Calculus: A Graphical Language for Coherent Control of Quantum Computations [77.34726150561087]
  We introduce the PBS-calculus to represent and reason on quantum computations involving coherent control of quantum operations. We equip the language with an equational theory, which is proved to be sound and complete. We consider applications like the implementation of controlled permutations and the unrolling of loops.
  arXiv  Detail & Related papers  (2020-02-21T16:15:58Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.