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

doi:10.3969/j.issn.0372-2112.2014.11.010

PDF(753 KB)

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

学术论文

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

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

作者信息 +

Model Checking of Safety Property over Quantum Markov Chain

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

Author information +

文章历史 +

摘要

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

导出引用

林运国, 雷红轩, 李永明. 量子马尔可夫链安全性模型检测[J]. 电子学报, 2014, 42(11): 2191-2197. https://doi.org/10.3969/j.issn.0372-2112.2014.11.010

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. https://doi.org/10.3969/j.issn.0372-2112.2014.11.010

中图分类号： TP301.6

参考文献

[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)