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

发布时间：2017-10-05 23:18

本文关键词：几类非确定型量子程序的终止验证

【摘要】：程序验证是保证程序正确性的关键技术.由于经典世界和量子世界的本质不同,经典程序验证的技术和工具不能直接应用到量子系统.而量子程序设计语言是描述量子系统的一种新的形式化模型,量子程序的验证问题就显得更为迫切和必要.本文首先讨论了量子通讯中常用的比特翻转、相位翻转、去极化、幅值阻尼、相位阻尼等信道作为特殊的非确定型量子程序从计算基态开始运行时的可达集合和终止集合等程序验证问题.其次,把上述五种量子程序两两组合组成非确定型量子程序,根据这五种量子程序的可达集合之相似点,最终合并成三种非确定型量子程序,重点讨论了这三种非确定型量子程序从计算基态开始运行时的终止和发散等程序验证问题.研究表明:这三种非确定型量子程序从计算基态0开始运行时都是终止的;而从计算基态1开始运行时:比特翻转信道和去极化信道组成的非确定型量子程序的终止和发散与分别刻画它们的两个参数有关;比特翻转信道和相位翻转信道组成的非确定型量子程序的终止和发散只与刻画比特翻转信道的参数有关;幅值阻尼信道和相位阻尼信道组成的非确定型量子程序是发散的,其发散条件与刻画量子信道的两个参数都没有关系.本文的结果可以为量子信息安全中量子通讯协议的验证提供理论和技术支持.
【作者单位】：内江师范学院数学与信息科学学院;四川省高等学校数值仿真重点实验室;
【关键词】： 量子通讯 量子程序 程序验证 信息安全
【基金】：四川省教育厅重点科研项目(No.14ZA0242);四川省教育厅科研创新团队基金(No.15TD0027) 教育部数学与应用数学专业综合改革(No.ZG0464) 四川省数学与应用数学专业综合改革(No.01249) 四川省应用基础研究计划(No.2015JY0120)
【分类号】：TP311.1
【正文快照】： 1引言Shor[1]关于大数的质因子分解算法以及Grover[2]关于数据库搜索算法的相继出现,显示出量子计算在某些计算领域比经典计算更有效[3].当前,量子算法还处在较低水平的量子线路的探索阶段.正如Abram-sky[4]所说的,高水平的概念化的方法对量子系统的设计、编程、推理是很必要

【相似文献】

中国期刊全文数据库前5条

1 王拥兵;张丽霞;雷红轩;;基于量子逻辑的确定型正则文法[J];计算机工程与科学;2013年09期

2 Paul Bourret;Patrice Cros;邵维忠;;一个确定型的操作系统模型[J];计算机科学;1981年05期

3 许道云;王晓峰;;一个可控制变迁系统模型[J];广西师范大学学报(自然科学版);2011年02期

4 李平;李永明;;伪加权转换器的极小确定实现化[J];陕西师范大学学报(自然科学版);2011年06期

5 ;[J];;年期

中国重要报纸全文数据库前1条

1 ;经营管理（35）[N];中国电力报;2000年

中国硕士学位论文全文数据库前2条

1 张文华;确定型和不确定型的施工成本管理研究[D];山东大学;2010年

2 李莹;大众购书行为及其模型研究[D];同济大学;2008年