量子马尔可夫链：混合系统的描述、等价性的可判定性以及线性时间性质的模型检测
量子物理
2015-07-01 v1 计算机科学中的逻辑
摘要
在本文中，我们研究了一种量子马尔可夫链模型，它是马尔可夫链的量子类比，通过用量子操作替换转移矩阵中的概率而获得。我们表明，尽管该模型与文献中提出的另一种量子马尔可夫模型具有相同的表达能力，但它非常适合于描述由量子组件和经典组件组成的混合系统。事实上，混合系统在量子信息处理中经常遇到；例如，量子程序和量子协议均可视为混合系统。因此，我们进一步提出一种称为混合量子自动机(HQA)的模型，可用于描述这些从外部世界接收输入（动作）的混合系统。我们证明HQA的语言等价问题可在多项式时间内判定。此外，我们将此结果应用于量子马尔可夫链的迹等价问题，因此其也可在多项式时间内判定。最后，我们讨论量子马尔可夫链的线性时间性质的模型检测，并表明正则安全性质的定量分析可成功处理。
引用
@article{arxiv.1506.08982,
title = {Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties},
author = {Lvzhou Li and Yuan Feng},
journal= {arXiv preprint arXiv:1506.08982},
year = {2015}
}
备注
This paper has been accepted for publication in Information and Computation