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 条
  • [1] Accepting predecessors are better than back edges in distributed LTL model-checking
    Brim, L
    Cerná, I
    Moravec, P
    Simsa, J
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2004, 3312 : 352 - 366
  • [2] How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
    Brim, L.
    Cerna, I.
    Moravec, P.
    Simsa, J.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 135 (02) : 3 - 18
  • [3] LTL Model-Checking for Malware Detection
    Song, Fu
    Touili, Tayssir
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 416 - 431
  • [4] LTL model-checking for security protocols
    Carbone, Roberto
    AI COMMUNICATIONS, 2011, 24 (03) : 281 - 283
  • [5] LTL Model-Checking for Communicating Concurrent Programs
    Pommellet, Adrien
    Touili, Tayssir
    VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS, 2018, 11181 : 150 - 165
  • [6] Is LTL model-checking effective for Diagnosability Verification?
    Tuxi, Thiago M.
    Carvalho, Lilian K.
    Nunes, Eduardo V. L.
    Da Cunha, Antonio E. C.
    IFAC PAPERSONLINE, 2020, 53 (04): : 256 - 262
  • [7] Scalable multi-core LTL model-checking
    Barnat, J.
    Brim, L.
    Rocksi, P.
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2007, 4595 : 187 - +
  • [8] On the complexity of LTL model-checking of recursive state machines*
    La Torre, Salvatore
    Parlato, Gennaro
    AUTOMATA, LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2007, 4596 : 937 - +
  • [9] Antichains: Alternative algorithms for LTL satisfiability and model-checking
    De Wulf, M.
    Doyen, L.
    Maquet, N.
    Raskin, J. -F.
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 63 - +
  • [10] The Tractability of Model-checking for LTL: The Good, the Bad, and the Ugly Fragments
    Bauland, Michael
    Mundhenk, Martin
    Schneider, Thomas
    Schnoor, Henning
    Schnoor, Ilka
    Vollmer, Heribert
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 277 - 292
123