Skip to main content
SpringerLink
Log in
Book cover

Concurrency, Security, and Puzzles pp 104–123Cite as

Abstractions for Transition Systems with Applications to Stubborn Sets

  • Chapter
  • First Online:

  • 717 Accesses

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

Abstract

Partial order reduction covers a range of techniques based on eliminating unnecessary transitions when generating a state space. On the other hand, abstractions replace sets of states of a system with abstract representatives in order to create a smaller state space. This article explores how stubborn sets and abstraction can be combined. We provide examples to provide intuition and expand on some recent results. We provide a classification of abstractions and give some novel results on what is needed to combine abstraction and partial order reduction in a sound way.

This is a preview of subscription content, 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

Learn about institutional subscriptions

References

  1. Bošnački, D., Scheffer, M.: Partial order reduction and symmetry with multiple representatives. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 97–111. Springer, Heidelberg (2015). doi:10.1007/978-3-319-17524-9_8

    Google Scholar 

  2. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi:10.1007/10722167_15

    Chapter  Google Scholar 

  3. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Programm. Lang. Syst. (TOPLAS) 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  4. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)

    Google Scholar 

  5. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463–478. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_38

    Chapter  Google Scholar 

  6. Engelfriet, J.: Determinancy \(\rightarrow \) (observation equivalence = trace equivalence). Theor. Comput. Sci. 36, 21–25 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  7. Geldenhuys, J., Hansen, H., Valmari, A.: Exploring the scope for partial order reduction. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 39–53. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_4

    Chapter  Google Scholar 

  8. Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X.: Practical partial order reduction for CSP. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 188–203. Springer, Heidelberg (2015). doi:10.1007/978-3-319-17524-9_14

    Google Scholar 

  9. Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). doi:10.1007/3-540-60761-7

    MATH  Google Scholar 

  10. Hansen, H., Kwiatkowska, M., Qu, H.: Partial order reduction for model checking Markov decision processes under unconditional fairness. In: Quantitative Evaluation of Systems (QEST 2011), pp. 203–212. IEEE (2011)

    Google Scholar 

  11. Hansen, H., Lin, S.-W., Liu, Y., Nguyen, T.K., Sun, J.: Diamonds are a girl’s best friend: partial order reduction for timed automata with abstractions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 391–406. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_26

    Google Scholar 

  12. Hansen, H., Valmari, A.: Operational determinism and fast algorithms. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 188–202. Springer, Heidelberg (2006). doi:10.1007/11817949_13

    Chapter  Google Scholar 

  13. Hansen, H., Valmari, A.: Safety property-driven stubborn sets. In: Larsen, K.G., Potapov, I., Srba, J. (eds.) RP 2016. LNCS, vol. 9899, pp. 90–103. Springer, Heidelberg (2016). doi:10.1007/978-3-319-45994-3_7

    Chapter  Google Scholar 

  14. Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: 2011 11th International Conference on Application of Concurrency to System Design (ACSD), pp. 36–43. IEEE (2011)

    Google Scholar 

  15. Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. Int. J. Softw. Tools Technol. Transfer 18(4), 427–448 (2016)

    Article  Google Scholar 

  16. Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). doi:10.1007/3-540-10235-3

    MATH  Google Scholar 

  17. Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_34

    Chapter  Google Scholar 

  18. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1997)

    Google Scholar 

  19. Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991). doi:10.1007/BFb0023729

    Chapter  Google Scholar 

  20. Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991). doi:10.1007/3-540-53863-1_36

    Chapter  Google Scholar 

  21. Valmari, A.: Stubborn set methods for process algebras. In: Proceedings of the DIMACS Workshop on Partial Order Methods in Verification (1997)

    Google Scholar 

  22. Valmari, A., Hansen, H.: Can stubborn sets be optimal? Fundamenta Informaticae 113(3–4), 377–397 (2011)

    MathSciNet  MATH  Google Scholar 

  23. Valmari, A., Hansen, H.: Stubborn set intuition explained. In: International Workshop on Petri Nets and Software Engineering 2016, pp. 213–232 (2016)

    Google Scholar 

  24. Valmari, A., Tienari, M.: Compositional failure-based semantic models for basic lotos. Formal Aspects Comput. 7(4), 440–468 (1995)

    Article  MATH  Google Scholar 

  25. Valmari, A., Vogler, W.: Fair testing and stubborn sets. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 225–243. Springer, Heidelberg (2016). doi:10.1007/978-3-319-32582-8_16

    Chapter  Google Scholar 

  26. Glabbeek, R.J.: The linear time — branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993). doi:10.1007/3-540-57208-2_6

    Google Scholar 

Download references

Acknowledgements

I wish to thank the editors for inviting me to submit an article, Antti Valmari for pioneering the field and his eagerness to discuss the topic after all these years, Xu Wang for discussions we have had over the years about the merits and pitfalls of various approaches, and Dragan Bosnacki for providing some insights on the matter. I am grateful to Bill Roscoe, for asking me one instrumental question about partial order reduction years ago. Answering that question led me to write a few articles, and, in a way, also this one.

Author information

Authors and Affiliations

  1. Department of Mathematics, Tampere University of Technology, Tampere, Finland

    Henri Hansen

Authors
  1. Henri Hansen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Henri Hansen .

Editor information

Editors and Affiliations

  1. University of Oxford, Oxford, United Kingdom

    Thomas Gibson-Robinson

  2. University of Oxford, Oxford, United Kingdom

    Philippa Hopcroft

  3. University of Warwick, Coventry, United Kingdom

    Ranko Lazić

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Hansen, H. (2017). Abstractions for Transition Systems with Applications to Stubborn Sets. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds) Concurrency, Security, and Puzzles. Lecture Notes in Computer Science(), vol 10160. Springer, Cham. https://doi.org/10.1007/978-3-319-51046-0_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51046-0_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51045-3

  • Online ISBN: 978-3-319-51046-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation