Technical Reports

The report FIMU-RS-2007-01

LTL model checking with I/O-Efficient Accepting Cycle Detection

by Jiøí Barnat, Lubo¹ Brim, Pavel ©imeèek, January 2007, 20 pages.

FIMU-RS-2007-01. Available as Postscript, PDF.

Abstract:

We show how to adopt existing non-DFS-based algorithm OWCTY for accepting cycle detection to the I/O efficient setting and compare the I/O efficiency and practical performance of the adopted algorithm to the existing I/O efficient LTL model checking approach of Edelkamp et al. We show that while the new algorithm exhibits similar I/O complexity with respect to the size of the graph, it avoids the quadratic increase in the size of the graph of the approach of Edelkamp et al. Therefore, the absolute numbers of I/O operations are significantly smaller and the algorithm exhibits better practical performance.