Accepting predecessors are better than back edges in distributed LTL model-checking

被引：0
|
作者：
Brim, L [1 ]
Cerná, I [1 ]
Moravec, P [1 ]
Simsa, J [1 ]
机构：
[1] Masaryk Univ, Dept Comp Sci, Fac Informat, Brno, Czech Republic
来源：
FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS | 2004年 / 3312卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of work-stations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.
引用
收藏
页码：352 / 366
页数：15
相关论文
共 26 条
  • [11] Parallel breadth-first search LTL model-checking
    Barnat, J
    Brim, L
    Chaloupka, J
    18TH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2003, : 106 - 115
  • [12] Distributed LTL Model Checking with Hash Compaction
    Barnat, J.
    Havlicek, J.
    Rockai, P.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2013, 296 : 79 - 93
  • [13] Model-checking Distributed Components: The Vercors Platform
    Barros, Tomas
    Cansado, Antonio
    Madelaine, Eric
    Rivera, Marcela
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 182 : 3 - 16
  • [14] When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
    Demri, Stephane
    Sangnier, Arnaud
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2010, 6014 : 176 - +
  • [15] Distributed colored petri net model-checking with CYCLADES
    Pajault, Christophe
    Pradat-Peyre, Jean-Francois
    FORMAL METHODS: APPLICATIONS AND TECHNOLOGY, 2007, 4346 : 347 - +
  • [16] Simple is better: Efficient bounded model checking for past LTL
    Latvala, T
    Biere, A
    Heljanko, K
    Junttila, T
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2005, 3385 : 380 - 395
  • [17] Distributed breadth-first search LTL model checking
    Jiří Barnat
    Ivana Černá
    Formal Methods in System Design, 2006, 29 : 117 - 134
  • [18] Distributed Firewall Anomaly Detection Through LTL Model Checking
    Halle, Sylvain
    Ngoupe, Eric Lunaud
    Villemaire, Roger
    Cherkaoui, Omar
    2013 IFIP/IEEE INTERNATIONAL SYMPOSIUM ON INTEGRATED NETWORK MANAGEMENT (IM 2013), 2013, : 194 - 201
  • [19] Distributed breadth-first search LTL model checking
    Barnat, Jiri
    Cerna, Ivana
    FORMAL METHODS IN SYSTEM DESIGN, 2006, 29 (02) : 117 - 134
  • [20] Model-checking multi-threaded distributed Java programs
    Stoller S.D.
    International Journal on Software Tools for Technology Transfer, 2002, 4 (01) : 71 - 91
123