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

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:January 29,2016
  • Revised:March 03,2016
  • Adopted:
  • Online: October 22,2016
  • Published:
Article QR Code
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-3
Address:4# South Fourth Street, Zhongguancun,Haidian, Beijing,Postal Code:100190
Phone:010-62661041 Fax: Email:csa (a) iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063