Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{569568,
author = {Moravec, Pavel},
address = {Bruxelles, Belgium},
booktitle = {MOVEP'04: 6th school on MOdeling and VErifying parallel Processes},
keywords = {LTL model checking; distributed algorithm},
language = {eng},
location = {Bruxelles, Belgium},
pages = {122-129},
publisher = {Universite Libre de Bruxelles},
title = {Using Accepting Predecessors in Distributed LTL Model-Checking},
year = {2004}
}
TY - JOUR
ID - 569568
AU - Moravec, Pavel
PY - 2004
TI - Using Accepting Predecessors in Distributed LTL Model-Checking
PB - Universite Libre de Bruxelles
CY - Bruxelles, Belgium
KW - LTL model checking
KW - distributed algorithm
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. The influence of the ordering on the algorithm performance is open as future work.
ER -
MORAVEC, Pavel. Using Accepting Predecessors in Distributed LTL Model-Checking. In \textit{MOVEP'04: 6th school on MOdeling and VErifying parallel Processes}. Bruxelles, Belgium: Universite Libre de Bruxelles. s.~122-129, 7 s. 2004.
|
