量子马尔可夫链安全性模型检测

doi:10.3969/j.issn.0372-2112.2014.11.010

电子学报 ›› 2014, Vol. 42 ›› Issue (11): 2191-2197.DOI: 10.3969/j.issn.0372-2112.2014.11.010

量子马尔可夫链安全性模型检测

林运国^1,2, 雷红轩³, 李永明¹

1. 陕西师范大学计算机科学学院, 陕西西安 710119;
2. 福建农林大学计算机与信息学院, 福建福州 350002;
3. 内江师范学院数学与信息科学学院, 四川内江 641112

收稿日期:2014-01-06 修回日期:2014-05-08 出版日期:2014-11-25
- 作者简介:
- 林运国 男,1979年出生于福建福清,博士研究生,讲师,主要研究领域为量子程序验证和量子模型检测. E-mail:fjaulyg@126.com;雷红轩 男,1967年出生于陕西洋县,博士,教授,主要研究领域为量子程序验证和量子模型检测.;李永明 男,1966年出生于陕西大荔,博士,教授,博士生导师,研究方向为计算智能、量子逻辑、量子计算、模型检测.
- 基金资助:
- 国家自然科学基金 (No.11271237,No.61228305); 高等学校博士学科点专项科研基金 (No.20130202110001,No.20130202120002); 中央高校基本科研业务费专项资金 (No.GK201302054)

Model Checking of Safety Property over Quantum Markov Chain

LIN Yun-guo^1,2, LEI Hong-xuan³, LI Yong-ming¹

1. School of Computer Science, Shaanxi Normal University, Xi'an, Shaanxi 710119, China;
2. College of Computer and Information Sciences, Fujian Agriculture and Forestry University, Fuzhou, Fujian 350002, China;
3. School of Mathematics and Information Science, Neijiang Normal University, Neijiang, Sichuan 641112, China

Received:2014-01-06 Revised:2014-05-08 Online:2014-11-25 Published:2014-11-25
- Supported by:
- National Natural Science Foundation of China (No.11271237, No.61228305); Research Fund for the Doctoral Program of Higher Education of China (No.20130202110001, No.20130202120002); Fundamental Research Funds for the Central Universities (No.GK201302054)

摘要/Abstract

摘要：

本文定义了量子线性时间属性,包括量子安全性,量子不变性,讨论了它们的关系和性质.结合测量一次、测量多次的单向量子有穷自动机,构建了两类乘积量子马尔可夫链,提出了基于自动机技术的量子正则安全性检测方法.通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性,并给出了可满足性的概率计算公式.作为应用,分析了广义量子loop程序,将程序终止归结为验证量子正则安全性的可满足性.

关键词: 量子马尔可夫链, 模型检测, 安全性, 量子有穷自动机, 广义量子loop程序

Abstract:

Quantum linear time property is defined,including quantum safety property,quantum invariant which their relationships and properties are studied.Together with measure-one and measure many one way quantum finite automata,two kinds of the product quantum markov chains are constructed,the checking method of quantum regular propertyis provided based on automaton technique.This method shows the satisfaction of quantum regular safety is decided by the reachable termination verification of the product quantum markov chain,and thecomputation formula of satisfaction probability is given.As an application example,the generalized quantum loop program is analyzed.It shows the termination of program is turned into the satisfaction for the verification of quantum regular safety property.

Key words: quantum Markov chain, model checking, safety property, quantum finite automata, generalized quantum loop program

中图分类号:

TP301.6

林运国, 雷红轩, 李永明. 量子马尔可夫链安全性模型检测[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.

参考文献

[1] C Baier,J P Katoen.Principles of Model Checking[M].Cambridge,Massachusetts:MIT Press,2008.
[2] Papanikolaou,Nikolaos K.Model checking quantum protocols[D].Coventry,England:the War wick University,2009.
[3] E Ardeshir Larijani,S J Gay,R Nagarajan.Equivalence checking of quantum protocols[A].Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[C].Heidelberg:Springer,2013,7795:466-480.
[4] T Davidson,S J Gay,H Mlnarik,R Nagarajan,N.Papanikolaou.Model checking forcommunicating quantum processes[J].International Journal of Unconventional Computing,2012,8(1):73-98.
[5] P Baltazar,R Chadha,P Mateus.Quantum computation tree logic model checking andcomplete calculus[J].International Journal of Quantum Information,2008,6(2):281-302.
[6] M S Ying,Y J Li,N K Yu,Y Feng.Model checking linear time properties of quan tum systems[DB/OL].http://arXiv.org/abs/Quant-ph/arXiv:1101.0303,2010.
[7] 雷红轩,席政军,李永明.量子最弱自由前置条件的交换性及其性质[J].软件学报,2013,24(5):933-941. H X Lei,Z J Xi,Y M Li.Commutativity of quantum weakest liberal precondition and its properties[J].Journal of Software,2013,24(5):933-941.(in Chinese)
[8] Jaroslav Novotny,Gernot Alber,Igor Jex.Asymptotic properties of quantum mark ovchains[DB/OL].http://arXiv.org/math-ph/arXiv:1208.0764,2012.
[9] Stan Gudder.Quantum markov chains.Journal of Mathematical Physics[J].2008,49(7):072105.
[10] Andris Ambainis.Quantum walks and their algorithmic applications[DB/OL].http://arXiv.org/quant-ph/arXiv:0403120v3,2006.
[11] Y Feng,N K Yu,M S Ying.Model checking quantum markov chains[DB/OL].http://arXiv.org/abs /Quant-ph/arXiv:1205.2187,2012.
[12] S G Ying,Y Feng,N K Yu,M S Ying.Reachability probabilities of quantum markovchains[DB/OL].http://arXiv.org/abs/Quant-ph/arXiv:1304.0060,2013.
[13] M A Nielsen,Chuang I L.Quantum computation and quantum Information[M].Cambridge:Canbridge University Press,2000.
[14] 李永明.基于量子逻辑的有穷自动机与单体二阶量子逻辑[J].中国科学F辑:信息科学,2009,39(11):1135-1145. Y M Li.Finite automata based on quantum logic and monadic second-order quantum logic[J].Science China Information Sciences,2009,39(11):1135-1145.(in Chinese)
[15] Ambainis,M Beaudry,M Golovkins,et al.Algebraic results on quantum automata [J].Theory of Computing Systems,2006,39(1):165-188.
[16] 李绿周.量子计算模型的等价性判定及量子通信中的若干基本问题[D].广州:中山大学,2009. L Z Li.Determination of equivalence between quantum computing models and some basic problems in quantum communication[D].Guang Zhou:Sun Yat-Sen University,2009.(in Chinese)
[17] P Selinger.Towards a quantum programming language[J].Mathematical Structures in Computer Science,2004,14(4):527-586.
[18] M S Ying,Y Feng.Quantum loop programs[J].Acta Informatica,2010,47(4):221-250.
[19] 雷红轩,席政军,李永明.广义量子loop程序的若干性质[J].电子学报,2013,41(4):727-732. H X Lei,Z J Xi,Y M Li.Some properties of generalized quantum loop program[J].Acta Electronica Sinica,2013,41(4):727-732.(in Chinese)

量子马尔可夫链安全性模型检测

Model Checking of Safety Property over Quantum Markov Chain

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	田晖, 严艳, 汤莉莉, 吴俊彦, 王慧东, 全韩彧. 基于分数基音延迟动态搜索的语音隐写算法[J]. 电子学报, 2023, 51(1): 67-75.
[2]	赵耿, 马英杰, 陈磊, 董有恒, 侯艳丽. 基于扰动时空混沌系统的动态S盒设计[J]. 电子学报, 2022, 50(8): 2037-2042.
[3]	胡文文, 周日贵. 基于d维单个量子态的半量子密钥分发方案[J]. 电子学报, 2022, 50(5): 1025-1032.
[4]	郑秋华, 胡程楠, 崔婷婷, 申延召, 曾英佩, 吴铤. 一种基于概率分析的DHR模型安全性分析方法[J]. 电子学报, 2021, 49(8): 1586-1598.
[5]	支婷, 刘颖, 周华春, 张宏科. 智慧标识网络服务机理研究进展及安全性分析[J]. 电子学报, 2021, 49(8): 1653-1664.
[6]	欧庆于, 罗芳, 吴晓平, 杨鹏. 基于电压毛刺故障扰动的分组密码安全性度量方法研究[J]. 电子学报, 2021, 49(3): 417-423.
[7]	汪榆淋, 窦家维. k-min问题安全多方计算方案及应用[J]. 电子学报, 2021, 49(11): 2256-2260.
[8]	王舜, 杜晔, 韩臻. 基于模块化Abstract-Refine算法框架的软件模型检测方法[J]. 电子学报, 2020, 48(5): 997-1002.
[9]	魏铎, 高海英. 一种支持算术张成程序的密文策略属性加密方案[J]. 电子学报, 2020, 48(10): 1993-2002.
[10]	宋云. 基于GHZ态局域测量的量子秘密共享[J]. 电子学报, 2019, 47(7): 1443-1448.
[11]	杨曦, 罗平, 贾古丽. 基于社会学信任理论的软件可信性概念模型[J]. 电子学报, 2019, 47(11): 2344-2353.
[12]	李俊志, 关杰. 非线性反馈移存器型序列密码的完全性通用算法[J]. 电子学报, 2018, 46(9): 2075-2080.
[13]	吴涛, 景晓军. 一种强不可伪造无证书签名方案的密码学分析与改进[J]. 电子学报, 2018, 46(3): 602-606.
[14]	房丙午, 黄志球, 王勇, 李勇. 状态不可观测的信息物理融合系统运行时验证[J]. 电子学报, 2018, 46(12): 2824-2831.
[15]	范艳焕, 李永明, 潘海玉. 不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 电子学报, 2018, 46(1): 152-159.