Abstract
In the past, several attempts have been made to deal with the state space explosion problem by equipping a depth-first search (Dfs) algorithm with a state cache, or by avoiding collision detection, thereby keeping the state hash table at a fixed size. Most of these attempts are tailored specifically for Dfs, and are often not guaranteed to terminate and/or to exhaustively visit all the states. In this paper, we propose a general framework of hierarchical caches which can also be used by breadth-first searches (Bfs). Our method, based on an adequate sampling of Bfs levels during the traversal, guarantees that the Bfs terminates and traverses all transitions of the state space. We define several (static or adaptive) configurations of hierarchical caches and we study experimentally their effectiveness on benchmark examples of state spaces and on several communication protocols, using a generic implementation of the cache framework that we developed within the Cadp toolbox.
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
Behrmann, G., Larsen, K.G., Pelánek, R.: To store or not to store. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 433–445. Springer, Heidelberg (2003)
Blom, S., Calamé, J.R., Lisser, B., Orzan, S., Pang, J., van de Pol, J., Dashti, M.T., Wijs, A.J.: Distributed analysis with μCRL: A compendium of case studies. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 683–689. Springer, Heidelberg (2007)
Blom, S.C.C., Orzan, S.: Distributed State Space Minimization. STTT 7(3), 280–291 (2005)
Chakrabarti, P.P., Ghose, S., Acharya, A., De Sarkas, S.C.: Heuristic Search in Restricted Memory. Artificial Intelligence 41(2), 197–222 (1989)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-Efficient Algorithms for the Verification of Temporal Properties. FMSD 1(2–3), 275–288 (1992)
Della Penna, G., Intrigila, B., Tronci, E., Venturini Zilli, M.: Exploiting Transition Locality in the Disk Based Murphi Verifier. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 202–219. Springer, Heidelberg (2002)
Edelkamp, S., Jabbar, S.: Real-time model checking on secondary storage. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol. 4428, pp. 67–83. Springer, Heidelberg (2007)
Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed Explicit-State Model Checking in the Validation of Communication Protocols. STTT 5(2–3), 247–267 (2004)
Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A.J., Fehnker, A., Aljazzar, H.: Survey on Directed Model Checking. In: Peled, D., Wooldridge, M. (eds.) MoChArt 2008. LNCS (LNAI), vol. 5348, pp. 65–89. Springer, Heidelberg (2009)
Garavel, H.: OPEN/CAESAR: An open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 217–234. Springer, Heidelberg (2001)
Geldenhuys, J.: State caching reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 23–38. Springer, Heidelberg (2004)
Godefroid, P., Holzmann, G.J., Pirottin, D.: State-Space Caching Revisited. FMSD 7(3), 227–241 (1995)
Godefroid, P., Wolper, P.: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 410–429. Springer, Heidelberg (1992)
Hammer, M., Weber, M.: ”To Store or Not To Store” Reloaded: Reclaiming Memory on Demand. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006. LNCS, vol. 4346, pp. 51–66. Springer, Heidelberg (2007)
Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 4th edn. Morgan Kaufmann, San Francisco (2006)
Holzmann, G.J.: Automated Protocol Validation in Argos, assertion proving and scatter searching. IEEE Trans. on Software Engineering 13(6), 683–696 (1987)
Holzmann, G.J.: An Improved Protocol Reachability Analysis Technique. Software - Practice and Experience 18(2), 137–161 (1988)
Jard, C., Jéron, T.: Bounded-memory Algorithms for Verification On-the-fly. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 192–202. Springer, Heidelberg (1992)
Knuth, D.E.: The Art of Computer Programming — Sorting and Searching. Computer Science and Information Processing, vol. III. Addison-Wesley, Reading (1973)
Korf, R.: Depth-First Iterative-Deepening: An Optimal Admissible Tree Search. Artificial Intelligence 27(1), 97–109 (1985)
Korf, R., Zhang, W., Thayer, I., Hohwald, H.: Frontier Search. J. ACM 52(5), 715–748 (2005)
Pelánek, R.: Properties of state spaces and their applications. STTT 10(5), 443–454 (2008)
Russell, S.: Efficient memory-bounded search methods. In: Neumann, B. (ed.) ECAI 1992, pp. 1–5. Wiley, Chichester (1992)
Stern, U., Dill, D.L.: Combining State Space Caching and Hash Compaction. In: 4. GI/ITG/GME Workshop, pp. 81–90. Shaker Verlag, Aachen (1996)
Stern, U., Dill, D.L.: A New Scheme for Memory-Efficient Probabilistic Verification. In: Gotzhein, R., Bredereke, J. (eds.) FORTE 1996, pp. 333–348. Chapman and Hall, Boca Raton (1996)
Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M.: Exploiting Transition Locality in Automatic Verification. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 259–273. Springer, Heidelberg (2001)
Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M.: A Probabilistic Approach to Automatic Verification of Concurrent Systems. In: APSEC 2001, pp. 317–324. IEEE Press, New York (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mateescu, R., Wijs, A. (2009). Hierarchical Adaptive State Space Caching Based on Level Sampling. In: Kowalewski, S., Philippou, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2009. Lecture Notes in Computer Science, vol 5505. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00768-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-00768-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00767-5
Online ISBN: 978-3-642-00768-2
eBook Packages: Computer ScienceComputer Science (R0)