以状态子集为中心的并行模型检测算法
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(91318301);中国科学院战略性科技先导专项(XDA06010600)


Parallel Model Checking Algorithm Based on State Subset
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 增强出版
  • |
  • 文章评论
    摘要:

    以线性时序逻辑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.

    参考文献
    相似文献
    引证文献
引用本文

张营飞,谢淼,张珩,杨秋松.以状态子集为中心的并行模型检测算法.计算机系统应用,2016,25(10):129-136

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2016-01-29
  • 最后修改日期:2016-03-03
  • 录用日期:
  • 在线发布日期: 2016-10-22
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号