-
题名量子马尔可夫链安全性模型检测
被引量:7
- 1
-
-
作者
林运国
雷红轩
李永明
-
机构
陕西师范大学计算机科学学院
福建农林大学计算机与信息学院
内江师范学院数学与信息科学学院
-
出处
《电子学报》
EI
CAS
CSCD
北大核心
2014年第11期2191-2197,共7页
-
基金
国家自然科学基金(No.11271237
No.61228305)
+2 种基金
高等学校博士学科点专项科研基金(No.20130202110001
No.20130202120002)
中央高校基本科研业务费专项资金(No.GK201302054)
-
文摘
本文定义了量子线性时间属性,包括量子安全性,量子不变性,讨论了它们的关系和性质.结合测量一次、测量多次的单向量子有穷自动机,构建了两类乘积量子马尔可夫链,提出了基于自动机技术的量子正则安全性检测方法.通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性,并给出了可满足性的概率计算公式.作为应用,分析了广义量子loop程序,将程序终止归结为验证量子正则安全性的可满足性.
-
关键词
量子马尔可夫链
模型检测
安全性
量子有穷自动机
广义量子loop程序
-
Keywords
quantum Markov chain
model checking
safety property
quantum finite automata
generalized quantum loop program
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
-
-
题名广义量子Loop程序的若干性质
被引量:5
- 2
-
-
作者
雷红轩
席政军
李永明
-
机构
陕西师范大学计算机科学学院
内江师范学院数学与信息科学学院
-
出处
《电子学报》
EI
CAS
CSCD
北大核心
2013年第4期727-732,共6页
-
基金
国家自然科学基金(No.11271237
No.61228305)
-
文摘
本文首先就广义量子loop程序(简记为GQLoop)的主体由比特翻转、去极化、幅值阻尼、相位阻尼等信道描述时,对它的终止(几乎终止)问题进行了研究.其次,讨论了两类GQLoop程序相互嵌套时loop程序的终止(几乎终止)的问题.研究表明:以量子运算的嵌套为主体的GQLoop程序终止(几乎终止)的条件依赖于刻画量子信道的参数.最后,当开放量子系统与其环境在酉运算下做为loop程序的主体时,讨论了在酉运算后去掉环境时的主系统上量子程序的执行过程.
-
关键词
广义量子loop程序
量子运算
终止
几乎终止
复合量子系统
-
Keywords
generalized quantum loop program
quantum operation
termination
almost termination
composite quantum sys-tem
-
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
-