题目：           Algorithmic Analysis of Termination Problems for Quantum Programs

报告人：     李杨佳  (中国科学院软件所)

时间地点：   2018.01.26  08:45am  N202

摘要：           We introduce the notion of linear ranking super-martingale (LRSM) for quantum programs (with nondeterministic choices, namely 

                       angelic and demonic choices). Several termination theorems are established showing that the existence of the LRSMs of a quantum 

                      program implies its termination. Thus, the termination problems of quantum programs is reduced to realisability and synthesis of 

                      LRSMs. We further show that the realisability and synthesis problem of LRSMs for quantum programs can be reduced to an SDP 

                      (Semi-Definite Programming) problem, which can be settled with the existing SDP solvers. The techniques developed in this paper 

                     are used to analyse the termination of several example quantum programs, including quantum random walks and quantum Bernoulli 

                     factory for random number generation. This work is essentially a generalization of constraint-based approach to the corresponding 

                     problems for probabilistic programs developed in the recent literature by adding two novel ideas: (1) employing the fundamental 

                     Gleason’s theorem in quantum mechanics to guide the choices of templates; and (2) a generalized Farkas’ lemma in terms of 

                     observables (Hermitian operators) in quantum physics.