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