## Quantum Temporal Logic

Nengkun Yu University of Technology Sydney

August 20, 2019

## Abstract

In this paper, we introduce a model of quantum concurrent program, which can be used to model the behaviour of reactive quantum systems and to design quantum compilers. We investigate quantum temporal logic, QTL, for the specification of quantum concurrent systems by suggesting the time-dependence of events. QTL employs the projections on subspaces as atomic propositions, which was established in the Birkhoff and von Neumann's classic treatise on quantum logic. For deterministic quantum program with exit, we prove a quantum B¨ ohm-Jacopini theorem which states that any such program is equivalent to a Q-While program. The decidability of basic QTL formulae for general quantum concurrent program is studied.

## 1 Introduction

The birth of science and logic are inextricably woven. The evolution of computer science and technology would have been impossible without its logical foundation. Conversely, the new model of computation has provided great opportunities for the development of logic. This 'entanglement' between logic and computer science has lasted throughout the last century till now, even before the emergence of ENIAC-the first electronic generalpurpose computer. Logic is ubiquitous in modern computer science. One typical example is temporal logic, the logical formulism for reasoning about time and the timing of events which was introduced to computer science by Pnueli in his seminal work [51]. Temporal logic has become a widely accepted language for stating and specifying properties of concurrent programs and general reactive systems [52]. It is interpreted over models that abstract away from the actual time at which events occur, retaining only temporal ordering information about the states of a system. The necessity of

introducing temporal logic is from the following observations. The correctness of concurrent programs and general reactive systems usually involves reasoning about the corresponding events at different moments in an execution of the system [47]. The expected property of reactive systems, e.g., the liveness properties-something good must eventually happen, as well as fairness properties-a fundamental concept of unbounded nondeterminism of concurrent systems [23], can not be stated as a formula of static logic.

Due to the increasing maturity in the research on quantum program verification, and the potential interest and understanding of the behavior of concurrency in quantum systems, great effort has been expended in the design of quantum programming language [37, 56, 10, 55, 58, 3, 29, 1, 65, 49, 50, 46, 28, 54, 27, 17, 33, 20, 32], as surveyed in [24, 57]. Simultaneously, various quantum logics and techniques have been developed for the verification of quantum programs [2, 5, 6, 13, 16, 18, 19, 21, 25, 34, 4, 53, 60, 67, 75, 72, 73]. Notably, Ying [66] established quantum Hoare logic for both partial correctness and total correctness with (relative) completeness for the notion of quantum weakest precondition proposed by D'Hondt and Panangaden [18]. Of all the properties, the termination of quantum programs has received a fair amount of attention [1, 69, 74, 41, 77, 40]. Quantum process algebra was introduced to model the quantum communication between quantum processors, and thus forms a model of concurrent quantum systems [33, 71, 20]. Temporal logics for quantum states were introduced and then the modelchecking problem for this logic was studied in [43, 8, 7, 42].

Concurrency is a necessary concept to explore the computational power of distributed quantum computing systems. Most of the aforementioned research on the correctness of quantum programs considered programs with exits only. Those are programs with a distinct beginning and end with computational instruction in between, whose correctness statement describes the relation between the input and successful completion of the program. These approaches completely ignore an important class of quantum operating systems or real-time type quantum programs, for instance, the quantum internet [44], for which halting is an abnormal situation.

Understanding the combined behaviour of quantum features and concurrency is nontrivial. Quantum mechanics naturally generate probabilistic branching due to quantum measurement as does quantum programs. On the other hand, non-determinism plays a central role in concurrent programs. A comprehensive definition of a quantum concurrent program which would intergrade quantum probability and non-determinism is still missing. Previous work including [77] should be regarded as concurrent quantum programs but not quantum concurrent programs because that concurrency does not

depend on quantum data but purely classical.

To define the propositional variables of quantum temporal logic, we revisit the (algebraic counter-part of) quantum logic of quantum mechanics which originated in the milestone paper [11] by Garrett Birkhoff and John von Neumann, who were attempting to reconcile the apparent inconsistency of classical logic with the facts concerning the measurement of complementary variables in quantum mechanics, at which time quantum logic was defined as the set of principles for manipulating the projections on a Hilbert space which was viewed as quantum propositions about physical observables in John von Neumann's classic treatise [64]. Projective operators in a Hilbert space correspond one-to-one with the closed subspaces, and the L¨ owner order restricted on projection operators coincides with the inclusion between the corresponding subspaces. The structure of the set of closed subspaces of a Hilbert has been thoroughly investigated in the development of quantum logic for over 80 years. The idea of using quantum projections as a quantum predicate was discussed in [68], where the algebraic structure of the set of closed subspaces and orthomodular lattices theory is reviewed [14, 35]. Recently, this idea was also used to develop quantum relational Hoare logic (qRHL) in [63, 62, 9]. It was employed in providing an applied quantum Hoare Logic in [78].

Contributions of the Paper : In this paper, we derive a quantum Temporal logic (QTL) as a verification tool of quantum concurrent programs. More precisely, our contribution is as follows:

- · We provide a model of quantum concurrent programs which combines quantum probability and non-determinism. In this model, the quantum concurrent program consists of a shared quantum register, a class of quantum programs which can access the quantum register and a scheduler (classical) register which records the program that needs to be performed in the next round. Each program is given as finite lines (locations) of commands with an initial location. Each command consists of a quantum super-operator and a measurement in which the classical index outcome of measurements is used to choose a location of this program and modify the scheduler register, which can be nondeterministically.
- · Weinvestigate quantum temporal logic, QTL, which generalizes Pnueli's classical temporal logic [51]. Birkhoff and von Neumann used projection as quantum atomic propositions where a state satisfies a proposition if the state falls into the subspace corresponding to the projection in [11]. In light of this method, we define the basic temporal operators,

- O (next), U (until), ˜ U (almost surely until) true , ♦ (eventually), ˜ ♦ (almost surely eventually) and /square (always). Note that we do not allow negation although ∧ (conjunction), ∨ (disjunction) are introduced as usual.
- · We study the QTL for deterministic quantum concurrent programs with exits as an example of the general model. We provide a quantum compiler for Q-While, a widely studied quantum extension of the while-language [66]. We prove a quantum B¨ ohm-Jacopini theorem [12] which states that any deterministic quantum concurrent program is equivalent to a Q-While program. Based on this theorem, for deterministic quantum concurrent program,
- -(a) we present a logic with completeness for reasoning and thus fill an important gap in the verification of quantum programs;
- -(b) we provide polynomial time algorithms which compute the reachability super-operator and average running time;
- -(c) we demonstrate a quantum analogue of the Kleene closure which compute the entanglement-assisted reachable space.
- · We study the decidability of basic QTL formulae. For deterministic quantum program, we show that /square ˜ U is decidable while the decidabilities of ♦ ♦ , ˜ , U and ˜ U are equivalent to the decidability of the famous Skolem problem. For general quantum concurrent programs, we prove that /square , /square♦ , ♦/square and /square U are all decidable which solves the open question of [39].

We list the reasons for employing projection as quantum atomic propositions in the following.

- · It enables us to define logical operators ∧ (conjunction), ∨ (disjunction).
- · Each projection P corresponds to a projective measurement { P, I -P } which is physically implementable. The state satisfies P if and only if the measurement outcomes P when applying { P, I -P } on the state. Moreover, the state, if satisfies P , will not collapse after applying the measurement. Therefore, our logic fits very well in the testing and debugging of quantum concurrent programs.
- · For deterministic quantum program with exit, the set of input states such that the program terminates in finite steps, and the set of input

states such that the program terminates with probability 1, can be characterized by closed subspaces, respectively, or equivalently projections, as observed in [78].

## 1.1 Related Work and Comparison

[70] defined a flowchart low-level quantum programming languages and provided a technique of translating quantum flowchart programs into Q-While.

[76] introduced a quantum Markov decision process is as a semantic model of non-deterministic and quantum concurrent programs in which each program is given as a quantum operation and a finite set of measurements is given. At each step, a quantum program is applied or a measurement is performed.

Compared with [70] and [76], the classical control of the model here has a richer structure. Each program consists of a class of commands, marked in corresponding program locations, where each command is a tuple of a quantum operation together with a quantum measurement. The classical control information is recorded in the scheduler register together with the locations of each program. At each step, according to the value of the schedule register, the command corresponding to the current location of the corresponding program is applied. Our quantum B¨hm-Jacopini theorem is o stronger than the one of [70] in the sense that we only need a single syntax of Q-While to characterize the original deterministic program.

Organisation of the Paper : We provide preliminaries about quantum information in Section 2. In Section 3, we introduce the model of quantum concurrent programs. In Section 4, we give the formal definition of quantum temporal logic (syntax, semantics). In Section 5, we study the deterministic quantum concurrent programs with exits as an example. In Section 6, we studied the decidability of quantum temporal logic.

## 2 Quantum Information: Preliminaries and Notations

This section presents the background and notations on quantum information and quantum computation mainly according to the textbook by [45].

## 2.1 Preliminaries

A Hilbert space H is a linear vector space which can be finite dimensional or separable. A separable Hilbert space has a countable orthonormal basis.

For any finite integer n , an n -dimensional Hilbert space H is the space C n of complex vectors. We use Dirac's notation, | ψ 〉 , to denote a complex vector in C n . The inner product of two vectors | ψ 〉 and | φ 〉 is denoted by 〈 ψ φ | 〉 , which is the product of the Hermitian conjugate of | ψ 〉 , denoted by 〈 ψ | , and vector | φ 〉 . The norm of a vector | ψ 〉 is denoted by ‖| ψ 〉‖ = 〈 ψ ψ | 〉 .

√ Linear operators are linear mappings between Hilbert spaces. Operators between n -dimensional Hilbert spaces are represented by n × n matrices. For example, the identity operator I H is the identity matrix on H . The Hermitian conjugate of operator A is denoted by A † . Operator A is Hermitian if A = A † . The trace of an operator A is the sum of the entries on the main diagonal, i.e., Tr( A ) = ∑ i A ii . We write 〈 ψ A ψ | | 〉 to mean the inner product between | ψ 〉 and A ψ | 〉 . A Hermitian operator A is positive semidefinite (resp., positive definite ) if for all vectors | ψ 〉 ∈ H , 〈 ψ A ψ | | 〉 ≥ 0 (resp., &gt; 0). This gives rise to the L¨ owner order /subsetsqequal among operators:

A /subsetsqequal B if B -A is positive semidefinite, A /squareimage B if B -A is positive definite. (1)

A positive semidefinite operator P is called a projection if

$$P = P ^ { \dagger } = P ^ { 2 }.$$

There is a one-to-one correspondence between projection and closed linear subspace. the L¨ owner order /subsetsqequal among projections is equivalent to the subset relation among closed linear subspaces.

## 2.2 Quantum States

The state space of a quantum system is a Hilbert space. The state space of a qubit , or quantum bit, is a 2-dimensional Hilbert space. One important orthonormal basis of a qubit system is the computational basis with | 0 〉 = (1 0) , † and | 1 〉 = (0 1) , which encode the classical bits 0 and 1 respectively. , † Another important basis, called the ± basis, consists of | + = 〉 1 √ 2 ( 0 | 〉 + 1 ) | 〉 and |-〉 = 1 √ 2 ( 0 | 〉 - | 1 ). 〉 The state space of multiple qubits is the tensor product of single qubit state spaces. For example, classical 00 can be encoded by | 0 〉⊗| 〉 0 (written | 0 〉| 0 〉 or even | 00 〉 for short) in the Hilbert space C 2 ⊗ C 2 . The Hilbert space for an m -qubit system is ( C 2 ) ⊗ m ∼ = C 2 m .

A pure quantum state is represented by a unit vector, i.e., a vector | ψ 〉 with ‖| ψ 〉‖ = 1. A mixed state can be represented by a classical distribution over an ensemble of pure states { ( p , i | ψ i 〉 } ) i , i.e., the system is in state | ψ i 〉 with probability p i . One can also use density operators to represent both pure and mixed quantum states. A density operator ρ for a mixed state

representing the ensemble { ( p , i | ψ i 〉 } ) i is a positive semidefinite operator ρ = ∑ i p i | ψ i 〉〈 ψ i | , where | ψ i 〉〈 ψ i | is the outer-product of | ψ i 〉 ; in particular, a pure state | ψ 〉 can be identified with the density operator ρ = | ψ 〉〈 ψ | . Note that Tr( ρ ) = 1 holds for all density operators. A positive semidefinite operator ρ on H is said to be a partial density operator if Tr( ρ ) ≤ 1. The set of partial density operators is denoted by D H ( ).

## 2.3 Quantum Operations

↦

More generally, the evolution of a quantum system can be characterized by an super-operator E , which is a completely-positive and trace-nonincreasing linear map from D H ( ) to D H ( ′ ) for Hilbert spaces H H , ′ . For every super-operator E : D H ( ) →D H ( ′ ), there exists a set of Kraus operators { E k } k such that E ( ρ ) = ∑ k E ρE k † k for any input ρ ∈ D H ( ). Note that the set of Kraus operators is finite if the Hilbert space is finite-dimensional. The Kraus form of E is written as E · ( ) = ∑ k E k · E † k . Aunitary evolution can be represented by the super-operator E · ( ) = U · U † . An identity operation refers to the super-operator I H ( ) · = I H · I H . A super-operator E is tracenon-increasing if for any initial state ρ ∈ D H ( ), the final state E ( ρ ) ∈ D H ( ′ ) after applying E satisfies Tr( E ( ρ )) ≤ Tr( ρ ). A super-operator E is called trace preserving if Tr( E ( ρ )) = Tr( ) holds for any initial state ρ ρ ∈ D H ( ). The Schr¨ odinger-Heisenberg dual of a super-operator E = ∑ k E k ◦ E † k , denoted by E ∗ , is defined as follows: for every state ρ ∈ D H ( ) and any operator A , Tr( A E ( ρ )) = Tr( E ∗ ( A ρ ) ). The Kraus form of E ∗ is ∑ k E † k · E k .

Operations on closed quantum systems can be characterized by unitary operators. An operator U is unitary if its Hermitian conjugate is its own inverse, i.e., U U † = UU † = I H . For a pure state | ψ 〉 , a unitary operator describes an evolution from | ψ 〉 to U ψ | 〉 . For a density operator ρ , the corresponding evolution is ρ → UρU † . The Hadamard operator H transforms between the computational and the ± basis. For example, H | 0 〉 = + | 〉 and H | 1 〉 = |-〉 .

## 2.4 Quantum Measurements

The way to extract information about a quantum system is called a quantum measurement . A quantum measurement on a system over Hilbert space H can be described by a set of linear operators { M m m } with ∑ m M M † m m = I H . If we perform a measurement { M m } on a state ρ , the outcome m is observed with probability p m = Tr( M ρM m † m ) for each m . A major difference between classical and quantum computation is that a quantum measurement changes the state. In particular, after a measurement yielding outcome m , the state

collapses to M ρM /p m † m m . For example, a measurement in the computational basis is described by M = { M 0 = 0 | 〉〈 0 | , M 1 = 1 | 〉〈 1 |} . If we perform the computational basis measurement M on state ρ = + | 〉〈 + , | then with probability 1 2 the outcome is 0 and ρ becomes | 0 〉〈 0 . | With probability 1 2 the outcome is 1 and ρ becomes | 1 〉〈 1 . | Quantum measurements are essentially probabilistic; but we adopt a convention from [58] to present them. We can combine probability p m and density operator ρ m into a partial density operator M ρM m † m = p m m ρ . This convention significantly simplifies the presentation.

A projective measurement on a system with state space H is described by a collection { P m } of projections over H satisfying ∑ m P m = I H , where index m stands for the measurement outcomes that may occur. If the state of a quantum system was ρ immediately before the measurement is performed on it, then the probability that outcome m occurs is p m = Tr( P m ρ , ) and the state of the system after the measurement is ρ m = P m ρP † m /p m . Actually, a general measurement can always be implemented by a projective measurement together with a unitary transformation if an ancillary system is allowed. In the circuit model of quantum computation, measurements are usually assumed to be in the computational basis, which is a special kind of projective measurement.

For a mixed state (density operator) ρ , its support supp( ρ ) is defined as the (topological) closure of the subspace spanned by the eigenvectors of ρ with nonzero eigenvalues. It is easy to see that supp( ρ ) = {| ϕ 〉 ∈ H : 〈 ϕ ρ ϕ | | 〉 = 0 } ⊥ , where ⊥ stands for ortho-complement. The definition of support can be naturally generalized to semi-definite positive operators. An important fact of projective measurements is that, given a state ρ and projection P such that supp( ρ ) ⊆ P , if we apply the (yes/no) projective measurement { P, I -P } on ρ , the state is not changed.

## 2.5 Jordan Canonical Forms

Let M ∈ Q d × d be a square matrix with rational entries. The minimal polynomial of M is the unique monic polynomial m x ( ) ∈ Q [ x ] of least degree such that m A ( ) = 0. By the Cayley-Hamilton Theorem, the degree of m x ( ) is at most d .

We can write any matrix M ∈ C d × d as M = P -1 JP for some invertible matrix P and block diagonal Jordan matrix J = diag J , ..., J ( 1 N ), with each

block J i with size l × l having the following form

$$J _ { i } = \begin{bmatrix} \cdot & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad &\quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \null & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad &
 & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \\ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \	 & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad &  \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ } & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad &	 \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \
 & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad \\ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & & & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \ \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \ \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \ \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \ \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \ \quad & \ \quad & \quad & \quad & \ \ & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \ \ & \quad & \ \ & & \quad & \quad & \quad & \quad & \ \quad & \ \quad & \quad & \quad & \ \quad & \ \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \quad & \quad & \ \quad & \quad & \quad & \ \quad & \quad & \ \quad & \ \ & \quad & \ \ } & \ \quad & \ \ } & \quad & \quad & \quad & \ \ & \quad & \ \ & & \quad & \quad & \ \quad & \quad & \quad & \ \ } & \quad & \ \quad & \ \quad & \ \ & & \ \quad & \quad & \quad & \quad & \quad & \ \quad & \ \quad & \ \ } & \ \ & \quad & \ \ & \quad & \ \quad & \ \quad & \ \ & & \ \ & & \ \ & & \ \ & & \ \ & & \ \ & & \quad & \ \ & & \ \ & & \ \ & & \ \ & & \ \ & & \ \ & & \ \ & \ \ & & \quad & \ \ \ & & \ \ & & \ \ & & \ \ & & \ \ & \ \ & & \ \ & & \quad & \ \quad & \ \quad & \ \ & & \ \ & & \ \ & & \ \ & & \ \$$

where the binomial coefficient ( m j ) is defined to be 0 for m&lt;j . Moreover, given a rational matrix M ∈ Q d × d , its Jordan Normal Form M = P -1 JP can be computed in polynomial time, as shown in [15]. Here, the input size of the problem is the total lengths of the binary representation of all the input entries, and the complexity is measured in terms of binary operations. We associate each algebraic number with its minimal polynomial (thus, irreducible) and a sufficiently good rational approximation, which uniquely identifies the particular root of the polynomial.

## 2.6 Matrix Representation of Super-Operators

The matrix representation of a super-operator is usually easier to manipulate than the super-operator itself.

Definition 2.1. Suppose super-operator E on a finite-dimensional Hilbert space H has the operator-sum representation E ( ρ ) = ∑ i E ρE i † i for all partial density operators ρ , and dim H = d . Then the matrix representation of E is the following d 2 × d 2 matrix:

$$M & = \sum _ { i } E _ { i } \otimes E _ { i } ^ { * }, \\. &. &. &. &.$$

where A ∗ stands for the conjugate of matrix A , i.e. A ∗ = ( a ∗ ij ) with a ∗ ij being the conjugate of complex number a ij , whenever A = ( a ij ) .

The following lemma illustrates the usefulness of the matrix representation of super-operator [74].

Lemma 2.1. We write | Φ 〉 = ∑ j | jj 〉 for the (unnormalized) maximally entangled state in H⊗H , where {| j 〉} is an orthonormal basis of H . Let M be the matrix representation of super-operator E . Then for any d × d matrix A , we have:

$$( \mathcal { E } ( A ) \otimes I ) | \Phi \rangle = M ( A \otimes I ) | \Phi \rangle.$$

Let the matrix representations of super-operators E be M with Jordan decomposition M = SJ M S ( ) -1 , where S is a nonsingular matrix, and J M ( ) is the Jordan normal form of M :

$$J ( M ) = d i a g ( J _ { k _ { 1 } } ( \lambda _ { 1 } ), J _ { k _ { 2 } } ( \lambda _ { 2 } ), \cdots, J _ { k _ { l } } ( \lambda _ { l } ) )$$

with J k s ( λ s ) being a k s × k s -Jordan block of eigenvalue λ s (1 ≤ s ≤ l ). The next lemma describes the structure of the matrix representation M of super-operator F .

$$\text{Lemma } 2. 2. \quad 1. \ | \lambda _ { s } | \leq 1 \text{ for all } 1 \leq s \leq l.$$

- 2. If | λ s | = 1 then the dimension of the s th Jordan block k s = 1 .

## 2.7 Convergence of the decreasing chain of finite union of subspaces

We use the following result proved in [41].

Lemma 2.3. Suppose X k is a union of a finite number of subspaces of H for all k ≥ 1 . If X k is a decreasing chain, i.e., X 1 ⊇ X 2 ⊇ · · · ⊇ X k ⊇ , then there exists n ≥ 1 such that X k = X n for all k ≥ n .

## 2.8 Kronecker's Theorem

The classical Kronecker approximation theorem is formulated as follows.

Theorem 2.1. Given real n-tuples α = ( α , 1 · · · , α n ) ∈ R n and β = ( β , 1 · · · , β n ) ∈ R n , the condition: ∀ /epsilon1 &gt; 0 , ∃ p, q j ∈ N such that

$$| p \alpha _ { i } - q _ { j } - \beta _ { i } | < \epsilon, \forall 1 \leq j \leq n$$

holds if and only if for any r , 1 · · · , r n ∈ Z with ∑ n j =1 r α j j ∈ Z , ∑ n j =1 r β j j is also an integer.

In simpler language, the first condition states that the tuple β = ( β , 1 · · · , β n ) ∈ R n can be approximated arbitrarily well by integer scaling of α and integer vectors. In other words, the decimal part of nα is dense in the set { ( β , 1 · · · , β n ) | n j =1 r β j j ∈ Z , ∀ r j ∈ Z s.t. n j =1 r α j j ∈ Z } .

∑ ∑ To characterize the limit points of nα , we also need the following result from [26] which characterized all ( r , 1 · · · , r n ) ∈ N n such that ∑ n j =1 r α j j ∈ Z , or equivalently Π n j =1 exp( 2 i πr α j j ) = 1.

Theorem 2.2. Given algebraic numbers, λ , 1 · · · , λ n , one can in polynomial time calculate the following set

$$L a \coloneqq \{ ( k _ { 1 }, \cdots, k _ { n } ) | \Pi _ { j = 1 } ^ { n } \lambda _ { j } ^ { k _ { j } } = 1 \} \subset \mathbb { Z } ^ { n }.$$

Remark: La is a lattice, i.e., av 1 + bv 2 ∈ La for all v , v 1 2 ∈ La and a, b ∈ Z . The algorithm outputs a basis of the lattice La .

## 2.9 Skolem-Mahler-Lech Theorem and Skolem Problem

The Skolem-Mahler-Lech theorem is useful in our analysis. We use the version in [31].

Theorem 2.3. If the zero set of a linear recurrence series a n = Tr( | u 〉〈 v A | n ) with | u , 〉 | v 〉 and A being d dimensional integer vectors and invertible matrix is infinite, it is eventually periodic, i.e. it agrees with a periodic set for sufficiently large n . In fact, a slightly stronger statement is true: the zero set is the union of a finite set and a finite number of residue classes { n ∈ N : n = k mod r } . For any prime number p /notbar 2det( A ) , r can be bounded by r ≤ p d 2 .

It is not known whether the following Skolem Problem is decidable for d ≥ 5.

Problem 2.1. Given a linear recurrence set a n = Tr( | u 〉〈 v A | n ) with | u , 〉 | v 〉 and A being d dimensional integer vectors and invertible matrix, determine whether the zero set of a n is empty.

## 3 Systems and Programs

Before providing the general model of quantum sequential and quantum concurrent programs, we recall the framework of classical systems provided in [36].

Definition 3.1. A dynamic discrete system consists of

$$< S, R, s _ { 0 } >$$

where:

- · S is the set of states the system may assume (possibly infinite).
- · R is the transition relation holding between a state and its possible successors, R ⊂ S × S .

- · s 0 is the initial state s 0 ∈ S .

An execution of the system is a sequence:

$$\mathfrak { S } = s _ { 0 } s _ { 1 } \cdots s _ { i } \cdots$$

where for each i ≥ 0 , R s , s ( i i +1 ) holds. The system is deterministic if for any s ∈ S , there is only one t ∈ S such that R s, t ( ) holds. Otherwise, it is non-deterministic.

Similarly, we can form our quantum system as follows: A dynamic discrete time quantum system consists of

$$< \mathcal { H }, R, \rho _ { 0 } >$$

## where:

- · H is the Hilbert space that the system may assume (finite dimensional or separable).
- · R is the transition relation holding between a state and its possible successors, R ⊂ D H ( ) ×D H ( ).
- · ρ 0 is the initial state with ρ 0 ∈ D H ( ).

An execution of the system is a sequence:

$$\mathfrak { S } = \rho _ { 0 } \rho _ { 1 } \cdots \rho _ { i } \cdots$$

where for each i ≥ 0, R ρ , ρ ( i i +1 ) holds. Many different execution sequences are possible as R is nondeterministic in general.

As quantum mechanics is linear, the most natural choice of R is a superoperator introduced in Section 2. However, this would not result in nondeterminism. Non-determinism always corresponds to a finite discrete set. Like the classical framework, we would like the non-determinism to depend on the state. This motivates us to introduced measurement at each step of transition because quantum measurement is the only way to extract classical information from quantum systems.

This concept of discrete quantum system discussed below is very general. Being chiefly motivated by problems in the quantum programming area, all the examples and following discussions will be addressed to the verification of programs. Further structuring of state notion is needed to particularize quantum system into quantum programs.

## 3.1 Sequential Quantum Programs

The sequential quantum programs is given in the following structure.

Definition 3.2. A sequential quantum program is a six tuple

$$\pi = ( \mathcal { H }, L, A c t, Q, \rho _ { 0 }, l ),$$

where

- · H is a Hilbert space, called the state space. H contains the data component and ranges over an infinite domain, the quantum state of H . It can be freely structured into individual variables and data structures for fitting actual applications.
- · L is the control component and assumes a finite number of values, taken to be labels or locations in the program. Without loss of generality, we let L = { l 0 , l 1 , · · · , l n } be the set of locations, | L | can be regarded as the program length.

↦

- · Act is a mapping which associates each location l i ∈ L with a corresponding trace preserving super-operator E l i : D H ( ) → D H ( ) and a quantum measurement M l i = { M l i , 0 , · · · , M l i ,N } satisfying M l i ,j : H ↦→ H . They are used to describe the evolution of the system caused by action. Note that we can assume a uniform N as the number of outcomes for the measurements at all locations because we assume L is finite.

↦

- · Q : { 0 1 , , · · · , N }× L → 2 { l 0 ,l 1 , ··· ,l n } \∅ denotes the next location choice mapping.
- · ρ 0 is the initial state of the system, which lies in H .
- · l 0 ∈ L is the initial location of the program.

where L can be regarded as the control component of the program.

To clarify the transition of the system, we look at the joint distribution of the locations and the quantum data. Due to the probability distribution induced by quantum measurements, the actual state including the location of the program, is not always of the form ρ ⊗| 〉〈 l i l i | , but is as follows:

$$\{ \sum _ { i = 0 } ^ { n } \rho _ { i } \otimes | l _ { i } \rangle \langle l _ { i } | | \rho _ { i } \geq 0, \sum _ { i = 0 } ^ { n } \text{Tr} ( \rho _ { i } ) = 1 \}$$

where ρ i ∈ D H ( ).

We express the transition as follows.

In the first step, E l 0 is applied on the initial state

$$\rho _ { 0 } \otimes | l _ { 0 } \rangle \langle l _ { 0 } | \mapsto \mathcal { E } _ { l _ { 0 } } ( \rho _ { 0 } ) \otimes | l _ { 0 } \rangle \langle l _ { 0 } |.$$

Then, measurement M l 0 is performed and based on the measurement outcome, classical index, and the corresponding location, the location is changed accordingly. In other words, any state of the following form with f ( j, l 0 ) ∈ Q j, l ( 0 ) is reachable non-deterministically

$$\sum _ { j = 0 } ^ { N } M _ { l _ { 0 }, j } \mathcal { E } _ { l _ { i } } ( \rho _ { i } ) M _ { l _ { 0 }, j } ^ { \dagger } \otimes | f ( j, l _ { 0 } ) \rangle \langle f ( j, l _ { 0 } ) |. \\ \dots \dots \dots \dots \dots \varpi n \quad. \ \sim \imath \vee \imath \vee \imath \dots \dots \dots.$$

Generally, at each step, the state ∑ n i =0 ρ i ⊗ | l i 〉〈 l i | is transformed by the following two sub-steps.

- · Apply super-operators according to the location and obtain ∑ n i =0 E l i ( ρ i ) ⊗ | l i 〉〈 l i | .
- · Apply quantum measurement and change location accordingly. The overall state becomes the following for any f ( j, l i ) ∈ Q j, l ( i ) nondeterministically

$$\sum _ { i = 0 } ^ { n } \sum _ { j = 0 } ^ { N } M _ { l _ { i }, j } \mathcal { E } _ { l _ { i } } ( \rho _ { i } ) M _ { l _ { i }, j } ^ { \dagger } \otimes | f ( j, l _ { i } ) \rangle \langle f ( j, l _ { i } ) |.$$

## 3.1.1 Quantum Sequential Program with Exit

This program becomes deterministic if and only if | Q j, l ( i ) | = 1 for all 0 ≤ j ≤ N and l i ∈ L .

We define two kinds of terminations of quantum programs with exits π with exit location l e .

Our model of sequential quantum program can also simulate quantum programs with exit by assuming an exit location l e ∈ L such that E l e and M l e do not change the state, and Q j, l ( e ) = { l e } for all 0 ≤ j ≤ N . More precisely, we let E l e ( ρ ) = ρ for all ρ ∈ D H ( ) and M l e = { I H , 0 0 , , · · · , 0 . }

Definition 3.3. Let σ 0 = ρ 0 ⊗| l 0 〉〈 l 0 | , and σ k denote the state of the system at step (time) k .

- · We say that π terminates if there exists n such that Tr[ σ n ( I H ⊗| l e 〉〈 l e | )] = 1 .

- · We say that π almost terminates if for any δ &gt; 0 there exists n such that Tr[ σ k ( I H ⊗| l e 〉〈 l e | )] &gt; 1 -δ for all k &gt; n .

The termination of a quantum program is rare whereas almost terminaition is much more common as illustrated in the following example.

## Example 3.1. 1. l 1 : ρ 0 = |-〉〈-| , goto l 2 ;

- 2. l 2 : Measure ρ using { M 0 = 0 | 〉〈 0 | , M 1 = 1 | 〉〈 1 |} , if the outcome is 0 , goto l 4 , otherwise, goto l 3 ;
- 3. l 3 : Apply H gate on ρ , goto l 2
- 4. l 4 : goto l 4 ;

This program π is a deterministic program with exit, with l 4 as the exit location.

- · The initial state is σ 0 = |-〉〈-| ⊗ | l 1 〉〈 l 1 | .
- · After the first step, the state becomes σ 1 = |-〉〈-| ⊗ | l 2 〉〈 l 2 | .
- · After the second step, the state becomes σ 2 = 1 2 | 0 〉〈 0 | ⊗ | l 4 〉〈 l 4 | + 1 2 | 1 〉〈 1 | ⊗ | l 3 〉〈 l 3 | .
- · After the third step, the state becomes σ 3 = 1 2 | 0 〉〈 0 |⊗| l 4 〉〈 l 4 | + 1 2 |-〉〈-|⊗ | l 2 〉〈 l 2 | .
- · After the fourth step, the state becomes σ 4 = 3 4 | 0 〉〈 0 | ⊗ | l 4 〉〈 l 4 | + 1 4 | 1 〉〈 1 | ⊗ | l 3 〉〈 l 3 | .
- · · · ·
- · After the 2 n -th step, the state becomes σ 2 n = (1 -1 2 n ) 0 | 〉〈 0 | ⊗| l 4 〉〈 l 4 | + 1 2 n | 1 〉〈 1 | ⊗ | l 3 〉〈 l 3 | .
- · After the 2 n +1-th step, the state becomes σ 2 n +1 = (1 -1 2 n ) 0 | 〉〈 0 | ⊗ | l 4 〉〈 l 4 | + 1 2 n |-〉〈-| ⊗ | l 4 〉〈 l 4 | .

•

· · ·

For any finite n , the program will not reach | l 4 〉〈 l 4 | exactly. That is, π does not terminate. On the other hand, π almost terminates because for any δ &gt; 0, we can find n such that for any k &gt; n such that Tr[ σ n ( I H ⊗| l e 〉〈 l e | )] &gt; 1 -δ .

## 3.2 Quantum Concurrent Programs

To illustrate the quantum concurrent programs, we allow more than one control component. The following model implements the process call, although it does not behave like the recursive model of the quantum programs with exits investigated in [22].

Definition 3.4. An m -party quantum concurrent program is an eight tuple

$$\pi = ( \mathcal { H }, L, A c t, S, Q, \rho _ { 0 }, l, s ),$$

where

- · H is a Hilbert space, called the state space.
- · L = ( L , L , 1 2 · · · , L m ) with L i = { l i, 0 , l i, 1 , · · · , l i,m i } being the control component, locations, of process P i .

↦

- · Act is a mapping which associates each location l i,j ∈ L i with a corresponding trace preserving super-operator E l i,j : D H ( ) →D H ( ) and a quantum measurement M l i,j = { M l i,j , 0 , · · · , M l i,j ,N } satisfying M l i,j ,k : H ↦→ H . They are used to describe the evolution of the system caused by action.
- · S = { 1 2 , , · · · , m } is the register of the scheduler, which records the acting program.

↦

- · Q = ( Q ,Q , 1 2 · · · , Q m ) with Q i : { 0 1 , , · · · , N }× L i → 2 { l i, 0 ,l i, 1 , ··· ,l i,n } × 2 { 1 2 , , ··· ,m } \ ∅ denoting the next location choice and the next program mapping.
- · ρ 0 is an initial state of the system, which lies in H .
- · l 0 = ( l 1 ,i 1 0 , , l 2 ,i 2 0 , , · · · , l m,i m, 0 ) ∈ L with l k,i k, 0 ∈ L k being the initial location of Program π k .
- · s 0 ∈ S denotes the acting program in the first round.

Intuitively, this model admits m programs running concurrently by m processors. At each step of the concurrent system, one program is selected, and the statement at its location is executed. The statement contains a quantum measurement which helps to select the program to be executed in the next step.

Formally, the state of the system always lies in ∆( H× L 1 × L 2 ×··· × L m × [ m ]) defined as

$$& \{ \sum _ { s = 1 } ^ { m } \sum _ { i _ { 1 }, \cdots, i _ { m } } \rho _ { s, i _ { 1 }, \cdots, i _ { m } } \otimes | l _ { 1, i _ { 1 } } \} \langle l _ { 1, i _ { 1 } } | \otimes \cdots \otimes | l _ { m, i _ { m } } \rangle \langle l _ { m, i _ { m } } | \otimes | s \rangle \langle s | | \rho _ { i _ { 0 }, \cdots, i _ { m } } \in \mathcal { D } ( \mathcal { H } ), \sum _ { s, i _ { 1 }, \cdots, i _ { m } } \text{Tr} \rho _ { s, i _ { 0 }, \cdots, i _ { m } } = 1 \} \\ & \dots \dots \dots \, \text{$1$} \quad \tau _ { 1 } \quad \dots \quad \dots 1$$

where [ m ] = 1 2 { , , · · · , m } .

The initial state is

$$\sigma _ { 0 } = \rho _ { 0 } \otimes | l _ { 1, i _ { 1, 0 } } \rangle \langle l _ { 1, i _ { 1, 0 } } | \otimes \cdots \otimes | l _ { m, i _ { m, 0 } } \rangle \langle l _ { m, i _ { m, 0 } } | \otimes | s _ { 0 } \rangle \langle s _ { 0 } |.$$

At the first step, according to data s 0 , π s 0 is chosen and E s 0 ,l s 0 ,i s 0 0 , is applied on the initial state to obtain

$$\mathcal { E } _ { s _ { 0 }, l _ { s _ { 0 }, i _ { s _ { 0 }, 0 } } } ( \rho _ { 0 } ) \otimes | l _ { 1, i _ { 1, 0 } } \rangle \langle l _ { 1, i _ { 1, 0 } } | \otimes \cdots \otimes | l _ { m, i _ { m, 0 } } \rangle \langle l _ { m, i _ { m, 0 } } | \otimes | s _ { 0 } \rangle \langle s _ { 0 } |.$$

Then measurement M l s 0 ,i s 0 0 , is performed and based on the measurement outcome, classical index, and the corresponding location, the location is changed according to Q s 0 . In other words, any state of the following form with ( f s 0 ,i s 0 0 , ,j , t s 0 ,i s 0 0 , ,j ) ∈ Q s 0 ( j, l s 0 ,i s 0 0 , ) is reachable non-deterministically

$$\sum _ { j = 0 } ^ { N } M _ { i _ { s _ { 0 }, i _ { s _ { 0 }, 0 }, i _ { s _ { 0 }, 0 } } }, _ { j } \varepsilon _ { s _ { 0 }, i _ { s _ { 0 }, 0 } } ( \rho _ { 0 } ) M _ { i _ { s _ { 0 }, i _ { s _ { 0 }, 0 } } } ^ { t } \otimes \{ l _ { 1, i _ { 1 } } \} ( l _ { 1, i _ { 1 }, 1 } \} \diamond \cdot \cdot \cdot \otimes l _ { s _ { 0 }, i _ { s _ { 0 }, 0 } } ) ( f _ { s _ { 0 }, i _ { s _ { 0 }, 0 } }, _ { j } \} \diamond \cdot \cdot \cdot \otimes l _ { m, i _ { m }, 0 } ) ( l _ { m, i _ { m }, 0 } ) ( \} ( i _ { s _ { 0 }, i _ { s _ { 0 }, 0 }, i _ { s _ { 0 }, 0 } } ) ) ( t _ { s _ { 0 }, i _ { s _ { 0 }, 0 }, i _ { s _ { 0 }, 0 } ) ),$$

where only π s 0 's location of all locations and the scheduler register would be changed.

Generally, at each step, the state

$$\sum _ { s = 1 } ^ { m } \sum _ { s, i _ { 1 }, \cdots, i _ { m } } \rho _ { s, i _ { 1 }, \cdots, i _ { m } } \otimes | l _ { 1, i _ { 1 } } \rangle \langle l _ { 1, i _ { 1 } } | \otimes \cdots \otimes | l _ { m, i _ { m } } \rangle \langle l _ { m, i _ { m } } | \otimes | s \rangle \langle s | \\ \vdots \colon \text{$\text{$\text{$k$} \quad $k$} \quad $k$} \quad $k$} \quad $k$} \quad $k$} \quad $k$} \quad $k$}$$

is transformed by the following two sub-steps

- · Apply super-operators according to the scheduler and location to obtain

$$\sum _ { s = 1 } ^ { m } \sum _ { i _ { 1 }, \cdots, i _ { m } } \mathcal { E } _ { s, l _ { s, i _ { s } } } ( \rho _ { s, i _ { 1 }, \cdots, i _ { m } } ) \otimes | l _ { 1, i _ { 1 } } \rangle \langle l _ { 1, i _ { 1 } } | \otimes \cdots \otimes | l _ { m, i _ { m } } \rangle \langle l _ { m, i _ { m } } | \otimes | s \rangle \langle s |.$$

- · Apply quantum measurement and change the location accordingly. The overall state becomes the following for any ( l s,i s ,j , t s,i s ,j ) ∈ Q s ( j, l s,i s ) non-deterministically

$$\sum _ { j = 0 } ^ { N } \sum _ { s = 1 } ^ { m } \sum _ { i _ { 1 }, \cdots, i _ { m } } M _ { l _ { s, i _ { s } } } _ { j } \hat { E } _ { s, l _ { s, i _ { s } } } ( \varphi _ { s, i _ { 1 }, \cdots, i _ { m } } ) M _ { l _ { s, i _ { s } } } ^ { \dagger } \otimes l _ { 1, i _ { 1 } } ) ( l _ { 1, i _ { 1 } } | \otimes \cdots \otimes l _ { s, i _ { s } } ) ( l _ { s, i _ { s } } | \otimes \cdots \otimes l _ { m, i _ { m } } ) ( l _ { m, i _ { m } } | \otimes l _ { s, i _ { s } } ) ( l _ { s, i _ { s } } |.$$

Definition 3.5. We say ω = σ σ 0 2 · · · σ k · · · is admissible of the system π if σ 0 = ρ 0 ⊗| l 1 ,i 1 0 , 〉〈 l 1 ,i 1 0 , | ⊗ · · · ⊗ | l m,i m, 0 〉〈 l m,i m, 0 | ⊗ | s 0 〉〈 s 0 | is the initial state and σ i can be obtained by executing the system upon state σ i -1 for all i ≥ 1 .

This program becomes deterministic if and only if | Q s ( j, l s,i s ) | = 1 for all 0 ≤ j ≤ N l , s,i s ∈ L s and 1 ≤ s ≤ m .

This model can also simulate a quantum program with exit by assuming an exit location l s,e s ∈ L s for each s such that E l s,es and M l s,es do not change the state, and Q j,l s ( s,e s ) = { ( l s,e s , s ) } for each 0 ≤ j ≤ N and 1 ≤ s ≤ m .

## 4 QTL: Specifications and Their Classification

To express the system properties and their development in time, we express the relations on states in a suitable language. When applied to programs, this will be a relation between the quantum data, the locations of all processors π , 1 · · · , π m together with the data of the scheduler.

The most general verification problem is to establish facts about the developments of the properties q ρ ( ) in time by introducing time variables t 1 , t 2 , · · · ∈ N as well as the time functional

$$H ( t, q ) \equiv q ( \rho _ { t } ),$$

where ρ t denotes the states, including the classical control components, in time t 1 , t 2 , · · · ∈ N . Arbitrary time dependency can be expressed in the above formulism.

To illustrate our ideas without lengthy demonstration, we limit the expression power of the language with respect to dependency in time. More precisely, we only investigate basic predicates with single time variable and two time variables.

## 4.1 Syntax of Quantum Temporal Logic

As previously mentioned, we only use projections as atomic propositions AP to build QTL, where AP consists of all the operators of the following form

$$\sum _ { s = 1 } ^ { m } \sum _ { l _ { 1 }, i _ { 1 } } \sum _ { l _ { 2 }, i _ { 2 } } P _ { s, l _ { 1 }, i _ { 1 } }, _ { l _ { 2 }, i _ { 2 } }, \cdots, l _ { m, i _ { m } } \otimes | l _ { 1, i _ { 1 } } \rangle \langle l _ { 1, i _ { 1 } } | \otimes | l _ { 2, i _ { 2 } } \rangle \langle l _ { 2, i _ { 2 } } | \otimes \cdots \otimes | l _ { m, i _ { m } } \rangle \langle l _ { m, i _ { m } } | \otimes | s \rangle \langle s |$$

(4)

where P s,l 1 ,i 1 ,l 2 ,i 2 , ··· ,l m,im are all projections of H . AP contains two special elements, I and { } 0 .

Definition 4.1. Let p ∈ AP and ρ ∈ ∆( H× L 1 × L 2 ×···× L m × [ m ]) . We say that ρ satisfies p , written ρ | = p , if supp( ρ ) ⊆ p ; that is, pρ = ρ .

More precisely, QTL is built up from the logical operators ∧ and ∨ , the temporal modal O (next), U (until), ˜ U (almost surely until), false , true , ♦ (eventually), ˜ ♦ (almost surely eventually) and /square (always). The operators ˜ U and ˜ ♦ are introduced to characterize the asymptotical probabilistic behaviour induced by the quantum probability.

Definition 4.2. Formally, the set of QTL formulas over AP is inductively defined as follows:

- · if p ∈ AP then p is an QTL formula;
- · if p, q ∈ AP then p ˜ U q is an QTL formula;
- · if p ∈ AP then ˜ ♦ p is an QTL formula;
- · if φ and ψ are QTL formulas then, φ ∧ ψ , φ ∨ ψ , O φ , ψ U φ , ♦ φ , and /square φ are QTL formulas.

Other than these fundamental operators, there are additional temporal operators defined in terms of the fundamental operators to write QTL formulas succinctly, for instance → and ↔ .

We do not allow ¬ because ρ | = ¬ p does not imply ρ | = q for any p, q ∈ AP .

## 4.2 Semantics of QTL

A QTL formula can be satisfied by an infinite sequence of admissible states w = σ σ 0 1 · · · σ k · · · . Let w i ( ) = σ i , and w i = σ σ i i +1 · · · Formally, the satisfaction relation /satisfies between a sequence of states ω and an QTL formula is defined as follows:

- · w /satisfies p if w (0) /satisfies p ;
- · w /satisfies q ˜ U p for p, q ∈ AP if for any δ &gt; 0 there exists i ≥ 0 such that Tr[ w i p ( ) ] &gt; 1 -δ and for all 0 ≤ k &lt; i , w k /satisfies q ;
- · w /satisfies ˜ ♦ p for p ∈ AP if for any δ &gt; 0, there exists i ≥ 0 such that Tr[ w i p ( ) ] &gt; 1 -δ ;
- · w /satisfies φ ∧ ψ if w /satisfies φ and w /satisfies ψ 1 ;
- · w /satisfies φ ∨ ψ if w /satisfies φ or w /satisfies ψ 2 ;

1 For p, q ∈ AP , p ∧ q denotes the intersection of subspaces p and q , p ∧ q ∈ AP .

2 For p, q ∈ AP , p ∨ q is the union of subspaces p and q , p ∨ q is not always in AP .

- · w /satisfies O φ if w 1 /satisfies φ (in the next time step p must be true);
- · ♦ φ if there exists i ≥ 0 such that w i /satisfies φ ;
- · w /satisfies ψ U φ if there exists i ≥ 0 such that w i /satisfies φ and for all 0 ≤ k &lt; i , w k /satisfies ψ ( ψ must remain true until φ becomes true);
- · w /square φ if for any i ≥ 0, w i /satisfies φ .

We say an ω -word w satisfies a QTL formula φ when w /satisfies φ . The ω -language L φ ( ) defined by φ is { w w | /satisfies φ, ∀ admissible w } , which is the set of ω -admissible states that satisfy φ . A formula φ is satisfiable if there exist ω -admissible states w such that w /satisfies φ .

The additional logical operators are defined as follows:

- · φ → ψ ≡ L φ ( ) ⊂ L ψ ( )
- · φ ↔ ψ ≡ ( ψ → φ ) ∧ ( φ → φ )
- · true ≡ I ,
- · false ≡ { } 0

Definition 4.3. For a quantum program π , we say that a QTL formula φ is valid if for any ω -sequence of admissible state, w , we have w /satisfies φ .

The reason that we use a sequence of quantum states rather than a sequence of subsets of AP is to introduce the ˜ and ♦ ˜ U which study the asymptotical behaviour of the probability induced by quantum measurements. ˜ ♦ p describes the property that the induced number series a , a 0 1 , · · · , a k , · · · with a i = Tr[ pσ i ] has, with 1 as a limit point. The reason for introducing ˜ U is similar.

We reconsider Example 3.1 to illustrate the usefulness to introduce ˜ ♦ p , as well as ˜ . U

$$\text{Example 4.1.} \quad 1. \ l _ { 1 } \colon \rho _ { 0 } = | - \rangle \langle - |, \ g o t o \ l _ { 2 } ;$$

- 2. l 2 : Measure ρ using { M 0 = 0 | 〉〈 0 | , M 1 = 1 | 〉〈 1 |} , if outcome is 0 , goto l 4 , otherwise, goto l 3 ;
- 3. l 3 : Apply H gate on ρ , goto l 2
- 4. l 4 : goto l 4 ;

As illustrated in Example 3.1, this program will not reach l 4 in finite steps. In other words, this program can not satisfy ♦ p with p = 0 | 〉〈 0 | ⊗ | l 4 〉〈 l 4 | . On the other hand, for any δ &gt; 0, we can choose n such that Tr( σ 2 n p ) = 1 -1 2 n &gt; 1 -δ . This program satisfies ˜ ♦ p .

This example indicates that for quantum programs with exits

- · ♦ and U are useful for tracking the total correctness of quantum programs which terminates in finite steps.
- · ˜ ♦ and ˜ U are useful for tracking the total correctness for quantum (probabilistic) programs which almost terminate.

/negationslash

In this example, we observe that p is satisfies at any step with p = 0 | 〉〈 0 | ⊗ | l 4 〉〈 l 4 | + I H ⊗ | ( l 1 〉〈 l 1 | + | l 2 〉〈 l 2 | + | l 3 〉〈 l 3 | ). In other words, /square p is valid. In general, /square is useful for tracking the partial correctness of the program with exit. /square p if we choose p = ∑ l i = l e ∈ L I H ⊗| 〉〈 l i l i | + P ⊗| l e 〉〈 l e | where P is the required property of output. It is invariantly true that whenever we reach the exit, the output satisfies its specification.

## 5 Example: Reasoning and Verification of Deterministic Quantum sequential Programs with Exits

In this section, we focus on a special case of quantum concurrent programsdeterministic quantum programs with exits as an example. We compare our model for deterministic quantum programs with exits with the widely studied Q-While language introduced in [66]. After reviewing the syntax and semantics of Q-While, we show that our model for deterministic quantum programs with exits can be used for designing a compiler for Q-While. Then, we prove a quantum B¨ ohm-Jacopini theorem [12] which states that any deterministic quantum program with exit of our model is equivalent to a Q-While program. In particular, we only need to use a single Q-While statement on a larger space. Using this powerful tool, we are able to analyze such program very clearly.

## 5.1 Q-While Language

We first recall the syntax and semantics of Q-While.

Definition 5.1 (Syntax [66]) . The quantum while -programs are defined by the grammar:

$$S \, \colon = \, & \text{ skip } \, | \, S _ { 1 } ; S _ { 2 } \, | \, q \, \colon = | 0 \rangle \, | \, \overline { q } \, \colon = U [ \overline { q } ] \ \ | \text{ if } \, ( \Box m \cdot \mathcal { M } [ \overline { q } ] = m \to S _ { m } ) \ \text{fi} \\ & | \text{ while } \mathcal { M } [ \overline { q } ] = 1 \, \text{ do } S \text{ od} \\ & \quad \text{$\iota \iota$} \quad. \ \. \ \. \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cdots \ \cd� \end{$$

q := | 0 〉 means that quantum variable q is initialised in a basis state | 0 . 〉 q := U q [ ] denotes that unitary transformation U is applied to a sequence q of quantum variables. In the case statement if · · · fi , quantum measurement M is performed on q and then a subprogram S m is chosen for the next execution according to the measurement outcome m . In the loop while · · · od , measurement M in the guard has only two possible outcomes 0 1: , if the outcome is 0 the loop terminates, and if the outcome is 1, it executes the loop body S and enters the loop again.

A configuration of a program is a pair C = 〈 S, ρ 〉 where S is a program or the termination symbol ↓ , and ρ ∈ D H ( S ) denotes the state of quantum system.

Definition 5.2 (Operational Semantics [66]) . The operational semantics of quantum while -programs is defined as a transition relation → by the transition rules in the following.

$$( \text{Sk} ) \ \langle \text{skip}, \rho \rangle \to \langle \downarrow, \rho \rangle \ ( \text{In} ) \ \ \langle q \coloneqq | 0 \rangle, \rho \rangle \to \langle \downarrow, \rho _ { 0 } ^ { q } \rangle \\ \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \$$

(IF) 〈 if ( /square m M q · [ ] = m → S m ) fi , ρ 〉 → 〈 S m , M m ρM † m 〉

$$& \langle \quad \rangle _ { \nu } \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \colon \\ & ( \text{UT} ) \quad \langle \overline { q } \colon = U [ \overline { q } ], \rho \rangle \to \langle \downarrow, U \rho U ^ { \dagger } \rangle \quad ( \text{SC} ) \quad \frac { \langle S _ { 1 }, \rho \rangle \to \langle S _ { 1 } ^ { \prime }, \rho ^ { \prime } \rangle } { \langle S _ { 1 } ; S _ { 2 }, \rho \rangle \to \langle S _ { 1 } ^ { \prime } ; S _ { 2 }, \rho ^ { \prime } \rangle } \\ & ( \text{IF} ) \quad \langle \text{if $(\sqcap_{m}m\cdot M[\overline { q }] = m \to S _ { \infty} )$} \text{ fi.\,} \alpha \rangle \to \langle S _ { \infty}.. M.. \, M.. \, \alpha M ^ { \dagger } \cdots \rangle$$

- (L0) 〈 while M q [ ] = 1 do S od , ρ 〉 → 〈↓ , M ρM 0 † 0 〉

(L1) 〈 while M q [ ] = 1 do S od , ρ 〉 → 〈 S ; while M q [ ] = 1 do S od , M ρM 1 † 1 〉

In (In), ρ q 0 = ∑ n | 0 〉 q 〈 n ρ n | | 〉 q 〈 0 . | In (SC), we make the convention ↓ ; S 2 = S . 2 In (IF), m ranges over every possible outcome of measurement M = { M m } . Rules (In), (UT), (IF), (L0) and (L1) are determined by the basic postulates of quantum mechanics.

Definition 5.3 (Denotational Semantics [66]) . For any quantum while -program S , its semantic function is the mapping /llbracket S /rrbracket : D H ( S ) → D H ( S ) defined by

$$\underset { \theta } { \in } \mathcal { D } ( \mathcal { H } _ { S } ), \underset { \theta } { \text{where} } \to ^ { * } \text{ is the reflexive and transitive closure of} \to,$$

for every ρ ∈ D H ( S ) , where → ∗ is the reflexive and transitive closure of → , and { | · | } denotes a multi-set.

## 5.2 Deterministic Quantum Program with Exit

The results given in this subsection are applicable for deterministic quantum program with exit, sequential or concurrent. To simplify the presentation, we only provide the proof detail for sequential quantum programs. We first illustrate that our model can be used to design a compiler for Q-While.

Theorem 5.1. Any Q-While program can be expressed in the sequential quantum program model.

Proof.

$$r o o f. \text{ The proof is given in Table 6}.$$

$$\text{skip} \equiv \begin{cases} l _ { 1 } \colon \text{goto } l _ { 2 } ; \\ l _ { 2 } \colon \cdots ; \end{cases}$$

$$S _ { 1 } ; S _ { 2 } \equiv \begin{cases} l _ { 1 } \colon S _ { 1 }, \ g o t o \, l _ { 2 } ; \\ l _ { 2 } \colon S _ { 2 }, \ g o t o \, l _ { 3 } ; \\ l _ { 3 } \colon \cdots ; \end{cases}$$

$$& \text{skip} = \left \{ l _ { 1 } \colon \Lambda _ { 1 } ; \right \} _ { \begin{array} { c } l _ { 2 } \colon \cdots ; \end{array} } & \text{$S_{1} ; S_{2} \equiv \left \{ l _ { 2 } \colon S_{2}, \ goto l_{3} ; \\ l _ { 3 } \colon \cdots ; \\ l _ { 3 } \colon \cdots ; \\ \end{array} \right \} _ { \begin{array} { c } q \colon = \left \{ l _ { 1 } \colon q \colon = \left \{ 0 \right \}, \ goto l _ { 2 } ; \\ l _ { 2 } \colon \cdots ; \end{array} } & q \colon = U [ \overline { q } ] \equiv \left \{ l _ { 1 } \colon \overline { q } \colon = U [ \overline { q } ], \ goto l _ { 2 } ; \\ l _ { 2 } \colon \cdots ; \\ & \text{if} \ ( \underline { m } \cdot \mathcal { M } [ \overline { q } ] = m \rightarrow S _ { m } ) \ \text{fi} \equiv \left \{ \begin{array} { c } l _ { 1 } \colon \text{Measure} \ \rho \ \text{in} \ \mathcal { M }, \text{ if outcome is $m$ goto l_{m+1}$} ; \\ l _ { 2 } \colon S _ { 1 }, \ goto l _ { N + 2 } ; \ \text{$N$ the total number of outcomes.} \\ & \text{if} \ ( \underline { m } \cdot \mathcal { M } [ \overline { q } ] = m \rightarrow S _ { m } ) \ \text{fi} \equiv \left \{ \begin{array} { c } l _ { 1 } \colon \text{Measure} \ \rho \ \text{in} \ \mathcal { M }, \text{ if outcome is $m$ goto l_{m+1}$} ; \\ l _ { 3 } \colon S _ { 2 }, \ goto l _ { N + 2 } ; \\ & \text{while} \ \mathcal { M } [ \overline { q } ] = 1 \ \text{do $S$ odd} \\ & \text{if} \ ( l _ { 1 } \colon \text{Measure} \ \rho \ \text{in} \ \mathcal { M }, \text{ if outcome is $0$ goto l_{3}$, otherwise goto l_{2}$} ; \\ \equiv \ \left \{ l _ { 2 } \colon S, \ goto l _ { 1 } ; \\ & \text{if} \ ( l _ { 3 } \colon \cdots \\ & \text{exit} \ \leftarrow l _ { 1 } \colon \ goto l _ { 1 } ; \\ & \text{else} \ \text{$L$} \ \text{$Minute} Q$-While}$$

$$& \equiv \begin{cases} l _ { 1 } \colon \text{goto $l_{2}$} ; & S _ { 1 } ; S _ { 2 } \equiv \begin{cases} l _ { 1 } \colon S _ { 1 }, \text{ goto $l$} \\ l _ { 2 } \colon S _ { 2 }, \text{ goto $l$} \\ l _ { 3 } \colon \cdots ; \end{cases} \\ & ) \rangle \equiv \begin{cases} l _ { 1 } \colon q \colon = | 0 \rangle, \text{ goto $l_{2}$} ; & q \colon = U [ \overline { q } ] \equiv \begin{cases} l _ { 1 } \colon \overline { q } \colon = l \\ l _ { 2 } \colon \cdots \colon \end{cases} \end{cases}$$

Table 1: Simulate Q-While

Suppose we have a deterministic program π with locations L , where each location l i ∈ L is associated with a trace preserving operation E l i and a measurement M l i = { M l i , 0 , · · · , M l i ,N } , and a function f : { 0 1 , , · · · , N } × L → L .

↦

By considering the state space

$$\Delta = \{ \sum _ { i = 0 } ^ { n } \rho _ { i } \otimes | l _ { i } \rangle \langle l _ { i } | \colon \rho _ { i } \geq 0, \sum _ { i = 0 } ^ { n } \text{Tr} ( \rho _ { i } ) = 1, \} \\ \text{ten's operation $\mathcal{L}_{-}$ can be written as}$$

Each step's operation E π can be written as

$$\mathcal { E } _ { \pi } ( \sum _ { i = 0 } ^ { n } \rho _ { i } \otimes | l _ { i } \rangle \langle l _ { i } | ) & = \sum _ { j = 0 } ^ { N } \sum _ { l _ { i } \in L } M _ { l _ { i }, j } \mathcal { E } _ { l _ { i } } ( \rho _ { i } ) M _ { l _ { i }, j } ^ { \dagger } \otimes | f ( j, l _ { i } ) \rangle \langle f ( j, l _ { i } ) |. \\ \intertext { t h o w m a d e } \epsilon \, - \, \mathcal { A } \sim \epsilon \, \text{when}.$$

In other words, E π = M◦E where

$$\mathcal { E } = \sum _ { l _ { i } } \mathcal { E } _ { l _ { i } } \otimes | l _ { i } \rangle \langle l _ { i } |, \\ N$$

$$\mathcal { M } ( \cdot ) = \sum _ { j = 0 } ^ { N } \sum _ { l _ { i } \in L } ( M _ { l _ { i }, j } \otimes | f ( j, l _ { i } ) \rangle \langle l _ { i } | ) \cdot ( M _ { l _ { i }, j } ^ { \dagger } \otimes | l _ { i } \rangle \langle f ( j, l _ { i } ) | ). \\ \text{similarity} \, \text{$a$ dotministic amount amount amount non-normal $b$ modal $b$}.$$

Similarly, a deterministic quantum concurrent program can be modeled by a super-operator. Therefore, we have the following lemma.

Lemma 5.1. A deterministic quantum program π can be modeled by a superoperator E π in a larger state space ∆ . After k step, the state becomes E k π ( σ 0 ) where σ 0 = ρ 0 ⊗| l 0 〉〈 l 0 | .

For programs with exits, we have the following:

Lemma 5.2. For deterministic quantum program, which contain an exit location l e , we have the following inequality

$$( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \mathcal { E } ( \sigma ) ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \geq ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \sigma ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \quad ( 6 )$$

which holds for any σ ∈ ∆ .

Proof. According to the definition of exit location, we have

$$\mathcal { E } _ { \pi } ( \rho _ { e } \otimes | l _ { e } \rangle \langle l _ { e } | ) = \rho _ { e } \otimes | l _ { e } \rangle \langle l _ { e } |.$$

We note the following

$$& ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \mathcal { E } ( \sigma ) ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) - ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \sigma ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \\ = \ & ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \mathcal { E } [ \sigma - ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \sigma ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) ] ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \\ \geq \ & 0, \\ \text{where we use the fact that any state $ \sigma \, \leq \, \sigma = [ I _ { \mathcal { H } } \otimes | I _ { \cdot } \otimes | I _ { \cdot } \cdot | \Lambda \, \rangle ( I _ { \mathcal { H } } \otimes | I _ { \cdot } \cdot | \Lambda \, \rangle ( I _ { \mathcal { H } } \otimes | I _ { \cdot } \cdot | \Lambda \, \rangle >$$

![image](https://ac.marcodsn.me/arxiv-markdown-images/1908.00158v2-figure-ee3cf621-494f-4ed0-81db-a584620ed984.jpg)

where we use the fact that any state σ ∈ ∆, σ -[ I H ⊗| l e 〉〈 l e | ) σ I ( H ⊗| l e 〉〈 l e | ) ≥ 0.

The above statement is also true for quantum concurrent program π consisting of π , π 1 2 , · · · , π m where each π s has an exit location l s,e s . where the only difference is that there is more than one exit location.

According to Lemma 5.1 and Lemma 5.2, we have the following quantum B¨ ohm-Jacopini theorem.

Theorem 5.2. Any deterministic program π with exit, including program written in Q-While, can be written as a single 'while' statement in Q-While for input σ 0 /satisfies I H ⊗| l 0 〉〈 l 0 | ,

$$\text{while } \mathcal { M } [ \overline { q } ] = 1 \text{ do } S \text{ od},$$

/negationslash

## 5.2.1 Proof System for Partial and Total Correctness

where S = E π , M = { M 0 = I H ⊗| l e 〉〈 l e | , M 1 = I H ⊗ ∑ l i = l e ,l i ∈ L | l i 〉〈 l i |} .

We borrow the idea from [78] to derive a proof system reasoning ˜ and ♦ /square for program π with exit. We first generalize the definition of partial correctness and total correctness of Q-While program [78] to deterministic program S with exit.

Definition 5.4. 1. { P S Q } { } is true in the sense of partial correctness in aQHL, written: | = a par { P S Q } { } , if for all ρ /satisfies P :

$$\left [ S \right ] ( \rho ) \models Q.$$

- 2. { P S Q } { } is true in the sense of total correctness in aQHL, written: | = a tot { P S Q } { } , if for all ρ /satisfies P :

$$\left [ S \right ] ( \rho ) \models Q \ \& \ \text{Tr} ( \left [ S \right ] \right ] ( \rho ) ) = \text{Tr} \rho.$$

Fact 5.1. For any deterministic program S with exit location l e , we employ Theorem 5.2 to transform it into a Q-While program π in state space H⊗ L . We have the following correspondence

/negationslash

- · | = a par { P S Q } { } is equivalent to /square q in π by choosing q = ∑ l i = l e ∈ L I H ⊗ | l i 〉〈 l i | + Q ⊗| l e 〉〈 l e | for input σ 0 /satisfies P ⊗| l 0 〉〈 l 0 | .
- · | = a tot { P S Q } { } is equivalent to ˜ ♦ q in π by choosing q = Q ⊗| l e 〉〈 l e | for input σ 0 /satisfies P ⊗| l 0 〉〈 l 0 | .

Due to this correspondence, we can derive a relatively complete proof system for general deterministic program with exit using the results of [78].

/negationslash

Proposition 5.1. For π = while M [ q ] = 1 do S od with S = E π , M = { M 0 = I H ⊗ | l e 〉〈 l e | , M 1 = I H ⊗ ∑ l i = l e ,l i ∈ L | l i 〉〈 l i |} and p, q ∈ AP , the following proof system is relatively complete for proving /square q and ˜ ♦ q respectively,

$$\Box \, \colon \quad \frac { \{ p \} S \{ \text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ] \} } { \{ \text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ] \} \pi \{ q \} }$$

$$\tilde { \diamond } \colon \ \frac { \text{for any } \epsilon > 0, \ t _ { \epsilon } \text{ is a (supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ], \epsilon ) \text{-ranking function of while} } { \{ \text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ] \} \pi \{ q \} }$$

$$\Box \colon \quad & \frac { \{ p \} S \{ \text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ] \} } { \{ \text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ] \} \pi \{ q \} } \\ & \{ p \} S \{ \text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ] \} \\ \tilde { \otimes } \colon \quad & \text{ for any $\epsilon > 0$, $t_{\epsilon}$ is a $(\text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ], \epsilon )$-ranking funct} } \{ \text{supp} [ ( M _ { 0 } \wedge q ) + ( M _ { 1 } \wedge p ) ] \} \pi \{ q \} \\ & \text{where $a$ function $t \colon \mathcal{D}(\mathcal{Hw}$}, ) \to \mathbb { N}$ is called $a$ (a.\epsilon)$-rankinx function}$$

where a function t : D H ( while ) → N is called a ( q, /epsilon1 ) -ranking function of while if for all σ with σ | = q , we have /llbracket S /rrbracket ( M ρM 1 1 ) = | q , t ( /llbracket S /rrbracket ( M ρM 1 1 )) ≤ t ( σ ) and Tr( σ ) ≥ /epsilon1 implies t ( /llbracket S /rrbracket ( M σM 1 1 )) &lt; t σ ( ) .

## 5.2.2 Compute the reachability super-operator for finite dimensional systems

By Theorem 5.2, we have

Theorem 5.3. Suppose the operation of π is E π with rational entries on quantum system H and locations L with l e as the exit location. The reachability super-operator is defined as

$$\mathcal { F } _ { \pi } ( \cdot ) = \lim _ { n \to \infty } ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | ) \mathcal { E } _ { \pi } ^ { n } ( \cdot ) ( I _ { \mathcal { H } } \otimes | l _ { e } \rangle \langle l _ { e } | )$$

and can be computed in polynomial time.

Moreover, the average running time of the program can be computed in polynomial time for any rational input σ 0 = ρ 0 ⊗| l 0 〉〈 l 0 | .

Proof. According to Theorem 5.2, we reformulate the program in

$$\text{while } \mathcal { M } [ \overline { q } ] = 1 \text{ do } S \text{ od},$$

/negationslash

$$\sum _ { i } F _ { i } \otimes F _ { i } ^ { * } & = ( M _ { 0 } \otimes M _ { 0 } ) ( I _ { \mathcal { H } \otimes L \otimes \mathcal { H } \otimes L } - N ) ^ { - 1 }, \quad \quad ( 8 ) \\ \dots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots$$

where S = E π , M = { M 0 = I H ⊗| l e 〉〈 l e | , M 1 = I H ⊗ ∑ l i = l e ,l i ∈ L | l i 〉〈 l i |} . From [74], we know that F π ( ) = · ∑ i F i · F † i satisfies where N is obtained by replacing M 's Jordan blocks with eigenvalues λ for | λ | = 1 with M = ( ∑ i E i ⊗ E ∗ i )( M 1 ⊗ M 1 ).

Moreover, the average running time of the while program equals the average running time of the original program for reaching the exit location, which can be written as

$$\langle \Phi | ( M _ { 0 } \otimes M _ { 0 } ) ( I - N ) ^ { - 2 } ( \sigma _ { 0 } \otimes I _ { \mathcal { H } \otimes L } ) | \Phi \rangle.$$

where | Φ 〉 = ∑ i,l | il 〉| il 〉 is the unnormalized maximally entangled state on H⊗ L ⊗H⊗ L .

Note that the Jordan block can be computed in the polynomial time of the input size [15], also verifying whether | λ | = 1 is valid in polynomial time for algebraic number λ [26].

Remark: Before this work, this is not known, even for the Q-While programs, because of the complexity of the composition of algebraic numbers due to the composition of whiles.

For deterministic program with exit, /square , ˜ and ♦ ♦ can be verified.

Theorem 5.4. Suppose the operation of π is E π with rational entries on d -dimensional quantum system H and locations L with l e as exit location, | L | = l . For p = P ⊗| l e 〉〈 l e | ∈ AP , ˜ ♦ p , /square p , ♦ p can be verified in polynomial time.

Proof. ˜ ♦ p can be verified using Theorem 5.3.

♦ p if the program terminates in finite steps and satisfies p . According to [74], a While program on dl dimensional system terminates if and only if it terminates in dl -1 steps. The rest is to verify p on E d -1 π ( ρ 0 ⊗| l 0 〉〈 l 0 | ).

/square p if and only if ∑ dl -1 k =0 E π k ( σ 0 ) /dl /satisfies p . The only if part is due to the definition of /square p : for any k and any σ 0 = ρ 0 ⊗ | l 0 〉〈 l 0 | , E π k ( σ 0 ) /satisfies p . Then, ∑ dl -1 k =0 E π k ( σ 0 ) /dl /satisfies p . To see the converse, we let P k = supp( ∑ k k =0 E π k ( σ 0 ) /dl ) /satisfies p , then P 0 ⊆ P 1 ⊆ ··· ⊆ P d -1 ⊆ H . Moreover, if P k = P k +1 , then P k +1 = P k +2 . By counting the dimensions, we know that the increasing chain of subspaces converge after dl -1 steps.

## 5.2.3 Quantum Kleene Closure

Note that the quantum state can always be entangled with other systems. For this situation, we can have the following result as the quantum analogue of the Kleene closure.

Theorem 5.5. Suppose the operation of π is E A with rational entries on d -dimensional system H A , and the input state is given as ρ AB which is a

general state in system H ⊗H A B . E A ⊗I B is an operator applied on H ⊗H A B with input ρ AB . Suppose p is a projection of H A ⊗H B , we have

$$\Box p & \Leftrightarrow \sum _ { k = 0 } ^ { t - 1 } \frac { ( \mathcal { E } _ { A } ^ { k } \otimes \mathcal { I } _ { B } ) ( \rho _ { A B } ) } { t } \models p \\. \quad. \quad. \quad. \quad. \quad. \quad. \quad.$$

where t can be chosen to be d 2 -1 , and does not need to depend on the dimension of H B .

Proof. By the fact of supp( ρ/ 2 + σ/ 2) = span supp( { ρ , ) supp( σ ) } , we only need to consider ρ AB = | χ 〉〈 χ | to be a pure state. Let | χ 〉 have a Schmidt decomposition | χ 〉 = ∑ s k =1 ν i | α i 〉| β i 〉 [45] with s ≤ d , then ( E k A ⊗I B )( ρ AB ) /satisfies q = H ⊗ A Q with Q being the subspace of H B spanned by | β i 〉 . This problem is transformed into system with dimension no more than d 2 . The rest is the same as the proof of Theorem 5.4.

This problem of determining the smallest t is related to the subalgebra generation problem [38], which has recently been shown to be less than √ 2 d 1 5 . +3 d [30, 48]. This implies that t of the above theorem can be chosen to be √ 2 d 1 5 . +3 . Very recently, this bound is improved into 2 d d log 2 d +4 d by Shitov in [59].

It is interesting that t can be chosen independent of the dimension of H B , even H B is infinite dimensional.

## 6 Decidability of QTL

According to the analysis of the last three sections, each deterministic quantum program is determined by a trace preserving super-operator. For nondeterministic quantum program (sequential or concurrent), each non-deterministic choice is correlated to a super-operator. Therefore, a non-deterministic quantum program can always be modeled as a quantum automaton.

Definition 6.1. A quantum automaton A = ( H , Act, {E α | α ∈ Act , ρ } 0 ) , where

- · H is a Hilbert space, called the state space;
- · Act is a set of finite action names;
- · for each α ∈ Act , E α is a trace preserving super-operator;
- · ρ 0 is an initial state of the system, which lies in H .

At the first step, E α 0 is applied on ρ 0 . After this, E α is chosen non-deterministically at each step.

For simplicity, we choose σ 0 = E α 0 ( ρ 0 ) as an initial state, and each w = w w 1 2 · · · w k · · · ∈ Act ω induces an admissible state sequence σ σ σ 0 1 2 · · · σ k · · · with σ i = E w i ( σ i -1 ) for all i ≥ 1.

To study the QTL of a general quantum concurrent system, we only need to study the QTL of the corresponding quantum automaton.

The following observation from [77] is useful.

Fact 6.1. For any p ∈ AP and super-operator E , we have

$$\{ \sigma | \mathcal { E } ( \sigma ) \models p \} = \{ \sigma | \sigma \models ( \mathcal { E } ^ { * } ( p ^ { \perp } ) ) ^ { \perp } \},$$

where for any non-negative matrix M M , ⊥ = supp( { M ) } ⊥ where supp( M ) denotes the subspace spanned by the eigenvectors of M with nonzero eigenvalues.

For p ∈ AP , let E -1 ( p ) := ( E ∗ ( p ⊥ )) ⊥ , we have E -1 ( ∨ r i =1 p i ) = ∨ r i =1 E -1 ( p i ) . For p ∈ AP , let E ( p ) = supp( E ( p d p )) , where d p denotes the dimension of p , we have E ∨ ( r i =1 p i ) = ∨ r i =1 E ( p i ) .

In the following, we study the decidability of the basic QTL formulae. We assume all the entries are rational numbers, and H is d -dimensional. If all E α are all unitaries, the decidability of /square ∨ n i =1 p i , /square♦ ∨ n i =1 p i and ♦/square ∨ n i =1 p i was presented in [39]. As part of our results below, we generalizing these results into general super-operators and thus solve the open questions of [39].

It worth to notice that /square♦ ∨ n i =1 p i and ♦/square ∨ n i =1 p i are highly nontrivial in the sense that no uniform time bound for the ♦ on different paths.

## 6.1 Next

To decide O ( p ), we only need to verify /satisfies p for the next step. In other words, it is enough to verify /satisfies p for the original system with different initial state σ = E α ( σ 0 ) for all α ∈ Act where σ 0 is the current state.

## 6.2 Invariance

One-time variable invariance is universally quantified. Invariance, denoted by /square , is a property holding throughout all states of all possible execution sequences.

Lemma 6.1. [77]. For p ∈ AP and | Act | &gt; 1 , we know that /square p if and only if E k ( σ 0 ) /satisfies p for 0 ≤ k ≤ d -1 with E = ∑ α ∈ Act E α | Act | .

If φ is not an element of AP , but a union of elements in AP , in other words, φ is a finite union of closed subspaces, the problem of determining /square φ becomes non-trivial. In the following, we consider the general case.

Theorem 6.1. If φ = ∨ n i =1 p i with p i ∈ AP , /square φ is decidable for | Act | &gt; 1 .

Proof. We can characterize all initial states σ 0 such that /square φ is valid in the following. In particular, we present ψ = ∨ r j =1 q i with q i ∈ AP and show that /square φ if and only if σ 0 /satisfies ψ . To see this, we let

$$\cdot \psi \cdot \, \gamma \cdot \, \lambda \, \infty \, \infty \, \varphi \,, \, \mu \, \infty \, \infty \\ Y _ { 0 } \, & = \, \phi, \\ Y _ { 1 } \, & = \, \Psi _ { 0 } \, \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Y _ { 0 } ), \\ & \cdots \,, \\ Y _ { k } \, & = \, \Psi _ { k - 1 } \, \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Y _ { k - 1 } ), \\ & \cdots \\ \text{the set of states that satisfies $\phi$ in $0$ step.}$$

Y 0 characterizes the set of states that satisfies φ in 0 step. Y 1 characterizes the set of states that satisfies φ in 0 step and 1 step. Y k characterizes the set of states that satisfies φ in less than k +1 step. Each Y i is a finite union of subspaces, and Y 0 ⊇ Y 1 ⊇ · · · Y k ⊇ . According to Lemma 2.3, there exists k such that Y k = Y m for all m ≥ k . Let Y k = ψ , then, we only need to verify σ 0 /satisfies ψ .

## 6.3 Eventually and Almost Surely Eventually

Eventually is another one time variable. Determining ♦ p is an open issue, even for | Act | = 1 and p ∈ AP . This is related to the famous Skolem problem [61] which asks whether there exists n such that A x n ∈ p for given rational square matrix A , vector x and subspace p .

Fact 6.2. For | Act | = 1 , ♦ p is decidable for p ∈ AP if and only if the Skolem Problem 2.1 is decidable.

Proof. For any A and x without loss of generality, assume A A † ≤ I H and x x † ≤ 1, and | 0 〉 ∈ p . We design the following trace preserving superoperator

$$\mathcal { E } ( \rho ) = A \rho A ^ { \dagger } + ( 1 - \text{Tr} A ^ { \dagger } A \rho ) | 0 \rangle \langle 0 |.$$

E n ( xx † ) /satisfies p if and only if A x n ∈ p .

On the other hand, if we can solve the Skolem problem, we can verify ♦ p for | Act | = 1 as follows. Let q = I -p where p ∈ AP is regarded as the projection onto subspace p .

$$\mathcal { E } ^ { n } ( \rho _ { 0 } ) \models p & \quad \Leftrightarrow \quad \text{Tr} [ \mathcal { E } ^ { n } ( \sigma _ { 0 } ) p ^ { \perp } ] = 0 \\ & \quad \Leftrightarrow \quad \langle \Phi | ( q \otimes I ) M ^ { n } ( \sigma _ { 0 } \otimes I ) | \Phi \rangle = 0 \\ & \quad \Leftrightarrow \quad M ^ { n } ( \sigma _ { 0 } \otimes I ) | \Phi \rangle \in \{ | v \rangle | | v \rangle \perp ( q \otimes I ) | \Phi \rangle \}, \\ \dots \dots \, M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon = M \colon$$

where M is the matrix representation of E and | Φ = 〉 ∑ d i =1 | ii 〉 . Concerning ˜ ♦ p , we have a similar result as ♦ p .

Fact 6.3. For | Act | = 1 , ˜ ♦ p is decidable for p ∈ AP if and only if the Skolem problem 2.1 is decidable.

Proof. ˜ ♦ p if and only if one of the following two cases is valid.

- · ♦ p ;
- · There exists a sequence of n , n 1 2 , · · · , n k such that the induced number sequence a , a 1 2 , · · · , a k , · · · converges to 1 where a k = Tr[ p E n k ( σ 0 )].

Case 2 is decidable via the following procedure. Let the linear recurrent series b n = 1 -a n = Tr[( I -p ) E n ( σ 0 )]. According to Subsection 2.6, we first write it as b n = Tr( M N n ) where M = ∑ j E j ⊗ E ∗ j and N is determined by ( I -p ) and σ 0 . Let M = SJ M S ( ) -1 be the Jordan decomposition of M , we have b n = Tr[ J M ( ) n S -1 NS ]. According to Lemma 2.2, we know that every Jordan block of M has eigenvalue with absolution no more than 1, and the size of the block with absolution 1 eigenvalue is 1. As we are only interested in the limit points, we only need to care about number series c n = Tr[ J M ( ) ′ n S -1 NS ], where we delete all the Jordan blocks whose absolution of eigenvalue is smaller than 1. In other words, J ′ = J M ( ) ′ is a diagonal matrix with eigenvalues either 0 or absolution 1. The problem becomes seeing whether 0 is a limit point of c n .

Note that these eigenvalues are all algebraic numbers. Without loss of generality, we assume these nonzero eigenvalues λ , 1 · · · , λ r lie at the leading principal submatrix. According to Theorem 2.2, one can compute a basis of lattice

$$L a \coloneqq \{ ( k _ { 1 }, \cdots, k _ { r } ) | \Pi _ { j = 1 } ^ { r } \lambda _ { j } ^ { k _ { j } } = 1 \} \subset \mathbb { Z } ^ { r },$$

in polynomial time. Assume the computed basis is v , v 1 2 , · · · , v t with v j = ( v j, 1 , · · · , v j,r ) T ∈ Z r . According to Theorem 2.1, the closure of { J ′ 0 , J ′ 1 , · · · } , the diagonal elements, is characterized by

$$\{ ( e ^ { i \theta _ { 1 } }, e ^ { i \theta _ { 2 } }, \cdots, e ^ { i \theta _ { r } } ) | \Pi _ { k = 1 } ^ { r } e ^ { i \theta _ { k } v _ { j, k } } = 1 \ \forall \ 1 \leq j \leq t. \}$$

Now the problem becomes to determine whether there exists ( e iθ 1 , e iθ 2 , · · · , e iθ r ) lying in the above set which satisfies Tr[ JS -1 NS ] = 0 with J = diag { e iθ 1 , e iθ 2 , · · · , e iθ r , 0 , · · · , 0 . } Let e iθ k = x k + y k , then Tr[ JS -1 NS ] = 0 is a polynomial equation of x k and y k with algebraic coefficients. Π r k =1 e iθ k v j,k = 1 can also be rewritten as polynomial equations of x k and y k with algebraic coefficients. The rest of the equations are x 2 k + y 2 k = 1 for 1 ≤ k ≤ t . According to Tarski's theorem on polynomial equations with algebraic coefficients, it is decidable to verify whether 0 is a limit point of c n .

Note that Case 2 of the above proof actually shows

Fact 6.4. For | Act | = 1 and p ∈ AP , /square♦ ˜ p is decidable.

We can further show that

Fact 6.5. For | Act | = 1 and p ∈ AP , /square♦ p is decidable.

Proof. /square♦ p if and only if there exist infinite n such that linear recurrent b n = Tr[( I -p ) E n ( ρ 0 )] = 0. We can always find an integer s such that c n = s n b n = Tr[ A M n ] for integer matrices A and rank 1 matrix M b . n = 0 if and only if c n = 0. If this is true, by Theorem 2.3, we can bound the period r ≤ p d 4 by choosing p /notbar 2det A . The rest is to verify whether c vr + u = 0 is valid for fixed u ≤ r and all v . This can be done as for fixed r and u , d v = c vr + u is still a linear recurrent series of degree d 2 . d v ≡ 0 if and only if the initial d 2 +1 element is 0.

To show the decidability of ♦/square φ with φ = ∨ t i =1 p i and p i ∈ AP for | Act | &gt; 1, the following lemmas are needed.

Lemma 6.2. For finite union of subspaces r ⊆ H , we can construct x ⊆ r in finite steps, such that

- · ∨ E α α ( x ) = x ;
- · For any x ′ ⊆ r such that ∨ E α α ( x ′ ) = x ′ , we always have x ′ ⊆ x .

Moreover, such x is also a finite union of subspaces, and x is called the maximal invariant of r .

Remark: All x ⊆ H can always be written as a union (a possibly infinite union or even a continuous union), for this sense, ∨ is still well defined as a union.

Proof. Our construction of x is as follows:

$$\cdots \cdots \cdots \cdots \cdots \cdots \cdots \\ Z _ { 0 } & = r, \\ Z _ { 1 } & = Z _ { 0 } \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Z _ { 0 } ) \bigcap [ \vee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( Z _ { 0 } ) ], \\ \cdots, \\ Z _ { k } & = Z _ { k - 1 } \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Z _ { k - 1 } ) \bigcap [ \vee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( Z _ { k - 1 } ) ], \\ \cdots$$

· · ·

First note that each Z i is a finite union of subspaces and forms a decreasing chain

$$p = Z _ { 0 } \supseteq Z _ { 1 } \supseteq \cdots \supseteq Z _ { k } \supseteq \cdots \\ \widehat { \ } \sim \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot$$

According to Lemma 2.3, there exists n such that Z n = Z m for any m ≥ n . Let x = Z n , we have

$$\text{we move} \\ x & = x \, \bigcap _ { \alpha \in A c t } \, \mathcal { E } _ { \alpha } ^ { - 1 } ( x ) \bigcap [ \bigvee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ) ] \\ \Rightarrow & \, x \subseteq \mathcal { E } _ { \alpha } ^ { - 1 } ( x ), \ x \subseteq \bigvee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ) \\ \Rightarrow & \, \mathcal { E } _ { \alpha } ( x ) \subseteq x, \ x \subseteq \bigvee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ) \\ \Rightarrow & \, \bigvee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ) \subseteq x, \ x \subseteq \bigvee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ) \\ \Rightarrow & \, x = \bigvee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ). \\ \text{is a finite union of subspaces.}$$

Moreover, x is a finite union of subspaces.

Assume ∨ α ∈ Act E α ( x ′ ) = x ′ ⊆ r = Z 0 , we have

$$& \quad \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \\ & \quad \mathcal { E } _ { \alpha } ( x ^ { \prime } ) \subset Z _ { 0 }, \ x ^ { \prime } \subseteq Z _ { 0 }, \\ \Rightarrow \quad & x ^ { \prime } \subseteq \mathcal { E } _ { \alpha } ^ { - 1 } ( Z _ { 0 } ), \mathcal { E } _ { \alpha } ( x ^ { \prime } ) \subseteq \mathcal { E } _ { \alpha } ( Z _ { 0 } ) \\ \Rightarrow \quad & x ^ { \prime } \subseteq \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Z _ { 0 } ), \ x ^ { \prime } = \vee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ^ { \prime } ) \subseteq \vee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( Z _ { 0 } ) \\ \Rightarrow \quad & x ^ { \prime } \in Z _ { 1 } \ \Rightarrow \ \cdots \ \Rightarrow \ x ^ { \prime } \subseteq Z _ { k } \ \Rightarrow \ x ^ { \prime } \subseteq x.$$

$$\Rightarrow \ x ^ { \prime } \in Z _ { 1 } ^ { \mu } \ \Rightarrow \ \cdots \ \Rightarrow \ x ^ { \prime } \subseteq Z _ { k } \ \Rightarrow \ x ^ { \prime } \subseteq x.$$

This completes the proof.

Lemma 6.3. For finite union of subspaces x ⊆ H with ∨ α ∈ Act E α ( x ) = x , we can construct y in finite steps such that

- · x ⊆ y and y = ⋂ α ∈ Act E -1 α ( y ) .
- · For any y ′ ⊆ H such that y ′ = ⋂ α ∈ Act E -1 α ( y ′ ) and x ⊆ y ′ we always have y ⊆ y ′ .

Moreover, such y is also a finite union of subspaces. We call y the maximal extension of x .

Proof. Observe that y is characterized as the limit by the following,

$$Y _ { 0 } \ & = \ x, \\ Y _ { 1 } \ & = \ \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Y _ { 0 } ),$$

$$Y _ { 0 } \ & = \ x, \\ Y _ { 1 } \ & = \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Y _ { 0 } ), \\ \dots \\ Y _ { k } \ & = \bigcap _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ^ { - 1 } ( Y _ { k - 1 } ), \\ \dots \\ \gamma _ { 0 }, \, \text{then} \ x \subseteq \mathcal { E } _ { \alpha } ^ { - 1 } ( x ). \ T h u s, \, x = Y _ { 0 }$$

Since E α ( x ) ⊆ x = Y 0 , then x ⊆ E -1 α ( x ). Thus, x = Y 0 ⊆ ⋂ α ∈ Act E -1 α ( Y 0 ) = Y 1 . By repeating this argument, we know that Y 0 ⊆ Y 1 ⊆ · · · ⊆ Y k ⊆ . Y k characterize the set of input states such that x is satisfied in the k -th steps. Unfortunately, with the general increasing of the chain of finite union of subspaces, there is no guarantee of termination.

To show the termination of the series, we first note that for each α , and z = ∨ s i =1 z i with z i ∈ AP , E -1 α ( z ) is still a union of no more than s subspaces. In other words, the number of unions is not increasing in computing the preimage. Now we can construct an | Act | -ary tree T whose nodes are all the union of at most s subspaces.

- · Let x = ∨ t i =1 x i be the root of T where x i ∈ AP .
- · At the first step, for each α , we generate E -1 α ( x ). If E -1 α ( x ) /supersetnoteql x , we add E -1 α ( x ) as a child of x . Otherwise E -1 α ( x ) = x , we mark x as a 'star' node. Now we have a tree of height at most 2.

•

· · ·

- · At the k -th step, for each α and each leaf node n d of the current tree, we generate E -1 α ( n d ). If E -1 α ( n d ) /supersetnoteql n d , we add E -1 α ( n d ) as a child of n d . Otherwise E -1 α ( n d ) = n d , we mark n d as a 'star' node.

•

· · ·

- · Stop if current leaves are all 'star' nodes.

One can verify that this tree is a strictly increasing tree, in the sense that each node (union of at most s elements) strictly contains its parent node. We can easily verify that the height of this tree is at most td according to the following fact via simply counting the dimension. For each strictly increasing chain of Z 0 /subsetnoteql Z 1 /subsetnoteql · · · /subsetnoteql Z k /subsetnoteql · · · where each Z i is a union of at most t subspaces, the chain terminates in at most td steps. Now we can claim that

$$y = \quad \bigcap \quad n _ { d }.$$

$$= \bigcap _ { n _ { d } \text{ is a "Star" node.} } n _ { d }$$

We provide the characterization of ♦/square φ ,

Lemma 6.4. For φ = ∨ t i =1 p i with p i ∈ AP , let x be the maximal invariant of φ defined in Lemma 6.2. ♦/square φ if and only if σ 0 /satisfies ψ where ψ is the maximal extension of x defined in Lemma 6.3.

Proof. Let η denote the set that ♦/square φ if and only if σ 0 /satisfies η . For any α , if σ 0 /satisfies E α ( η ), ♦/square φ is valid. This implies E α ( η ) ⊆ η , therefore, ∨ α ∈ Act E α ( η ) ⊆ η . We define the sequence Z 0 = η , Z 1 = ∨ α ∈ Act E α ( Z 0 ), · · · , Z k = ∨ α ∈ Act E α ( Z k -1 ), · · · . We can verify Z 0 ⊇ Z 1 ⊇ ··· ⊇ Z k ⊇ ··· . Let y = ⋂ ∞ k =0 Z k , we have y = ∨ α ∈ Act E α ( y ). According to ♦/square φ , we know that y ⊆ φ . This means y ⊆ x according to the fact x is the maximal invariant of φ in Lemma 6.2. By defining an increasing sequence V 0 = x , V 1 = ∨ α ∈ Act E -1 α ( V 0 ), · · · , V k = ∨ α ∈ Act E -1 α ( V k -1 ), · · · we have η ⊆ ∨ ∞ k =0 V k = ψ .

On the other hand, if σ 0 /satisfies ψ , for each ω path α α 1 2 · · · , let state σ k = E α k ( σ k -1 ). According to the proof of Lemma 6.3, there exists k 0 such that ρ k /satisfies x for all k &gt; k 0 . Therefore ♦/square φ is valid.

The following theorem naturally follows from Lemma 6.2, Lemma 6.3 and Lemma 6.4.

Theorem 6.2. ♦/square φ is decidable for φ = ∨ t i =1 p i and | Act | &gt; 1 with p i ∈ AP .

The following lemma is crucial in proving the decidability of /square♦ φ .

Lemma 6.5. For φ = ∨ s i =1 p i with p i ∈ AP , we can construct x ⊆ H in finite steps, such that

$$1. \vee _ { \alpha \in A c t } \mathcal { E } _ { \alpha } ( x ) = x.$$

- 2. For any simple loop (distinct elements of the loop at different locations),

$$x _ { j _ { 1 } } & \xrightarrow { \mathcal { E } _ { \alpha _ { 1 } } } x _ { j _ { 2 } } \xrightarrow { \mathcal { E } _ { \alpha _ { 2 } } } \cdots x _ { j _ { k } } \xrightarrow { \mathcal { E } _ { \alpha _ { k } } } x _ { j _ { 1 } } \\ \nolimits _ { \alpha } \, \kappa \, \left ( \Delta D \, \nolimits _ { \alpha } \, \nolimits _ { \alpha } \, \nolimits _ { \alpha } \, \kappa \, \right ) \, \kappa \, \right )$$

where x j 1 , x j 2 , · · · , x j k ∈ AP , x j 1 , x j 2 , · · · , x j k ⊆ x and E α 1 ( x j 1 ) = x j 2 , · · · , E α k ( x j k ) = x j 1 , there exists an element x j r of the loop and 1 ≤ i ≤ s such that x j r ⊆ p i .

- 3. For any x ′ ⊆ H satisfies the first two conditions, we always have x ′ ⊆ x .

Moreover, such x is also a finite union of subspaces.

The proof of this theorem depends on Lemma 6.6.

Proof. We can construct x using the following procedure.

- · l 0 : Set x = H , goto l 1 ;
- · l 1 : If Condition 1 and 2 of Lemma 6.5 are satisfied, return x ; otherwise, goto l 2 ;
- · l 2 : Run procedure of Lemma 6.2, goto l 3 ;
- · l 3 : Run procedure of Lemma 6.6, goto l 1 ;

For any finite union of subspaces as input, Lemma 6.2 and Lemma 6.6 terminate within finite time. l 1 , l 2 , l 3 can only be executed a finite number of times according to Lemma 2.3 because the intermediate data is always a finite union of subspaces in decreasing order.

For any x ′ ⊆ H satisfies the first two conditions, x ′ ⊆ x is always valid during the execution of the above procedure. Therefore, x ′ ⊆ x is valid for the final x .

In the proof of Lemma 6.5, if Condition (1) of Lemma 6.5 is satisfied, but Condition (2) is not satisfied, we need the following lemma.

Lemma 6.6. Given φ = ∨ t i =1 p i and x = ∨ l i =1 x i with p , x i i ∈ AP , if ∨ α ∈ Act E α ( x ) = x and there is a simple loop (distinct elements of the loop at different locations),

$$x _ { j _ { 1 } } \xrightarrow { \mathcal { E } _ { \alpha _ { 1 } } } x _ { j _ { 2 } } \xrightarrow { \mathcal { E } _ { \alpha _ { 2 } } } \cdots x _ { j _ { k } } \xrightarrow { \mathcal { E } _ { \alpha _ { k } } } x _ { j _ { 1 } } \\ \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \colon \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \ddots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots \cdots.$$

/negationslash where x j 1 , x j 2 , · · · , x j k ∈ AP and E α 1 ( x j 1 ) = x j 2 , · · · , E α k ( x j k ) = x j 1 , such that x j r ⊆ φ for any j r . We can find z as a finite union of proper subspaces in x j 1 such that any x ′ ⊆ x satisfies

- · There are infinite many i such that σ i /satisfies p , for any ω sequence σ σ 0 1 · · · with σ i = E β i ( σ i -1 ) for any β i ∈ Act with σ 1 /satisfies x ′ .

must satisfy

/negationslash

$$x ^ { \prime } \subseteq \vee _ { i = 1, i \neq j _ { 1 } } ^ { l } x _ { i } \vee z.$$

Proof. For any σ 0 /satisfies x j 1 ⋂ x ′ , we consider sequence ω = σ σ 0 1 · · · σ r · · · such that σ i = E α i ( σ i ). We can divide ω into k subsequence, ω 1 = σ σ 1 k +1 · · · , · · · , ω k = σ σ k 2 k · · · . According to the properties x ′ satisfies, we know that there exist 1 ≤ s ≤ t and 1 ≤ r ≤ k such that the sequence ω r contains infinite state which satisfies p s . In other words, there exists infinite n such that σ nk + r = F n r ( ξ ) /satisfies p s where ξ = E α r ◦ E α r -1 ◦ · · · ◦ E α 1 ( σ 0 ), and F r = E α r ◦ · · · ◦ E α 1 ◦ E α k ◦ · · · E α r +1 . Let a i = Tr( F n r ( ξ p ) ⊥ s ). Then the linear recurrent series a i has infinite zero points. Theorem 2.3 implies that, there is a finite b, c such that a bu + c = 0 for all u ∈ N . Moreover, one can compute a g ≥ b which depends on F r only. Therefore, we can choose b = g ! and let c range over all integer less than b . Interestingly, for fixed c , we only need to verify a bu + c = 0 for 0 ≤ u ≤ d 2 +1 since a bu + c is a linear recurrent series with degree d 2 . In other words, σ 0 should satisfy that for some 1 ≤ s ≤ t , 1 ≤ r ≤ k , 1 ≤ c ≤ b , the following is true for any 0 ≤ u ≤ d 2 +1,

$$\mathcal { F } _ { r } ^ { b u + c } \circ \mathcal { E } _ { \alpha _ { r } } \circ \mathcal { E } _ { \alpha _ { r - 1 } } \circ \cdots \circ \mathcal { E } _ { \alpha _ { 1 } } ( \sigma _ { 0 } ) \models p _ { s }.$$

For each s, r, c , the constrain is equivalent to a subspace z s,r,c . Moreover, x j 1 is not a subspace of any z s,r,c according to the condition of x . Let z = ∨ s,r,c ( x j 1 ⋂ z s,r,c ) and it satisfies the requirement. Now we show the following

Theorem 6.3. For p i ∈ AP and φ = ∨ t i =1 p i , /square♦ φ is decidable.

Proof. Let ψ ′ denote the set that ♦/square φ if and only if σ 0 /satisfies ψ ′ .

We first compute x = ∨ l i =1 x i of φ as illustrated in Lemma 6.5, then compute ψ as the maximal extension of x in Lemma 6.3. We prove that ψ ′ = ψ .

To show ψ ⊆ ψ ′ , we choose σ 0 /satisfies ψ . For each ω path α α 1 2 · · · , we let state σ k = E α k ( σ k -1 ). According to the proof of Lemma 6.3, there exists k 0 such that σ k /satisfies x for any k &gt; k 0 . For any k &gt; k 0 , the state sequence σ σ k k +1 · · · σ k + s satisfies σ k + i /satisfies x j i for some 1 ≤ j i ≤ l . Moreover, there is a simple loop for sufficiently large s because l is finite. Invoking the Condition (2) of Lemma 6.5, σ k + u /satisfies x for some 1 ≤ u ≤ s . /square♦ φ is valid. Therefore, ψ ⊆ ψ ′ .

To show ψ ⊇ ψ ′ , we observe that for any α , if σ 0 /satisfies E α ( ψ ′ ), /square♦ φ is valid. This implies E α ( ψ ′ ) ⊆ ψ ′ . Therefore, ∨ α ∈ Act E α ( ψ ′ ) ⊆ ψ ′ . We define the sequence Z 0 = ψ ′ , Z 1 = ∨ α ∈ Act E α ( Z 0 ), · · · , Z k = ∨ α ∈ Act E α ( Z k -1 ), · · · . We can verify Z 0 ⊇ Z 1 ⊇ ·· · ⊇ Z k ⊇ ·· · . Let x ′ = ⋂ ∞ k =0 Z k , we have x ′ = ∨ α ∈ Act E α ( x ′ ). Moreover, for any σ 0 /satisfies x , there are infinite many i such that σ i /satisfies p , for any ω sequence σ σ σ 0 1 2 · · · with σ i = E β i ( σ i -1 ) for any β i ∈ Act with σ 1 /satisfies x ′ . By the proof of Lemma 6.5 and Lemma 6.6, x ′ ⊆ x . By defining an increasing sequence V 0 = x , V 1 = ∨ α ∈ Act E -1 α ( V 0 ), · · · , V k = ∨ α ∈ Act E α ( V k -1 ), · · · we have ψ ′ ⊆ ∨ ∞ k =0 V k = ψ .

Therefore ψ = ψ ′ . This implies /square♦ φ is decidable.

## 6.4 Until and Almost Surely Until

According to the results of ♦ . we have

Fact 6.6. For | Act | = 1 , q ∈ AP and φ = ∨ t i =1 p i with p i ∈ AP ,

- · φ U q is decidable if ♦ q is decidable.
- · φ ˜ U q is decidable if ˜ ♦ q is decidable.

Proof. We first verify /square φ . If this is valid, we only need to verify ♦ q or ˜ ♦ q . Otherwise, we find n such that E n ( σ 0 ) /notsatisfies φ , we only need to verify E n ( σ 0 ) /notsatisfies q .

Fact 6.7. For | Act | = 1 , q ∈ AP and φ = ∨ t i =1 p i with p i ∈ AP , /square φ ˜ U q is decidable.

Proof. /square φ ˜ U q iff /square φ and /square♦ ˜ q . The rest follows from Theorem 6.1 and Fact 6.4.

We observe the following, for general | Act | &gt; 1.

Theorem 6.4. /square φ U ψ is decidable for φ = ∨ t i =1 p i and ψ = ∨ s j =1 p j .

Proof. /square φ U ψ iff /square φ and /square♦ ψ . Verification of /square φ and /square♦ ψ follows from Theorem 6.1 and Theorem 6.3.

## 7 Discussion and Conclusion

In this paper, we introduce a quantum temporal logic for quantum concurrent programs. Our quantum temporal logic supports hierarchical specification and reasoning in a simple, natural way. By proving a quantum

B¨ ohm-Jacopini theorem of deterministic quantum concurrent programs, we provide a simple and new insight of quantum programs written in the widely studied Q-While language. We study the decidability of basic QTL formulae and solve the open question in [39].

We are fully aware of the fact that, in this paper, we have only touched upon the topic of quantum temporal logic. There are several important directions for future work. First, it is interesting to further develop the decidability of hierarchical specification in quantum temporal logic. Secondly, we would like to introduce linear-time properties including fairness and liveness into the quantum concurrent program model. A framework for reasoning about the linear-time properties of concurrent unitary program is given in [72].

Thirdly, we expect our quantum temporal logic will be useful in designing quantum computing systems. We believe it is possible because our quantum temporal logic describs a complex quantum system through a hierarchy of levels of abstraction, starting from a high-level specification and ending with implementation in some programming language.

## 8 Acknowledgement

We thank Prof Mingsheng Ying's help discussion on B¨hm-Jacopini theorem o and change the name of functional program. We thank Prof Yaroslav Shitov for telling us the new bound [59].

This work is supported by DE180100156.

## References

- [1] A. J. Abhari, A. Faruque, M. J. Dousti, L. Svec, O. Catu, A. Chakrabati, C.-F. Chiang, S. Vanderwilt, J. Black, F. Chong, M. Martonosi, M. Suchara, K. Brown, M. Pedram, and T. Brun. Scaffold: Quantum programming language. Technical Report TR-934-12, Dept. of Computer Science, Princeton University NJ, 2012.

[2] D. Akatov. The logic of quantum program verification. Master's thesis, Oxford University Computing Laboratory, 2005.

- [3] T. Altenkirch and J. Grattage. A functional quantum programming language. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05) , pages 249-258. IEEE, 2005.

- [4] E. Ardeshir-Larijani, S. J. Gay, and R. Nagarajan. Verification of concurrent quantum protocols by equivalence checking. In Tools and Algorithms for the Construction and Analysis of Systems , pages 500-514, 2014.
- [5] A. Baltag and S. Smets. The logic of quantum programs. In P. Selinger, editor, Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL 2004) , pages 39-56, 2004.
- [6] A. Baltag and S. Smets. Lqp: the dynamic logic of quantum information. Mathematical Structures in Computer Science , 16(3):491-525, 2006.
- [7] P. Baltazar, R. Chadha, and P. Mateus. Quantum computation tree logic - model checking and complete calculus. International Journal of Quantum Information , pages 219-236, 2008.
- [8] P. Baltazar, R. Chadha, P. Mateus, and A. Sernadas. Towards modelchecking quantum security protocols. In 2007 First International Conference on Quantum, Nano, and Micro Technologies (ICQNM'07) , pages 14-14, 2007.
- [9] G. Barthe, J. Hsu, M. Ying, N. Yu, and L. Zhou. Coupling techniques for reasoning about quantum programs. 2019.
- [10] S. Bettelli, T. Calarco, and L. Serafini. Toward an architecture for quantum programming. The European Physical Journal D - Atomic, Molecular, Optical and Plasma Physics , 2003.
- [11] G. Birkhoff and J. Von Neumann. The logic of quantum mechanics. Annals of Mathematics , 37(4):823-843, 1936.
- [12] C. B¨ ohm and G. Jacopini. Flow diagrams, turing machines and languages with only two formation rules. Commun. ACM , 9(5):366-371, 1966.
- [13] O. Brunet and P. Jorrand. Dynamic quantum logic for quantum programs. International Journal of Quantum Information , 2(01):45-54, 2004.
- [14] G. Bruns and J. Harding. Algebraic Aspects of Orthomodular Lattices , pages 37-65. Springer Netherlands, Dordrecht, 2000.

| [15]   | J. Cai. Computing jordan normal forms exactly for commuting matrices in polynomial time. Int. J. Found. Comput. Sci. , 5(3/4):293-302, 1994.                                                                                                                                           |
|--------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| [16]   | R. Chadha, P. Mateus, and A. Sernadas. Reasoning about imperative quantum programs. Electronic Notes in Theoretical Computer Science , 158:19-39, 2006.                                                                                                                                |
| [17]   | U. Dal Lago, C. Faggian, B. Valiron, and A. Yoshimizu. The geom- etry of parallelism: Classical, probabilistic, and quantum effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages , POPL 2017, pages 833-845, New York, NY, USA, 2017. ACM. |
| [18]   | E. D'hondt and P. Panangaden. Quantum weakest preconditions. Math- ematical Structures in Computer Science , 16(3):429-451, 2006.                                                                                                                                                      |
| [19]   | Y. Feng, R. Duan, Z. Ji, and M. Ying. Proof rules for the correctness of quantum programs. Theoretical Computer Science , 386(1-2):151-166, 2007.                                                                                                                                      |
| [20]   | Y. Feng, R. Duan, and M. Ying. Bisimulation for quantum processes. ACM Trans. Program. Lang. Syst. , 34(4):17:1-17:43, 2012.                                                                                                                                                           |
| [21]   | Y. Feng, N. Yu, and M. Ying. Model checking quantum markov chains. Journal of Computer and System Sciences , 79(7):1181 - 1198, 2013.                                                                                                                                                  |
| [22]   | Y. Feng, N. Yu, and M. Ying. Reachability analysis of recursive quan- tum markov chains. In K. Chatterjee and J. Sgall, editors, Mathematical Foundations of Computer Science 2013 , pages 385-396, 2013.                                                                              |
| [23]   | N. Francez. Fairness . Springer, 1986.                                                                                                                                                                                                                                                 |
| [24]   | S. J. Gay. Quantum programming languages: Survey and bibliography. Mathematical Structures in Computer Science , 16(4):581-600, 2006.                                                                                                                                                  |
| [25]   | S. J. Gay, R. Nagarajan, and N. Papanikolaou. Qmc: A model checker for quantum systems. In Computer Aided Verification , pages 543-547, 2008.                                                                                                                                          |
| [26]   | G. Ge. Algorithms Related to Multiplicative Representations . PhD the- sis, University of California, Berkeley, 1993.                                                                                                                                                                  |
| [27]   | Google and Microsoft. Quantum computing course. 2019.                                                                                                                                                                                                                                  |
| [28]   | Google AI Quantum team. 2018.                                                                                                                                                                                                                                                          |

- [29] A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron. Quipper: a scalable quantum programming language. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation , PLDI '13, pages 333-342, New York, NY, USA, 2013. ACM.
- [30] A. Guterman, T. Laffey, O. Markova, and H. Smigoc. A resolution of paz's conjecture in the presence of a nonderogatory matrix. Linear Algebra and its Applications , 543:234 - 250, 2018.
- [31] G. Hansel. A simple proof of the skolem-mahler-lech theorem. Theor. Comput. Sci. , 43(1):91-98, 1986.
- [32] S.-H. Hung, K. Hietala, S. Zhu, M. Ying, M. Hicks, and X. Wu. Quantitative robustness analysis of quantum programs. Proc. ACM Program. Lang. , 3(POPL):31:1-31:29, 2019.
- [33] P. Jorrand and M. Lalire. From quantum physics to programming languages: A process algebraic approach. In Unconventional Programming Paradigms , 2005.
- [34] Y. Kakutani. A logic for formal verification of quantum programs. In A. Datta, editor, Proceedings of the 13th Asian conference on Advances in Computer Science: information Security and Privacy (ASIAN 2009) , pages 79-93, Berlin, Heidelberg, 2009. Springer, Springer Berlin Heidelberg.
- [35] G. Kalmbach. Orthomodular lattices , volume 18. Academic Press, 1983.
- [36] R. M. Keller. Formal verification of parallel programs. Commun. ACM , 19(7):371-384, 1976.
- [37] E. Knill. Conventions for quantum pseudocode, 1996.
- [38] T. J. Laffey. Simultaneous reduction of sets of matrices under similarity. Linear Algebra and its Applications , 84:123 - 138, 1986.
- [39] Y. Li and M. Ying. Debugging quantum processes using monitoring measurements. Physical Review A , 89(4):042338, 2014.
- [40] Y. Li and M. Ying. Algorithmic analysis of termination problems for quantum programs. In Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages , POPL 2018, pages 35:1-35:29, New York, NY, USA, 2017. ACM.

| [41]   | Y. Li, N. Yu, and M. Ying. Termination of nondeterministic quantum programs. Acta Informatica , 51(1):1-24, 2014.                                                                                                                      |
|--------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| [42]   | P. Mateus, J. A. M. Ramos, A. Sernadas, and C. Sernadas. Temporal logicsfor reasoning about quantum systems. Semantic Techniques in Quantum Computation , pages 389-413, 2009.                                                         |
| [43]   | P. Mateus and A. Sernadas. Weakly complete axiomatization of ex- ogenous quantum propositional logic. Information and Computation , 204(5):771 - 794, 2006.                                                                            |
| [44]   | Y. Nengkun, C.-Y. Lai, and L. Zhou. Protocols for packet quantum network intercommunication. arxiv:1903.10685 , 2019.                                                                                                                  |
| [45]   | M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition . Cambridge University Press, New York, NY, USA, 10th edition, 2011.                                                             |
| [46]   | B. ¨ Omer. Structured quantum programming . PhD thesis, Institute for Theoretical Physics, Vienna University of Technology, 2003.                                                                                                      |
| [47]   | S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. , 4(3):455-495, July 1982.                                                                                               |
| [48]   | C. J. Pappacena. An upper bound for the length of a finite-dimensional algebra. Journal of Algebra , 197(2):535 - 545, 1997.                                                                                                           |
| [49]   | J. Paykin, R. Rand, and S. Zdancewic. Qwire: a core language for quan- tum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages , POPL 2017, pages 846-858, New York, NY, USA, 2017. ACM. |
| [50]   | J. Paykin and S. Zdancewic. A hott quantum equational theory, 2019.                                                                                                                                                                    |
| [51]   | A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977) , pages 46-57, Oct 1977.                                                                                            |
| [52]   | A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science , 13(1):45 - 60, 1981.                                                                                                                          |
| [53]   | R. Rand. Verification logics for quantum programs, 2016.                                                                                                                                                                               |
| [54]   | Rigetti Forest team, 2018.                                                                                                                                                                                                             |

| [55]   | A. Sabry. Modeling quantum computing in haskell. In Proceedings of the 2003 ACM SIGPLAN Workshop on Haskell , 2003.                                                                                                                                       |
|--------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| [56]   | J. W. Sanders and P. Zuliani. Quantum programming. In R. Backhouse and J. N. Oliveira, editors, International Conference on Mathematics of Program Construction (MPC 2000) , pages 80-99, Berlin, Heidelberg, 2000. Springer, Springer Berlin Heidelberg. |
| [57]   | P. Selinger. A brief survey of quantum programming languages. In Y. Kameyama and P. J. Stuckey, editors, International Symposium on Functional and Logic Programming (FLOPS 2004) , pages 1-6, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.      |
| [58]   | P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science , 14(4):527-586, 2004.                                                                                                                                   |
| [59]   | Y. Shitov. An improved bound for the length of matrix algebras. Algebra and Number Theory , 2019.                                                                                                                                                         |
| [60]   | S. Staton. Algebraic effects, linearity, and quantum programming lan- guages. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL '15, pages 395-406, New York, NY, USA, 2015. ACM.              |
| [61]   | T. Tao. Open question: effective skolem-mahler-lech the- orem. https://terrytao.wordpress.com/2007/05/25/open-question- effective-skolem-mahler-lech-theorem/ , 2007.                                                                                     |
| [62]   | D. Unruh. Quantum hoare logic with ghost variables. In ACM/IEEE Symposium on Logic in Computer Science , LICS 2019, 2019.                                                                                                                                 |
| [63]   | D. Unruh. Quantum relational hoare logic. In Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages , POPL 2019, New York, NY, USA, 2019. ACM.                                                                              |
| [64]   | J. von Neumann. On infinite direct products. Compositio Mathematica , 6:1-77, 1939.                                                                                                                                                                       |
| [65]   | D. Wecker and K. M. Svore. Liqui |〉 : A software design architecture and domain-specific language for quantum computing. 2014.                                                                                                                           |
| [66]   | M. Ying. Floyd-hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS) , 33(6):19:1-19:49, 2011.                                                                                                                 |

| [67]   | M. Ying. Foundations of Quantum Programming . Morgan Kaufmann, 2016.                                                                                                                                                                                 |
|--------|------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| [68]   | M. Ying, R. Duan, Y. Feng, and Z. Ji. Predicate transformer semantics of quantum programs. Semantic Techniques in Quantum Computation , (8):311-360, 2010.                                                                                           |
| [69]   | M. Ying and Y. Feng. Quantum loop programs. Acta Inf. , 47(4):221- 250, 2010.                                                                                                                                                                        |
| [70]   | M. Ying and Y. Feng. A flowchart language for quantum programming. IEEE Transactions on Software Engineering , 37(4):466-485, 2011.                                                                                                                  |
| [71]   | M. Ying, Y. Feng, R. Duan, and Z. Ji. An algebra of quantum processes. ACM Trans. Comput. Logic , 10(3):19:1-19:36, 2009.                                                                                                                            |
| [72]   | M. Ying, Y. Li, N. Yu, and Y. Feng. Model-checking linear-time proper- ties of quantum systems. ACM Trans. Comput. Logic , 15(3):22:1-22:31, 2014.                                                                                                   |
| [73]   | M. Ying, S. Ying, and X. Wu. Invariants of quantum programs: char- acterisations and generation. In Proceedings of the 44th ACM SIG- PLAN Symposium on Principles of Programming Languages , POPL 2017, pages 818-832, New York, NY, USA, 2017. ACM. |
| [74]   | M. Ying, N. Yu, Y. Feng, and R. Duan. Verification of quantum pro- grams. Science of Computer Programming , 78(9):1679 - 1700, 2013.                                                                                                                 |
| [75]   | S. Ying, Y. Feng, N. Yu, and M. Ying. Reachability probabilities of quantum markov chains. In CONCUR 2013 - Concurrency Theory , pages 334-348, 2013.                                                                                                |
| [76]   | S. Ying and M. Ying. Reachability analysis of quantum markov decision processes. Information and Computation , 263:31 - 51, 2018.                                                                                                                    |
| [77]   | N. Yu and M. Ying. Reachability and termination analysis of concurrent quantum programs. In Proceedings of the 23rd International Conference on Concurrency Theory , CONCUR'12, pages 69-83, 2012.                                                   |
| [78]   | L. Zhou, N. Yu, and M. Ying. An applied quantum hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , PLDI 2019, pages 1149-1162, New York, NY, USA, 2019. ACM.                         |
Nengkun Yu
Quantum Temporal Logic
In this paper, we introduce a model of quantum concurrent program, which can
be used to model the behaviour of reactive quantum systems and to design
quantum compilers. We investigate quantum temporal logic, QTL, for the
specification of quantum concurrent systems by suggesting the time-dependence
of events. QTL employs the projections on subspaces as atomic propositions,
which was established in the Birkhoff and von Neumann's classic treatise on
quantum logic. For deterministic functional quantum program, We prove a quantum
B\"{o}hm-Jacopini theorem which states that any such program is equivalent to a
Q-While program. The decidability of basic QTL formulae for general quantum
concurrent program is studied.