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í
Brno, 22 s. Technical Reports, FIMU-RS-2004-09, 2004
Nakladatel
Faculty of Informatics
Další údaje
Jazyk
angličtina
Typ výsledku
Odborná kniha
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Odkazy
Kód RIV
RIV/00216224:14330/04:00010740
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
distributed - memory LTL model checking; accepting predecessors
Štítky
Změněno: 14. 2. 2005 10:48, Mgr. Pavel Moravec
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 |
|