作 者:周从华 著
定 价:88
出 版 社:科学出版社
出版日期:2014年09月01日
页 数:203
装 帧:平装
ISBN:9787030418920
●前言
章随机模型检测概述
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连续随机逻辑
……
《随机模型检测理论与应用》是作者多年从事随机模型检测相关科研工作的结晶。《随机模型检测理论与应用》致力于缓解随机模型检测中的状态空间爆炸问题,深入系统地论述克服状态空间爆炸的两种基本技术:限界模型检测技术与抽象技术。首先,介绍离散时间马尔可夫链、马尔可夫决策过程、连续时间马尔可夫链和概率实时解释系统中的限界检测技术。然后,讨论模型检测概率、实时认知时态逻辑中的二值与三值抽象技术。后,探讨随机模型检测技术在云计算和物联网领域的应用。