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

International Journal of Quantum Information

QUANTUM COMPUTATION TREE LOGIC — MODEL CHECKING AND COMPLETE CALCULUS

Pedro Baltazar, Rohit Chadha, Paulo Mateus

Published Apr 1, 2008• 41 citations
Publisher

Abstract

Logics for reasoning about quantum states and their evolution have been given in the literature. In this paper, we consider quantum computation tree logic (QCTL), which adds temporal modalities to exogenous quantum propositional logic. We give a sound and complete axiomatization of QCTL and combine the standard CTL model-checking algorithm with the dEQPL model-checking algorithm to obtain a model-checking algorithm for QCTL. Finally, we illustrate the use of the logic by reasoning about the BB84 key distribution protocol.

DOI
10.1142/s0219749908003530

Related papers

Towards Model-Checking Quantum Security Protocols

Pedro Baltazar, Rohit Chadha, Paulo Mateus +1 more

Logics for reasoning about quantum states have been given in the literature. In this paper, we extend one such logic with temporal constructs mimicking the standard computational tree logic used to reason about classical transition systems. We investigate the model-checking problem for this temporal quantum logic and illustrate its use by reasoning about the BB84 key distribution protocol.

International Conference on Quantum, Nano and Micro Technologies (ICQNM)•Jan 1, 2007•19 citations

Temporal Logics for Reasoning about Quantum Systems

Paulo Mateus, Jaime Ramos, Amı́lcar Sernadas +1 more

Reasoning about quantum systems has gained prominence due to a big potential in applications such as information processing, security, distributed systems, and randomized algorithms. This fact has attracted research in formal reasoning about quantum states, programs, and processes. On the other hand, temporal logics have proved to be successful in the verification of classical distributed systems and security protocols. In this chapter we extend exogenous quantum propositional logic with temporal modalities, considering both linear and branching time. We provide a weakly complete Hilbert calculi for the proposed quantum temporal logics and study their SAT and model-checking problems. 10.1 Introduction Reasoning about quantum systems has gained prominence due to their potential applications in information processing, security, distributed systems and randomized algorithms. This has attracted research in formal reasoning about quantum states (see for instance van der Meyden and Patra 2003b, a; Mateus and Sernadas 2006; Chadha et al. 2009; Caleiro et al. 2006) and quantum programs (cf. Knill 1996; Sanders and Zuliani 2000; Abramsky and Coecke 2004; D'Hondt and Panangaden 2004; Altenkirch and Grattage 2005; Selinger and Valiron 2005; Baltag and Smets 2006; Baltazar et al. 2007; Chadha et al. 2006, 2007; Baltazar et al. 2008). On the other hand, formal methods have proved to be successful in design and verification of classical distributed systems and security protocols (e.g., Clarke and Wing 1996; Meadows 2003). Herein, we present branching and linear temporal logics for reasoning about evolution of quantum systems composed of a fixed finite set of qubits.

Cambridge University Press eBooks•Nov 30, 2009•12 citations

QMC: A Model Checker for Quantum Systems

Simon J. Gay, Rajagopal Nagarajan, Nickolas K. Papanikolaou

We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of quantum computational tree logic (QCTL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run.

arXiv:0704.3705•Apr 27, 2007•0 citations

Model checking quantum protocols

Nickolas K. Papanikolaou

This thesis describes model checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We detail the syntax, semantics and type system of QMC’s modelling language, the logic QCTL which is used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies.

•Sep 9, 2026•18 citations

An Introduction to Quantum Model Checking

Andrea Turrini

Model checking is a well-established and widely adopted framework used to verify whether a given system satisfies the desired properties. Properties are usually given by means of formulas from a specific logic; there are several logics that can be used, such as CTL and LTL, which permit the expression of different types of properties on the branching-time or on the linear-time evolution of the system. In this paper, we will consider the problem of model checking quantum systems and present the solutions given in literature for solving such a problem with respect to different types of properties.

Applied Sciences•Feb 15, 2022•10 citations

Temporal Logic-Based Formal Verification of Quantum Circuits

Jincheng Zhang

This paper presents a novel approach to verifying the correctness of quantum circuits using temporal logic. Traditional verification methods often rely on gate-level simulation, which can be computationally expensive and insufficient for complex quantum algorithms. This work addresses this limitation by formally modeling quantum circuits as temporal logic systems. We leverage the expressive power of temporal logic to capture the desired behavior of quantum algorithms, including their evolution over time and the effects of quantum phenomena like superposition and entanglement. The core of our method involves mapping the circuit's operations onto temporal logic specifications and utilizing automated theorem proving and model checking techniques, tailored to the probabilistic nature of quantum systems. We demonstrate that this approach provides a more rigorous and scalable verification framework compared to existing methods, offering a pathway to ensuring the reliability of quantum computations. The key contributions of this work are the formalization of quantum circuits with temporal logic, the adaptation of theorem proving and model checking techniques for quantum systems, and the potential for significantly improving the trustworthiness of quantum algorithms.

•Aug 28, 2026•0 citations
Logics for reasoning about quantum states and their evolution have been given in the literature. In this paper, we consider quantum computation tree logic (QCTL), which adds temporal modalities to exogenous quantum propositional logic. We give a sound and complete axiomatization of QCTL and combine the standard CTL model-checking algorithm with the dEQPL model-checking algorithm to obtain a model-checking algorithm for QCTL. Finally, we illustrate the use of the logic by reasoning about the BB84 key distribution protocol.
Reasoning about quantum systems has gained prominence due to a big potential in applications such as information processing, security, distributed systems, and randomized algorithms. This fact has attracted research in formal reasoning about quantum states, programs, and processes. On the other hand, temporal logics have proved to be successful in the verification of classical distributed systems and security protocols. In this chapter we extend exogenous quantum propositional logic with temporal modalities, considering both linear and branching time. We provide a weakly complete Hilbert calculi for the proposed quantum temporal logics and study their SAT and model-checking problems. 10.1 Introduction Reasoning about quantum systems has gained prominence due to their potential applications in information processing, security, distributed systems and randomized algorithms. This has attracted research in formal reasoning about quantum states (see for instance van der Meyden and Patra 2003b, a; Mateus and Sernadas 2006; Chadha et al. 2009; Caleiro et al. 2006) and quantum programs (cf. Knill 1996; Sanders and Zuliani 2000; Abramsky and Coecke 2004; D'Hondt and Panangaden 2004; Altenkirch and Grattage 2005; Selinger and Valiron 2005; Baltag and Smets 2006; Baltazar et al. 2007; Chadha et al. 2006, 2007; Baltazar et al. 2008). On the other hand, formal methods have proved to be successful in design and verification of classical distributed systems and security protocols (e.g., Clarke and Wing 1996; Meadows 2003). Herein, we present branching and linear temporal logics for reasoning about evolution of quantum systems composed of a fixed finite set of qubits.
We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of quantum computational tree logic (QCTL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run.
This thesis describes model checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We detail the syntax, semantics and type system of QMC’s modelling language, the logic QCTL which is used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies.
Model checking is a well-established and widely adopted framework used to verify whether a given system satisfies the desired properties. Properties are usually given by means of formulas from a specific logic; there are several logics that can be used, such as CTL and LTL, which permit the expression of different types of properties on the branching-time or on the linear-time evolution of the system. In this paper, we will consider the problem of model checking quantum systems and present the solutions given in literature for solving such a problem with respect to different types of properties.
This paper presents a novel approach to verifying the correctness of quantum circuits using temporal logic. Traditional verification methods often rely on gate-level simulation, which can be computationally expensive and insufficient for complex quantum algorithms. This work addresses this limitation by formally modeling quantum circuits as temporal logic systems. We leverage the expressive power of temporal logic to capture the desired behavior of quantum algorithms, including their evolution over time and the effects of quantum phenomena like superposition and entanglement. The core of our method involves mapping the circuit's operations onto temporal logic specifications and utilizing automated theorem proving and model checking techniques, tailored to the probabilistic nature of quantum systems. We demonstrate that this approach provides a more rigorous and scalable verification framework compared to existing methods, offering a pathway to ensuring the reliability of quantum computations. The key contributions of this work are the formalization of quantum circuits with temporal logic, the adaptation of theorem proving and model checking techniques for quantum systems, and the potential for significantly improving the trustworthiness of quantum algorithms.