Model Checking Reachability Properties for Quantum Markov Chains

Godskesen, Jens Christian

Published Aug 1, 2025• 0 citations

Abstract

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.

Related papers

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 ComputationMay 18, 20260 citations

Measurement-Based Verification of Quantum Markov Chains

Ji Guan, Yuan Feng, Andrea Turrini +1 more

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.

arXiv:2405.05825Lecture notes in computer scienceJan 1, 20246 citations

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 TheoryJan 1, 201710 citations

Quantum Markov Chain Semantics for Quip-E Programs

Linda Anticoli, Leonardo Taglialegne

In this work we present a mapping from a fragment of the quantum programming language Quipper, called Quip-E, to the semantics of the QPMC model checker, aiming at the automatic verification of quantum programs. As a main outcome, we define a structural operational semantics for the Quip-E language corresponding to quantum Markov chains, and we use it as a basis for analysing quantum programs through the QPMC model checker. The properties of the semantics are proved and contextualised in the development of a tool translating from quantum programs to quantum Markov chains.

arXiv:2006.02847Jun 4, 20200 citations

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.00382Leibniz international proceedings in informaticsJan 1, 20212 citations

Model Checking of Safety Property over Quantum Markov Chain

Lin Yun-gu

Quantum linear time property is defined,including quantum safety property,quantum invariant which their relationships and properties are studied. Together with measure-one and measure many one way quantum finite automata,two kinds of the product quantum markov chains are constructed,the checking method of quantum regular propertyis provided based on automaton technique. This method shows the satisfaction of quantum regular safety is decided by the reachable termination verification of the product quantum markov chain,and thecomputation formula of satisfaction probability is given. As an application example,the generalized quantum loop program is analyzed. It shows the termination of program is turned into the satisfaction for the verification of quantum regular safety property.

Dianzi xuebaoJan 1, 20140 citations