Memory efficient state storage in SPIN
Willem I. Visser, Howard Barringer · DIMACS series in discrete mathematics and theoretical computer science · 1997
The use of an Ordered Binary Decision Diagram (OBDD) to store all visited states during on-they model checking (or reachability analysis) is investigated. To improve the time and space e ciency a state compression technique is introduced. This compression technique is safe, in the sense that no two unique states will have the same compressed representation. A number of examples are used to evaluate an experimental implementation of the OBDD state store within the SPIN validation tool. In all the examples a reduction in space is achieved when using the OBDD state store as opposed to the more traditional hash table state store. The memory and time usage when combining partial orders with the OBDD state store is also considered.