BARNAT, Jiří, Luboš BRIM and Pavel ŠIMEČEK. I/O Efficient Accepting Cycle Detection. In 19th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2007, p. 281-293. ISBN 978-3-540-73367-6. |
Other formats:
BibTeX
LaTeX
RIS
|
Basic information | |
---|---|
Original name | I/O Efficient Accepting Cycle Detection |
Name in Czech | I/O Efektivní detekce akceptujícího cyklu |
Authors | BARNAT, Jiří (203 Czech Republic, guarantor), Luboš BRIM (203 Czech Republic) and Pavel ŠIMEČEK (203 Czech Republic). |
Edition | Berlin, Heidelberg, 19th International Conference on Computer Aided Verification, p. 281-293, 13 pp. 2007. |
Publisher | Springer |
Other information | |
---|---|
Original language | English |
Type of outcome | Proceedings paper |
Field of Study | 10201 Computer sciences, information science, bioinformatics |
Country of publisher | Germany |
Confidentiality degree | is not subject to a state or trade secret |
RIV identification code | RIV/00216224:14330/07:00019426 |
Organization unit | Faculty of Informatics |
ISBN | 978-3-540-73367-6 |
UT WoS | 000248222700029 |
Keywords in English | I/O efficient; accepting cycle detection |
Tags | accepting cycle detection, I/O efficient |
Tags | International impact, Reviewed |
Changed by | Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/6/2009 21:05. |
Abstract |
---|
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. |
Abstract (in Czech) |
---|
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í. |
Links | |
---|---|
GA201/06/1338, research and development project | Name: Automatizovaná verifikace softwaru |
Investor: Czech Science Foundation, Automated software verification | |
MSM0021622419, plan (intention) | Name: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems | |
1ET408050503, research and development project | Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems | |
1M0545, research and development project | Name: Institut Teoretické Informatiky |
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science |
PrintDisplayed: 15/10/2024 16:58