Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Applied Sciences

Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic

Alexandru Baltag, Sonja Smets

Published Apr 28, 2022• 5 citations
Publisher

Abstract

This paper provides an overview of quantum dynamic logics, showing how they have been designed and illustrating how these logics can be applied to verify the correctness of quantum protocols. Similar to the advantages of using dynamic logics to reason about the flow of classical information, the quantum analogues of these logics are tailored to the task of reasoning about the flow of quantum information. We present our logical systems in a modular way, starting with the qualitative logic of quantum measurements and unitary evolutions in single quantum systems, which can already express non-classical effects, e.g., the state-changing interference induced by quantum tests, their non-commutativity, etc. We then move on to logics for compound quantum systems that can capture the non-local features of quantum information: separability, entanglement, correlated measurements, Bell states, etc. We then briefly summarize the logic of quantum probabilities and sketch some applications to quantum protocols.

DOI
10.3390/app12094458

Related papers

The Logic of Quantum Programs

Alexandru Baltag, Sonja Smets

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. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell states) and various linear operators. As an example we sketch an analysis of the teleportation protocol.

arXiv:2109.06792•Sep 14, 2021•41 citations

LQP: the dynamic logic of quantum information

Alexandru Baltag, Sonja Smets

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.

Mathematical Structures in Computer Science•Jun 1, 2006•102 citations

Temporal Logic Formalization for Quantum State Evolution

Jincheng Zhang

This paper introduces a novel temporal logic formalism, termed Temporal Quantum Logic (TQL), specifically tailored for representing and reasoning about the continuous evolution of quantum states. The core challenge in applying temporal logic to quantum mechanics lies in effectively capturing the inherent complexities of superposition, entanglement, and decoherence, particularly the non-commutativity of quantum operations. Existing temporal logics lack the necessary tools to accurately model these phenomena. TQL addresses this limitation by employing a multi-valued logic built upon tensor networks and process algebra concepts. This approach enables a precise and explicit representation of quantum operations, measurement outcomes, and their temporal dependencies, incorporating probabilistic semantics directly into the logic. The formalization utilizes a state representation based on tensor network contractions, allowing for the dynamic tracking of quantum state evolution over time. The logic incorporates operators that explicitly handle non-commutativity and decoherence, offering a framework for formally verifying the correctness of quantum algorithms and protocols. The key innovation is the combination of tensor network formalism with temporal logic, providing a rigorous method for describing the evolution of quantum systems and enabling a deeper understanding of their behavior. This work lays the foundation for future research in quantum verification, quantum algorithm design, and the development of quantum software.

•Aug 28, 2026•0 citations

Logic Column 13: Reasoning Formally about Quantum Systems: An Overview

Nickolas K. Papanikolaou

This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, our objective is to provide a high-level presentation of the logical aspects of quantum theory. Mateus' and Sernadas' EQPL logic is illustrated with a small example, namely the state of an entangled pair of qubits. The "KT" logic of van der Meyden and Patra is demonstrated briefly in the context of the B92 protocol for quantum key distribution.

arXiv:cs/0508005•Aug 1, 2005•1 citation

What Can Logic Learn from Quantum Mechanics

Alexandru Baltag, Sonja Smets

We give a logical analysis of quantum measurements as forms of information update. We enumerate some of the “lessons ” that Logic can learn from Quantum Mechanics: (1) the importance of logical dynamics; (2) the fact that quantum physics does not require any modification of the classical laws of “static ” propositional logic, but only a non-classical dynamics of information flow; (3) the fact that all information-gathering actions have ontic side-effects; (4) the fact that this ontic impact might in its turn affect the flow of information, leading to non-classical epistemic effects and to states of “objectively imperfect information”. 1

Finds and Results from the Swedish Cyprus Expedition: A Gender Perspective at the Medelhavsmuseet•Jan 1, 2005•5 citations

LQP: The Dynamic Logic of Quantum Information

Alexandru Baltag, Sonja Smets

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.

arXiv:2110.01361•Oct 4, 2021•1 citation
This paper provides an overview of quantum dynamic logics, showing how they have been designed and illustrating how these logics can be applied to verify the correctness of quantum protocols. Similar to the advantages of using dynamic logics to reason about the flow of classical information, the quantum analogues of these logics are tailored to the task of reasoning about the flow of quantum information. We present our logical systems in a modular way, starting with the qualitative logic of quantum measurements and unitary evolutions in single quantum systems, which can already express non-classical effects, e.g., the state-changing interference induced by quantum tests, their non-commutativity, etc. We then move on to logics for compound quantum systems that can capture the non-local features of quantum information: separability, entanglement, correlated measurements, Bell states, etc. We then briefly summarize the logic of quantum probabilities and sketch some applications to quantum protocols.
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. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell states) and various linear operators. As an example we sketch an analysis of the teleportation protocol.
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.
This paper introduces a novel temporal logic formalism, termed Temporal Quantum Logic (TQL), specifically tailored for representing and reasoning about the continuous evolution of quantum states. The core challenge in applying temporal logic to quantum mechanics lies in effectively capturing the inherent complexities of superposition, entanglement, and decoherence, particularly the non-commutativity of quantum operations. Existing temporal logics lack the necessary tools to accurately model these phenomena. TQL addresses this limitation by employing a multi-valued logic built upon tensor networks and process algebra concepts. This approach enables a precise and explicit representation of quantum operations, measurement outcomes, and their temporal dependencies, incorporating probabilistic semantics directly into the logic. The formalization utilizes a state representation based on tensor network contractions, allowing for the dynamic tracking of quantum state evolution over time. The logic incorporates operators that explicitly handle non-commutativity and decoherence, offering a framework for formally verifying the correctness of quantum algorithms and protocols. The key innovation is the combination of tensor network formalism with temporal logic, providing a rigorous method for describing the evolution of quantum systems and enabling a deeper understanding of their behavior. This work lays the foundation for future research in quantum verification, quantum algorithm design, and the development of quantum software.
This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, our objective is to provide a high-level presentation of the logical aspects of quantum theory. Mateus' and Sernadas' EQPL logic is illustrated with a small example, namely the state of an entangled pair of qubits. The "KT" logic of van der Meyden and Patra is demonstrated briefly in the context of the B92 protocol for quantum key distribution.
We give a logical analysis of quantum measurements as forms of information update. We enumerate some of the “lessons ” that Logic can learn from Quantum Mechanics: (1) the importance of logical dynamics; (2) the fact that quantum physics does not require any modification of the classical laws of “static ” propositional logic, but only a non-classical dynamics of information flow; (3) the fact that all information-gathering actions have ontic side-effects; (4) the fact that this ontic impact might in its turn affect the flow of information, leading to non-classical epistemic effects and to states of “objectively imperfect information”. 1
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.