Verification Of Quantum Concurrent Programs With Bisimulations

In this thesis,we verify the correctness of quantum programs,especially for quantum communication protocols,through quantum bisimulation checking.Quantum process algebra is one of the useful techniques to formally verify quantum communication programs.It is based on the classical process algebras and used for the formalisation of quantum programs.By using a quantum process algebra,we can determine if an implementation of a protocol is consistent with its specification with a suitable notion of behavioural equivalence and a corresponding decision method.Ground bisimulation is a convenient behavioural equivalence for quantum processes which we will consider.We use qCCS processes to model quantum programs and protocols.Quantum calculus of communicating system(qCCS)is a general framework proposed by Feng et al.for describing communication and concurrency in complex quantum systems which is a quantum extension of Milner’s classical value-passing CCS.Furthermore,the behaviour of a quantum process can be simply interpreted by a probabilisitic labelled transition system(pLTS)while the equivalence between qCCS models is represented by the bisimulation.It enables us to make use of the classical algorithms of checking probabilistic bisimulations for quantum bisimulation checking.This thesis focuses on the design and the implementation of the checking algorithms for the following three versions of quantum ground bisimulations:-Quantum strong ground bisimulation.The definition of quantum strong ground bisimulation extends the classical strong ground bisimulation,adding constraints on quantum registers and the context of quantum program statements.We design and implement an on-the-fly algorithm for the quantum strong ground bisimulation to check if two given processes in quantum CCS are bisimilar.A lifting operation is introduced to lift the bisimulation between states to distributions of states when matching state distributions.But it also brings the problem that there are more constraints to satisfy when using the lifting operation.The problem is treated as a bipartite matching problem in the implementation of the algorithm,and solved by a max-flow algorithm.-Quantum weak ground bisimulation.The quantum weak ground bisimulation builds on the definition of the quantum strong ground bisimulation,but a weak transition can be used to match a strong transition when checking whether two states are bisimilar.Different from the strong transitions before,a weak transition allows several τ actions to be added before or after the required visible action.As the transition to match is a weak transition,the next state or distribution of states to match might be the combination of all the possible target states or distributions of the weak transition.It brings a new problem.We still design and implement an on-the-fly algorithm for the quantum weak ground bisimulation.The algorithm reduces the problem to a linear programming problem.-Distribution-based quantum ground bisimulation.Different from the state-based quantum ground bisimulations above,the transitions to be matched in the distributionbased quantum ground bisimulation are not from a state to another state or a distribution of states,they are transitions between distributions of states.It is even not the same as the state-based bisimulation after a lifting operation.We develop an on-the-fly algorithm and a checking algorithm using bisimulation matrix.Both of them can only verify quantum programs with some constraints.The former requires all the pLTSs to be finite trees.The latter can check pLTSs which are not trees,however,it can only verify closed quantum systems without external communications.It constructs a matrix to characterize the bisimulation between two systems.The algorithm traverses the distributions in the systems,and checks whether the result of multiplying the difference of distributions with each column of the matrix is 0 in order to verify the bisimulation.We prove termination and correctness of the algorithms,and we also analyze their time complexities.We develop a tool,called QBisim,that can verify interesting quantum protocols.The verifying process is totally automated after inputting required information.We have conducted experiments on several quantum communication protocols,such as the protocols based on the entanglement of quantum states like quantum teleportation protocol,and the quantum key distribution protocols like the BB84 quantum key distribution scheme,and the experimental results show that our tool is useful.