Efficient Path Finding with the Sweep-Line Method Using External Storage

Abstract

The sweep-lino method deletes states on-the-fly during state space exploration to reduce peak memory usage. This deletion of states prohibits the immediate generation of, e.g., an error-trace when the violation of a safety property is detected. We address this problem by combining the sweep-line method with storing a spanning tree of the explored state space in external storage on a magnetic disk. We show how this allows us to easily obtain paths in the state space, such as error-traces. A key property of the proposed technique is that it avoids searching in external storage during the state space exploration and gives the same reduction in peak memory usage as the stand-alone sweep-line method. We evaluate the proposed technique on a number of example systems, and compare its performance to a related technique. These practical experiments demonstrate how the suggested technique complements existing techniques based on using external storage. © Springer-Verlag 2003.