随机模型检测理论与应用
作者：周从华 著
出版时间：2014年版
内容简介
　　《随机模型检测理论与应用》致力于缓解随机模型检测中的状态空间爆炸问题。首先介绍了离散时间马尔科夫链、马尔科夫决策过程、连续时间马尔科夫链和概率实时解释系统上的限界检测技术。然后讨论了模型检测概率、实时认知时态逻辑中的二值与三值抽象技术。最后从应用出发，探讨了随机模型检测技术在云计算和物联网领域的应用。
目录
前言
第1章　随机模型检测概述
　1.1　模型检测
　1.2　状态空间约简
　　1.2.1　基于有序二叉决策图的符号化模型检测方法
　　1.2.2　基于命题公式可满足性判定的限界模型检测方法
　　1.2.3　抽象方法
　　1.2.4　组合验证
　　1.2.5　其他约简方法
　1.3　线性时态逻辑的限界模型检测
　　1.3.1　示例
　　1.3.2　线性时态逻辑
　　1.3.3　线性时态逻辑的限界语义
　　1.3.4　转换
　1.4　抽象
　　1.4.1　互模拟与模拟
　　1.4.2　数据抽象
　1.5　随机模型检测
　1.6　本章小结
　参考文献
第2章　离散时间马尔可夫链的限界模型检测
　2.1　概述
　2.2　离散时间马尔可夫链与概率计算树逻辑
　2.3　概率计算树逻辑的限界模型检测
　　2.3.1　概率计算树逻辑的等价性
　　2.3.2　概率计算树逻辑的限界语义
　　2.3.3　限界模型检测过程终止的判断
　　2.3.4　概率计算树逻辑的限界模型检测算法
　2.4　实例：IPv4零配置协议
　2.5　实验结果
　2.6　限界模型检测过程终止判断标准的修正
　2.7　相关工作
　2.8　本章小结
　参考文献
第3章　马尔可夫决策过程的限界模型检测
　3.1　概述
　3.2　马尔可夫决策过程与概率计算树逻辑
　3.3　概率计算树逻辑的限界模型检测
　　3.3.1　概率计算树逻辑的等价性
　　3.3.2　概率计算树逻辑的限界语义
　　3.3.3　限界模型检测过程终止的判断
　　3.3.4　限界模型检测算法
　3.4　实例研究
　3.5　实验结果
　3.6　终止标准的修正
　3.7　本章小结
　参考文献
第4章　连续时间马尔可夫链的限界模型检测
　4.1　连续随机逻辑与连续时间马尔可夫链
　　4.1.1　连续随机逻辑
　　4.1.2　连续时间马尔可夫链
　　4.1.3　转移概率与极限概率
　　4.1.4　连续随机逻辑的语义
　4.2　连续随机逻辑的限界模型检测
　　4.2.1　连续随机逻辑的限界语义
　　4.2.2　限界下转移概率的计算
　　4.2.3　限界检测算法
　4.3　实验结果
　4.4　本章小结
　参考文献
第5章　多智体系统的限界模型检测
　5.1　概述
　5.2　相关工作
　5.3　概率实时解释系统
　　5.3.1　概率时间自动机
　　5.3.2　概率时间自动机的平行组合
　　5.3.3　概率时间自动机的语义
　　5.3.4　概率实时解释系统
　5.4　概率实时认知逻辑
　　5.4.1　概率实时认知逻辑的语法
　　5.4.2　概率实时认知逻辑的语义
　5.5　概率知识区域图
　5.6　基于概率知识区域图的限界模型检测
　　5.6.1　时态逻辑的转换
　　5.6.2　转换逻辑的限界模型检测
　5.7　限界模型检测算法
　5.8　线性方程组的求解
　5.9　实例研究
　　5.9.1　火车穿越控制系统
　　5.9.2　控制系统的限界模型检测
　5.10　终止性选择标准
　5.11　本章小结
　参考文献
第6章　模型检测多智体系统中的抽象技术
　6.1　概述
　6.2　相关工作
　6.3　解释系统与时态逻辑
　6.4　验证属性驱动的抽象
　　6.4.1　属性驱动的存在性抽象
　　6.4.2　属性的可满足性保持
　6.5　反例真实性确认
　　6.5.1　什么是反例
　　6.5.2　识别虚假反例
　　6.5.3　反例引导的求精
　6.6　实例研究
　　6.6.1　扑克游戏
　　6.6.2　抽象
　6.7　实验
　　6.7.1　密码学家就餐协议
　　6.7.2　实验结果
　6.8　本章小结
　参考文献
第7章　概率时态认知逻辑模型检测中的抽象技术
　7.1　概率时态认知逻辑语法和语义
　7.2　建立抽象模型
　7.3　属性保持关系
　7.4　概率时态认知逻辑模型检测算法
　7.5　抽象模型的求精
　　7.5.1　抽象失败原因分析
　　7.5.2　抽象求精
　7.6　模型检测密码学家就餐协议
　　7.6.1　密码学家就餐协议的概率Kripke结构
　　7.6.2　建立密码学家就餐协议的抽象模型
　　7.6.3　实验结果
　7.7　本章小结
　参考文献
第8章　实时时态认知逻辑模型检测中的抽象技术
　8.1　实时时态认知逻辑语法和语义
　　8.1.1　实时时态认知逻辑的语法
　　8.1.2　实时解释系统
　　8.1.3　实时时态认知逻辑的语义
　8.2　建立抽象模型
　8.3　属性保持关系
　8.4　实例分析
　　8.4.1　铁路道口系统介绍
　　8.4.2　建立铁路道口系统的抽象模型
　　8.4.3　模型检测铁路道口系统
　8.5　抽象模型及实时时态认知逻辑的三值语义
　8.6　三值抽象下的属性保持关系
　8.7　模型检测主动结构控制系统-
　　8.7.1　主动结构控制系统的一个演变形式
　　8.7.2　建立主动结构控制系统的抽象模型
　　8.7.3　模型检测主动结构控制系统
　8.8　铁路道口系统的进一步验证
　8.9　本章小结
　参考文献
第9章　快速安全协议的性能分析
　9.1　模型检测工具PRISM
　9.2　基本建模过程
　9.3　快速安全协议
　9.4　FASP建模
　9.5　FASP模型统计
　9.6　性能属性分析
　　9.6.1　FASP的可靠性分析
　　9.6.2　FASP的快速性分析
　　9.6.3　吞吐量分析
　9.7　本章小结
　参考文献
第1O章　IEEE802.11P中MAC协议的性能分析
　10.1　IEEE802.11P中MAC协议的工作特性
　10.2　MAC协议的概率时间自动机模型
　10.3　IEEE802.11P模型的静态数据分析
　10.4　IEEE802.11P模型的验证分析
　　10.4.1　IEEE802.11P模型的概率可达性
　　10.4.2　IEEE802.11P模型的期望可达性
　10.5　本章小结
　参考文献
第11章　RFID中S-ALOHA协议的性能分析
　11.1　概述
　11.2　协议建模
　　11.2.1　协议工作原理
　　11.2.2　协议的马尔可夫决策过程模型
　11.3　模型的验证与分析
　　11.3.1　模型统计
　　11.3.2　概率可达性
　　11.3.3　S-ALOHA与ALOHA的属性验证对比
　　11.3.4　预期可达性
　11.4　本章小结
　参考文献
后记