本书致力于缓解随机模型检测中的状态空间爆炸问题。首先介绍了离散时间马尔科夫链、马尔科夫决策过程、连续时间马尔科夫链和概率实时解释系统上的限界检测技术。然后讨论了模型检测概率、实时认知时态逻辑中的二值与三值抽象技术。最后从应用出发，探讨了随机模型检测技术在云计算和物联网领域的应用。
样章试读
目录
前言第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 实例 :v 27
IP4零配置协议 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章 IEEE802 11P中 MAC协议的性能分析 178 10 1 IEEE802 11P中 MAC协议的工作特性 178 10 2 MAC协议的概率时间自动机模型 180 10 3 IEEE802 11P模型的静态数据分析 183 10 4 IEEE802 11P模型的验证分析 184 10 4 1 IEEE802 11P模型的概率可达性 184 10 4 2 IEEE802 11P模型的期望可达性 185 10 5 本章小结 188 参考文献 189第11章 RFID中SGALOHA协议的性能分析 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 SGALOHA与 ALOHA的属性验证对比 196 11 3 4 预期可达性 198 11 4 本章小结 200 参考文献 201后记 202]]>
京公网安备 11010102004214号