Abstract
This paper presents regular hashing functions. Used in conjunction with differential computation process, regular hashing functions enable searching time of global state to be optimized. After a formal definition of the regular property for hashing functions, we propose a characterization of this property. Then the formal definition of differential hashing function is given. Next, we show the performance acceleration produced by the precomputed differential computation process applied to three hashing functions commonly used. The observed accelerations can be significant because the complexity of proposed implementation is independent of key length or respectively of item difference contrary to the usual or respectively differential implementations. Last we study the performances of precomputed differential hashing computation process on reachability graph exploration of distributed systems specified by Petri net using the Bouster tool, and on state space exploration of protocols specified by Lotos using the Open/Caesar environment.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
B.Algayres, & all, “Vesar: a Pragmatic Approach to Formal Specification and Verification”, Computer Network and ISDN Systems, vol 25 nℴ7, February 1991.
B.Bonafos, E.Domingo, “Leda: Structured Language for Automata Description and Verification”, rapp. de recherche, Bordeaux-France, June 1990.
C.Campergue, C.Nouaille, “Bouster: génération parallèle du graphe des marquages accessibles”, rapport ENSERB, Bordeaux-France, Juin 1992.
B.Cousin, “Differential Hashing Functions: Application to Reachability Graph Generation”. ICCI'93. Sudbury — Canada, 26–29 May 1993.
B.Cousin, “Les fonctions de hachage différentielles”. CFIP'93. Montréal — Canada, 7–9 septembre 1993. Hermès, p525–541.
G.Deudon, C.Houillon, “Techniques de hachage”, rapport interne ENSERB, Bordeaux-France, Juin 1992.
D.D.Dimitrijevic, M.S. Chen, “Dynamic State Explosion in Quantitative Protocol Analysis”,PSTV-IX, Twente-Netherland, 6–9June 1989.
L.Doldi, P.Gauthier, “Veda-2: Power to the Protocol Designers”, FORTE'92, Lannion-France, 13–16 Octobre 1992.
H.Garavel, J.Sifakis, “Compilation and Verification of Lotos Specifications”, PSTV-X, Ottawa, June 1990.
G.J.Holzmann, “An Improved Protocol Reachability Analysis Technique”, Sofware, Practice and Experience, vol 18 nℴ2, Feb. 1988.
G.J.Holzmann, “Design and Validation of Computer Protocols”, Prentice-Hall, 1991.
D.E.Knuth, “The Art of Computer Programming: Sorting and Searching”, vol 3, Addison-Wesley, 1973.
G.D.Knott, “Hashing Functions”, The Computer Journal, vol 18, nℴ3, August 1975, p265–278.
V.Y.Lum, P.S.T.Yuen, M.Dodd, “Key-to-Adress Transform Techniques: a Fundamental Performance Study on Large Existing Formatted Files”, Communications of the ACM vol14 nℴ4, April 1971.
C.H.West, “Protocol Validation by Random State Exploration”, PSTV-VI, Montréal — Canada, June 1986.
P.Wolper, D.Leroy, “Reliable Hashing without Collision Detection”, CAV, Elounda — Greece, June 1993.
J.Zhao, G.Bochmann, “Reduced Reachability Analysis of Communication Protocols: a New Approach”, PSTV-VI, Montréal — Canada, June 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousin, B., Hélary, Jm. (1994). Performance improvement of state space exploration by regular & differential hashing functions. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_68
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_68
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive