为了刻画开放量子系统的量子属性,扩展现有的量子马尔可夫链是有必要的.通过构建Exogenous量子算子逻辑,定义了Exogenous量子马尔可夫链.作为新型量子马尔可夫链,重点研究了4种可达性公式,给出可达性公式可满足性问题的求解,并分析了它们的可判定性问题.作为应用,实例说明广义量子Loop程序的终止问题可以归结为Exogenous量子马尔可夫链的最终可达性,进而通过检测量子公式可满足性来判定程序的终止问题.
In order to describe quantum properties of open quantum system, it is necessary to extend the existing quantum Markov chains. In this paper, Exogenous quantum Markov chains is introduced through building Exogenous quantum operator logic. For this new type of quantum Markov chain, the paper focuses on four reachability formulas, gives the solution of their satisfiability problems, and analyzes their decidability problems. As an application, an example is provided to show that the termination of the generalized quantum loop program corresponds to the future reachability of Exogenous quantum Markov chains, and therefore can be decided by checking satisfaction of quantum formulas.