nach oben

vorheriges Kapitel A Tour in Process Mining: From Practice to Algo...

nächstes Kapitel Parametric Verification: An Introduction

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

2019 | OriginalPaper | Buchkapitel

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

Erstes Kapitel lesen

Autor: Karsten Wolf

Verlag: Springer Berlin Heidelberg

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

» Jetzt Zugang zum Volltext erhalten

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.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Jetzt einloggen Kostenlos registrieren

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

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

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 CrossRef

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

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

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 CrossRef

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

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

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 CrossRef

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

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

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

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

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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

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

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

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 CrossRef

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 CrossRef

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

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

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

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

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

DOI

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

Autor:

Karsten Wolf

Verlag

Springer Berlin Heidelberg

Sequenznummer