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

Dianzi xuebao

Model Checking of Safety Property over Quantum Markov Chain

Lin Yun-gu

Published Jan 1, 2014• 0 citations
OpenAlex

Abstract

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.

Related papers

基于安全性检测的广义量子Loop程序终止验证

Yunguo Lin, Yongming Li

To address the termination problem of the generalized quantum Loop program, in this paper, we first introduce two definitions of termination and almost termination. We show that their expressive power regarding the termination of a program is not sufficient. To compensate for this, we define two other definitions:the nth termination with a specified probability and terminability, and we obtain some conclusions by comparing these four definitions. Secondly, we introduce the definition of the quantum (regular) safety property, which is an important kind of linear-time property of quantum Markov chains. We show that the satisfiability probability of the quantum (regular) safety property is equivalent to the unreachability probability of the termination state in the product of the quantum Markov chains. Then, we discuss a checking technique for the quantum regular safety property. By applying this technique, we reduce the termination problem of the generalized quantum Loop program into the satisfiability problem of the quantum regular safety property, and we propose an algorithm to calculate the probability and the termination state of the nth termination and the terminability. To determine the termination state and the probability of a multi-qubit (single-qubit) quantum system, compound quantum system, and nested quantum system, we derive the probability and the termination state of their nth termination and their terminability, and we present expressions for calculating them. Finally, we prove the necessary and sufficient conditions for the finite-step termination and terminability of the generalized quantum Loop program.

Scientia Sinica Informationis•Dec 1, 2015•0 citations

Model-Checking Linear-Time Properties of Quantum Systems

Mingsheng Ying, Yangjia Li, Nengkun Yu +1 more

We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω--properties recognizable by reversible Büchi automata.

arXiv:1101.0303•ACM Transactions on Computational Logic•Jul 8, 2014•38 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 Theory•Jan 1, 2017•10 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.05825•Lecture notes in computer science•Jan 1, 2024•6 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

Model Checking Quantum Automata

Mingsheng Ying, Yuan Feng

Quantum systems are modelled as different mathematical structures, depending on their nature and complexity. This chapter considers one of the simplest (discrete-time) models of quantum systems, namely quantum automata. It introduces a way of describing linear-time (dynamic) properties of quantum systems and presents several algorithms for checking certain linear-time properties of quantum automata, for example, invariants and reachability.

Cambridge University Press eBooks•Jan 14, 2021•0 citations
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.
To address the termination problem of the generalized quantum Loop program, in this paper, we first introduce two definitions of termination and almost termination. We show that their expressive power regarding the termination of a program is not sufficient. To compensate for this, we define two other definitions:the nth termination with a specified probability and terminability, and we obtain some conclusions by comparing these four definitions. Secondly, we introduce the definition of the quantum (regular) safety property, which is an important kind of linear-time property of quantum Markov chains. We show that the satisfiability probability of the quantum (regular) safety property is equivalent to the unreachability probability of the termination state in the product of the quantum Markov chains. Then, we discuss a checking technique for the quantum regular safety property. By applying this technique, we reduce the termination problem of the generalized quantum Loop program into the satisfiability problem of the quantum regular safety property, and we propose an algorithm to calculate the probability and the termination state of the nth termination and the terminability. To determine the termination state and the probability of a multi-qubit (single-qubit) quantum system, compound quantum system, and nested quantum system, we derive the probability and the termination state of their nth termination and their terminability, and we present expressions for calculating them. Finally, we prove the necessary and sufficient conditions for the finite-step termination and terminability of the generalized quantum Loop program.
We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω--properties recognizable by reversible Büchi automata.
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.
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.
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.