Verification of Scenarios in Petri Nets Using Compact Tokenflows

• Autorzy: Bergenthum R. , Lorenz R.

Identyfikatory

DOI

10.3233/FI-2015-1172

• Języki publikacji: EN

Abstrakty

EN

In this paper we tackle the problem of verifying whether a scenario is executable in a Petri net. In contrast to sequentially ordered runs, a scenario includes both information about dependencies and independencies of events. Consequently, a scenario allows a precise and intuitive specification of a run of a concurrent or distributed system. In this paper we consider Petri nets with arc weights, namely marked place/transition-nets (p/t-nets) and p/t-nets with inhibitor arcs (pti-nets). A scenario of a p/t-net is a labelled partial order (lpo). A scenario of a pti-net is a labelled stratified order structure (lso). Accordingly, the question is either whether a given lpo is in the language of a given p/t-net or whether an lso is in the language of a given pti-net. Different approaches exist to define the partial language of a Petri net. Each definition yields a different verification algorithm, but existing algorithms perform quite poorly in terms of runtime for most examples. We introduce a new compact characterization of the partial language of a Petri net. This characterization is optimized with respect to the verification problem. The paper is a revised and extended version of the conference paper [10].

Słowa kluczowe

EN

Petri nets; information theory; algorithms; problem solving; language

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 137, nr 1
• Strony: 117--142
• Opis fizyczny: Bibliogr. 40 poz., rys., tab.

Twórcy

autor

Bergenthum R.

• Department of Software Engineering and Theory of Programming, FernUniversit¨at in Hagen, Germany

autor

Lorenz R.

• Lecturing Professorship for Computer Science University of Augsburg, Germany

Bibliografia

• [1] van der Aalst, W. M. P.; van Dongen, B. F.: Discovering Petri Nets from Event Logs. Transactions on Petri Nets and other Models of Concurrency 7 (K. Jensen, W.M.P. van der Aalst, G. Balbo, M. Koutny, K. Wolf, Eds.), LNCS 7480, Springer, 2013 , 372–422
• [2] Ahuja, R. K.; Magnanti T. L.; Orlin J.B.: Network flows: Theory, algorithms, and applications. Prentice Hall (Englewood Cliffs), 1993
• [3] Bergenthum, R.: Algorithmen zur Verifikation von halbgeordneten Petrinetz-Abläufen: Implementierung und Anwendungen. Diplomarbeit, Katholische Universität Eichstätt-Ingolstadt, 2006
• [4] Bergenthum, R.; Desel, J.; Juhás, G.; Lorenz, R.: Can I Execute My Scenario in Your Net? VipTool Tells You! Proc. of Petri Nets and Other Models of Concurrency 2006 (S. Donatelli, P. S. Thiagarajan, Eds.), LNCS 4024, Springer, 2006, 381 – 390
• [5] Bergenthum, R.; Desel, J.; Lorenz, R.; Mauser, S.: Synthesis of Petri Nets from Finite Partial Languages. Fundamenta Informaticae 88, Nr. 4, 2008, S. 437–468
• [6] Bergenthum, R.; Desel, J.; Mauser, S.: Comparison of Different Algorithms to Synthesize a Petri Net from a Partial Language. Transactions on Petri Nets and other Models of Concurrency 3 (K. Jensen, J. Billington, M. Koutny, Eds.), LNCS 5800, Springer, 2009 , 216–243
• [7] Bergenthum, R.; Desel, J.; Mauser, S.; Lorenz, R.: Synthesis of Petri Nets from Term Based Representations of Infinite Partial Languages. Fundamenta Informaticae 95, Nr. 1, 2009, 187–217
• [8] Bergenthum, R.; Juhás, G.; Lorenz, R.; Mauser, S.: Unfolding Semantics of Petri Nets Based on Token Flows. Fundamenta Informaticae 94, Nr. 3-4, 2009, 331–360
• [9] Bergenthum, R.; Lorenz, R.; Mauser, S.: Faster Unfolding of General Petri Nets Based on Token Flows. Proc. of Applications and Theory of Petri Nets (K.M. van Hee, R. Valk, Eds.), LNCS 5062, Springer, 2008, 13–32
• [10] Bergenthum, R.: Faster Verification of Partially Ordered Runs in Petri Nets Using Compact Tokenflows. Proc. of Applications and theory of Petri nets (J.M. Colom, J. Desel, Eds.), LNCS 7927, Springer, 2013, 330–348
• [11] Bergenthum, R.; Desel, J.; Mauser, S.; Harrer, A.: Modeling and Mining of Learnflows. Transactions on Petri Nets and other Models of Concurrency 5 (K. Jensen, S. Donatelli, J. Kleijn, Eds.), LNCS 6900, Springer, 2012, 22–50
• [12] Bergenthum, R.: Verifikation von halbgeordneten Abläufen. PhD-thesis, FernUniversität in Hagen, 2013
• [13] Best, E.; Devillers, R.: Sequential and concurrent behaviour in Petri net theory. Theoretical Computer Science 55, Nr. 1, 87 – 136
• [14] Desel, J.; Juhás, G.: ”What Is a Petri Net?”. Unifying Petri Nets, Advances in Petri Nets (H. Ehrig, G. Juhás, J. Padberg, G. Rozenberg, Eds.), LNCS 2128, Springer, 2001, 1–25
• [15] Desel, J.; Juhás, G.; Lorenz, R.; Neumair, C.: Modelling and Validation with VipTool. Proc. of Business Process Management 2003 (W.M.P. van der Aalst, A.H.M. Hofstede, M.Weske, Eds.), LNCS 2678, Springer, 2003, 380–389
• [16] Desel, J.; Reisig, W.: Place/Transition Petri Nets. Lectures on Petri Nets I: Basic Models, Advances in Petri Nets (W. Reisig, G. Rozenberg, Eds.), LNCS 1491, Springer, 1998, 122 – 173
• [17] DINIC, E. A.: Algorithm for Solution of a Problem of Maximum Flow in a Network with Power Estimation. In: Soviet Math Doklady 11, 1970, S. 1277 – 1280
• [18] Donatelli, S.; Franceschinis, G.: Modelling and Analysis of Distributed Software Using GSPNs. Proc. Of Applications and Theory of Petri Nets 1998, LNCS 1492, Springer, 1998, 438–476
• [19] Ford, L. R. ; Fulkerson, D. R.: Maximal Flow Through A Network. Canadian Journal of Mathematics 8, 1956, 399–404
• [20] Goltz, U.; Reisig, W.: Processes of Place/Transition-Nets. Automata Languages and Programming 154 (J. Diaz, Eds.), Springer, 1983, 264–277
• [21] Goltz, U.; Reisig, W.: The Non-sequential Behavior of Petri Nets. Information and Control 57, 2/3, 1983, 125–147
• [22] Grabowski, J.: On partial languages. Fundamenta Informaticae 4, nr. 2, 1981, 427–498
• [23] Janicki, R.; Koutny, M.: Structure of concurrency. Theoretical Computer Science 112, nr. 1, 1993, 5–52
• [24] Janicki, R.; Koutny, M.: Semantics of Inhibitor net. Information and Computation 123, (1), 1995, 1–16
• [25] Juhás, G.; Lorenz, R.; Desel, J.: Can I Execute My Scenario in Your Net? Proc. of Applications and Theory of Petri Nets 2005 (G. Ciardo, P. Darondeau, Eds.) LNCS 3536, Springer, 2005, 289–308
• [26] Karzanov, A. V.: Determining the maximal flow in a network by the method of preflows. Soviet Mathematics Doklady 15, 1974, 434–437
• [27] Kiehn, A.: On the Interrelation Between Synchronized and Non-Synchronized Behaviour of Petri Nets. Elektronische Informationsverarbeitung und Kybernetik 24, nr. 1/2, 1988, 3–18
• [28] Kleijn, J.; Koutny, M.: Process Semantics of general Inhibitor nets. Information and Computation 190, (1), 2004, 18–69
• [29] Lorenz, R.: Szenario-basierte Verifikation und Synthese von Petrinetzen: Theorie und Anwendungen. Habilitation, Katholische Universität Eichstätt-Ingolstadt, 2006
• [30] Lorenz, R.; Mauser, S.; Bergenthum, R.: Testing the executability of scenarios in general inhibitor nets. Proc. of Application of Concurrency to System Design 2007 (T. Basten, G. Juhás, S.K. Sandeep, Eds.), IEEE Computer Society, 2007, 167–176
• [31] Lorenz, R.; Juhás, G.; Bergenthum, R.; Desel, J.; Mauser, S.: Executability of Scenarios in Petri Nets. Theoretical Computer Science Volume 410, Issue 12-13, 2009, 1190–1216
• [32] Malhotra, V. M.; Kumar, M. P.; Maheshwari, S.N.: An O(jVj 3) Algorithm for Finding Maximum Flows in Networks. Information Processing Letters 7, nr. 6, 1994, 277–278
• [33] McMillan, K.L.; Probst, D.K.: A Technique of State Space Search Based on Unfolding. Formal Methods in System Design, 1992, 45–65
• [34] Oliveira, M.: Hasse Diagram Generators and Petri Net. Fundamenta Informaticae 105 (3), 2012, 263–289
• [35] Peterson, J.L.: Petri net theory and the modeling of systems. Prentice-Hall (Englewood Cliffs), 1981
• [36] Pratt, V.: Modelling Concurrency with Partial Orders. International Journal of Parallel Programming 15 , 1986
• [37] Reisig, W.: Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013
• [38] Solé, M.; Carmona, J.: Process Mining from a Basis of State Regions. Proc. of Applications and Theory of Petri Nets 2010 (J. Lilius, W. Penczek, Eds.), LNCS 6128, Springer, 2010, 226–245
• [39] Vogler, W.: Modular construction and partial order semantics of Petri nets. LNCS 625, Springer, 1992
• [40] Winskel, G.: Event structures. Petri Nets: Applications and Relationships to Other Models of Concurrency (W. Brauer, W. Reisig, G. Rozenberg, Eds.), Bd. 255, Springer , 1987, 325–392