模型检测量子系统：原理与算法

　　本书系统且全面地梳理了模型检测量子系统的原理以及基于这些原理的算法，涵盖作者相关论文中的重要研究成果。本书讲解如何应用模型检测技术来验证量子工程系统的正确性、安全性和可靠性，包含步骤详尽的算法以及丰富的示例和练习。书中首先介绍模型检测和量子理论的基础知识，然后讨论量子自动机、量子马尔可夫链和量子马尔可夫决策过程的可达性问题，介绍求解这些问题所需的数学工具和算法，之后介绍一系列用于检测超算子值马尔可夫链的计算树逻辑或线性时序逻辑的算法，后指明该领域的发展方向。

　　应明生清华大学计算机科学与技术系智能技术与系统国家重点实验室教授，清华大学量子软件研究中心主任。中国科学院软件研究所研究员、学术副所长。悉尼科技大学量子软件与信息中心杰出教授。曾获中国青年科技奖、自然科学一等奖、中国计算机学会王选奖一等奖。他的研究领域包括量子计算、程序设计语言的语义学以及人工智能中的逻辑。他为量子程序建立了包括部分正确性与完全正确性的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.2Birkhoffvon 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检测