Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F04%3A00010529" target="_blank" >RIV/00216224:14330/04:00010529 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
Original language description
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 thesubsequent 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.
Czech name
Akceptující předchůdci v distrubuovaném LTL ověřování modelů
Czech description
Článek prezentuje nový distribuovaný algoritmus pro ověřování LTL vlastností založený na akceptujících předchůdcích. Je prezentováné několik optimalizací a experimentální výsledky
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2004
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Formal Methods in Computer-Aided Design (FMCAD)
ISBN
3-540-23738-0
ISSN
—
e-ISSN
—
Number of pages
24
Pages from-to
352-366
Publisher name
Springer-Verlag, LNCS 3312
Place of publication
Neuveden
Event location
Austin, USA
Event date
Jan 1, 2004
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—