Skip to main content
SpringerLink
Log in

Optimal Storage of Combinatorial State Spaces

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10811))

Included in the following conference series:

Abstract

Efficiently deciding reachability for model checking problems requires storing the entire state space. We provide an information theoretical lower bound for these storage requirements and demonstrate how it can be reached using a binary tree in combination with a compact hash table. Experiments confirm that the lower bound is reached in practice in a majority of cases, confirming the combinatorial nature of state spaces.

This work is part of the research programme VENI with project number 639.021.649, which is (partly) financed by the Netherlands Organisation for Scientific Research (NWO).

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 EPUB and 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

Notes

  1. 1.

    We opt to order vectors as follows: variables and program counter of Process 0 (\( pc _0\)), variables and program counter of Process 1 (\( pc _1\)), etc. Section 6 discusses the effect of orderings.

  2. 2.

    The assumption that predecessor is always known of course breaks down for the initial state \(\iota \). Our model does not account for the initial storage required for \(\iota \). However, as the number of states \(\left| {V}\right| \) typically grows very large, this space is negligible.

  3. 3.

    [21] explains in detail how this can be achieved.

  4. 4.

    Solely assumed to simplify the formulae below.

  5. 5.

    The DVE models are translated to Promela and we only selected those (76/267) which preserved state count. This comparison can be examined interactively at http://fmt.ewi.utwente.nl/tools/ltsmin/performance/ (select LTSmin-cleary-dfs).

References

  1. Baranová, Z., Barnat, J., Kejstová, K., Kučera, T., Lauko, H., Mrázek, J., Ročkai, P., Štill, V.: Model checking of C and C++ with DIVINE 4. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 201–207. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_14

    Chapter  Google Scholar 

  2. van der Berg, F., Laarman, A.: SpinS: extending LTSmin with Promela through SpinJa. ENTCS 296, 95–105 (2013)

    Google Scholar 

  3. Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_31

    Chapter  Google Scholar 

  4. Blom, S., Lisser, B., van de Pol, J., Weber, M.: A database approach to distributed state space generation. ENTCS 198(1), 17–32 (2008)

    MathSciNet  MATH  Google Scholar 

  5. Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45, 993–1002 (1996)

    Article  MATH  Google Scholar 

  6. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  7. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. In: LICS, pp. 428–439 (1990)

    Google Scholar 

  8. Cleary, J.G.: Compact hash tables using bidirectional linear probing. IEEE Trans. Comput. C-33(9), 828–834 (1984)

    Google Scholar 

  9. Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199–213. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_15

    Chapter  Google Scholar 

  10. Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_25

    Chapter  Google Scholar 

  11. Evangelista, S., Kristensen, L.M., Petrucci, L.: Multi-threaded explicit state space exploration with state reconstruction. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 208–223. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_16

    Chapter  Google Scholar 

  12. Geldenhuys, J., Valmari, A.: A nearly memory-optimal data structure for sets and mappings. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 136–150. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44829-2_9

    Chapter  Google Scholar 

  13. Holzmann, G.J.: An analysis of bitstate hashing. In: Dembiński, P., Średniawa, M. (eds.) PSTV 1995. IFIPAICT, pp. 301–314. Springer, Boston (1996). https://doi.org/10.1007/978-0-387-34892-6_19

    Chapter  Google Scholar 

  14. Holzmann, G.J.: State compression in SPIN: recursive indexing and compression training runs. In: Proceedings of 3rd International SPIN Workshop (1997)

    Google Scholar 

  15. Holzmann, G.J.: The model checker SPIN. IEEE TSE 23, 279–295 (1997)

    Google Scholar 

  16. Jensen, P.G., Larsen, K.G., Srba, J.: PTrie: data structure for compressing and storing sets via prefix sharing. In: Hung, D., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 248–265. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67729-3_15

    Chapter  Google Scholar 

  17. Jensen, P.G., Larsen, K.G., Srba, J., Sørensen, M.G., Taankvist, J.H.: Memory efficient data structures for explicit verification of timed systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 307–312. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_26

    Chapter  Google Scholar 

  18. Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_61

    Google Scholar 

  19. Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 489–507. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0013032

    Chapter  Google Scholar 

  20. Kordon, F., et al.: Complete results for the 2016 edition of the model checking contest, June 2016. http://mcc.lip6.fr/2016/results.php

  21. Laarman, A., van de Pol, J., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 38–56. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22306-8_4

    Chapter  Google Scholar 

  22. Laarman, A., van de Pol, J., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506–511. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_40

    Chapter  Google Scholar 

  23. Laarman, A.: Scalable multi-core model checking. Ph.D. thesis, UTwente (2014)

    Google Scholar 

  24. 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). https://doi.org/10.1007/978-3-540-73370-6_17

    Chapter  Google Scholar 

  25. Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60385-9_13

    Chapter  Google Scholar 

  26. Valmari, A.: Error detection by reduced reachability graph generation. In: APN, pp. 95–112 (1988)

    Google Scholar 

  27. Valmari, A.: What the small Rubik’s cube taught me about data structures, information theory, and randomisation. STTT 8(3), 180–194 (2006)

    Article  Google Scholar 

  28. van der Vegt, S., Laarman, A.: A parallel compact hash table. In: Kotásek, Z., Bouda, J., Černá, I., Sekanina, L., Vojnar, T., Antoš, D. (eds.) MEMICS 2011. LNCS, vol. 7119, pp. 191–204. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-25929-6_18

    Chapter  Google Scholar 

  29. de Vries, S.H.S.: Optimizing state vector compression for program verification by reordering program variables. In: 21st Twente SConIT, vol. 21, 23 June 2014

    Google Scholar 

  30. Wahl, T., Donaldson, A.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2(2), 799–847 (2010)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

The author thanks Yakir Vizel for promptly pointing out the natural number as a limit and Tim van Erven for a fruitful discussion.

Author information

Authors and Affiliations

  1. Leiden University, Leiden, The Netherlands

    Alfons Laarman

Authors
  1. Alfons Laarman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alfons Laarman .

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, Hampton, Virginia, USA

    Aaron Dutle

  2. NASA Langley Research Center, Hampton, Virginia, USA

    César Muñoz

  3. NASA Langley Research Center, Hampton, Virginia, USA

    Anthony Narkawicz

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Laarman, A. (2018). Optimal Storage of Combinatorial State Spaces. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds) NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science(), vol 10811. Springer, Cham. https://doi.org/10.1007/978-3-319-77935-5_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-77935-5_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-77934-8

  • Online ISBN: 978-3-319-77935-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation