| BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. Brno: Faculty of Informatics, 2004, 22 s. Technical Reports, FIMU-RS-2004-09. |
Další formáty:
BibTeX
LaTeX
RIS
@book{563169,
author = {Brim, Luboš and Černá, Ivana and Moravec, Pavel and Šimša, Jiří},
address = {Brno},
keywords = {distributed - memory LTL model checking; accepting predecessors},
language = {eng},
location = {Brno},
note = {Full version of the FMCAD'04 paper},
publisher = {Faculty of Informatics},
title = {Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.},
url = {http://www.fi.muni.cz/informatics/reports/files/2004/FIMU-RS-2004-09.pdf},
year = {2004}
}
TY - BOOK
ID - 563169
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.
VL - Technical Reports, FIMU-RS-2004-09
PB - Faculty of Informatics
CY - Brno
N1 - Full version of the FMCAD'04 paper
KW - distributed - memory LTL model checking
KW - accepting predecessors
UR - http://www.fi.muni.cz/informatics/reports/files/2004/FIMU-RS-2004-09.pdf
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 a Jiří ŠIMŠA. \textit{Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.}. Brno: Faculty of Informatics, 2004, 22 s. Technical Reports, FIMU-RS-2004-09.
|
