Semi-external LTL Model Checking
| Authors | |
|---|---|
| Year of publication | 2008 |
| Type | Article in Proceedings |
| Conference | 20th International Conference on Computer Aided Verification |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | semi-external;model checking;external;I/O complexity |
| Description | In this paper we establish c-bit semi-external graph algorithms, - i.e., algorithms which need only a constant number c of bits per vertex in the internal memory. In this setting, we obtain new trade-offs between time and space for I/O efficient LTL model checking. First, we design a c-bit semi-external algorithm for depth-first search. To achieve a low internal memory consumption, we construct a RAM-efficient perfect hash function from the vertex set stored on disk. We give a similar algorithm for double depth-first search, which checks for presence of accepting cycles and thus solves the LTL model checking problem. The I/O complexity of the search itself is proportional to the time for scanning the search space. For on-the-fly model checking we apply iterative-deepening strategy known from bounded model checking. |
| Related projects: |