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

项目名称： 基于量子马尔可夫链的模型检测理论的研究

项目编号： No.61472412

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 尚云

作者单位： 中国科学院数学与系统科学研究院

项目金额： 87万元

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

中文关键词： 量子马尔可夫链；模型检测；量子计算树逻辑；量子逻辑

英文摘要： 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.

英文关键词： quantum markov chains;model checking;quantum computation tree logic;quantum logic