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

译者序
前言
第1章 引言
1.1 第二次量子革命需要新的验证技术
1.2 经典系统的模型检测技术
1.3 模型检测量子系统的困难
1.4 模型检测量子系统的研究现状
1.5 本书结构
第2章 模型检测基础
2.1 系统建模
2.2 时序逻辑
2.2.1 线性时序逻辑
2.2.2 计算树逻辑
2.3 模型检测算法
2.3.1 线性时序逻辑模型检测
2.3.2 计算树逻辑模型检测
2.4 模型检测概率系统
2.4.1 马尔可夫链和马尔可夫决策过程
2.4.2 概率时序逻辑
2.4.3 概率模型检测算法
2.5 文献注记
第3章 量子理论基础
3.1 量子系统的状态空间
3.1.1 希尔伯特空间
3.1.2 子空间
3.1.3 量子力学的基本假设I
3.2 量子系统的动态过程
3.2.1 线性算子
3.2.2 酉算子
3.2.3 量子力学的基本假设II
3.3 量子测量
3.3.1 量子力学的基本假设III
3.3.2 投影测量
3.4 量子系统的复合
3.4.1 张量积
3.4.2 量子力学的基本假设IV
3.5 混合态
3.5.1 密度算子
3.5.2 混合态的演化和测量
3.5.3 约化密度算子
3.6 量子操作
3.6.1 量子力学基本假设II的一个推广
3.6.2 量子操作的表示
3.7 文献注记
第4章 模型检测量子自动机
4.1 量子自动机
4.2 Birkhoff-von Neumann量子逻辑
4.3 量子系统的线性时间性质
4.3.1 基本定义
4.3.2 安全性质
4.3.3 不变性
4.3.4 存活性质
4.3.5 持续性质
4.4 量子自动机的可达性
4.4.1 量子系统的(元)命题逻辑
4.4.2 量子自动机可达性的满足
4.5 量子自动机不变性的检测算法
4.6 量子自动机可达性的检测算法
4.6.1 检测A|=If的最简单情形
4.6.2 检测A|=If的一般情形
4.6.3 检测A|=Gf以及A=Uf
4.7 量子自动机可达性检测的不可判定性
4.7.1 A|=Gf、A|=Uf和A|=If的不可判定性
4.7.2 A|=Ff的不可判定性
4.8 文献注记
第5章 模型检测量子马尔可夫链
5.1 量子马尔可夫链
5.2 量子图论
5.2.1 邻接性和可达性
5.2.2 底部强连通分量
5.3 状态希尔伯特空间的分解
5.3.1 瞬态子空间
5.3.2 底部强连通分量分解
5.3.3 周期性分解
5.4 量子马尔可夫链的可达性分析
5.4.1 可达性概率
5.4.2 重复可达性概率
5.4.3 持续性概率
5.5 检测量子马尔可夫决策过程
5.5.1 不变子空间和可达性概率
5.5.2 经典MDP、POMDP和qMDP的比较
5.5.3 有限边界下的可达性
5.5.4 无限边界下的可达性
5.6 文献注记
第6章 模型检测超算子值马尔可夫链
6.1 超算子值马尔可夫链
6.2 超算子值马尔可夫链上的正算子值测度
6.3 正算子值时序逻辑
6.3.1 量子计算树逻辑
6.3.2 线性时序逻辑
6.4 检测超算子值马尔可夫链的算法
6.4.1 模型检测量子计算树逻辑公式
6.4.2 模型检测线性时序逻辑性质
6.5 文献注记
第7章 总结与展望
7.1 状态空间爆炸
7.2 应用
7.2.1 量子电路的验证与测试
7.2.2 量子密码协议的验证与分析
7.2.3 量子程序的验证与分析
7.3 工具：量子系统的模型检测器
7.4 从模型检测量子系统到量子模型检测
附录A 第4章中技术引理的证明
附录B 第5章中技术引理的证明
附录C 第6章中技术引理的证明
参考文献