基于量子马尔可夫链的模型检测理论的研究

In order to ensure that the correctness and safety of quantum cryptography protocols,quantum communication systems and other quantum engineering systems, it is necessary to set up the model checking theory and technology for general quantum engineering systems. However, the research in this field has just begun. Based on quantum markov chains, this project mainly aims to set up quantum model checking theory and technologies. Combining postulates of quantum mechanics with traditional quantum logics and probabilistic model checking framework, by use of formal methods, we define quantum markov chains and quantum computation tree logic, and then set up theory of model checking based on quantum markov chains. The following topics will be studied. (1) For closed quantum systems, choosing pure states of Hilber space as basic states, unitary evolution and projector valued measurement as main actions, we set up quantum markov chains and quantum computation tree logic; (2) For open quantum systems, choosing mixed states of Hilbert space as basic states, super operator evolution and positive operator valued measurement as main actions, we set up markov chains and quantum computation logic; (3) We develop quantum model checking algorithms and analyze its complexity;(4) We design automatic verification tools, and further verify typical quantum cryptography protocolas and other quantum engineering systems. This project can not only provide theory and techniques in designing and verifying quantum hardware systems, software systems and quantum communication protocols, but also promote the development of traditional quantum logic.

为保证实际量子密码协议和量子工程系统的正确性与安全性，有必要建立适合一般量子系统的模型检测理论。然而，这方面的研究刚刚起步。本项目从封闭或开量子系统的动力学特征与量子测量特点出发，借鉴经典和概率模型检测框架，结合传统量子逻辑，建立以量子马尔可夫链为系统模型、以量子计算树逻辑为推理基础的量子模型检测理论。主要包括：(1)对于封闭量子系统，以纯态为基本状态，以酉演化、投影值测量为主要行为，建立量子马尔可夫模型与反映上述行为的量子计算树逻辑；(2)对于开量子系统，以混合态为基本状态，以超算子演化、正算子值测量为主要行为，建立量子马尔可夫链模型与量子计算树逻辑；(3)提出量子模型检测算法并分析复杂度；(4)建立自动验证工具，验证相关量子工程系统、量子密码协议的正确性。本项目的研究不仅能够为量子计算机软硬件设计、量子通讯协议的正确性与可靠性验证提供理论基础，而且能够推动传统量子逻辑的研究与发展。

量子游走是经典随机游走的量子推广，它是量子马尔可夫链的基本模型，它在设计某些量子算法中比经典算法可以达到指数加速，另外它也是一个通用的量子计算模型，它在量子通讯中也起着重要的作用。本项目主要研究了多硬币量子游走的性质特点，以及在量子通讯协议的应用，进而讨论他们在设计量子算法中的优缺点；研究了封闭量子系统和开量子系统中量子测量算子及测量基的优化问题，彼此无偏问题，进而讨论了他们在量子状态重构中应用；研究了基于传统von Neumann量子逻辑的图灵机的可计算性问题,发现它们超出了经典图灵机和模糊图灵机的计算能力；在上述研究分析的基础上，定义了新型量子马尔可夫链模型,建立了基于此的量子计算树逻辑，给出了基于量子进程代数的量子模型检测的一套理论框架；最后，作为扩展，本项目还研究了纠缠在量子态的分配问题，进而为纠缠如何引进到量子逻辑，量子计算树逻辑中打下了基础。