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 条

[21] From Distributed Memory Cycle Detection to Parallel LTL Model Checking
Barnat, J.
Brim, L.
Chaloupka, J.
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 133 : 21 - 39
[22] Model-checking multi-threaded distributed Java']Java programs
Stoller, SD
SPIN MODEL CHECKING AND SOFTWARE VERIFICATON, 2000, 1885 : 224 - 244
[23] Integrated Model-Checking for the Design of Safe and Efficient Distributed Software Commissioning
Coullon, Helene
Jard, Claude
Lime, Didier
INTEGRATED FORMAL METHODS, IFM 2019, 2019, 11918 : 120 - 137
[24] Semi-Distributed LTL Model Checking for Actor Based Modeling Languages
Khamespanah, Ehsan
Razzazi, Mohamadreza
2009 INTERNATIONAL CONFERENCE ON SOFTWARE, TELECOMMUNICATIONS AND COMPUTER NETWORKS, 2009, : 265 - 269
[25] Timing analysis of distributed end-to-end task graphs with model-checking
Gu, Z
EMBEDDED AND UBIQUITOUS COMPUTING - EUC 2005, 2005, 3824 : 214 - 223
[26] Model-checking distributed real-time systems with states, events, and multiple fairness assumptions
Wang, F
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 553 - 567

← 1 2 3 →