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%3A00010740" target="_blank" >RIV/00216224:14330/04:00010740 - 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
B - Specialist book
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
ISBN
—
Number of pages
22
Publisher name
Faculty of Informatics
Place of publication
Brno
UT code for WoS book
—