等价化简和抽象的概率模型检测

摘要

模型检测是一项很成功的自动化系统验证技术，对于不满足的验证属性，需要额外输出一个反例。为了生成更好的模型反例，对原始系统模型进行等价化简和抽象。
　　在概率模型检测中，使用离散时间的马尔科夫链描述系统，使用时态逻辑的分支概率计算树时态逻辑表示系统的属性。本文设计了新的概率模型检测算法，针对特定的模型属性，将系统模型转化为仅仅含有单个初始状态和单个目标状态的马尔科夫链模型。根据状态之间的传递关系，得到新模型上的初始状态传递闭包和目标状态逆传递闭包，进而实现对原始模型的等价化简。采用深度优先算法获得所有极小连通分量，通过将抽象后的极小连通分量代替原始模型中的极小连通分量，进而实现对原始模型的等价抽象。在无环路的模型上，采用关键子系统描述反例，采用局部搜索和全局搜索两种策略生成反例，采用预防避免策略防止新路径重复，采用运筹学上最短路径的算法获得大概率路径。
　　综上所述，本文针对离散时间的马尔科夫链模型，设计了一套基于等价化简和抽象的反例生成框架。选取领导选举协议和人群协议作为实验检测模型，实验结果表明了新算法大简化了模型规模，生成的反例具有更少的路径和状态。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1国内外研究现状

1.2主要内容和研究目标

1.3论文组织结构

第二章 相关研究综述

2.1离散时间的马尔科夫链

2.2状态的概率空间

2.3概率计算树逻辑

2.4概率模型检测的反例

2.5马尔科夫链的目标状态

第三章 等价化简和抽象

3.1模型等价化简

3.2模型抽象

3.3模型反例

第四章 实验的设计和分析

4.1模型化简实验的设计和分析

4.2模型抽象实验的设计和分析

4.3模型化简和抽象的算法评价

第五章 总结与展望

5.1总结

5.2展望

参考文献

发表论文和参加科研情况说明

致谢