摘要： 提出了一种基于差分进化算法的模型检测算法，用以解决模型检测中的死锁检测 问题。模型检测方法通过抽象出一个系统的模型和定义关于该系统的具体规范，模型检测器就 可以自动验证系统是否满足规范。由于一般的显式模型检测器是采用确定性算法来完成检测 的（如深度优先搜索），因此在对状态空间较大的系统进行检测时，模型检测的效率较低，甚至 不能完成检测。为了缓解这种问题，提出了一种基于差分进化算法的启发式模型检测算法。同 时基于原有算法框架扩展了基于路径的编码、模拟退火、关键参数自适应等操作用于提高算法 表现。结果表明，该算法可以在较少的时间内找到含有死锁状态的反例路径，并且与确定性算 法和 ２种不确定性算法（粒子群算法，遗传算法）比较，在状态搜索方面与生成反例长度方面均 有更好的表现。

关键词: 模型检测；差分进化算法；死锁检测

中图分类号: 

• TP311