I/O Efficient Accepting Cycle Detection

• Authors: BARNAT Jiří; BRIM Luboš; ŠIMEČEK Pavel
• Year of publication: 2007
• Type: Article in Proceedings
• Conference: 19th International Conference on Computer Aided Verification
• MU Faculty or unit: Faculty of Informatics
• Field: Informatics
• Keywords: I/O efficient; accepting cycle detection
• Description: 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.

Related projects

• Techniques for automatic verification and validation of software nad hardware systems
• Institute for Theoretical Computer Science
• Highly Parallel and Distributed Computing Systems
• Automated software verification