模型检测是一种成功的自动化验证技术，主要用于验证有限状态系统的动态性质，广泛应用于传统的计算和通信行业。本书系统介绍了适用于量子系统的模型检测技术，这种技术在量子计算、量子通信以及量子物理等新兴产业中具有广泛的应用潜力。书中讨论了如何应用模型检测技术来验证量子工程系统的正确性、安全性和可靠性，主要内容涵盖基本原理和算法两方面。本书首先介绍模型检测和量子理论的基础知识，然后讨论量子自动机、量子马尔可夫链和量子马尔可夫决策过程的可达性问题，介绍求解这些问题所需的数学工具和算法，之后介绍一系列用于检测超算子值马尔可夫链的计算树逻辑或线性时序逻辑的算法，zui后指明模型检测量子系统领域的发展方向。本书适合用作高年级本科生和研究生的课程教材，同时也适合用作相关领域从业人员和工程师的参考资料。

梳理基础知识和重要研究成果，涵盖详尽的解释和练习

计算机/量子

本书讲解量子系统的模型检测原理，涵盖验证定性性质（如可达性）以及验证量子马尔可夫链的定量性质的基础知识。对于这个发展时间不长但令人兴奋的研究领域，本书给出了目前为止最全面的综述。
—— Joost-Pieter Katoen，亚琛工业大学
从量子计算机科学开始，两位作者就一直走在量子计算逻辑方法研究的前沿。因此，对于模型检测量子系统这一主题，他们是作者的最佳人选。
—— Bob Coecke，牛津大学
本书系统且全面地梳理了模型检测量子系统的原理以及基于这些原理的算法，涵盖作者相关论文中的重要研究成果。
本书讲解如何应用模型检测技术来验证量子工程系统的正确性、安全性和可靠性，包含步骤详尽的算法以及丰富的示例和练习。书中首先介绍模型检测和量子理论的基础知识，然后讨论量子自动机、量子马尔可夫链和量子马尔可夫决策过程的可达性问题，介绍求解这些问题所需的数学工具和算法，之后介绍一系列用于检测超算子值马尔可夫链的计算树逻辑或线性时序逻辑的算法，最后指明该领域的发展方向。