2004
Using Accepting Predecessors in Distributed LTL Model-Checking
MORAVEC, PavelZákladní údaje
Originální název
Using Accepting Predecessors in Distributed LTL Model-Checking
Název česky
Použití akceptujících předchůdců u distribuovaného ověřování LTL vlastností modelu
Autoři
MORAVEC, Pavel (203 Česká republika, garant)
Vydání
Bruxelles, Belgium, MOVEP'04: 6th school on MOdeling and VErifying parallel Processes, od s. 122-129, 7 s. 2004
Nakladatel
Universite Libre de Bruxelles
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Belgie
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/04:00011071
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
LTL model checking; distributed algorithm
Změněno: 1. 4. 2005 09:08, 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. The influence of the ordering on the algorithm performance is open as future work.
Česky
Prezentujeme nový algoritmus s distribuovanou pamětí pro ověřování LTL vlastností modelu, který je navržen pro síť počítačů komunikujících pomocí MPI. Detekce akceptujících cyklů je založena na počítání největších akceptujících předchůdců a na následném rozkladu grafu na nezávislé předchůdcovské podgrafy indukované největšími akceptujícími předchůdci. Vliv uspořádání vrcholů na chování algoritmu je otevřena jako budoucí práce.
Návaznosti
| GA201/03/0509, projekt VaV |
| ||
| MSM 143300001, záměr |
|