模型检验是一种对软件和硬件系统的可靠性进行自动验证的形式化技术。使用这种技术，可以自动验证和排除正在开发的系统投入使用后是否存在影响系统安全运行的微小瑕疵。本书全面、系统、详细地介绍了模型检验的逻辑和理论基础、原理、验证工具的使用方法以及软件和硬件系统的建模与验证方法，主要内容包括系统验证、并发系统的建模、线性时间性质、正则性质、线性时序逻辑、计算树逻辑、等价和抽象、偏序约简、时控自动机和概率系统等10章。 本书可作为计算机科学与技术、软件工程、电子信息科学与技术及相关专业本科生、研究生的教材，也可作为模型检验领域研究人员及关注系统可靠性的设计与开发人员的参考书。

第1章 系统验证
1.1 模型检验
1.2 模型检验的特征
1.2.1 模型检验的步骤
1.2.2 模型检验的优点与缺点
1.3 文献说明
第2章 并发系统的建模
2.1 迁移系统
2.1.1 执行
2.1.2 硬件和软件系统的建模
2.2 并行与通信
2.2.1 并发与交错
2.2.2 用共享变量通信
2.2.3 握手
2.2.4 通道系统
2.2.5 nanoPromela
2.2.6 同步并行性
2.3 状态空间爆炸问题
2.4 总结
2.5 文献说明
2.6 习题
第3章 线性时间性质
3.1 死锁
3.2 线性时间行为
3.2.1 路径与状态图
3.2.2 迹
3.2.3 线性时间性质
3.2.4 迹等价与线性时间性质
3.3 安全性质与不变式
3.3.1 不变式
3.3.2 安伞件质
3.3.3 迹等价与安全性质
3.4 活性性质
3.4.1 活性性质概念
3.4.2 安全性质与活性性质
3.5 公平性
3.5.1 公平性约束
3.5.2 公平性策略
3.5.3 公平性与安全性
3.6 总结
3.7 文献说明
3.8 习题
第4章 正则性质
4.1 有限单词上的自动机
4.2 正则安全性质的模型检验
4.2.1 正则安全性质
4.2.2 验证正则安全性质
4.3 无限单词上的自动机
4.3.1 ω正则语言与性质
4.3.2 未定Buchi自动机
4.3.3 确定Buchi自动机
4.3.4 广义未定Buchi自动机
4.4 模型检验ω正则性质
4.4.1 持久性质与乘积
4.4.2 嵌套深度优先搜索
4.5 总结
4.6 文献说明
4.7 习题
第5章 线性时序逻辑
5.1 线性时序逻辑述要
5.1.1 语法
5.1.2 语义
5.1.3 准述性质
5.1.4 LTL公式的等价性
5.1.5 弱直到、释放和正范式
5.1.6 LTL中的公平性
5.2 基于自动机的LTL模型检验
5.2.1 LTL模型检验问题的复杂度
5.2.2 LTL可满足性和有效性检验
5.3 总结
5.4 文献说明
5.5 习题
第6章 计算树逻辑
6.1 引言
6.2 计算树逻辑
6.2.1 语法
6.2.2 语义
6.2.3 CTL公式的等价性
6.2.4 CTL范式
6.3 LTL与CTL的表达力对比
6.4 CTL模型检验
6.4.1 基本算法
6.4.2 直到和存在总是运算符
6.4.3 时间复杂度和空间复杂度
6.5 CTL的公平性
6.6 反例和证据
6.6.1 CTL中的反例
6.6.2 公平CTL中的反例和证据
6.7 符号CTL模型检验
6.7.1 开关函数
6.7.2 用开关函数编码迁移系统
6.7.3 有序二叉决策图
6.7.4 实现基于ROBDD的算法
6.8 CTL
6.8.1 逻辑、表达力和等价
6.8.2 CTL模型检验
6.9 总结
6.10 文献说明
6.11 习题
第7章 等价和抽象
7.1 互模拟
7.1.1 互模拟商
7.1.2 基于动作的互模拟
7.2 互模拟和CTL等价
7.3 求互模拟商的算法
7.3.1 确定初始划分
7.3.2 细化划分
7.3.3 第一个划分细化算法
7.3.4 效率改进
7.3.5 迁移系统的等价检验
7.4 模拟关系
7.4.1 模拟等价
7.4.2 互模拟、模拟与迹等价
7.5 模拟等价和CTL等价
7.6 求模拟商的算法
7.7 踏步线性时间关系
7.7.1 踏步迹等价
7.7.2 踏步迹等价和LTL\O等价
7.8 踏步互模拟
7.8.1 发散敏感的踏步互模拟
7.8.2 赋范互模拟
7.8.3 踏步互模拟和CTL\O等价
7.8.4 踏步互模拟求商
7.9 总结
7.10 文献说明
7.11 习题
第8章 偏序约简
8.1 动作的无关性
8.2 线性时间的充足集方法
8.2.1 充足集的条件
8.2.2 动态偏序约简
8.2.3 计算充足集
8.2.4 静态偏序约简
8.3 分支时间的充足集方法
8.4 总结
8.5 文献说明
8.6 习题
第9章 时控自动机
9.1 时控自动机述要
9.1.1 语义
9.1.2 时间发散、时间锁定和芝诺性
9.2 时控计算树逻辑
9.3 TCTL模型检验
9.3.1 消去时间参数
9.3.2 区域迁移系统
9.3.3 TCTL模型检验算法
9.4 总结
9.5 文献说明
9.6 习题
第10章 概率系统
10.1 马尔可夫链
10.1.1 可达性概率
10.1.2 定性性质
10.2 概率计算树逻辑
10.2.1 PCTL模型检验
10.2.2 PCTL的定性片段
10.3 线性时间性质
10.4 PCTL和概率互模拟
10.4.1 PCTL
10.4.2 概率互模拟
10.5 带成本的马尔可夫链
10.5.1 成本有界可达性
10.5.2 长远性质
10.6 马尔可夫决策过程
10.6.1 可达性概率
10.6.2 PCTL模型检验
10.6.3 极限性质
10.6.4 线性时间性质和PCTL
10.6.5 公平性
10.7 总结
10.8 文献说明
10.9 习题
附录A 预备知识
A.1 常用符号与记号
A.2 形式语言
A.3 命题逻辑
A