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.
@article{bwmeta1.element.doi-10_2478_forma-2013-0026,
author = {Mitsuru Jitsukawa and Pauline N. Kawamoto and Yasunari Shidama},
title = {Formulation of Cell Petri Nets},
journal = {Formalized Mathematics},
volume = {21},
year = {2013},
pages = {241-247},
zbl = {1298.68193},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_forma-2013-0026}
}
Mitsuru Jitsukawa; Pauline N. Kawamoto; Yasunari Shidama. Formulation of Cell Petri Nets. Formalized Mathematics, Tome 21 (2013) pp. 241-247. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_forma-2013-0026/
[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] | Zbl 1296.68085
[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. | Zbl 06213858
[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.