图书介绍
随机模型检测理论与应用2025|PDF|Epub|mobi|kindle电子书版本百度云盘下载
- 周从华著 著
- 出版社： 北京：科学出版社
- ISBN：9787030418920
- 出版时间：2014
- 标注页数：203页
- 文件大小：26MB
- 文件页数：214页
- 主题词：随机过程－数学模型－检测
PDF下载
下载说明
随机模型检测理论与应用PDF格式电子书版下载
下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！
（文件页数 要大于 标注页数，上中下等多册电子书除外）
注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具
图书目录
第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 模型检测工具PRISM162
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