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

• 作者: 张珩 张营飞 杨秋松 谢淼
• 来源期刊: 计算机系统应用
• 关键词: LTL模型检测 状态子集 并行 在线方法 图计算
• 年，卷（期）: 2016,（10）
• 所属期刊栏目: 软件技术·算法
• 页码范围: 129-136
• 页数: 8页
• 字数: 7146字
• 语种: 中文
• DOI: 10.15888/j.cnki.csa.005361

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张珩	中国科学院软件研究所基础软件国家工程研究中心	52	651	11.0	24.0
5	杨秋松	中国科学院软件研究所基础软件国家工程研究中心	20	33	3.0	5.0
6	谢淼	中国科学院软件研究所基础软件国家工程研究中心	3	0	0.0	0.0
10	张营飞	中国科学院软件研究所基础软件国家工程研究中心	1	0	0.0	0.0