本文已被：浏览 1319次 下载 2300次
Received:January 29, 2016 Revised:March 03, 2016
Received:January 29, 2016 Revised:March 03, 2016
中文摘要: 以线性时序逻辑LTL（Linear Temporal Logic）模型检测算法为研究对象，提出以状态子集为中心的并行模型检测算法.针对传统单机多核算法同步开销大的缺点，新算法充分利用状态子集的稠密特性动态调度任务，从而降低同步开销，提高算法并行度.本文基于轻量级单机图计算框架Ligra，结合检测过程中状态子集的特性，设计并实现新的在线（on-the-fly）模型检测算法.与现有算法相比，在模型检测的效率上可以提升20-30%，具有高扩展性特征.
Abstract:Logic model checking raise unique challenges to the efficiency and scalability of various algorithms. In this paper, it argues that the linear temporal logic model checking algorithm calls for an efficient and common solution. We then introduces a novel parallel on-the-fly model checking algorithm based on subset of states, namely SCPLM. According to the density property of subgraph with active states subset, SCPLM schedules parallel computing tasks dynamically, which has been proven to reduce the synchronization overhead significantly. It implements SCPLM on a lightweight parallel graph processing system, Ligra. A detailed evaluation using benchmarks shows that SCPLM outperforms the existing state-of-art algorithm by up to 1.2~1.3X, yet with much better scalability.
文章编号： 中图分类号： 文献标志码：
基金项目:国家自然科学基金（91318301）；中国科学院战略性科技先导专项（XDA06010600）
引用文本：
张营飞,谢淼,张珩,杨秋松.以状态子集为中心的并行模型检测算法.计算机系统应用,2016,25(10):129-136
ZHANG Ying-Fei,XIE Miao,ZHANG Heng,YANG Qiu-Song.Parallel Model Checking Algorithm Based on State Subset.COMPUTER SYSTEMS APPLICATIONS,2016,25(10):129-136
张营飞,谢淼,张珩,杨秋松.以状态子集为中心的并行模型检测算法.计算机系统应用,2016,25(10):129-136
ZHANG Ying-Fei,XIE Miao,ZHANG Heng,YANG Qiu-Song.Parallel Model Checking Algorithm Based on State Subset.COMPUTER SYSTEMS APPLICATIONS,2016,25(10):129-136
