Formulation of Cell Petri Nets

• Autorzy: Mitsuru Jitsukawa , Pauline N. Kawamoto , Yasunari Shidama
• Języki publikacji: EN

Abstrakty

EN

Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended to produce the synthesis of a family of colored Petri nets. Specifically, the extension to a CPNT family is performed by specifying how to link the outbound transitions of each colored Petri net to the place elements of other nets to form a neighborhood relationship. Finally, the activation of colored Petri nets was formalized.

Słowa kluczowe

EN

Petri net; system modelling

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2013
• Tom: 21
• Numer: 4
• Strony: 241-247

Daty

otrzymano

2013-12-08

Twórcy

autor

Mitsuru Jitsukawa

• Shinshu University Nagano, Japan

autor

Pauline N. Kawamoto

• Shinshu University Nagano, Japan

autor

Yasunari Shidama

• Shinshu University Nagano, Japan

Bibliografia

• [1] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990.
• [2] Grzegorz Bancerek. Free term algebras. Formalized Mathematics, 20(3):239-256, 2012. doi:10.2478/v10037-012-0029-6.[Crossref]
• [3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.
• [4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
• [5] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
• [6] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
• [7] Czesław Bylinski. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521-527, 1990.
• [8] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
• [9] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
• [10] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
• [11] Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama, and Yatsuka Nakamura. Cell Petri net concepts. Formalized Mathematics, 17(1):37-42, 2009. doi:10.2478/v10037-009-0004-z.[Crossref]
• [12] Pauline N. Kawamoto and Yatsuka Nakamura. On Cell Petri Nets. Journal of Applied Functional Analysis, 1996.
• [13] Pauline N. Kawamoto, Yasushi Fuwa, and Yatsuka Nakamura. Basic Petri net concepts. Formalized Mathematics, 3(2):183-187, 1992.
• [14] Krzysztof Retel. Properties of first and second order cutting of binary relations. Formalized Mathematics, 13(3):361-365, 2005.
• [15] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115-122, 1990.
• [16] Andrzej Trybulec. Many sorted sets. Formalized Mathematics, 4(1):15-22, 1993.
• [17] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
• [18] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
• [19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.

Identyfikatory

DOI

10.2478/forma-2013-0026