@MISC{PETRI_3.miz,
  AUTHOR = {Jitsukawa, Mitsuru and Kawamoto, Pauline N. and Shidama,
  Yasunari},
  TITLE = {Formulation of Cell Petri Nets},
  ACKNOWLEDGEMENT = {I am thankful to Mr. Yatsuka Nakamura who is
  the former professor of Shinshu University. There was no
  completion of this article without the deep insight to the
  automatic proof verification system of Mr. Nakamura. Thank you.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Synthesis of CPNT, I},
  SECTION3 = {Extension to a family of colored Petri nets},
  SECTION4 = {Definition of Cell Petri nets},
  SECTION5 = {Activation of Petri nets},
  DAY = {08},
  MONTH = {December},
  YEAR = {2013},
  ADDRESS1 = {Shinshu University Graduate School,
           Nagano-ken Nagano-shi Wakasato 4-17-1, 380-8553 JAPAN},
  ADDRESS2 = {Shinshu University, Faculty of Engineering
           Dept. of Information Engineering,
           Nagano-ken Nagano-shi Wakasato 4-17-1, 380-8553 JAPAN},
  ADDRESS3 = {Shinshu University, Faculty of Engineering
           Dept. of Information Engineering,
           Nagano-ken Nagano-shi Wakasato 4-17-1, 380-8553 JAPAN},
  SUMMARY = {Based on the Petri net definitions and theorems already
  formalized in the Mizar article \cite{PETRI.ABS},
  in this article we were able to formalize
  the definition of Cell Petri nets. It is based on \cite{Kawamoto}.
  Colored Petri net is already have been defined in
  \cite{PETRI_2.ABS}. In addition the conditions
  of the firing-rule and ColoredSet to this definition,
  that defines the Cell Petri nets extended to CPNT.i further.
  Although it was synthesis of two Petri nets in \cite{PETRI_2.ABS},
  it is synthesis from the family of Colored Petri nets
  (Colored-PT-net-Family of I) of finite number of pieces.
  That is, extension to a CPNT family is performed by defining
  the output arc from the transition of a certain Colored Petri nets
  to Place of a certain another Colored Petri nets
  (definition of the neighborhood).
  Finally, activation of Colored Petri nets was formalized.}}

@BOOK{Kawamoto,
 AUTHOR={Kawamoto, Pauline N. and Nakamura, Yatsuka},
 TITLE={On Cell Petri Nets},
 PUBLISHER={Journal of Applied Functional Analysis},
 YEAR=1996}
