基于安全性检测的广义量子Loop程序终止验证

针对广义量子Loop程序的终止问题,首先介绍终止和几乎终止的两种定义,说明它们在刻画程序终止问题上的能力不足.为了弥补这种缺陷,引入另外两种定义:以一定概率在第n步终止和可终止,并且对这四种终止定义进行比较.其次,量子(正则)安全性是量子Markov链中重要的一类线性时间属性,证明出量子正则安全性的可满足概率等于乘积量子Markov链终状态不可达的概率,从而给出量子正则安全性检测技术.运用该检测技术,将广义量子Loop程序的终止问题归结为量子正则安全性的可满足性问题,并给出算法来计算第n步终止、可终止的概率和量子终态.针对多(单)量子比特系统、复合系统、嵌套系统,推导出第n步终止、可终止的终态和概率,并提供计算的显式表达式.最后证明广义量子Loop程序有限步内终止和可终止的充要条件.