A Decidable Dynamic Logic for Quantum Reasoning

A Decidable Dynamic Logic for Quantum Reasoning J. M. Bergfeld∗

A. Baltag

K. Kishida∗

S. J. L. Smets∗

S. Zhong†

Institute for Logic, Language and Computation, Universiteit van Amsterdam Science Park 904, 1098XH Amsterdam, The Netherlands.

1

Introduction

It is well-known that Propositional Dynamic Logic (PDL), and its important fragment known as the Hoare Logic, are among the main logical formalisms used in automated program verification of classical programs (based on formal checking of the correctness of a given classical program). It is thus a natural idea to look for quantum analogues of these logics, that could play a similar role in the automated verification of quantum programs. The search for such a “Quantum Propositional Dynamic Logic” has been one of the main objectives of previous investigations by two of the authors (Baltag and Smets) into the logic of quantum information flow. In a series of papers [1, 3, 2, 4, 5, 6, 7], these authors proposed several logical systems: in [1] they focused on single systems1 and presented two equivalent complete axiomatizations for a Logic of Quantum Actions (LQA, allowing actions such as measurements and unitary evolutions, but no entanglements). The completeness result was obtained with respect to infinite-dimensional classical Hilbert spaces, as models for single quantum systems. The challenge of providing a similar axiomatization for compound systems was taken up in [3], where a proposal for a dynamic logic LQP of multi-partite quantum systems was sketched, and applications to Teleportation and other quantum-computational notions were provided. Further developments and elaborations were presented in [2, 4, 5, 6, 7]. But, unlike the case of infinite-dimensional single systems, for which a complete logic was given in [1], the problem of finding a complete proof system for the logic LQP of compound quantum systems is still open. Even more so, the harder problem of whether this logic is decidable or not has been until now a long-standing open question. However, the results and methods in this paper imply a positive answer to this question. In this short paper, we introduce a new variant of the logic LQP introduced in [3], itself a multi-partite extension of the dynamic quantum logic introduced in [1]. Our new variant, called Quantum PDL, is shown to be expressive enough, not only to encode useful states and properties such as entanglement, Bell states, GHZ states, various quantum gates, but also to formally prove the correctness of the Teleportation protocol. (And in fact, this logic can be used to formally verify a number of other standard quantum protocols, such as Super-dense Coding, Logic-Gate Teleportation, Entanglement Swapping, Quantum Secret Sharing etc.) Moreover, it does this in a way that is simpler, more natural and direct (and closer ∗ The

research of these authors has been funded by VIDI grant 639.072.904 of NWO. Zhong’s research has been funded by China Scholarship Council. 1 A single system is just an isolated physical system; the possible states of such a system are represented in Quantum Mechanics as rays in some Hilbert space. In contrast, a composite (also called compound, or multi-partite) system is one that we can think of as being composed of two (or more) distinct physical (sub)systems. The corresponding Hilbert space is the tensor product of each of the spaces associated to the subsystems. † Shengyang

To appear in EPTCS.

2

Decidable Logic for Quantum Reasoning

to the usual way of reasoning in Quantum Computation) than the way in which the old LQP was dealing with this problem. The new logic we propose, Quantum PDL, essentially differs from LQP in two ways. First, all the formulas and program expressions are typed, the type index indicating the qubits involved in the formula or program; e.g. a formula of type {1, 3, 4} denotes a property of qubits 1, 3 and 4 (where we assume as given a countable set of qubits indexed by natural numbers), i.e. a subset of the Hilbert space H1 ⊗ H3 ⊗ H4 (where H = H ⊗ H is the 2-dimensional Hilbert space describing one qubit); while a program expression of type {1, 3, 4} → {1, 2, 3} denotes a quantum “action” that changes a system composed of qubits 1, 3, 4 into a system composed of qubits 1, 2, 3, (i.e. a linear map from H1 ⊗H3 ⊗H4 to H1 ⊗ H2 ⊗ H3 ). The second difference (made possible by the first) is that explicit tensor operators are added to the syntax, both on the side of propositional formulas and on the side of program expressions. They capture the usual quantum-theoretic way to combine properties of two subsystems (or actions on the two subsystems) to produce a property of the global multi-partite system (or an action on this multi-partite system). There are other differences, but these are minor: we consider “quantum tests” (i.e. Hilbert-space projectors, encoding quantum measurements) only for atomic properties. In fact, we impose this restriction just to make our decidability proof easier and more transparent (though the result surely holds without the restriction!). As a result of this limitation, one of the operators that was definable via dynamic modalities in LQP (the  operator, quantifying over measurements) is no longer definable in this way; hence, we just add it to the syntax as a primitive operator. Finally, our main result in this paper is that (the new variant of) Quantum PDL is decidable, by generalizing and extending the method used in [8]: namely, we show that this logic is translatable into the first-order logic of complex numbers (with addition and multiplication), whose decidability follows from a classical result by Tarski [12]. We regard this result as potentially very important for the theory of quantum computation. Decidability of this logic obviously implies the decidability of the correctness problem for all quantum programs that can be expressed in this logic. In unpublished and on-going work (summarized in the Conclusions section), we extend this result further, to even more powerful quantum-dynamic logics, able to express much more complex properties of quantum states and quantum programs, and also to capture much more sophisticated types of quantum computation, such as probabilistic quantum protocols.

2

Preliminary

We fix a set of countably many qubits, indexed by natural numbers i ∈ ω, as the domain of our discourse. Following the common practise in quantum computation and quantum information, we are only interested in quantum systems built with finitely many of these qubits. We write [ω]