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

• 学术论文 • 上一篇    下一篇

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

林运国1,2, 雷红轩3, 李永明1   

  1. 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-guo1,2, LEI Hong-xuan3, LI Yong-ming1   

  1. 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)

摘要:

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

中图分类号: