本书系统且全面地梳理了模型检测量子系统的原理以及基于这些原理的算法，涵盖作者相关论文中的重要研究成果。本书讲解如何应用模型检测技术来验证量子工程系统的正确性、安全性和可靠性，包含步骤详尽的算法以及丰富的示例和练习。书中首先介绍模型检测和量子理论的基础知识，然后讨论量子自动机、量子马尔可夫链和量子马尔可夫决策过程的可达性问题，介绍求解这些问题所需的数学工具和算法，之后介绍一系列用于检测超算子值马尔可夫链的计算树逻辑或线性时序逻辑的算法，后指明该领域的发展方向。
模型检测是一种主要用于验证有限状态系统的动态性质的算法技术。经过35年以上的发展，已经成为一种重要的硬件和软件系统验证技术，并在信息与通信技术（ICT）行业中得到了许多成功的应用。模型检测的特殊吸引力主要得益于以下两个特征：
完全自动的；
当性质不满足时提供反例，因此在调试中作用显著。
由于计算和通信系统中存在各种随机现象，模型检测已被系统地扩展用于验证概率系统，例如马尔可夫链和马尔可夫决策过程。
随着量子计算和量子通信的出现，特别是其在过去几年的快速发展，人们自然期望进一步扩展模型检测技术以验证量子系统。事实上，从将概率模型检测直接应用于量子系统（特别是量子通信协议）开始，对模型检测量子系统的研究已经进行了10多年。在处理越来越一般的量子系统时，人们逐渐认识到，模型检测量子系统需要某些与经典系统（包括概率系统）从根本上不同的原理。在近期的研究中，模型检测量子系统的一些基本原理得到了发展，但相关研究成果分散在各种会议和期刊论文中。
本书试图系统地阐述到写作时间为止提出的模型检测量子系统的原理以及基于这些原理的算法。本书末尾简要讨论了一些潜在的应用和未来研究的主题。希望本书可以作为研究人员踏入这一新领域时的入门指南，并为该领域的进一步发展奠定基础。
本书还计划作为研究生的教学用书，因此其内容组织基于一定的教学目标。鉴于量子计算和信息的学习者可能具备计算机科学或物理学背景，在章节的安排上，第2章和第3章为预备章节，其中第2章为物理学背景的学生简要介绍模型检测，第3章为计算机科学背景的学生简要介绍量子理论。之后，从简单的模型和检测性质到更复杂的模型和检测性质，逐步介绍量子系统的模型检测技术。
致谢
本书的材料主要来自作者及合作者的一系列论文。在此感谢俞能昆博士、李杨佳博士、应圣钢博士和官极博士，与他们的合作愉快且富有成效。没有他们的贡献，这本书是不可能完成的。
本书中的工作得到了中国国家重点研发计划（批准号：2018YFA0306701）、澳大利亚研究委员会（批准号：DP160101652和DP180100691）、中国国家自然科学基金（批准号：61832015）和中国科学院前沿科学重点研究计划的支持。谨此致谢。
应明生
清华大学计算机科学与技术系智能技术与系统国家重点实验室教授，清华大学量子软件研究中心主任。中国科学院软件研究所研究员、学术副所长。悉尼科技大学量子软件与信息中心杰出教授。曾获中国青年科技奖、自然科学一等奖、中国计算机学会王选奖一等奖。
他的研究领域包括量子计算、程序设计语言的语义学以及人工智能中的逻辑。他为量子程序建立了包括部分正确性与完全正确性的Floyd-Hoare型逻辑，特别是证明了其（相对）完备性。他将高级量子控制结构引入量子语言中，以更加严格、完整和系统的形式推出了量子case结构、量子递归结构、二次量子化、量子程序叠加等一系列概念。
他著有Foundations of Quantum Programming（2016）和Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs（2001）。此外，他目前还担任ACM Transactions on Quantum Computing的（联合）主编。
冯元
悉尼科技大学量子软件与信息中心教授。曾任清华大学计算机系副研究员。他的研究兴趣包括量子系统的形式化验证、量子程序理论、量子信息与计算以及概率系统。已在国际重要期刊和主流会议上发表论文70余篇。曾获得澳大利亚研究理事会（ARC）未来研究基金（2010）。
译者序
前言
第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
2.4.1马尔可夫链和马尔可夫
决策过程25
2.4.2概率时序逻辑26
2.4.3概率模型检测算法27
2.5文献注记30
第3章量子理论基础31
3.1量子系统的状态空间32
3.1.1希尔伯特空间32
3.1.2子空间35
3.1.3量子力学的基本假设I
36
3.2量子系统的动态过程36
3.2.1线性算子37
3.2.2酉算子39
3.2.3量子力学的基本假设II
40
3.3量子测量41
3.3.1量子力学的基本假设III
41
3.3.2投影测量42
3.4量子系统的复合44
3.4.1张量积44
3.4.2量子力学的基本假设IV
45
3.5混合态46
3.5.1密度算子46
3.5.2混合态的演化和测量47
3.5.3约化密度算子47
3.6量子操作48
3.6.1量子力学基本假设II的
一个推广48
3.6.2量子操作的表示50
3.7文献注记51
第4章模型检测量子自动机53
4.1量子自动机54
4.2Birkhoffvon Neumann量子
逻辑56
4.3量子系统的线性时间性质61
4.3.1基本定义61
4.3.2安全性质62
4.3.3不变性63
4.3.4存活性质66
4.3.5持续性质67
4.4量子自动机的可达性70
4.4.1量子系统的(元)命题
逻辑71
4.4.2量子自动机可达性的
满足72
4.5量子自动机不变性的检测
算法74
4.6量子自动机可达性的检测
算法77
4.6.1检测
书单推荐
