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

doi:10.3969/j.issn.0372-2112.2016.12.017

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

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

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

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-xuan^1,2, PENG Jia-yin^1,2, LIU Yi^1,2

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

摘要/Abstract

摘要：

程序验证是保证程序正确性的关键技术.由于经典世界和量子世界的本质不同，经典程序验证的技术和工具不能直接应用到量子系统.而量子程序设计语言是描述量子系统的一种新的形式化模型，量子程序的验证问题就显得更为迫切和必要.本文首先讨论了量子通讯中常用的比特翻转、相位翻转、去极化、幅值阻尼、相位阻尼等信道作为特殊的非确定型量子程序从计算基态开始运行时的可达集合和终止集合等程序验证问题.其次，把上述五种量子程序两两组合组成非确定型量子程序，根据这五种量子程序的可达集合之相似点，最终合并成三种非确定型量子程序，重点讨论了这三种非确定型量子程序从计算基态开始运行时的终止和发散等程序验证问题.研究表明：这三种非确定型量子程序从计算基态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

中图分类号:

TP301.6

雷红轩, 彭家寅, 刘熠. 几类非确定型量子程序的终止验证[J]. 电子学报, 2016, 44(12): 2932-2938.

LEI Hong-xuan, PENG Jia-yin, LIU Yi. Termination Verification of Some Kinks Nondeterministic Quantum Programs[J]. Acta Electronica Sinica, 2016, 44(12): 2932-2938.

参考文献

[1] P W Shor.Algorithms for quantum computation:discrete logarithms and factoring[A].Proc.35th Annual Symp.on Foundations of Computer Science[C].Los Alamitos,CA:IEEE Press,1994.124-134.
[2] L Grover.A fast quantum mechanical algorithm for database search[A].Proc 28th Annual ACM Symp on the Theory of Computing[C].New York:ACM Press,1996.212-219.
[3] M A Nielsen,I L C'huang.Quantum Computation and Quantum Information[M].Cambridge:Cambridge University Press,2000.
[4] S Abramsky.High-level methods for quantum computation and information[A].Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)[C].USA:IEEE Computer Society,2004.410-414.
[5] E H Knill.Conventions for Quantum Pseudocode[R].USA:Los Alamos National Laboratory,1996.
[6] Bömer.A Procedural Formalism for Quantum Computing[D].Vienna:Department of Theoretical Physics,Technical University of Vienna,1998.
[7] P Selinger.Towards a quantum programming language[J].Mathematics Structures in Computer Science,2004,14(4):527-586.
[8] S J Gay,R Nagarajan.Communicating quantum processes,annual symposium on principles of programming languages[A].Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages[C].USA:Programming Language,2005.145-157.
[9] Y Feng,R Y Duan,M S Ying.Bisimulation for quantum processes[A].Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)[C].New York:ACM Press,2011.523-534.
[10] Y J Li,N K Yu,M S Ying.Termination of nodeterministic quantum programs[J].Acta Informatica,2014,51(1):1-24.
[11] N K Yu,M S Ying.Reachability and termination analysis of concurrent quantum programs[J].Lecture Notes in Computer Science,2012,7454:69-83.
[12] M S Ying,N K Yu,Y Feng,R Y Duan.Verification of quantum programs[J].Sci Comput Program,2013,78(9):1679-1700.
[13] 雷红轩,席政军,李永明.广义量子Loop程序的若干性质[J].电子学报,2013,41(4):727-732. LEI Hong-xuan,XI Zheng-jun,LI Yong-ming.Some properties of genaralized quantum loop program[J].Acta Electronica Sinica,2013,41(4):727-732.(in Chinese)
[14] 雷红轩,席政军,李永明.量子最弱自由前置条件的交换性及其性质[J].软件学报,2013,24(5):933-941. LEI Hong-xuan,XI Zheng-jun,LI Yong-ming.Commutativity of quantum weakest liberal precondition and its properties[J].Journal of Software,2013,24(5):933-941.(in Chinese)
[15] 林运国,雷红轩,李永明.量子马尔可夫链安全性模型检测[J].电子学报,2014,42(11):2191-2197. LIN Yun-guo,LEI Hong-xuan,LI Yong-ming.Model checking of safety property over quantum markov chain[J].Acta Electronica Sinica,2014,42(11):2191-2197.(in Chinese)

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

Termination Verification of Some Kinks Nondeterministic Quantum Programs

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	朱健, 胡凯, 张伯钧. 智能合约的形式化验证方法研究综述[J]. 电子学报, 2021, 49(4): 792-804.
[2]	王继军, 李国祥, 夏国恩, 孙泽锐. 图像插值空间完全可逆可分离密文域信息隐藏算法[J]. 电子学报, 2020, 48(1): 92-100.
[3]	王继军, 孙泽锐, 李国祥. 图像抛物线插值空间大容量可逆信息隐藏算法[J]. 电子学报, 2019, 47(1): 137-144.
[4]	房卫东, 张武雄, 杨旸, 张传雷, 陈伟. 基于生物特征标识的无线传感器网络三因素用户认证协议[J]. 电子学报, 2018, 46(3): 702-713.
[5]	王森, 邱扬, 田锦, 许清琳. 基于视觉效应的视频信息电磁泄漏抑制方法研究[J]. 电子学报, 2017, 45(8): 2038-2043.
[6]	付立仕, 崔霆, 金晨辉. 嵌套SP网络的New-Structure系列结构的零相关线性逼近与不可能差分性质研究[J]. 电子学报, 2017, 45(6): 1367-1374.
[7]	肖玮, 陈性元, 包义保. 可重构信息安全系统研究综述[J]. 电子学报, 2017, 45(5): 1240-1248.
[8]	曹东, 宋耀良. 基于纠缠辅助码的量子模糊承诺和生物认证[J]. 电子学报, 2012, 40(7): 1492-1496.
[9]	朱允敏, 张丽伟, 王生原, 董渊, 张素琴. 面向多核处理器的低级并行程序验证[J]. 电子学报, 2009, 37(S1): 1-6.
[10]	蔡涛, 鞠时光, 仲巍, 牛德姣. 基于切割的检测器生成与匹配算法[J]. 电子学报, 2009, 37(S1): 131-134,86.
[11]	赵险峰;李宁;邓艺. 一种保护芯片设计的多变量加密及其电路结构[J]. 电子学报, 2009, 37(6): 1300-1306.
[12]	赵和平;赵聆波. 一种基于物理噪声源的复合加密算法[J]. 电子学报, 2009, 37(10): 2193-2198.
[13]	杨庚;程宏兵;. 一种有效的无线传感器网络密钥协商方案[J]. 电子学报, 2008, 36(7): 1389-1395.
[14]	邱扬;魏丽丽;田锦;陈光达;钱柳宇. 基于数字滤波的计算机视频信息防泄漏研究[J]. 电子学报, 2008, 36(6): 1188-1192.
[15]	章文辉;杜百川;杨盈昀. 模糊层次分析法在广播电视信息安全保障评价指标体系中的应用研究[J]. 电子学报, 2008, 36(10): 2060-2064.