SpringerLink
Log in

Leveraging polyhedral reductions for solving Petri net reachability problems

  • General
  • Special Issue: SPIN 2021
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We propose a new method that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. Our approach relies on a state space abstraction, called polyhedral abstraction, which involves a combination between structural reductions and sets of linear arithmetic constraints between the marking of places. We propose a new data structure, called a Token Flow Graph (TFG), that captures the particular structure of constraints occurring in polyhedral abstractions. We leverage TFGs to efficiently solve two reachability problems: first to check the reachability of a given marking and then to compute the concurrency relation of a net, that is, all pairs of places that can be marked together in some reachable marking. Our algorithms are implemented in a tool, called Kong, that we evaluate on a large collection of models used during the 2020 edition of the Model Checking Contest. Our experiments show that the approach works well, even when a moderate amount of reductions applies.

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

Access this article

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

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10

Similar content being viewed by others

Notes

  1. https://github.com/nicolasAmat/Kong.

References

  1. Amat, N., Berthomieu, B., Dal Zilio, S.: On the combination of polyhedral abstraction and SMT-based model checking for Petri nets. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 164–185. Springer, Cham (2021)

    Chapter  MATH  Google Scholar 

  2. Amat, N., Berthomieu, B., Dal Zilio, S.: A polyhedral abstraction for Petri nets and its application to SMT-based model checking. Fundam. Inform. 187, 2–4 (2022)

    Article  MathSciNet  MATH  Google Scholar 

  3. Amat, N., Dal Zilio, S., Le Botlan, D.: Accelerating the computation of dead and concurrent places using reductions. In: Model checking software (SPIN), pp. 45–62. Springer (2021)

    Chapter  Google Scholar 

  4. Amparore, E., Berthomieu, B., Ciardo, G., Dal Zilio, S., Gallà, F., Hillah, L.M., Hulin-Hubard, F., Jensen, P.G., Jezequel, L., Kordon, F., Le Botlan, D., Liebke, T., Meijer, J., Miner, A., Paviot-Adet, E., Srba, J., Thierry-Mieg, Y., van Dijk, T., Wolf, K.: Presentation of the 9th edition of the model checking contest. In: Tools and algorithms for the construction and analysis of systems (TACAS), pp. 50–68. Springer (2019)

    Google Scholar 

  5. Berthelot, G.: Transformations and decompositions of nets. In: Petri nets: central models and their properties, pp. 359–376. Springer (1987)

    Chapter  Google Scholar 

  6. Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Petri net reductions for counting markings. In: Model checking software (SPIN), pp. 65–84. Springer (2018)

    Chapter  Google Scholar 

  7. Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Counting Petri net markings from reduction equations. Int. J. Softw. Tools Technol. Transf. 22(2), 163–181 (2019)

    Article  Google Scholar 

  8. Bønneland, F.M., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Stubborn versus structural reductions for Petri nets. J. Log. Algebraic Methods Program. 102, 46–63 (2019)

    Article  MathSciNet  MATH  Google Scholar 

  9. Bouvier, P., Garavel, H.: Efficient algorithms for three reachability problems in safe petri nets. In: Application and theory of Petri Nets and concurrency (Petri nets), pp. 339–359. Springer (2021)

    Chapter  MATH  Google Scholar 

  10. Bouvier, P., Garavel, H., Ponce-de León, H.: Automatic decomposition of Petri nets into automata networks—a synthetic account. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 3–23. Springer (2020)

    Chapter  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  12. Garavel, H.: Proposal for adding useful features to Petri-net model checkers. Research Report 03087421, Inria Grenoble-Rhône-Alpes (2020)

  13. Garavel, H., Serwe, W.: State space reduction for process algebra specifications. In: Algebraic methodology and software technology, pp. 164–180. Springer (2004)

    Chapter  Google Scholar 

  14. Giua, A., DiCesare, F., Silva, M.: Generalized mutual exclusion contraints on nets with uncontrollable transitions. In: IEEE international conference on systems, man, and cybernetics, pp. 974–979. IEEE (1992)

    Google Scholar 

  15. Hillah, L.-M., Kordon, F.: Petri nets repository: a tool to benchmark and debug Petri net tools. In: Application and theory of Petri Nets and concurrency (Petri nets), pp. 125–135. Springer (2017)

  16. Hillah, L.-M., Kordon, F., Petrucci, L., Treves, N.: PNML framework: an extendable reference implementation of the Petri Net Markup Language. In: International conference on applications and theory of Petri nets, pp. 318–327. Springer (2010)

    Chapter  Google Scholar 

  17. Hujsa, T., Berthomieu, B., Dal Zilio, S., Le Botlan, D.: Checking marking reachability with the state equation in Petri net subclasses. Technical Report 20278, LAAS-CNRS (2020)

  18. INRIA: CADP. (2020). https://cadp.inria.fr/

  19. Janicki, R.: Nets, sequential components and concurrency relations. Theor. Comput. Sci. 29, 1–2 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  20. Kovalyov, A.V.: Concurrency relations and the safety problem for Petri nets. In: Application and theory of Petri nets, pp. 299–309. Springer, Heidelberg (1992)

    Google Scholar 

  21. Kovalyov, Andrei: A polynomial algorithm to compute the concurrency relation of a regular STG. Hardware design and Petri nets, Springer, Boston (2000)

    Book  Google Scholar 

  22. LAAS-CNRS. Tina toolbox. (2020). http://projects.laas.fr/tina

  23. Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18, 717–721 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  24. Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  25. Semenov, A., Yakovlev, A.: Combining partial orders and symbolic traversal for efficient verification of asynchronous circuits. In: Proceedings of ASP-DAC’95/CHDL’95/VLSI’95 with EDA Technofair (1995)

  26. Silva, M., Terue, E., Colom, J.M.: Linear algebraic and linear programming techniques for the analysis of place/transition net systems. In: Lectures on Petri nets I: basic models: advances in Petri nets, pp. 309–373. Springer (1996)

    Google Scholar 

  27. Thierry-Mieg, Y.: Structural reductions revisited. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 303–323. Springer (2020)

    Chapter  Google Scholar 

  28. Wisniewski, R., Karatkevich, A., Adamski, M., Costa, A., Gomes, L.: Prototy** of Concurrent Control Systems with Application of Petri Nets and Comparability Graphs. IEEE Trans. Control Syst. Technol. 26(2), 575–586 (2018)

    Article  Google Scholar 

  29. Wiśniewski, R., Wiśniewska, M., Jarnut, M.: C-exact hypergraphs in concurrency and sequentiality analyses of cyber-physical systems specified by safe Petri nets. IEEE Access 7, 13510–13522 (2019)

    Article  Google Scholar 

Download references

Acknowledgements

We would like to thank Pierre Bouvier and Hubert Garavel for their insightful suggestions that helped improve the quality of this paper.

Author information

Authors and Affiliations

  1. LAAS-CNRS, Université de Toulouse, CNRS, INSA, Toulouse, France

    Nicolas Amat, Silvano Dal Zilio & Didier Le Botlan

Authors
  1. Nicolas Amat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvano Dal Zilio
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Didier Le Botlan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nicolas Amat.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Amat, N., Dal Zilio, S. & Le Botlan, D. Leveraging polyhedral reductions for solving Petri net reachability problems. Int J Softw Tools Technol Transfer 25, 95–114 (2023). https://doi.org/10.1007/s10009-022-00694-8

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-022-00694-8

Keywords

Search

Navigation