nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

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

verfasst von : Karsten Wolf

Erschienen in: Transactions on Petri Nets and Other Models of Concurrency XIV

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel A Tour in Process Mining: From Practice to Algorithmic Challenges

Nächstes Kapitel Parametric Verification: An Introduction

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.

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_40CrossRef

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_8CrossRef

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

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)

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)

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_31CrossRefMATH

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

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)CrossRef

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

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)

11.

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

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_93CrossRef

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_26CrossRef

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

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_9CrossRefMATH

16.

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

17.

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

18.

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

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_16CrossRefMATH

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_14CrossRef

21.

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

22.

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

23.

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

24.

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

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_12CrossRef

26.

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

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_31CrossRef

28.

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

29.

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

30.

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

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-7CrossRefMATH

32.

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

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_14CrossRef

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_24CrossRef

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_2CrossRef

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_16CrossRef

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_3CrossRef

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_23CrossRef

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_34CrossRef

40.

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

41.

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

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_4CrossRef

43.

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

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_35CrossRef

45.

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

46.

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

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)

48.

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

49.

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

50.

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

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_36CrossRef

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_21CrossRef

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_7CrossRef

54.

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

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_31CrossRef

56.

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

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_18CrossRef

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)

Titel: How Petri Net Theory Serves Petri Net Model Checking: A Survey
verfasst von: Karsten Wolf
Verlag: Springer Berlin Heidelberg
Buch: Transactions on Petri Nets and Other Models of Concurrency XIV
Print ISBN: 978-3-662-60650-6

Electronic ISBN: 978-3-662-60651-3

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-662-60651-3_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"