BARNAT, Jiří, Luboš BRIM a Pavel ŠIMEČEK. I/O Efficient Accepting Cycle Detection. In 19th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2007, s. 281-293. ISBN 978-3-540-73367-6. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | I/O Efficient Accepting Cycle Detection |
Název česky | I/O Efektivní detekce akceptujícího cyklu |
Autoři | BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika) a Pavel ŠIMEČEK (203 Česká republika). |
Vydání | Berlin, Heidelberg, 19th International Conference on Computer Aided Verification, od s. 281-293, 13 s. 2007. |
Nakladatel | Springer |
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/07:00019426 |
Organizační jednotka | Fakulta informatiky |
ISBN | 978-3-540-73367-6 |
UT WoS | 000248222700029 |
Klíčová slova anglicky | I/O efficient; accepting cycle detection |
Štítky | accepting cycle detection, I/O efficient |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 1. 6. 2009 21:05. |
Anotace |
---|
We show how to adapt an existing non-DFS-based accepting cycle detection algorithm OWCTY [10,15,29] to the I/O efficient setting and compare its I/O efficiency and practical performance to the existing I/O efficient LTL model checking approach of Edelkamp and Jabbar [14]. The new algorithm exhibits similar I/O complexity with respect to the size of the graph while it avoids quadratic increase in the size of the graph. Therefore, the number of I/O operations performed is significantly lower and the algorithm exhibits better practical performance. |
Anotace česky |
---|
Výsledkem je adaptace existujícího algoritmu OWCTY pro detekci akceptujících cyklů bez použití DFS na I/O efektivni verzi a porovnání I/O efektivity s existujícím algoritmem pro daný problém publikovaný Edelkampem a Jabbarem v [14]. Nově navržený algoritmus vykazuje podobnou I/O složitost vzhledem k velikosti grafu, ale vyhýbá se kvadratickému nárůstu prohledáváného grafu, která je přítomna v algoritmu Edelkampa a Jabbara a je vynucena technikou převedení detekce cyklů na testování relace dosažitelnosti. Ve skutečnosti tedy nový algoritmus provádí výrazně menší počet I/O operací. |
Návaznosti | |
---|---|
GA201/06/1338, projekt VaV | Název: Automatizovaná verifikace softwaru |
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1ET408050503, projekt VaV | Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 12. 10. 2024 08:20