SpringerLink
Log in

How Petri Net Theory Serves Petri Net Model Checking: A Survey

  • Chapter
  • First Online:
Transactions on Petri Nets and Other Models of Concurrency XIV

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 11790))

  • 735 Accesses

Abstract

Structure theory is a unique treasure of the Petri net community. It was originally studied as a set of stand-alone techniques for exploring Petri net properties such as liveness, boundedness, reachability, and deadlock freedom. Today, methods based on the exploration of the reachability graph (state space methods) dominate Petri net verification. Thanks to the concept of model checking, these methods can deal with a much larger range of verification problems, and thanks to state space reduction methods (symmetries, partial order reduction, and other abstraction techniques), they became tractable for many practical applications. However, in the course of pushing model checking technology to its limits, several elements of Petri net structure theory celebrate a resurrection, being viewed from a different angle. This time, they are used for acceleration of the state space methods. In this article, we give an overview on the use of structural methods in Petri net model checking. We further report on our experience with combining state space and structural methods.

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 42.79
Price includes VAT (France)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 52.74
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.

    Stubborn set methods are a class of state space reduction methods. In every marking m, they explore only a subset (“stubborn set”) of the enabled transitions. The stubborn sets are selected such that a given property is preserved (holds in the reduced state space if and only it holds in the full state space). The surveys [52, 53] present stubborn sets in full breadth.

References

  1. Behrmann, G., Larsen, K.G., Pelánek, R.: To store or not to store. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 433–445. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_40

    Chapter  Google Scholar 

  2. Bønneland, F., Dyhr, J., Jensen, P.G., Johannsen, M., Srba, J.: Simplification of CTL formulae for efficient model checking of Petri nets. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 143–163. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91268-4_8

    Chapter  Google Scholar 

  3. Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)

    Article  MathSciNet  Google Scholar 

  4. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pp. 1–12 (1962)

    Google Scholar 

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

    Google Scholar 

  6. Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_31

    Chapter  MATH  Google Scholar 

  7. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7–34 (2001)

    Article  Google Scholar 

  8. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)

    Article  Google Scholar 

  9. Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. 5(5), 511–523 (1971)

    Article  MathSciNet  Google Scholar 

  10. Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151–158 (1971)

    Google Scholar 

  11. Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)

    Article  Google Scholar 

  12. Esparza, J.: Model checking using net unfoldings. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 613–628. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56610-4_93

    Chapter  Google Scholar 

  13. Esparza, J., Melzer, S.: Model checking LTL using constraint programming. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 1–20. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63139-9_26

    Chapter  Google Scholar 

  14. Evangelista, S., Kristensen, L.M.: A sweep-line method for Büchi automata-based model checking. Fundam. Inform. 131(1), 27–53 (2014)

    MATH  Google Scholar 

  15. Garavel, H.: Nested-unit Petri nets: a structural means to increase efficiency and scalability of verification on elementary nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 179–199. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19488-2_9

    Chapter  MATH  Google Scholar 

  16. Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305–326 (1994)

    Article  MathSciNet  Google Scholar 

  17. Hack, M.: Analysis of production schemata by Petri nets. Technical report, MS thesis, Department of Electrical Engineering, MIT, Cambridge, Massachusetts (1972)

    Google Scholar 

  18. Hack, M.: Decidability questions for Petri nets. Outstanding Dissertations in the Computer Sciences. Garland Publishing, New York (1975)

    Google Scholar 

  19. Hajdu, Á., Vörös, A., Bartha, T.: New search strategies for the Petri net CEGAR approach. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 309–328. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19488-2_16

    Chapter  MATH  Google Scholar 

  20. Heiner, M., Rohr, C., Schwarick, M., Tovchigrechko, A.A.: MARCIE’s secrets of efficient model checking. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 286–296. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53401-4_14

    Chapter  Google Scholar 

  21. Holt, A.W., Commoner, F.: Events and conditions. In: MAC Conference on Concurrent Systems and Parallel Computation, pp. 3–52 (1970)

    Google Scholar 

  22. Jensen, K.: Condensed state spaces for symmetrical coloured Petri nets. Formal Methods Syst. Des. 9(1/2), 7–40 (1996)

    Article  Google Scholar 

  23. Kam, T., Villa, T., Brayton, R.K.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(01), 9–62 (1998)

    MathSciNet  MATH  Google Scholar 

  24. Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)

    Article  MathSciNet  Google Scholar 

  25. Kordon, F., et al.: MCC’2015 – the fifth model checking contest. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 262–273. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53401-4_12

    Chapter  Google Scholar 

  26. Kosaraju, S.R.: Decidability of reachability on vector addition systems. In: ACM Symposium on Theory Computing, pp. 267–281 (1982)

    Google Scholar 

  27. Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549–567. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45614-7_31

    Chapter  Google Scholar 

  28. Lautenbach, K., Schmid, H.A.: Use of Petri nets for proving correctness of concurrent process systems. In: IFIP Congress, pp. 187–191 (1974)

    Google Scholar 

  29. Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. In: Proceedings of the LICS, pp. 4–13. IEEE (2009)

    Google Scholar 

  30. Lipton, R.J.: The reachability problem requires exponential space. Technical report 62, Department of Computer Science, Yale University (1976)

    Google Scholar 

  31. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992). https://doi.org/10.1007/978-1-4612-0931-7

    Book  MATH  Google Scholar 

  32. Mayr, E.W.: An algroithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)

    Article  MathSciNet  Google Scholar 

  33. McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56496-9_14

    Chapter  Google Scholar 

  34. Memmi, G., Roucairol, G.: Linear algebra in net theory. In: Brauer, W. (ed.) Net Theory and Applications. LNCS, vol. 84, pp. 213–223. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10001-6_24

    Chapter  Google Scholar 

  35. Miner, A.S., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 6–25. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48745-X_2

    Chapter  Google Scholar 

  36. Oanea, O., Wimmel, H., Wolf, K.: New algorithms for deciding the siphon-trap property. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 267–286. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13675-7_16

    Chapter  Google Scholar 

  37. Pastor, E., Cortadella, J., Peña, M.A.: Structural methods to improve the symbolic analysis of Petri nets. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 26–45. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48745-X_3

    Chapter  Google Scholar 

  38. Pastor, E., Roig, O., Cortadella, J., Badia, R.M.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416–435. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58152-9_23

    Chapter  Google Scholar 

  39. 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 

  40. Ridder, H.: Analyse von Petri-Netz-Modellen mit Entscheidungsdiagrammen. Ph.D. thesis, Koblenz, Landau, University (1997)

    Google Scholar 

  41. Roch, S., Starke, P.H.: INA: integrated net analyzer (1999)

    Google Scholar 

  42. 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 

  43. Schmidt, K.: How to calculate symmetries of Petri nets. Acta Inf. 36(7), 545–590 (2000)

    Article  MathSciNet  Google Scholar 

  44. Schmidt, K.: Using Petri net invariants in state space construction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 473–488. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_35

    Chapter  Google Scholar 

  45. Schmidt, K.: Automated generation of a progress measure for the sweep-line method. STTT 8(3), 195–203 (2006)

    Article  Google Scholar 

  46. Starke, P.H.: Reachability analysis of Petri nets using symmetries. Syst. Anal. Model. Simul. 8(4–5), 293–303 (1991)

    MathSciNet  MATH  Google Scholar 

  47. Strehl, K., Thiele, L.: Interval diagram techniques for symbolic model checking of Petri nets. In: Proceedings of the Design, Automation and Test in Europe, pp. 756–757 (1999)

    Google Scholar 

  48. Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)

    Article  MathSciNet  Google Scholar 

  49. Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215–225 (1975)

    Article  MathSciNet  Google Scholar 

  50. Triebel, M., Sürmeli, J.: Characterizing stable and deriving valid inequalities of Petri nets. Fundam. Inform. 146(1), 1–34 (2016)

    Article  MathSciNet  Google Scholar 

  51. 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 

  52. 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 

  53. Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Koutny, M., Kleijn, J., Penczek, W. (eds.) Transactions on Petri Nets and Other Models of Concurrency XII. LNCS, vol. 10470, pp. 140–165. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55862-1_7

    Chapter  Google Scholar 

  54. Vardi, M.Y.: Verification of concurrent programs: the automata-theoretic framework. In: Proceedings of the LICS, pp. 167–176. IEEE (1987)

    Google Scholar 

  55. Vergauwen, B., Lewi, J.: A linear local model checking algorithm for CTL. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 447–461. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_31

    Chapter  Google Scholar 

  56. Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Log. Methods Comput. Sci. 8(3) (2012)

    Google Scholar 

  57. Wolf, K.: Petri net model checking with LoLA 2. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 351–362. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91268-4_18

    Chapter  Google Scholar 

  58. Wolf, K.: A simple abstract interpretation for Petri net queries. In: Proceedings of the PNSE, CEUR Workshop Proceedings, vol. 2138, pp. 163–170 (2018)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Rostock, Rostock, Germany

    Karsten Wolf

Authors
  1. Karsten Wolf
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Karsten Wolf .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, UK

    Maciej Koutny

  2. Università degli Studi di Milano, Milan, Italy

    Lucia Pomello

  3. Western Norway University of Applied Sciences, Bergen, Norway

    Lars Michael Kristensen

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer-Verlag GmbH Germany, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Wolf, K. (2019). How Petri Net Theory Serves Petri Net Model Checking: A Survey. In: Koutny, M., Pomello, L., Kristensen, L. (eds) Transactions on Petri Nets and Other Models of Concurrency XIV. Lecture Notes in Computer Science(), vol 11790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-60651-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-60651-3_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-60650-6

  • Online ISBN: 978-3-662-60651-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation