SpringerLink
Log in

Experimenting with Stubborn Sets on Petri Nets

  • Conference paper
  • First Online:
Application and Theory of Petri Nets and Concurrency (PETRI NETS 2023)

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

  • 464 Accesses

Abstract

The implementation of model checking algorithms on real life systems usually suffers from the well known state explosion problem. Partial order reduction addresses this issue in the context of asynchronous systems. We review in this article algorithms developped by the Petri nets community and contribute with simple heuristics and variations of these. We also report on a large set of experiments performed on the models of a Model Checking Contest hosted by the Petri Nets conference since 2011. Our study targets the verification of deadlock freeness and liveness properties.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (France)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 67.40
Price includes VAT (France)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 84.39
Price includes VAT (France)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    See https://mcc.lip6.fr/models.php for the list of models. All models from 2011 to 2022 (included) have been considered.

  2. 2.

    We implemented the ColoredDest variant of [5] which makes use of state tagging mechanisms to avoid useless full expansions.

References

  1. Barnat, J., Brim, L., Rockai, P.: Parallel partial order reduction with topological sort proviso. In: SEFM’2010, pp. 222–231. IEEE Computer Society Press (2010)

    Google Scholar 

  2. Bošnački, D., Holzmann, G.J.: Improving spin’s partial-order reduction for breadth-first search. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 91–105. Springer, Heidelberg (2005). https://doi.org/10.1007/11537328_10

    Chapter  Google Scholar 

  3. 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). https://doi.org/10.1007/11691617_16

    Chapter  Google Scholar 

  4. Cappello, F., et al.: Grid’5000: A large scale and highly reconfigurable grid experimental testbed. In SC’05: Proc. The 6th IEEE/ACM International Workshop on Grid Computing CD, pp. 99–106, Seattle, Washington, USA, November 2005. IEEE/ACM

    Google Scholar 

  5. Duret-Lutz, A., Kordon, F., Poitrenaud, D., Renault, E.: Heuristics for checking liveness properties with partial order reductions. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 340–356. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_22

    Chapter  Google Scholar 

  6. Evangelista, S.: High level petri nets analysis with Helena. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 455–464. Springer, Heidelberg (2005). https://doi.org/10.1007/11494744_26

    Chapter  MATH  Google Scholar 

  7. Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. Int. J. Softw. Tools Technol. Transfer (STTT) 12(2) (2010)

    Google Scholar 

  8. Garavel, H.: Nested-unit Petri nets. J. Log. Algebraic Methods Program. 104, 60–85 (2019)

    Article  MathSciNet  MATH  Google Scholar 

  9. 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). https://doi.org/10.1007/978-3-642-04761-9_4

    Chapter  MATH  Google Scholar 

  10. Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032, pp. 41–73. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60761-7_31

    Book  MATH  Google Scholar 

  11. Kristensen, L.M., Valmari, A.: Improved question-guided stubborn set methods for state properties. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 282–302. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44988-4_17

    Chapter  Google Scholar 

  12. Kurshan, R., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 345–357. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054182

    Chapter  Google Scholar 

  13. Lehmann, A., Lohmann, N., Wolf, K.: Stubborn sets for simple linear time properties. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 228–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31131-4_13

    Chapter  Google Scholar 

  14. Nalumasu, R., Gopalakrishnan, G.: An efficient partial order reduction algorithm with an alternative proviso implementation. FMSD 20(3), 231–247 (2002)

    MATH  Google Scholar 

  15. 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). https://doi.org/10.1007/3-540-56922-7_34

    Chapter  Google Scholar 

  16. Schmidt, K.: Stubborn sets for standard properties. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 46–65. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48745-X_4

    Chapter  Google Scholar 

  17. Stern, U., Dill, D.L.: Parallelizing the Mur\({\Phi }\) verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–267. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_26

    Chapter  Google Scholar 

  18. 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). https://doi.org/10.1007/BFb0023729

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  20. Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-65306-6_21

    Chapter  Google Scholar 

  21. Valmari, A., Hansen, H.: Can stubborn sets be optimal? In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 43–62. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13675-7_5

    Chapter  Google Scholar 

  22. Varpaaniemi, K.: Finding small stubborn sets automatically. In: Proceedings of the 11th International Symposium on Computer and Information Sciences, pp. 133–142 (1996)

    Google Scholar 

  23. Varpaaniemi, K., Heljanko, K., Lilius, J.: Prod 3.2 an advanced tool for efficient reachability analysis. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 472–475. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_51

    Chapter  Google Scholar 

Download references

Acknowledgments

We thank the organizers of the Model Checking Contest and all people that contribute to its model database for providing such a database. Experiments presented in this paper were carried out using the Grid’5000 [4] testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organisations (see https://www.grid5000.fr). We thank Laure Petrucci for her comments on the first version of this paper.

Author information

Authors and Affiliations

  1. LIPN, CNRS UMR 7030, Université Paris 13, Sorbonne Paris Cité, 99, av. J.-B. Clément, 93430, Villetaneuse, France

    Sami Evangelista

Authors
  1. Sami Evangelista
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sami Evangelista .

Editor information

Editors and Affiliations

  1. NOVA University Lisbon, Caparica, Portugal

    Luis Gomes

  2. University of Augsburg, Augsburg, Germany

    Robert Lorenz

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Evangelista, S. (2023). Experimenting with Stubborn Sets on Petri Nets. In: Gomes, L., Lorenz, R. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2023. Lecture Notes in Computer Science, vol 13929. Springer, Cham. https://doi.org/10.1007/978-3-031-33620-1_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-33620-1_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-33619-5

  • Online ISBN: 978-3-031-33620-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation