Abstract
A novel, very memory-efficient hash table structure for representing a set of bit vectors — such as the set of reachable states of a system — is presented. Let the length of the bit vectors be w. There is an information-theoretic lower bound on the average memory consumption of any data structure that is capable of representing a set of at most n such bit vectors. We prove that, except in extreme cases, this bound is within 10% of nw – nlog2 n+n. In many cases this is much smaller than what typical implementations of hash tables, binary trees, etc., require, because they already use nw bits for representing just the payload. We give both theoretical and experimental evidence that our data structure can attain an estimated performance of 1.07nw – 1.05nlog2 n + 6.12n, which is close to the lower bound and much better than nw for many useful values of n and w. We show how the data structure can be extended to mappings while retaining its good performance. Furthermore, our data structure is not unduly slow.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
T. M. Cormen, C. E. Leiserson, R. L. Rivest & C. Stein. Introduction to Algorithms, 2nd edition. The MIT Press. 2001.
J. Geldenhuys & P. J. A. de Villiers. Runtime efficient state compaction in Spin. In Proc. 5th Spin Workshop, LNCS #1680, pp. 12–21. Springer-Verlag. 1999.
P. Godefroid, G. J. Holzmann & D. Pirottin. State space caching revisited. In CAV’92: Proc. of the 4th Intl. Conf. on Computer-Aided Verification, LNCS #663, pp. 175–186. Springer-Verlag. 1992.
J. C. Grégoire. State space compression with GETSs. In Proc. 2nd Spin Workshop, Held Aug 1996, DIMACS Series No. 32, pp. 90–108. AMS. 1997.
G. J. Holzmann. On limits and possibilities of automated protocol analysis. In PSTV’87: Proc. 7th Intl. Conf. on Protocol Specification, Testing, and Verification, pp. 339–344. Elsevier. 1987.
G. J. Holzmann, P. Godefroid & D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In PSTV’92: Proc. 12th Intl. Conf. on Protocol Specification, Testing, and Verification, pp. 349–363. Elsevier. 1992.
G. J. Holzmann. State compression in Spin: recursive indexing and compression training runs. In Proc. 3rd Spin Workshop. 1997.
G. J. Holzmann & A. Puri. A minimized automaton representation of reachable states. Software Tools for Technology Transfer, 2(3), pp. 270–278. Springer-Verlag. 1999.
D. E. Knuth. The Art of Computer Programming, Vol. 3: Searching and Sorting. Addison-Wesley. 1973.
A. Papoulis. Poisson Process and Shot Noise. Ch. 16 in Probability, Random Variables, and Stochastic Processes, 2nd ed., pp. 554–576. McGraw-Hill. 1984.
B. Parreaux. Difference compression in Spin. In Proc. 4th Spin Workshop. 1998.
P. E. Pfeiffer & D. A. Schum. Introduction to Applied Probability. Academic Press. 1973.
U. Stern & D. L. Dill. Improved probabilistic verification by hash compaction. In CHARME’95: Advanced Research Working Conf. Correct Hardware Design and Verification Methods, LNCS #987, pp. 206–224. Springer-Verlag. 1995.
W. C. Visser. Memory efficient storage in Spin. In Proc. 2nd Spin Workshop, Held Aug 1996, DIMACS Series No. 32, pp. 21–35. AMS. 1997.
P. Wolper & D. Leroy. Reliable hashing without collision detection. In CAV’93: Proc. of the 5th Intl. Conf. on Computer-Aided Verification, LNCS #697, pp. 59–70. Springer-Verlag. 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geldenhuys, J., Valmari, A. (2003). A Nearly Memory-Optimal Data Structure for Sets and Mappings. In: Ball, T., Rajamani, S.K. (eds) Model Checking Software. SPIN 2003. Lecture Notes in Computer Science, vol 2648. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44829-2_9
Download citation
DOI: https://doi.org/10.1007/3-540-44829-2_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40117-9
Online ISBN: 978-3-540-44829-7
eBook Packages: Springer Book Archive