Parallel Breadth-First Search LTL Model-Checking

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F03%3A00009034" target="_blank" >RIV/00216224:14330/03:00009034 - isvavai.cz</a>
Alternative codes found
RIV/00216224:14330/03:00008593
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Parallel Breadth-First Search LTL Model-Checking
Original language description
We propose a practical parallel on-the-fly algorithm for enumerative LTL model-checking. The algorithm is designed for a cluster of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level-synchronized breadth-first search of the graph is performed to discover back-level edges. For each level the back-level edges are checked in parallel by a nested depth-first search to confirm or refute the presence ofa cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental implementation of the algorithm shows promising results.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automated Verification of Parallel and Distributed Systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2003
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
18th IEEE International Conference on Automated Software Engineering (ASE'03)
ISBN
0-7695-2035-9
ISSN
—
e-ISSN
—
Number of pages
10
Pages from-to
106-115
Publisher name
IEEE Computer Society
Place of publication
Montreal
Event location
Montreal, Canada
Event date
Jan 1, 2003
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)