电子学报 ›› 2016, Vol. 44 ›› Issue (12): 2932-2938.DOI: 10.3969/j.issn.0372-2112.2016.12.017

• 学术论文 • 上一篇    下一篇

几类非确定型量子程序的终止验证

雷红轩1,2, 彭家寅1,2, 刘熠1,2   

  1. 1. 内江师范学院数学与信息科学学院, 四川内江 641112;
    2. 四川省高等学校数值仿真重点实验室, 四川内江 641112
  • 收稿日期:2015-07-06 修回日期:2015-11-06 出版日期:2016-12-25
    • 作者简介:
    • 雷红轩,男,1967年出生于陕西洋县,博士,教授,主要研究领域为自动机理论,量子程序验证和量子模型检测.E-mail:hongxuan_lei@163.com;彭家寅,男,1962出生于四川资中县,博士,教授,主要研究领域为量子信息处理.E-mail:pengjiayin62226@163.com;刘熠,男,1979年出生于四川仪陇县,博士,副教授,主要研究领域为智能信息处理.E-mail:liuyiyl@126.com
    • 基金资助:
    • 四川省教育厅重点科研项目 (No.14ZA0242); 教育部数学与应用数学专业综合改革 (No.ZG0464); 四川省数学与应用数学专业综合改革 (No.01249); 四川省教育厅科研创新团队基金 (No.15TD0027); 四川省应用基础研究计划 (No.2015JY0120)

Termination Verification of Some Kinks Nondeterministic Quantum Programs

LEI Hong-xuan1,2, PENG Jia-yin1,2, LIU Yi1,2   

  1. 1. School of Mathematics and Information Science of Neijiang Normal University, Neijiang, Sichuan 641112, China;
    2. Key Laboratory of Numerical Simulation of Sichuan Province, Neijiang, Sichuan 641112, China
  • Received:2015-07-06 Revised:2015-11-06 Online:2016-12-25 Published:2016-12-25

摘要:

程序验证是保证程序正确性的关键技术.由于经典世界和量子世界的本质不同,经典程序验证的技术和工具不能直接应用到量子系统.而量子程序设计语言是描述量子系统的一种新的形式化模型,量子程序的验证问题就显得更为迫切和必要.本文首先讨论了量子通讯中常用的比特翻转、相位翻转、去极化、幅值阻尼、相位阻尼等信道作为特殊的非确定型量子程序从计算基态开始运行时的可达集合和终止集合等程序验证问题.其次,把上述五种量子程序两两组合组成非确定型量子程序,根据这五种量子程序的可达集合之相似点,最终合并成三种非确定型量子程序,重点讨论了这三种非确定型量子程序从计算基态开始运行时的终止和发散等程序验证问题.研究表明:这三种非确定型量子程序从计算基态0开始运行时都是终止的;而从计算基态1开始运行时:比特翻转信道和去极化信道组成的非确定型量子程序的终止和发散与分别刻画它们的两个参数有关;比特翻转信道和相位翻转信道组成的非确定型量子程序的终止和发散只与刻画比特翻转信道的参数有关;幅值阻尼信道和相位阻尼信道组成的非确定型量子程序是发散的,其发散条件与刻画量子信道的两个参数都没有关系.本文的结果可以为量子信息安全中量子通讯协议的验证提供理论和技术支持.

关键词: 量子通讯, 量子程序, 程序验证, 信息安全

Abstract:

Program verification is the key technology to ensure the correctness of the program.However,due to essential differences of the classical and quantum world,classical program verification techniques and tools cannot be applied directly to the quantum system.Since quantum programming language is a new formal model of quantum system,the verification problem of quantum program is more urgent and necessary.We investigate the program verification for the reachable set and the terminating set of specific nondeterministic quantum program described respectively by bit flip channel,phase flip channel,depolarizing channel,amplitude damping channel and phase damping channel starting from computational basic states in quantum communication systems.Then,we combine pairwise the above five quantum programs into nondeterministic quantum programs,and merge these nondeterministic quantum programs into three nondeterministic quantum programs in terms of the similarities of the reachable set of five quantum programs,and discuss the problem for termination and divergence of these three nondeterministic quantum programs starting from computational basic states.The results shows that these three nondeterministic quantum programs starting from computational basic state 0 are terminated,while starting from computational basic state 1,the termination and the divergence of nondeterministic quantum program consisted by bit flip channel and depolarizing channel relates to the two parameters describing two quantum channels,the termination and the divergence of nondeterministic quantum program consisted by bit flip channel and phase flip channel relates to one parameter describing bit flip channel,and nondeterministic quantum program consisted by amplitude damping channel and phase damping channel is divergence without the two parameters describing quantum channel.And the results provide theoretical and technical support for verification of quantum communication protocol in quantum information security.

Key words: quantum communication, quantum programs, program verification, information security

中图分类号: