第1章 随机模型检测概述 1
1.1 模型检测 1
1.2 状态空间约简 3
1.2.1 基于有序二叉决策图的符号化模型检测方法 3
1.2.2 基于命题公式可满足性判定的限界模型检测方法 4
1.2.3 抽象方法 5
1.2.4 组合验证 6
1.2.5 其他约简方法 6
1.3 线性时态逻辑的限界模型检测 7
1.3.1 示例 7
1.3.2 线性时态逻辑 7
1.3.3 线性时态逻辑的限界语义 8
1.3.4 转换 9
1.4 抽象 11
1.4.1 互模拟与模拟 11
1.4.2 数据抽象 12
1.5 随机模型检测 14
1.6 本章小结 16
参考文献 16
第2章 离散时间马尔可夫链的限界模型检测 19
2.1 概述 19
2.2 离散时间马尔可夫链与概率计算树逻辑 19
2.3 概率计算树逻辑的限界模型检测 21
2.3.1 概率计算树逻辑的等价性 21
2.3.2 概率计算树逻辑的限界语义 22
2.3.3 限界模型检测过程终止的判断 23
2.3.4 概率计算树逻辑的限界模型检测算法 26
2.4 实例：IPv4零配置协议 27
2.5 实验结果 30
2.6 限界模型检测过程终止判断标准的修正 32
2.7 相关工作 34
2.8 本章小结 34
参考文献 35
第3章 马尔可夫决策过程的限界模型检测 36
3.1 概述 36
3.2 马尔可夫决策过程与概率计算树逻辑 36
3.3 概率计算树逻辑的限界模型检测 38
3.3.1 概率计算树逻辑的等价性 38
3.3.2 概率计算树逻辑的限界语义 39
3.3.3 限界模型检测过程终止的判断 42
3.3.4 限界模型检测算法 44
3.4 实例研究 48
3.5 实验结果 50
3.6 终止标准的修正 53
3.7 本章小结 55
参考文献 56
第4章 连续时间马尔可夫链的限界模型检测 57
4.1 连续随机逻辑与连续时间马尔可夫链 57
4.1.1 连续随机逻辑 57
4.1.2 连续时间马尔可夫链 57
4.1.3 转移概率与极限概率 59
4.1.4 连续随机逻辑的语义 60
4.2 连续随机逻辑的限界模型检测 60
4.2.1 连续随机逻辑的限界语义 60
4.2.2 限界下转移概率的计算 62
4.2.3 限界检测算法 63
4.3 实验结果 68
4.4 本章小结 74
参考文献 74
第5章 多智体系统的限界模型检测 75
5.1 概述 75
5.2 相关工作 76
5.3 概率实时解释系统 77
5.3.1 概率时间自动机 77
5.3.2 概率时间自动机的平行组合 79
5.3.3 概率时间自动机的语义 81
5.3.4 概率实时解释系统 82
5.4 概率实时认知逻辑 85
5.4.1 概率实时认知逻辑的语法 85
5.4.2 概率实时认知逻辑的语义 85
5.5 概率知识区域图 87
5.6 基于概率知识区域图的限界模型检测 91
5.6.1 时态逻辑的转换 91
5.6.2 转换逻辑的限界模型检测 93
5.7 限界模型检测算法 96
5.8 线性方程组的求解 99
5.9 实例研究 100
5.9.1 火车穿越控制系统 100
5.9.2 控制系统的限界模型检测 102
5.10 终止性选择标准 106
5.11 本章小结 107
参考文献 107
第6章 模型检测多智体系统中的抽象技术 109
6.1 概述 109
6.2 相关工作 109
6.3 解释系统与时态逻辑 110
6.4 验证属性驱动的抽象 111
6.4.1 属性驱动的存在性抽象 111
6.4.2 属性的可满足性保持 113
6.5 反例真实性确认 115
6.5.1 什么是反例 115
6.5.2 识别虚假反例 119
6.5.3 反例引导的求精 119
6.6 实例研究 120
6.6.1 扑克游戏 120
6.6.2 抽象 122
6.7 实验 123
6.7.1 密码学家就餐协议 123
6.7.2 实验结果 124
6.8 本章小结 125
参考文献 125
第7章 概率时态认知逻辑模型检测中的抽象技术 126
7.1 概率时态认知逻辑语法和语义 126
7.2 建立抽象模型 127
7.3 属性保持关系 130
7.4 概率时态认知逻辑模型检测算法 131
7.5 抽象模型的求精 134
7.5.1 抽象失败原因分析 134
7.5.2 抽象求精 135
7.6 模型检测密码学家就餐协议 139
7.6.1 密码学家就餐协议的概率Kripke结构 139
7.6.2 建立密码学家就餐协议的抽象模型 140
7.6.3 实验结果 141
7.7 本章小结 142
参考文献 142
第8章 实时时态认知逻辑模型检测中的抽象技术 143
8.1 实时时态认知逻辑语法和语义 143
8.1.1 实时时态认知逻辑的语法 143
8.1.2 实时解释系统 143
8.1.3 实时时态认知逻辑的语义 144
8.2 建立抽象模型 145
8.3 属性保持关系 146
8.4 实例分析 148
8.4.1 铁路道口系统介绍 148
8.4.2 建立铁路道口系统的抽象模型 149
8.4.3 模型检测铁路道口系统 151
8.5 抽象模型及实时时态认知逻辑的三值语义 151
8.6 三值抽象下的属性保持关系 153
8.7 模型检测主动结构控制系统 156
8.7.1 主动结构控制系统的一个演变形式 156
8.7.2 建立主动结构控制系统的抽象模型 158
8.7.3 模型检测主动结构控制系统 159
8.8 铁路道口系统的进一步验证 160
8.9 本章小结 161
参考文献 161
第9章 快速安全协议的性能分析 162
9.1 模型检测工具PRISM 162
9.2 基本建模过程 163
9.3 快速安全协议 165
9.4 FASP建模 165
9.5 FASP模型统计 169
9.6 性能属性分析 171
9.6.1 FASP的可靠性分析 171
9.6.2 FASP的快速性分析 173
9.6.3 吞吐量分析 175
9.7 本章小结 176
参考文献 177
第10章 IEEE 802.11P中MAC协议的性能分析 178
10.1 IEEE 802.11P中MAC协议的工作特性 178
10.2 MAC协议的概率时间自动机模型 180
10.3 IEEE 802.11P模型的静态数据分析 183
10.4 IEEE 802.11P模型的验证分析 184
10.4.1 IEEE 802.11P模型的概率可达性 184
10.4.2 IEEE 802.11P模型的期望可达性 185
10.5 本章小结 188
参考文献 189
第11章 RFID中S-ALOHA协议的性能分析 190
11.1 概述 190
11.2 协议建模 191
11.2.1 协议工作原理 191
11.2.2 协议的马尔可夫决策过程模型 192
11.3 模型的验证与分析 194
11.3.1 模型统计 194
11.3.2 概率可达性 195
11.3.3 S-ALOHA与ALOHA的属性验证对比 196
11.3.4 预期可达性 198
11.4 本章小结 200
参考文献 201
后记 202