Bitstate hashing is a
hashing method invented in 1968 by Morris. 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
A hash function is any Function (mathematics), function that can be used to map data (computing), data of arbitrary size to fixed-size values, though there are some hash functions that support variable-length output. The values returned by a ...
.
The result of the function is then taken as the index to an array of bits (a
bit-field
A bit field is a data structure that maps to one or more adjacent bits which have been allocated for specific purposes, so that any single bit or group of bits within the structure can be set or inspected. A bit field is most commonly used to repre ...
), 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 Filter
In computing, a Bloom filter is a space-efficient probabilistic data structure, conceived by Burton Howard Bloom in 1970, that is used to test whether an element is a member of a set. False positive matches are possible, but false negatives ar ...
s.
Use
* Bitstate hashing is utilized in the
SPIN
Spin or spinning most often refers to:
* Spin (physics) or particle spin, a fundamental property of elementary particles
* Spin quantum number, a number which defines the value of a particle's spin
* Spinning (textiles), the creation of yarn or thr ...
model checker for deciding whether a state was already visited by a nested-
depth-first search
Depth-first search (DFS) is an algorithm for traversing or searching tree or graph data structures. The algorithm starts at the root node (selecting some arbitrary node as the root node in the case of a graph) and explores as far as possible al ...
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.
[Holzmann, G. J. (2003) Addison Wesley. ''Spin Model Checker, The: Primer and Reference Manual'']
References
Hash functions