ČERNÁ, Ivana a Radek PELÁNEK. Distributed Explicit Fair Cycle Detection. In SPIN Workshop 2003. Portland (Oregon, USA): Springer-Verlag, 2003, s. 49-74, 25 s. ISBN 3-540-40117-2.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Distributed Explicit Fair Cycle Detection
Autoři ČERNÁ, Ivana (203 Česká republika, garant) a Radek PELÁNEK (203 Česká republika).
Vydání Portland (Oregon, USA), SPIN Workshop 2003, od s. 49-74, 25 s. 2003.
Nakladatel Springer-Verlag
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/03:00008589
Organizační jednotka Fakulta informatiky
ISBN 3-540-40117-2
UT WoS 000183490400004
Klíčová slova anglicky distributed model checking; cycle detection
Štítky cycle detection, distributed model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 8. 6. 2009 16:11.
Anotace
The fair cycle detection problem is at the heart of both LTL and fair CTL model checking. This paper presents a new distributed scalable algorithm for explicit fair cycle detection. Our method combines the simplicity of the distribution of explicitly presented data structure and the features of symbolic algorithm allowing for an efficient parallelisation. If a fair cycle (i.e. counterexample) is detected, then the algorithm produces a cycle, which is in general shorter than that produced by depth-first search based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.
Návaznosti
GA201/03/0509, projekt VaVNázev: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 143300001, záměrNázev: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů
VytisknoutZobrazeno: 4. 5. 2024 02:39