量子马尔可夫链的模型检查
Model Checking Quantum Markov Chains
Feng、Yu 与 Ying 用量子马尔可夫链和量子 PCTL 建立量子协议的模型检查方法。
论文信息（2013，Journal of Computer and System Sciences 79:1181–1198；预印本：2012）：Yuan Feng、Nengkun Yu、Mingsheng Ying。arXiv:1205.2187
工作
本文针对量子密码协议的验证和调试提出量子模型检查框架。由于有限维量子系统的状态空间仍是连续的，作者把量子效应编码在转移边上的 superoperator 中，而让节点保持经典，从而定义量子马尔可夫链。论文进一步定义量子版 probabilistic computation tree logic（量子 PCTL）并给出模型检查算法。
主要贡献
- 提出适合量子协议的量子马尔可夫链模型。
- 用 superoperator 标记转移，避免直接枚举连续量子状态空间。
- 建立量子 PCTL 以表达概率和时序性质。
- 给出量子马尔可夫链的模型检查方法，用于验证和调试协议。
局限与适用范围
模型检查结果依赖有限维状态空间、转移 superoperator、逻辑表达能力和数值判定假设。抽象节点结构不自动覆盖硬件噪声的全部细节，也不保证任意量子程序或密码协议都能高效建模。算法通过模型证明性质，不能替代实现级测试、密钥安全审计或硬件认证。
与其他工作的关系
它把验证方法与工具中的模型检查方向扩展到量子系统，并与 量子进程的互模拟 的过程等价分析互补：前者验证逻辑性质，后者比较进程行为。与 量子程序的 Floyd–Hoare 逻辑 相比，本文以状态转移系统和时序逻辑为中心，而不是以程序断言规则为中心。
原论文
Yuan Feng, Nengkun Yu, and Mingsheng Ying, Model Checking Quantum Markov Chains, Journal of Computer and System Sciences 79, 1181–1198 (2013). arXiv:1205.2187