Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 1/2023

22-12-2022 | General

Leveraging polyhedral reductions for solving Petri net reachability problems

Authors: Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

Published in: International Journal on Software Tools for Technology Transfer | Issue 1/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference 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)CrossRefMATH 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)CrossRefMATH
2.
go back to reference 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
3.
go back to reference 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)CrossRef 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)CrossRef
4.
go back to reference 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) 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)
5.
go back to reference Berthelot, G.: Transformations and decompositions of nets. In: Petri nets: central models and their properties, pp. 359–376. Springer (1987)CrossRef Berthelot, G.: Transformations and decompositions of nets. In: Petri nets: central models and their properties, pp. 359–376. Springer (1987)CrossRef
6.
go back to reference Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Petri net reductions for counting markings. In: Model checking software (SPIN), pp. 65–84. Springer (2018)CrossRef Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Petri net reductions for counting markings. In: Model checking software (SPIN), pp. 65–84. Springer (2018)CrossRef
7.
go back to reference 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)CrossRef 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)CrossRef
8.
go back to reference 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
9.
go back to reference 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)CrossRefMATH 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)CrossRefMATH
10.
go back to reference 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)CrossRefMATH 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)CrossRefMATH
12.
go back to reference Garavel, H.: Proposal for adding useful features to Petri-net model checkers. Research Report 03087421, Inria Grenoble-Rhône-Alpes (2020) Garavel, H.: Proposal for adding useful features to Petri-net model checkers. Research Report 03087421, Inria Grenoble-Rhône-Alpes (2020)
13.
go back to reference Garavel, H., Serwe, W.: State space reduction for process algebra specifications. In: Algebraic methodology and software technology, pp. 164–180. Springer (2004)CrossRef Garavel, H., Serwe, W.: State space reduction for process algebra specifications. In: Algebraic methodology and software technology, pp. 164–180. Springer (2004)CrossRef
14.
go back to reference 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) 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)
15.
go back to reference 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) 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.
go back to reference 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)CrossRef 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)CrossRef
17.
go back to reference 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) 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)
20.
go back to reference 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) 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)
21.
go back to reference Kovalyov, Andrei: A polynomial algorithm to compute the concurrency relation of a regular STG. Hardware design and Petri nets, Springer, Boston (2000)CrossRef Kovalyov, Andrei: A polynomial algorithm to compute the concurrency relation of a regular STG. Hardware design and Petri nets, Springer, Boston (2000)CrossRef
24.
go back to reference Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRef Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRef
25.
go back to reference 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) 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.
go back to reference 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) 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)
27.
go back to reference Thierry-Mieg, Y.: Structural reductions revisited. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 303–323. Springer (2020)CrossRef Thierry-Mieg, Y.: Structural reductions revisited. In: Application and theory of Petri nets and concurrency (Petri nets), pp. 303–323. Springer (2020)CrossRef
28.
go back to reference Wisniewski, R., Karatkevich, A., Adamski, M., Costa, A., Gomes, L.: Prototyping of Concurrent Control Systems with Application of Petri Nets and Comparability Graphs. IEEE Trans. Control Syst. Technol. 26(2), 575–586 (2018)CrossRef Wisniewski, R., Karatkevich, A., Adamski, M., Costa, A., Gomes, L.: Prototyping of Concurrent Control Systems with Application of Petri Nets and Comparability Graphs. IEEE Trans. Control Syst. Technol. 26(2), 575–586 (2018)CrossRef
29.
go back to reference 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)CrossRef 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)CrossRef
Metadata
Title
Leveraging polyhedral reductions for solving Petri net reachability problems
Authors
Nicolas Amat
Silvano Dal Zilio
Didier Le Botlan
Publication date
22-12-2022
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 1/2023
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00694-8

Other articles of this Issue 1/2023

International Journal on Software Tools for Technology Transfer 1/2023 Go to the issue

Premium Partner