Formulation of Cell Petri Nets

Mitsuru Jitsukawa; Pauline N. Kawamoto; Yasunari Shidama

Formalized Mathematics (2013)

  • Volume: 21, Issue: 4, page 241-247
  • ISSN: 1426-2630

Abstract

top
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.

How to cite

top

Mitsuru Jitsukawa, Pauline N. Kawamoto, and Yasunari Shidama. "Formulation of Cell Petri Nets." Formalized Mathematics 21.4 (2013): 241-247. <http://eudml.org/doc/267226>.

@article{MitsuruJitsukawa2013,
abstract = {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.},
author = {Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {Petri net; system modelling},
language = {eng},
number = {4},
pages = {241-247},
title = {Formulation of Cell Petri Nets},
url = {http://eudml.org/doc/267226},
volume = {21},
year = {2013},
}

TY - JOUR
AU - Mitsuru Jitsukawa
AU - Pauline N. Kawamoto
AU - Yasunari Shidama
TI - Formulation of Cell Petri Nets
JO - Formalized Mathematics
PY - 2013
VL - 21
IS - 4
SP - 241
EP - 247
AB - 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.
LA - eng
KW - Petri net; system modelling
UR - http://eudml.org/doc/267226
ER -

References

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

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.