Bitstate hashing

Bitstate hashing is a hashing method invented in 1968 by Morris.^[1] It is used for state hashing, where each state (e.g. of an automaton) is represented by a number and it is passed to some hash function.

The result of the function is then taken as the index to an array of bits (a bit-field), where one looks for 1 if the state was already seen before or stores 1 by itself if not.

It usually serves as a yes–no technique without a need of storing whole state bit representation.

A shortcoming of this framework is losing precision like in other hashing techniques. Hence some tools use this technique with more than one hash function so that the bit-field gets widened by the number of used functions, each having its own row. And even after all functions return values (the indices) point to fields with contents equal to 1, the state may be uttered as visited with much higher probability.

Bitstate Hashing, although proposed earlier in time, is an application of Bloom Filters.^[2]

Use

Bitstate hashing is utilized in the SPIN model checker for deciding whether a state was already visited by a nested-depth-first search algorithm or not. This purportedly led to memory savings of 98% in the case of using one hash function (175 MB to 3 MB) and 92% when two hash functions are used (13 MB). The state coverage dropped to 97% in the former case. ^[3]

References

^ Morris, R. (1968). Scatter Storage Techniques
^ Edelkamp, S., & Stein, B. (Eds.). (2004). New Results in Planning, Scheduling, and Design (Puk2004): Workshop; Proceedings. Universität Ulm.
^ Holzmann, G. J. (2003) Addison Wesley. Spin Model Checker, The: Primer and Reference Manual

[1] Morris, R. (1968). Scatter Storage Techniques

[2] Edelkamp, S., & Stein, B. (Eds.). (2004). New Results in Planning, Scheduling, and Design (Puk2004): Workshop; Proceedings. Universität Ulm.

[3] Holzmann, G. J. (2003) Addison Wesley. Spin Model Checker, The: Primer and Reference Manual

[1]

[2]

[3]