多核模型检测工具CTAV的实现与优化

摘要

在计算机计算能力大大增强的时代, 为了提高对时间自动机进行空性检测的效率, 进一步高效利用多核处理器的优势, 研究了利用Büchi自动机的多核空性判定算法改造CTAV, 使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具, 从而提高模型检测的效率. 通过对符号化状态之间包含关系的研究, 利用这种状态之间的包含关系更快的找到接收路径并避免不必要的状态展开, 实现了多核模型检测算法的优化, 对比了一些常见模型的验证数据, 取得了更好的效果.