© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

arXiv:2405.05825 · Lecture notes in computer science

Measurement-Based Verification of Quantum Markov Chains

Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying

Published Jan 1, 2024• 6 citations

Abstract

Abstract Model-checking techniques have been extended to analyze quantum programs and communication protocols represented as quantum Markov chains, an extension of classical Markov chains. To specify qualitative temporal properties, a subspace-based quantum temporal logic is used, which is built on Birkhoff-von Neumann atomic propositions. These propositions determine whether a quantum state is within a subspace of the entire state space. In this paper, we propose the measurement-based linear-time temporal logic MLTL to check quantitative properties. MLTL builds upon classical linear-time temporal logic (LTL) but introduces quantum atomic propositions that reason about the probability distribution after measuring a quantum state. To facilitate verification, we extend the symbolic dynamics-based techniques for stochastic matrices described by Agrawal et al. (JACM 2015) to handle more general quantum linear operators (super-operators) through eigenvalue analysis. This extension enables the development of an efficient algorithm for approximately model checking a quantum Markov chain against an MLTL formula. To demonstrate the utility of our model-checking algorithm, we use it to simultaneously verify linear-time properties of both quantum and classical random walks. Through this verification, we confirm the previously established advantages discovered by Ambainis et al. (STOC 2001) of quantum walks over classical random walks and discover new phenomena unique to quantum walks.

DOI: 10.1007/978-3-031-65633-0_24

Related papers

Model Checking Quantum Continuous-Time Markov Chains

Ming Xu, Jingyi Mei, Ji Guan +1 more

Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialise the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-the-art real root isolation algorithm under Schanuel’s conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.

arXiv:2105.00382•Leibniz international proceedings in informatics•Jan 1, 2021•2 citations

Classical-quantum state quantum Markov chains and finiteness

Jens Chr. Godskesen

• Quantum Markov chain for quantum programs based on classical control and quantum data • A QCTL where a proposition is a pair of a classical state and a projection • Sound and complete translation of quantum Markov chains to DTMCs • Convergence and simple cycles make model checking decidable Several quantum Markov chains and temporal quantum logics have been considered in the literature. In this paper we propose a discrete time classical-quantum state quantum Markov chain (cqQMC) with super-operators over a finite dimensional Hilbert space H . The cqQMC is related to previous proposals but yet with a different semantics in that states are pairs of a classical and a quantum state. We define a quantum temporal logic (QCTL) where propositions are pairs of a classical state and a projection over H . We demonstrate how a cqQMC can be translated to a discrete time Markov chain (DTMC). The translation is sound and complete in that model checking any QCTL formula for a cqQMC can equivalently be carried out by checking the same formula for the inferred DTMC. Taking advantage of the finite classical control we show that even though a cqQMC may have infinitely many states then under certain restrictions the inferred DTMC is finite, and hence model checking is decidable.

Information and Computation•May 18, 2026•0 citations

Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains

Ming Xu, Jingyi Mei, Ji Guan +2 more

Verifying quantum systems has attracted a lot of interest in the last decades.In this paper, we study the quantitative model-checking of quantum continuous-time Markov chains (quantum CTMCs). The branching-time properties of quantum CTMCs are specified by continuous stochastic logic (CSL), which is well-known for verifying real-time systems, including classical CTMCs. The core of checking the CSL formulas lies in tackling multiphase until formulas. We develop an algebraic method using proper projection, matrix exponentiation, and definite integration to symbolically calculate the probability measures of path formulas. Thus the decidability of CSL is established. To be efficient, numerical methods are incorporated to guarantee that the time complexity is polynomial in the encoding size of the input model and linear in the size of the input formula. A running example of Apollonian networks is further provided to demonstrate our method.

arXiv:2202.05412•Logical Methods in Computer Science•Nov 11, 2025•3 citations

Model Checking Applied to Quantum Physics

Ji Guan, Yuan Feng, Andrea Turrini +1 more

Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications in quantum physics. More explicitly, we show how quantum statistical and many-body systems can be modeled as quantum Markov chains, and some of their properties that interest physicists can be specified in linear-time temporal logics. Then we present an efficient algorithm to check these properties. A few case studies are given to demonstrate the use of our algorithm to actual quantum physical problems.

arXiv:1902.03218•Feb 8, 2019•1 citation

Model Checking Omega-regular Properties for Quantum Markov Chains

Yuan Feng, Ernst Moritz Hahn, Andrea Turrini +1 more

Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking omega-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking omega-regular properties for quantum Markov chains.

International Conference on Concurrency Theory•Jan 1, 2017•10 citations

Model Checking Reachability Properties for Quantum Markov Chains

Godskesen, Jens Christian

We propose a discrete time quantum Markov chain (QMC) related to previous proposals but yet with a different semantics. A probability measure is defined similar to as for DTMCs in contrast to e.g.\ the super operator valued measure. Our work is based on a simple imperative quantum pseudo programming language and its denotational semantics which naturally leads to a definition of a QMC. As a novelty we demonstrate how reachability events of a QMC expressed in a simple temporal logic like notation may be checked similar to as for DTMCs as transient state probabilities and how probability intervals of such events may be computed by smallest fixed-point solutions to linear equations.

•Aug 1, 2025•0 citations

Abstract Model-checking techniques have been extended to analyze quantum programs and communication protocols represented as quantum Markov chains, an extension of classical Markov chains. To specify qualitative temporal properties, a subspace-based quantum temporal logic is used, which is built on Birkhoff-von Neumann atomic propositions. These propositions determine whether a quantum state is within a subspace of the entire state space. In this paper, we propose the measurement-based linear-time temporal logic MLTL to check quantitative properties. MLTL builds upon classical linear-time temporal logic (LTL) but introduces quantum atomic propositions that reason about the probability distribution after measuring a quantum state. To facilitate verification, we extend the symbolic dynamics-based techniques for stochastic matrices described by Agrawal et al. (JACM 2015) to handle more general quantum linear operators (super-operators) through eigenvalue analysis. This extension enables the development of an efficient algorithm for approximately model checking a quantum Markov chain against an MLTL formula. To demonstrate the utility of our model-checking algorithm, we use it to simultaneously verify linear-time properties of both quantum and classical random walks. Through this verification, we confirm the previously established advantages discovered by Ambainis et al. (STOC 2001) of quantum walks over classical random walks and discover new phenomena unique to quantum walks.

Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialise the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-the-art real root isolation algorithm under Schanuel’s conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.

• Quantum Markov chain for quantum programs based on classical control and quantum data • A QCTL where a proposition is a pair of a classical state and a projection • Sound and complete translation of quantum Markov chains to DTMCs • Convergence and simple cycles make model checking decidable Several quantum Markov chains and temporal quantum logics have been considered in the literature. In this paper we propose a discrete time classical-quantum state quantum Markov chain (cqQMC) with super-operators over a finite dimensional Hilbert space H . The cqQMC is related to previous proposals but yet with a different semantics in that states are pairs of a classical and a quantum state. We define a quantum temporal logic (QCTL) where propositions are pairs of a classical state and a projection over H . We demonstrate how a cqQMC can be translated to a discrete time Markov chain (DTMC). The translation is sound and complete in that model checking any QCTL formula for a cqQMC can equivalently be carried out by checking the same formula for the inferred DTMC. Taking advantage of the finite classical control we show that even though a cqQMC may have infinitely many states then under certain restrictions the inferred DTMC is finite, and hence model checking is decidable.

Verifying quantum systems has attracted a lot of interest in the last decades.In this paper, we study the quantitative model-checking of quantum continuous-time Markov chains (quantum CTMCs). The branching-time properties of quantum CTMCs are specified by continuous stochastic logic (CSL), which is well-known for verifying real-time systems, including classical CTMCs. The core of checking the CSL formulas lies in tackling multiphase until formulas. We develop an algebraic method using proper projection, matrix exponentiation, and definite integration to symbolically calculate the probability measures of path formulas. Thus the decidability of CSL is established. To be efficient, numerical methods are incorporated to guarantee that the time complexity is polynomial in the encoding size of the input model and linear in the size of the input formula. A running example of Apollonian networks is further provided to demonstrate our method.

Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications in quantum physics. More explicitly, we show how quantum statistical and many-body systems can be modeled as quantum Markov chains, and some of their properties that interest physicists can be specified in linear-time temporal logics. Then we present an efficient algorithm to check these properties. A few case studies are given to demonstrate the use of our algorithm to actual quantum physical problems.

Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking omega-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking omega-regular properties for quantum Markov chains.

We propose a discrete time quantum Markov chain (QMC) related to previous proposals but yet with a different semantics. A probability measure is defined similar to as for DTMCs in contrast to e.g.\ the super operator valued measure. Our work is based on a simple imperative quantum pseudo programming language and its denotational semantics which naturally leads to a definition of a QMC. As a novelty we demonstrate how reachability events of a QMC expressed in a simple temporal logic like notation may be checked similar to as for DTMCs as transient state probabilities and how probability intervals of such events may be computed by smallest fixed-point solutions to linear equations.