模型检测是一种成功的自动化验证技术，主要用于验证有限状态系统的动态性质，广泛应用于传统的计算和通信行业。本书系统介绍了适用于量子系统的模型检测技术，这种技术在量子计算、量子通信以及量子物理等新兴产业中具有广泛的应用潜力。书中讨论了如何应用模型检测技术来验证量子工程系统的正确性、安全性和可靠性，主要内容涵盖基本原理和算法两方面。本书首先介绍模型检测和量子理论的基础知识，然后讨论量子自动机、量子马尔可夫链和量子马尔可夫决策过程的可达性问题，介绍求解这些问题所需的数学工具和算法，之后介绍一系列用于检测超算子值马尔可夫链的计算树逻辑或线性时序逻辑的算法，最后指明模型检测量子系统领域的发展方向。本书适合用作高年级本科生和研究生的课程教材，同时也适合用作相关领域从业人员和工程师的参考资料。
译者序
前言
第1章引言1
1.1第二次量子革命需要新的验证技术2
1.2经典系统的模型检测技术2
1.3模型检测量子系统的困难3
1.4模型检测量子系统的研究现状3
1.5本书结构5
第2章模型检测基础7
2.1系统建模8
2.2时序逻辑10
2.2.1线性时序逻辑10
2.2.2计算树逻辑13
2.3模型检测算法16
2.3.1线性时序逻辑模型检测16
2.3.2计算树逻辑模型检测23
2.4模型检测概率系统25
……
