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.
Use
- It is utilized in SPIN model checker for decision whether a state was already visited by nested-depth-first search searching algorithm or not. They mention savings of 98% of memory 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. [2]
References
- ↑ Morris, R. (1968). Scatter Storage Techniques
- ↑ Holzmann, G. J. (2003) Addison Wesley. Spin Model Checker, The: Primer and Reference Manual