| 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. p. 281-293. ISBN 978-3-540-73367-6. 2007. |
|
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: 19/4/2024 03:45