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.
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.
Loop is a powerful program construct in classical computation, but its power is still not exploited fully in quantum computation. The exploitation of such power definitely requires a deep understanding of the mechanism of quantum loop programs. In this paper, we introduce a general scheme of quantum loops and describe its computational process. The notions of termination and almost termination are proposed for quantum loops, and the function computed by a quantum loop is defined. To show their expressive power, quantum loops are applied in describing quantum walks. Necessary and sufficient conditions for termination and almost termination of a general quantum loop on any mixed input state are presented. A quantum loop is said to be (almost) terminating if it (almost) terminates on any input state. We show that a quantum loop is almost terminating if and only if it is uniformly almost terminating. It is observed that a small disturbance either on the unitary transformation in the loop body or on the measurement in the loop guard can make any quantum loop (almost) terminating. Moreover, a representation of the function computed by a quantum loop is given in terms of finite summations of matrices. To illustrate the notions and results obtained in this paper, two simplest classes of quantum loop programs, one qubit quantum loops, and two qubit quantum loops defined by controlled gates, are carefully examined.
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.
Loop is a very important program construct in classical computation. So, it is necessary to study the structure of the quantum Loop programs. This paper defines a general quantum Loop program whose body is a quantum operation, and gives the definitions for termination, almost termination and non-termination of the general quantum Loop program with respect to any input state. It proves the necessary and sufficient conditions for termination of the general quantum Loop programs given input state. As applications, it finally verifies the embedded quantum Loop programs whose body is unitary operation is a general quantum Loop program.
In this paper,the termination(almost termination)of generalized quantum loop program(for short GQLoop)is firstly investigated,where the loop bodies of GQLoop are described by bit flip channel,depolarizing channel,amplitude damping channel and phase damping channel,respectively.Secondly,when the loop bodies are the embedding of two kinds of GQLoop,the conditions of the termination(almost termination)of GQLoop are addressed.It shows that the conditions of the termination(almost termination)of GQLoop depend on the parameters occuring in the quantum channels.Finally,when the loop bodies are an unitary operation on the principle system and the environment under the open quantum system,after implementing unitary operation,the computed processing of the quantum program is discussed by performing a partial trace over the environment.
Verifying quantum programs has attracted a lot of interest in recent years. In this article, we consider the following two categories of termination problems of quantum programs with nondeterminism, namely: (1) (termination) Is an input of a program terminating with probability one under all schedulers? If not, how can a scheduler be synthesized to evidence the nontermination? (2) (universal termination) Are all inputs terminating with probability one under their respective schedulers? If yes, a further question asks whether there is a scheduler that forces all inputs to be terminating with probability one together with how to synthesize it; otherwise, how can an input be provided to refute the universal termination? For the effective verification of the first category, we over-approximate the reachable set of quantum program states by the reachable subspace, whose algebraic structure is a linear space. On the other hand, we study the set of divergent states from which the program terminates with probability zero under some scheduler. The divergent set also has an explicit algebraic structure. Exploiting these explicit algebraic structures, we address the decision problem by a necessary and sufficient condition, i.e., the disjointness of the reachable subspace and the divergent set. Furthermore, the scheduler synthesis is completed in exponential time, whose bottleneck lies in computing the divergent set reported for the first time. For the second category, we reduce the decision problem to the existence of an invariant subspace, from which the program terminates with probability zero under all schedulers. The invariant subspace is characterized by linear equations and thus can be efficiently computed. The states on that invariant subspace are evidence of the nontermination. Furthermore, the scheduler synthesis is completed by seeking a pattern of finite schedulers that forces all inputs to be terminating with positive probability. The repetition of that pattern yields the desired universal scheduler that forces all inputs to be terminating with probability one. All the problems in the second category are shown, also for the first time, to be solved in polynomial time. Finally, we demonstrate the aforementioned methods via a running example—the quantum Bernoulli factory protocol.
We consider the two categories of termination problems of quantum programs with nondeterminism: 1) Is an input of a program terminating with probability one under all schedulers? If not, how can a scheduler be synthesized to evidence the nontermination? 2) Are all inputs terminating with probability one under their respective schedulers? If yes, a further question asks whether there is a scheduler that forces all inputs to be terminating with probability one together with how to synthesize it; otherwise, how can an input be provided to refute the universal termination? For the effective verification of the first category, we over-approximate the reachable set of quantum program states by the reachable subspace, whose algebraic structure is a linear space. On the other hand, we study the set of divergent states from which the program terminates with probability zero under some scheduler. The divergent set has an explicit algebraic structure. Exploiting them, we address the decision problem by a necessary and sufficient condition, i.e. the disjointness of the reachable subspace and the divergent set. Furthermore, the scheduler synthesis is completed in exponential time. For the second category, we reduce the decision problem to the existence of invariant subspace, from which the program terminates with probability zero under all schedulers. The invariant subspace is characterized by linear equations. The states on that invariant subspace are evidence of the nontermination. Furthermore, the scheduler synthesis is completed by seeking a pattern of finite schedulers that forces all inputs to be terminating with positive probability. The repetition of that pattern yields the desired universal scheduler that forces all inputs to be terminating with probability one. All the problems in the second category are shown to be solved in polynomial time.