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

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.

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

在本项目的资助下，发表论文35篇，SCI收录33篇，培养研究生13余名(含3名博士生），并获后续国家自然科学基金、省自然科学基金、市科技计划项目各1项。取得的主要代表性工作如下：1.提出半量子自动机的一般性模型，首次揭示几个重要半量子自动机模型之间的关系，提出并解决半量子系统的模型检测问题，相关成果发表在Information and Computation，Theoretical Computer Science ，Journal of Computer and System Sciences等国际期刊；2.在量子信息的区分、中继等基础问题做了较深入的研究，特别是证明了对于作用了任意二体系统上的两个酉变换，都存在串行方案可以以LOCC方案区分，并且区分过程中不需要用到酉变换的逆。以上成果大大提供了酉变换LOCC区分在物理实验上的可行性，成果发表在Physical Review A。3.在量子密码与量子博弈方面取得了一些新进展，特别是在三种贝尔不等式的基础上构造出三个新的利益冲突贝叶斯博弈，博弈者使用量子建议可得到比经典建议更高的收益。其中一个博弈的输出有三种取值，因此回答了文献【Phys. Rev. Lett. 114, 020401, 2015】提出的能否使用高维量子态提高利益冲突贝叶斯博弈收益的问题。相关研究成果发表在Quantum Informantion and Computation, Quantum Information Processing, International Journal of Quantum Information等国际期刊。除了研究计划中有关“建立合适的经典-量子协同下推自动机模型，使其符合当前量子程序设计的实际情况”的目标还未有较成熟的结果之外，其他计划研究内容均涉及到。总的来说，本项目的研究基本达到预期目标。