Publication details
Semi
-external LTL Model Checking
| Basic information | |
|---|---|
| Original title: | Semi-external LTL Model Checking |
| Authors: | Stefan Edelkamp, Peter Sanders, Pavel Šimeček |
| Further information | |
|---|---|
| Citation: | EDELKAMP, Stefan - SANDERS, Peter - ŠIMEČEK, Pavel. Semi-external LTL Model Checking. In 20th International Conference on Computer Aided Verification. Berlin, Heidelberg : Springer, 2008. ISBN 978-3-540-70543-7, pp. 530-542. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | semi-external;model checking;external;I/O complexity |
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:
- Techniques for automatic verification and validation of software nad hardware systems
- Highly Parallel and Distributed Computing Systems
- Automated software verification
