Semi-external LTL 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

EDELKAMP Stefan SANDERS Peter ŠIMEČEK Pavel

Year of publication 2008
Type Article in Proceedings
Conference 20th International Conference on Computer Aided Verification
MU Faculty or unit

Faculty of Informatics

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:

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