以状态子集为中心的并行模型检测算法

摘要

以线性时序逻辑LTL(Linear Temporal Logic)模型检测算法为研究对象,提出以状态子集为中心的并行模型检测算法.针对传统单机多核算法同步开销大的缺点,新算法充分利用状态子集的稠密特性动态调度任务,从而降低同步开销,提高算法并行度.本文基于轻量级单机图计算框架Ligra,结合检测过程中状态子集的特性,设计并实现新的在线(on-the-fly)模型检测算法.与现有算法相比,在模型检测的效率上可以提升20-30％,具有高扩展性特征.