Model Checking of Safety Property over Quantum Markov Chain

LIN Yun-guo; LEI Hong-xuan; LI Yong-ming

doi:10.3969/j.issn.0372-2112.2014.11.010

您当前的位置：

首页 >

文章列表页 >

Model Checking of Safety Property over Quantum Markov Chain

更新时间：2025-07-16

- Model Checking of Safety Property over Quantum Markov Chain
- Acta Electronica Sinica Vol. 42, Issue 11, Pages: 2191-2197(2014)
- 作者机构：
  
  1. 陕西师范大学计算机科学学院,陕西,西安,710119
  2. 福建农林大学计算机与信息学院,福建,福州,350002
  3. 内江师范学院数学与信息科学学院,四川,内江,641112
  4. 陕西师范大学计算机科学学院,陕西,西安,710119
  5. 福建农林大学计算机与信息学院,福建,福州,350002
  6. 内江师范学院数学与信息科学学院,四川,内江,641112
- 作者简介：
- 基金信息：
  
  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)
- DOI：10.3969/j.issn.0372-2112.2014.11.010
  CLC： TP301.6
- Published：2014
- 稿件说明：
移动端阅览
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.
DOI：

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. DOI： 10.3969/j.issn.0372-2112.2014.11.010.

摘要

本文定义了量子线性时间属性

包括量子安全性

量子不变性

讨论了它们的关系和性质.结合测量一次、测量多次的单向量子有穷自动机

构建了两类乘积量子马尔可夫链

提出了基于自动机技术的量子正则安全性检测方法.通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性

并给出了可满足性的概率计算公式.作为应用

分析了广义量子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.

关键词

Keywords

references

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on Interaction Modeling and Mismatch Checking of Time-Aware Web Services

Exact Acceleration of Real-Time Model Checking Based on Parking Cycle

Specification and Verification of Web Service Composition Based on XYZ/ADL

Precisely Detecting Buffer Overflow Vulnerabilities

Model Checking: Theories, Techniques and Applications

Related Author

Sheng

WANG Sheng

RONG Mei

ZHANG Guang-quan

WANG Cong-yin

ZHUANG Lei

YIN Chuan-long

HE Ya-Li

Related Institution

Shenzhen Tourism CollegeJinan UniversityShenzhenGuangdong 518053China

State Key Laboratory of Computer ScienceChinese Academy of ScienceBeijing 100190China

School of Computer Science and TechnologySoochow UniversitySuzhouJiangsu 215006China

Shenzhen Tourism College,Jinan University

State Key Laboratory of Computer Science,Chinese Academy of Science

⁰