Flash-Efficient LTL Model Checking with Minimal Counterexamples

Solid state disks based on flash memory are an apparent alternative to hard disks for external memory search. Random reads are much faster, while random writes are generally not. In this paper, we illustrate how this influences the time-space trade-offs for scaling semi-external LTL model checking algorithms that request a constant number of bits per state in internal, and full state vectors on external memory. We invent a complexity model to analyze the effect of outsourcing the perfect hash function from random access to flash memory. In this model a 1-bit semi-external I/O efficient LTL model checking algorithm is proposed that generates minimal counterexamples.