Unfolding Semantics of Petri Nets Based on Token Flows

• Autorzy: Bergenthum R. , Mauser S. , Lorenz R. , Juhas G.
• Języki publikacji: EN

Abstrakty

EN

In this paper we propose two new unfolding semantics for general Petri nets combining the concept of prime event structures with the idea of token flows developed in [13]. In contrast to the standard unfolding based on branching processes, one of the presented unfolding models avoids to represent isomorphic processes while the other additionally reduces the number of (possibly nonisomorphic) processes with isomorphic underlying runs. We show that both the proposed unfolding models still represent the complete partial order behavior. Moreover, in both cases it is possible to construct complete finite prefixes for bounded nets through applying the known theory of cut-off events. In particular, canonical prefixesw.r.t. a given cutting context can be defined and computed for bounded nets. We present implementations of construction algorithms for complete finite prefixes of both the unfolding models. Experimental results show that the computed prefixes are much smaller and can be constructed significantly faster than in the case of the standard unfolding.

Słowa kluczowe

EN

unfoldings; prime event structure; canonical prefix; cutting context; Petri net

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 94, nr 3/4
• Strony: 331--360
• Opis fizyczny: Bibliogr. 23 poz., wykr., tab.

Twórcy

autor

Bergenthum R.

autor

Mauser S.

autor

Lorenz R.

autor

Juhas G.

• Department of Applied Computer Science, Catholic University of Eichstätt-Ingolstadt,

Bibliografia

• [1] Bergenthum, R., Lorenz, R.,Mauser, S.: Faster Unfolding of General Petri Nets Based on Token Flows, Petri Nets (K. M. van Hee, R. Valk, Eds.), 5062, Springer, 2008.
• [2] Best, E., Devillers, R.: Sequential and Concurrent Behaviour in Petri Net Theory., Theoretical Computer Science, 55(1), 1987, 87-136.
• [3] Couvreur, J.-M., Poitrenaud, D., Weil, P.: Unfoldings for General Petri Nets., http://www.labri.fr/perso/weil/publications/depliage.pdf, 2004.
• [4] Desel, J., Bergenthum, R., Mauser, S.: VipTool-Homepage., 2008, Http://viptool.ku-eichstaett.de.
• [5] Desel, J., G., Neumair, C.: Finite Unfoldings of Unbounded Petri Nets, ICATPN (J. Cortadella, W. Reisig, Eds.), 3099, Springer, 2004.
• [6] Desel, J., Juhàs, G., Lorenz, R., Neumair, C.: Modelling and Validation with VipTool., Business Process Management (W.M.P. van der Aalst; A.H.M. ter Hofstede; M. Weske, Ed.), 2678, Springer, 2003.
• [7] Engelfriet, J.: Branching Processes of Petri Nets., Acta Informatica, 28(6), 1991, 575-591.
• [8] Esparza, J., Heljanko, K.: Implementing LTL Model Checking with Net Unfoldings., SPIN (M. B. Dwyer, Ed.), 2057, Springer, 2001.
• [9] Esparza, J., Rőmer, S., Vogler, W.: An Improvement of McMillan's Unfolding Algorithm., Formal Methods in System Design, 20(3), 2002, 285-310.
• [10] Goltz, U., Reisig,W.: The Non-Sequential Behaviour of Petri Nets., Information and Control, 57(2/3), 1983, 125-147.
• [11] Haar, S.: Branching Processes of general S/T-Systems and their properties., Electr. Notes Theor. Comput. Sci., 18, 1998.
• [12] Hoogers, P., Kleijn, H., Thiagarajan, P.: An Event Structure Semantics for General Petri Nets., Theoretical Computer Science, 153(1&2), 1996, 129-170.
• [13] Juhàs, G., Lorenz, R., Desel, J.: Can I ExecuteMy Scenario in Your Net?., ICATPN (G. Ciardo, P. Darondeau, Eds.), 3536, Springer, 2005.
• [14] Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings, Ph.D. Thesis, University of Newcastle upon Tyne, 2003.
• [15] Khomenko, V., Kondratyev, A., Koutny, M., Vogler, W.: Merged processes: a new condensed representation of Petri net behaviour, Acta Inf., 43(5), 2006, 307-330.
• [16] Khomenko, V., Koutny, M.: Towards an Efficient Algorithm for Unfolding Petri Nets, CONCUR (K. G. Larsen, M. Nielsen, Eds.), 2154, Springer, 2001.
• [17] Khomenko, V., Koutny, M.: Branching Processes of High-Level Petri Nets, TACAS (H. Garavel, J. Hatcliff, Eds.), 2619, Springer, 2003.
• [18] Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings, Acta Inf., 40(2), 2003, 95-118.
• [19] McMillan, K. L.: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits., CAV (G. von Bochmann; D. K. Probst, Ed.), 663, Springer, 1992.
• [20] Meseguer, J., Montanari, U., Sassone, V.: On the Model of Computation of Place/Transition Petri Nets., Application and Theory of Petri Nets (R. Valette, Ed.), 815, Springer, 1994.
• [21] Meseguer, J., Montanari, U., Sassone, V.: On the Semantics of Place/Transition Petri Nets., Mathematical Structures in Computer Science, 7(4), 1997, 359-397.
• [22] Nielsen, M., Plotkin, G., Winskel, G.: Petri Nets, Event Structures and Domains, Part I., Theoretical Computer Science, 13, 1981, 85-108.
• [23] Winskel, G.: Event Structures., Advances in Petri Nets (W. Brauer, W. Reisig, G. Rozenberg, Eds.), 255, Springer, 1986.