小规模量子混成系统的验证

项目名称： 小规模量子混成系统的验证

项目编号： No.61502467

项目类型： 青年科学基金项目

立项/批准年度： 2016

项目学科： 计算机科学学科

项目作者： 李杨佳

作者单位： 中国科学院软件研究所

项目金额： 20万元

中文摘要： 量子验证是实现量子计算机的重要辅助手段，对于保证量子系统的可靠性和有效性有着至关重要的作用。本项目结合当前量子计算系统的主要特征，重点研究小规模量子混成系统（SQHS）的验证问题，力图建立起解决这一问题的理论框架，并开发出相关验证技术。项目首先基于状态迁移机的概念以及Birkhoff-von Neumann量子逻辑，给出SQHS及其动态性质的形式化描述。接着对系统的可达性问题进行研究，利用问题归约以及降链条件等数学技巧，分别获得不可判定情形与可判定情形的条件。通过对可达性的判定算法进行扩展与优化，进一步得到验证SQHS安全性、活跃性等关键时序性质的有效算法。项目最后将这些结果应用于真实的量子物理系统进行实验和分析，可以得到系统正确性、可靠性等方面的评价，从而能够实现辅助量子系统设计与开发的自动化工具。

中文关键词： 量子程序；量子验证；可达性分析；量子逻辑；算法分析

英文摘要： Quantum verification is an important assisting method for implementation of quantum computers, and is essential to guarantee reliability and effectiveness of quantum systems. In this project, we study the verification problem for Small-scale Quantum Hybrid Systems (SQHS), as most existing quantum computing systems are of this type. We attempt to build the theoretical framework of the problem solving, and to develop corresponding verification techniques. Specifically, we first propose the formal description of SQHS and their dynamical properties, based on the concept of state transition automata and Birkhoff-von Neumann quantum logic. Then we investigate the reachability problem of the systems to obtain the conditions of undecidable results and decidable results, by problems reduction and other mathematical techniques such as descending chain conditions, respectively. Furthermore, we find efficient algorithms to check important temporal properties such as safety and liveness properties, by optimizing and generalizing the reachability checking algorithms. These results will be applied to practical quantum physical systems for experiments and analysis, in order to assess correctness and reliability of the systems, and thus we can implement automatic assisting tools for designing and developing quantum systems.

英文关键词： quantum program;quantum verification;reachability analysis;quantum logic;algorithm analysis