2004
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠAZákladní údaje
Originální název
Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking.
Název česky
Akceptující předchůdci v distrubuovaném LTL ověřování modelů
Autoři
BRIM, Luboš (203 Česká republika, garant), Ivana ČERNÁ (203 Česká republika), Pavel MORAVEC (203 Česká republika) a Jiří ŠIMŠA (203 Česká republika)
Vydání
Neuveden, Formal Methods in Computer-Aided Design (FMCAD), od s. 352-366, 24 s. 2004
Nakladatel
Springer-Verlag, LNCS 3312
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/04:00010529
Organizační jednotka
Fakulta informatiky
ISBN
3-540-23738-0
UT WoS
000226785300025
Klíčová slova anglicky
distributed - memory LTL model checking; graph predecessors
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 8. 6. 2009 16:08, prof. RNDr. Ivana Černá, CSc.
V originále
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.
Česky
Č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
Návaznosti
| GA201/03/0509, projekt VaV |
| ||
| MSM 143300001, záměr |
|