Semi-External LTL Model Checking
| Authors | |
|---|---|
| Year of publication | 2008 |
| Type | Conference abstract |
| MU Faculty or unit | |
| Citation | |
| 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: In comparison to former external memory algorithms, the new algorithm is faster, but its internal memory complexity is proportional to the size of a state space. 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. Perfect hash function construction is based on the algorithm by Botelho et al. With perfect hash function, the search itself stores only one bit per vertex denoting which vertices have already been visited. Since storage of the perfect hash function takes also only the constant number of bits per state, the overall number of bits per state is constant. 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: |