Skip to main content
SpringerLink
Log in

Search-Order Independent State Caching

  • Chapter
Book cover Transactions on Petri Nets and Other Models of Concurrency IV

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 6550))

Abstract

State caching is a memory reduction technique used by model checkers to alleviate the state explosion problem. It has traditionally been coupled with a depth-first search to ensure termination. We propose and experimentally evaluate an extension of the state caching method for general state exploring algorithms that are independent of the search order (i.e., search algorithms that partition the state space into closed (visited) states, open (to visit) states and unmet states).

Supported by the Danish Research Council for Technology and Production.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bao, T., Jones, M.: Time-Efficient Model Checking with Magnetic Disk. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 526–540. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P.: DiVinE – A Tool for Distributed Verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 278–281. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Bošnački, D., Elkind, E., Genest, B., Peled, D.: On Commutativity Based Edge Lean Search. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 158–170. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Bošnački, D., Leue, S., Lafuente, A.L.: Partial-Order Reduction for General State Exploring Algorithms. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 271–287. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. DVE Language, http://divine.fi.muni.cz/page.php?page=language

  8. Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed Explicit-State Model Checking in the Validation of Communication Protocols. STTT 5, 247–267 (2004)

    Article  MATH  Google Scholar 

  9. Evangelista, S., Kristensen, L.M.: Search-Order Independent State Caching. Technical report (2009), http://daimi.au.dk/~evangeli/doc/caching.pdf

  10. Evangelista, S., Pradat-Peyre, J.-F.: Memory Efficient State Space Storage in Explicit Software Model Checking. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 43–57. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Geldenhuys, J.: State Caching Reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 23–38. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  13. Godefroid, P., Holzmann, G.J., Pirottin, D.: State-Space Caching Revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 178–191. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  14. Holzmann, G.J.: Tracing Protocols. AT&T Technical J. 64(10), 2413–2434 (1985)

    Article  Google Scholar 

  15. Holzmann, G.J.: Automated Protocol Validation in Argos: Assertion Proving and Scatter Searching. IEEE Trans. Software Eng. 13(6), 683–696 (1987)

    Article  Google Scholar 

  16. Holzmann, G.J.: State Compression in Spin: Recursive Indexing and Compression Training Runs. In: SPIN 1997 (1997)

    Google Scholar 

  17. Jard, C., Jéron, T.: On-Line Model Checking for Finite Linear Temporal Logic Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 189–196. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Jensen, K., Kristensen, L.M.: Coloured Petri Nets — Modeling and Validation of Concurrent Systems. Springer, Heidelberg (2009)

    Book  MATH  Google Scholar 

  20. Kristensen, L.M., Mailund, T.: A Generalised Sweep-Line Method for Safety Properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549–567. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Mateescu, R., Wijs, A.: Hierarchical Adaptive State Space Caching Based on Level Sampling. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 215–229. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Pelánek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  23. Pelánek, R., Rosecký, V., Sedenka, J.: Evaluation of State Caching and State Compression Techniques. Technical report, Masaryk University, Brno (2008)

    Google Scholar 

  24. Stern, U., Dill, D.L.: Parallelizing the Murphi Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–278. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  25. 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–274. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  26. Westergaard, M., Evangelista, S., Kristensen, L.M.: ASAP: An Extensible Platform for State Space Analysis. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 303–312. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  27. Westergaard, M., Kristensen, L.M., Brodal, G.S., Arge, L.: The ComBack Method – Extending Hash Compaction with Backtracking. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 445–464. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Aarhus University, Denmark

    Sami Evangelista

  2. LIPN, Université Paris 13, France

    Sami Evangelista

  3. Department of Computer Engineering, Bergen University College, Norway

    Lars Michael Kristensen

Authors
  1. Sami Evangelista
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lars Michael Kristensen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Aarhus, Faculty of Science, IT-parken, Aabogade 34, 8200, Aarhus N, Denmark

    Kurt Jensen

  2. Computer Science Department, University of Turin, Corso Svizzera 185, 10149, Turin, Italy

    Susanna Donatelli

  3. School of Computing Science, Newcastle upon Tyne, Newcastle University, NE1 7RU, UK

    Maciej Koutny

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Evangelista, S., Kristensen, L.M. (2010). Search-Order Independent State Caching. In: Jensen, K., Donatelli, S., Koutny, M. (eds) Transactions on Petri Nets and Other Models of Concurrency IV. Lecture Notes in Computer Science, vol 6550. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18222-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-18222-8_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-18221-1

  • Online ISBN: 978-3-642-18222-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation