BARNAT, Jiří, Luboš BRIM, Pavel ŠIMEČEK a Michael WEBER. Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2008. s. 48-62, 15 s. ISBN 978-3-540-78799-0.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking
Název česky Odolnost vůči znovu-navštívení zrychluje I/O efektivní ověřování modelu
Autoři BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika), Pavel ŠIMEČEK (203 Česká republika) a Michael WEBER (528 Nizozemsko).
Vydání Berlin, Heidelberg, Tools and Algorithms for the Construction and Analysis of Systems, od s. 48-62, 15 s. 2008.
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í
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/08:00024177
Organizační jednotka Fakulta informatiky
ISBN 978-3-540-78799-0
ISSN 0302-9743
UT WoS 000254735100005
Klíčová slova anglicky I/O efficient; accepting cycle detection; revisiting resistance
Štítky accepting cycle detection, I/O efficient, revisiting resistance
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 30. 3. 2010 09:16.
Anotace
Revisiting resistance graph algorithms are those, whose correctness is not vulnerable to repeated edge exploration. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.
Anotace česky
Korektnost některý grafových algoritmů je nezávislá od počtu vykonání, potažmo opakování, akcí spojených s průzkumem jedné hrany grafu. Takové algoritmy nazýváme RR-algorimty. V článku je ukázáno, že této vlastnosti algoritmů lze využít pro výrazné zrychlení výpočtu algoritmu v kontextu algoritmů používajících při výpočtu externí paměť (tj. disk).
Návaznosti
GA201/06/1338, projekt VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET400300504, projekt VaVNázev: Realistická aplikace formálních metod v komponentových systémech
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 18. 1. 2020 18:14