I/O Efficient Model Checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ŠIMEČEK Pavel

Year of publication 2008
Type Appeared in Conference without Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Description One way to increase a memory available to model checking algorithms is to employ the external memory, namely hard disks. Unfortunately, no DFS-based algorithm behaving efficiently in external memory environment is known. We show how to adapt an existing BFS-based accepting cycle detection algorithms OWCTY and MAP to the I/O efficient setting and compare their I/O efficiency and practical performance to the existing I/O efficient LTL model checking approach of Edelkamp and Jabbar. New algorithms exhibit similar I/O complexity with respect to the size of the graph while they avoid quadratic increase in the size of the graph. Therefore, the number of I/O operations performed is significantly lower and the algorithms exhibit better practical performance.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.