Access Restriction

Author Visser, Willem ♦ Barringer, Howard
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Obdd State Store ♦ Memory Efficient State Storage ♦ Ordered Binary Decision Diagram ♦ State Compression Technique ♦ Partial Order ♦ Compressed Representation ♦ Visited State ♦ Compression Technique ♦ On-the-fly Model Checking ♦ Experimental Implementation ♦ Time Usage ♦ Spin Validation Tool ♦ Traditional Hash Table State Store ♦ Reachability Analysis ♦ Space Efficiency ♦ Unique State
Abstract The use of an Ordered Binary Decision Diagram (OBDD) to store all visited states during on-the-fly model checking (or reachability analysis) is investigated. To improve the time and space efficiency 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.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Publisher Date 1995-01-01