I/O Efficient Model Checking
| Authors | |
|---|---|
| Year of publication | 2008 |
| Type | Appeared in Conference without Proceedings |
| MU Faculty or unit | |
| 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: |