| BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC and Jiří ŠIMŠA. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In Formal Methods in Computer-Aided Design (FMCAD). Neuveden: Springer-Verlag, LNCS 3312, 2004, p. 352-366, 24 pp. ISBN 3-540-23738-0. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{561310,
author = {Brim, Luboš and Černá, Ivana and Moravec, Pavel and Šimša, Jiří},
address = {Neuveden},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
keywords = {distributed - memory LTL model checking; graph predecessors},
language = {eng},
location = {Neuveden},
isbn = {3-540-23738-0},
pages = {352-366},
publisher = {Springer-Verlag, LNCS 3312},
title = {Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.},
year = {2004}
}
TY - JOUR
ID - 561310
AU - Brim, Luboš - Černá, Ivana - Moravec, Pavel - Šimša, Jiří
PY - 2004
TI - Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
PB - Springer-Verlag, LNCS 3312
CY - Neuveden
SN - 3540237380
KW - distributed - memory LTL model checking
KW - graph predecessors
N2 - We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations 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.
ER -
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC and Jiří ŠIMŠA. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In \textit{Formal Methods in Computer-Aided Design (FMCAD)}. Neuveden: Springer-Verlag, LNCS 3312, 2004, p.~352-366, 24 pp. ISBN~3-540-23738-0.
|
