随机模型检测理论与应用

内容简介

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

目录

目 录

前言第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