I/O Efficient Accepting Cycle Detection

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.

Basic information

Original name

I/O Efficient Accepting Cycle Detection

Name in Czech

I/O Efektivní detekce akceptujícího cyklu

Authors

BARNAT, Jiří; Luboš BRIM and Pavel ŠIMEČEK

Edition

Berlin, Heidelberg, 19th International Conference on Computer Aided Verification, p. 281-293, 13 pp. 2007

Publisher

Springer

---

Other information

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

---

Abstract

In the original language

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.

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