经典-量子协同计算：形式化模型、计算复杂性与模型检测

项目名称： 经典-量子协同计算：形式化模型、计算复杂性与模型检测

项目编号： No.61472452

项目类型： 面上项目

立项/批准年度： 2015

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

项目作者： 李绿周

作者单位： 中山大学

项目金额： 83万元

中文摘要： 由于量子资源是昂贵的、不易物理实现，因此研究那些能融合经典和量子资源,并且计算能力上依然大大超越经典计算系统的经典-量子协同计算系统是很有意义的。该类系统含有一个经典部件和一个小规模的量子部件，两者之间可以相互通信、协同工作。本项目首先研究该类系统的形式化模型，特别是要建立一个合适的经典-量子协同下推自动机模型，使之能刻画当前量子程序是量子数据加经典控制这一背景下的递归量子程序。进一步，我们讨论该类系统的计算复杂性问题，包括状态复杂性和交互式证明系统相关问题，这对深入认识该类系统的计算能力是很有必要的。最后，我们建立模型检测的理论与方法，对该类系统的正确性、可靠性、安全性等进行验证。注意到，由于经典系统与量子系统的本质差异，经典模型检测领域的方法已不再适用。通过本项目的研究，有望解决有关经典-量子协同计算系统的若干基本问题，达到对其全面而深入的认识，为进一步的应用奠定基础。

中文关键词： 量子计算；量子自动机；量子模型检测

英文摘要： Since quantum resources are very expensive and are hard to be physically implemented, it is of both theoretical and practical importance to study classical-quantum collaborative computing systems that consist of a classical component and a relatively small quantum component, with communication allowed between them. First, we study the formal models of such systems; specially, we aim to build an appropriate model of classical-quantum collaborative pushdown automata, such that it can characterize the recurrent quantum programs under the background of quantum programs consist of quantum data and classical control flows''. Second, we discuss the computational complexity of these systems, including the state complexity and the related problems on interactive proof systems, which is necessary for deeply understanding the computational power of such systems. Finally, in order to verify the safety, reliability, security and so on of such systems, we try to develop some methods for model-checking such systems. Note that due to the essential differences between classical and quantum systems, the methods for model-checking classical systems no longer work for the systems here. This project will achieve a deep and systemic insight into the classical-quantum collaborative computing systems, laying a solid foundation for their further applications.

英文关键词： quantum computing;quantum automata;quantum model checking