Verification of termination of generalized quantum Loop program based on safety checking

Ilias Cherkaoui

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.

Mingsheng Ying, Nengkun Yu, Yuan Feng +1 more

Mingsheng Ying

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.

Yongming Li

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.