Skip to main content
SpringerLink
Log in

Typical Structural Properties of State Spaces

  • Conference paper
Model Checking Software (SPIN 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2989))

Included in the following conference series:

Abstract

Explicit model checking algorithms explore the full state space of a system. We have gathered a large collection of state spaces and performed an extensive study of their structural properties. The results show that state spaces have several typical properties and that they differ significantly from both random graphs and regular graphs. We point out how to exploit these typical properties in practical model checking algorithms.

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. http://www.fi.muni.cz/~xpelanek/state_spaces

  2. Barabasi, A.L.: Linked: How Everything Is Connected to Everything Else and What It Means, Plume (2003)

    Google Scholar 

  3. Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL modelchecking. In: Proc. Automated Software Engineering (ASE 2003), pp. 106–115. IEEE Computer Society, Los Alamitos (2003)

    Chapter  Google Scholar 

  4. 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 

  5. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Černá, I., Pelánek, R.: Distributed explicit fair cycle detection. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 49–73. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured petri nets exploiting strongly connected components. In: Proc. International Workshop on Discrete Event Systems, pp. 169–177 (1996)

    Google Scholar 

  8. 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 

  9. David, A., Behrmann, G., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 225–229. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol verification as a hardware design aid. In: Proc. Computer Design: VLSI in Computers and Processors, pp. 522–525. IEEE Computer Society, Los Alamitos (1992)

    Chapter  Google Scholar 

  11. Erdős, P., Renyi, A.: On random graphs. Publ. Math. 6, 290–297 (1959)

    Google Scholar 

  12. Fisler, K., Fraer, R., Kamhi, G., Vardi, Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 420–434. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Benchmarking finite-state verifiers. International Journal on Software Tools for Technology Transfer (STTT) 2(4), 317–320 (2000)

    Google Scholar 

  14. Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter 4, 13–24 (2002)

    Google Scholar 

  15. Godefroid, P., Holzmann, G.J., Pirottin, D.: State space caching revisited. Formal Methods in System Design 7(3), 227–241 (1995)

    Article  Google Scholar 

  16. Groote, J.F., Ponse, A.: The syntax and semantics of μCRL. In: Algebra of Communicating Processes 1994. Workshops in Computing Series, pp. 26–62 (1995)

    Google Scholar 

  17. Groote, J.F., van Ham, F.: Large state space visualization. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 585–590. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Holzmann, G.J.: An analysis of bitstate hashing. In: Proc. Protocol Specification, Testing, and Verification, INWG/IFIP, pp. 301–314 (1995)

    Google Scholar 

  19. Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proc. SPIN Workshop, Twente Univ. (1997)

    Google Scholar 

  20. Holzmann, G.J.: Algorithms for automated protocol verification. AT&T Technical Journal 69(2), 32–44 (1990)

    Google Scholar 

  21. Holzmann, G.J.: The engineering of a model checker: the gnu i-protocol case study revisited. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 232–244. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  22. Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)

    Google Scholar 

  23. Lafuente, A.L.: Simplified distributed LTL model checking by localizing cycles. Technical Report 176, Institut für Informatik, Universität Freiburg (July 2002)

    Google Scholar 

  24. Penna, G.D., Intrigila, B., Tronci, E., Zilli, M.V.: 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)

    Chapter  Google Scholar 

  25. Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 143–160. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  26. Ruys, T.C.: Low-fat recipes for SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 287–321. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic SCC hull algorithms. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 88–105. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  28. Stern, U.: Algorithmic Techniques in Verification by Explicit State Enumeration. PhD thesis, Technical University of Munich (1997)

    Google Scholar 

  29. Stern, U., Dill, D.L.: Using magnatic disk instead of main memory in the Murphi verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 172–183. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  30. Tronci, E., Penna, G.D., Intrigila, B., Venturini, M.: A probabilistic approach to automatic verification of concurrent systems. In: Proc. Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 317–324. IEEE Computer Society, Los Alamitos (2001)

    Google Scholar 

  31. Tronci, E., Penna, G.D., Intrigila, B., Zilli, M.V.: 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 

  32. Watts, D.J.: Six Degrees: The Science of a Connected Age. W.W. Norton & Company, New York (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic

    Radek Pelánek

Authors
  1. Radek Pelánek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. VERIMAG, 2 Avenue de Vignate, Centre Equitation, 38610, Grenoble-Gières, France

    Susanne Graf

  2. Vérimag Laboratory, 2 avenue de Vignate, 38610, Gières, France

    Laurent Mounier

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pelánek, R. (2004). Typical Structural Properties of State Spaces. In: Graf, S., Mounier, L. (eds) Model Checking Software. SPIN 2004. Lecture Notes in Computer Science, vol 2989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24732-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24732-6_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21314-7

  • Online ISBN: 978-3-540-24732-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation