随机模型检测理论与应用

v27IP4零配置协议 25 实验结果 30 26 限界模型检测过程终止判断标准的修正 32 27 相关工作 34 28 本章小结 34 参考文献 35第3章 马尔可夫决策过程的限界模型检测 36 31 概述 36 32 马尔可夫决策过程与概率计算树逻辑 36 33 概率计算树逻辑的限界模型检测 38 331 概率计算树逻辑的等价性 38 332 概率计算树逻辑的限界语义 39 333 限界模型检测过程终止的判断 42 334 限界模型检测算法 44 34 实例研究 48 35 实验结果 50 36 终止标准的修正 53 37 本章小结 55 参考文献 56第4章 连续时间马尔可夫链的限界模型检测 57 41 连续随机逻辑与连续时间马尔可夫链 57 411 连续随机逻辑 57 412 连续时间马尔可夫链 57 413 转移概率与极限概率 59 414 连续随机逻辑的语义 60 42 连续随机逻辑的限界模型检测 60 421 连续随机逻辑的限界语义 60 422 限界下转移概率的计算 62 423 限界检测算法 63 43 实验结果 68 44 本章小结 74 参考文献 74第5章 多智体系统的限界模型检测 75 51 概述 75 52 相关工作 76 53 概率实时解释系统 77 531 概率时间自动机 77 532 概率时间自动机的平行组合 79 533 概率时间自动机的语义 81 534 概率实时解释系统 82 54 概率实时认知逻辑 85 541 概率实时认知逻辑的语法 85 542 概率实时认知逻辑的语义 85 55 概率知识区域图 87 56 基于概率知识区域图的限界模型检测 91 561 时态逻辑的转换 91 562 转换逻辑的限界模型检测 93 57 限界模型检测算法 96 58 线性方程组的求解 99 59 实例研究 100 591 火车穿越控制系统 100 592 控制系统的限界模型检测 102 510 终止性选择标准 106 511 本章小结 107 参考文献 107第6章 模型检测多智体系统中的抽象技术 109 61 概述 109 62 相关工作 109 63 解释系统与时态逻辑 110 64 验证属性驱动的抽象 111 641 属性驱动的存在性抽象 111 642 属性的可满足性保持 113 65 反例真实性确认 115 651 什么是反例 115 652 识别虚假反例 119 653 反例引导的求精 119 66 实例研究 120 661 扑克游戏 120 662 抽象 122 67 实验 123 671 密码学家就餐协议 123 672 实验结果 124 68 本章小结 125 参考文献 125第7章 概率时态认知逻辑模型检测中的抽象技术 126 71 概率时态认知逻辑语法和语义 126 72 建立抽象模型 127 73 属性保持关系 130 74 概率时态认知逻辑模型检测算法 131 75 抽象模型的求精 134 751 抽象失败原因分析 134 752 抽象求精 135 76 模型检测密码学家就餐协议 139 761 密码学家就餐协议的概率 Kripke结构 139 762 建立密码学家就餐协议的抽象模型 140 763 实验结果 141 77 本章小结 142 参考文献 142第8章 实时时态认知逻辑模型检测中的抽象技术 143 81 实时时态认知逻辑语法和语义 143 811 实时时态认知逻辑的语法 143 812 实时解释系统 143 813 实时时态认知逻辑的语义 144 82 建立抽象模型 145 83 属性保持关系 146 84 实例分析 148 841 铁路道口系统介绍 148 842 建立铁路道口系统的抽象模型 149 843 模型检测铁路道口系统 151 85 抽象模型及实时时态认知逻辑的三值语义 151 86 三值抽象下的属性保持关系 153 87 模型检测主动结构控制系统 156 871 主动结构控制系统的一个演变形式 156 872 建立主动结构控制系统的抽象模型 158 873 模型检测主动结构控制系统 159 88 铁路道口系统的进一步验证 160 89 本章小结 161 参考文献 161第9章 快速安全协议的性能分析 162 91 模型检测工具 PRISM 162 92 基本建模过程 163 93 快速安全协议 165 94 FASP建模 165 95 FASP模型统计 169 96 性能属性分析 171 961 FASP的可靠性分析 171 962 FASP的快速性分析 173 963 吞吐量分析 175 97 本章小结 176 参考文献 177第10章 IEEE80211P中 MAC协议的性能分析 178 101 IEEE80211P中 MAC协议的工作特性 178 102 MAC协议的概率时间自动机模型 180 103 IEEE80211P模型的静态数据分析 183 104 IEEE80211P模型的验证分析 184 1041 IEEE80211P模型的概率可达性 184 1042 IEEE80211P模型的期望可达性 185 105 本章小结 188 参考文献 189第11章 RFID中SGALOHA协议的性能分析 190 111 概述 190 112 协议建模 191 1121 协议工作原理 191 1122 协议的马尔可夫决策过程模型 192 113 模型的验证与分析 194 1131 模型统计 194 1132 概率可达性 195 1133 SGALOHA与 ALOHA的属性验证对比 196 1134 预期可达性 198 114 本章小结 200 参考文献 201后记 202

《随机模型检测理论与应用》可作为高等院校计算机专业高年级本科生和研究生的教材,也可供相关领域的科研人员参考.《随机模型检测理论与应用》是作者多年从事随机模型检测相关科研工作的结晶.《随机模型检测理论与应用》致力于缓解随机模型检测中的状态空间爆炸问题,深入系统地论述克服状态空间爆炸的两种基本技术限界模型检测技术与抽象技术.首先,介绍离散时间马尔可夫链、马尔可夫决策过程、连续时间马尔可夫链和概率实时解释系统中的限界检测技术.然后,讨论模型检测概率、实时认知时态逻辑中的二值与三值抽象技术.最后,探讨随机模型检测技术在云计算和物联网领域的应用.