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

• 作者: 刘熠 彭家寅 雷红轩
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 量子通讯 量子程序 程序验证 信息安全
• 年，卷（期）: 2016,（12）
• 所属期刊栏目: 学术论文
• 页码范围: 2932-2938
• 页数: 7页
• 分类号: TP301.6
• 字数: 7266字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2016.12.017

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘熠	内江师范学院数学与信息科学学院	27	88	5.0	8.0
3	雷红轩	内江师范学院数学与信息科学学院	22	103	7.0	9.0
7	彭家寅	内江师范学院数学与信息科学学院	17	85	7.0	8.0