Termination And Reachability Problems Of Quantum Programs

Quantum program is the key concept for designing, implementation of, reason-ing about and verification of quantum computation. As many physical techniques forquantum computation have been implemented and are being commercialized, the im-portance of quantum programs is more and more realized. However, since the physicalbehaviors of quantum systems are quite diferent from that of classical systems, quan-tum programs can not be well developed and investigated in classical program theory.So, a quantum program theory, which is compatible with quantum physics, should beestablished for developing analysis methods and verification techniques for quantumcomputing systems and quantum programs. This dissertation presents the results aboutthis issue obtained by the author during his study toward a PhD degree. By investi-gating the reachability problem of quantum programs, the author builds a systematicframework for studying properties of quantum programs. Specifically,1. The author establishes the basis about quantum programs, including some mod-els of quantum programs and related concepts such as the terminating probability,reachable space, and the set of diverging states.2. The author develops two new analysis techniques for quantum programs: a quan-tum version of0–1law and a descending chain condition of quantum sets. Byemploying both of them, the termination problem for finite dimensional quantumprograms is solved.3. The author investigates the general reachability problem of quantum programs.It is pointed out that the problem is generally undecidable, which is essentially d-iferent from the classical cases where the same problem is completely decidablefor classical programs.4. The author designs schemes and constructs algorithms for verification of quan-tum positive reachability properties, and then obtains decidable results.5. The author proposes a method of debugging quantum processes using quantum measurements, such that bugs of a quantum system may be found and repairedat an acceptable cost in time. The previous reachability checking algorithms areapplied to construction of the debugging protocols.In conclusion, it is demonstrated that the behaviors and properties of quantumprograms are essentially diferent from that of classical programs, and new methodsand techniques are proposed to deal with the problems caused by these diferences. Allof them enrich the emerging theory about quantum programs.