Exogenous量子马尔可夫链及其可达性分析

来源：软件学报杂志2016年第12期北京时间：

作者：林运国,李永明

单位：林运国，陕西师范大学 计算机科学学院, 陕西 西安 710119;福建农林大学 计算机与信息学院, 福建 福州 35000211,李永明，陕西师范大学 计算机科学学院, 陕西 西安 71011902

摘要：为了刻画开放量子系统的量子属性，扩展现有的量子马尔可夫链是有必要的.通过构建Exogenous量子算子逻辑，定义了Exogenous量子马尔可夫链.作为新型量子马尔可夫链，重点研究了4种可达性公式，给出可达性公式可满足性问题的求解，并分析了它们的可判定性问题.作为应用，实例说明广义量子Loop程序的终止问题可以归结为Exogenous量子马尔可夫链的最终可达性，进而通过检测量子公式可满足性来判定程序的终止问题.

关键词：量子马尔可夫链;量子逻辑;可达性;可满足性问题;可判定性问题

基金资助：国家自然科学基金（11271237，61228305）；福建省自然科学基金资助项目（2016J01283）；福建省教育厅中青年教师教育科研项目（JA13115）