@MISC{PETRI_DF.MIZ,
  AUTHOR = {Shah, Pratima K. and Kawamoto, Pauline N. and Giero, Mariusz},
  TITLE = {The Formalization of Decision Free {P}etri Net},
  NOTE = {This work was supported in part by JSPS Kakenhi Grant Number
          2230028502.},
  SECTION1 = {Preliminaries},
  SECTION2 = {The Number of Tokens in a Circuit},
  SECTION3 = {Decision-Free Petri Net Concept},
  SECTION4 = {The Concept of Directed Path and Directed Circuit in Petri Net},
  SECTION5 = {Firable and Firing Conditions for Transitions and Transition
              Sequences with Natural Marking},
  SECTION6 = {The Theorem Stating that the Number of Tokens in a Circuit
               Remains the Same after any Firing Sequences},
  DAY = {31},
  MONTH = {March},
  YEAR = {2014},
  ADDRESS1 = {Shinshu University, Faculty of Engineering, Dept. of Information
             Engineering, 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 = {Bia{\l}ystok\\Poland},
  SUMMARY = {In this article we formalize the definition of decision-free Petri
  net (DFPN) presented in \cite{Wang:1998}. Then we formalize the concept of
  directed path and directed circuit nets in Petri Nets to prove properties of
  DFPN. We also present the definition of firing transitions and transition
  sequences with NAT marking that always check whether transition is enabled or
  not and after firing it only removes the available tokens (i.e., it does not
  remove from zero number of tokens). At the end of this article, we show that
  the total number of tokens in a circuit of decision free Petri net always
  remains same after firing any sequences of the transition.}}

@BOOK{Wang:1998,
 AUTHOR={Wang, Jiacun},
 TITLE={Timed Petri Nets, Theory and Application},
 PUBLISHER={Kluwer Academic Publishers},
 YEAR=1998}

