Research On Several Problems In Open Quantum System Model Detection

With the development of quantum computation,quantum information and quantum physics technology,the formal verification methods for quantum systems have become increasingly prominent.Because of physical interference and system complexity,it is in-eluctable in designing and implementing quantum systems with a large numbers of faults and errors.Therefore,it is vitally important to verify the correctness,safety and sound-ness of quantum systems.The theories of the formal verification are important to solve these problems,which are applied to verify the safety property of quantum communica-tion and the correctness of quantum program.Regardless of quantum analog computing or quantum parallel computing,they ex-ploit quantum coherence.However,real quantum systems are open rather than the iso-lated systems.They could interact with the external environment,which lead to quantum coherence difficult to be kept and the decreased quantum coherence.Namely,that is called be decoherence.In contrast with closed quantum systems,it is more necessity to do some research about the formal verification for open quantum systems.The formal verification includes three types,namely,equivalence checking,model checking and theorem proving.And,model checking is one of the most successful formal verification methods,which has been widely concerned and broadly used in academia and industry.Because of the fundamental difference between quantum systems and classical systems,the techniques of formal verification for classical systems could not be directly extended to quantum systems.Hence,model checking for quantum systems is difficult and challengeable.The research of this thesis is mainly about model checking for open quantum sys-tems.The purpose of this thesis is:(1)to build a logical language for open quantum sys-tems;(2)to define quantum transition systems and to check quantum linear time proper-ties;(3)to check quantum Markov chains and(4)to verify the termination of generalized quantum Loop programs.The main contributions in this thesis are listed as follows:(1)In Chapter 3,we build a logical language to describe open quantum systems with respect to syntax and semantic,which is called by quantum operator logic.As an axiom system,we prove that quantum operator logic is sound and complete.And for a satisfiability system,we discuss the satisfiability problem of quantum operator logic.We show that there exists a finite model for the satisfiability problem of any formula.Given a model structure,we present a checking algorithm for the satisfiability of a formula.Finally,we present two illustrations to describe the entanglement property of the Bell state and reason the safety property of BB84 protocols.(2)In Chapter 4,based on quantum operator logic,we give a definition of open quantum transition system which could be used to describe the evolution of quantum sys-tems.Since a quantum system has infinite quantum states,then there are great difficulties to propose an efficient searching algorithm.In order to solve this problem,we propose a kind of finite and abstract quantum states.We also introduce a kind of quantum linear time properties including quantum safety properties,quantum invariant properties,quan-tum liveness properties and quantum persistence properties.We present an algorithm for checking quantum invariant properties of quantum transition systems.Based on finite au-tomata,we propose a checking technique for quantum regular safety properties.With this checking technique,we verify the reachability of target vertex for open quantum walk.(3)In Chapter 5,based on quantum operator logic,we introduce a novel kind of quantum Markov chains,define quantum linear time properties and analyze the reach-ability problem of quantum Markov chains.Considering the measurement-once and measurement-many cases,we present a checking technique of quantum regular safety properties based on quantum finite automata.(4)In Chapter 6,we develop a mathematical model of generalized quantum Loop programs based on quantum Markov chains.Through introducing the nth termination with a specified probability and terminability,we resolve the problems of what their ex-pressive power is not sufficient regarding the existing terminations of generalized quan-tum Loop programs.After analyzing the reduction of the termination problems and the reachability of the ending states,we present a verification technique of the program termi-nations.For single-qubit quantum systems,multi-qubits quantum systems,compounding quantum systems and nesting quantum systems,we propose the explicit formulas for computing the termination probabilities and the ending states of generalized quantum Loop programs.Finally,we conclude several sufficient and necessary conditions of the terminations for generalized quantum Loop programs.