<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In this article we formalize the definition of Decision-Free Petri Net (DFPN) presented in [19]. 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 natural numbers 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 the same after firing any sequences of the transition.</p></abstract>

In this article we formalize the definition of Decision-Free Petri Net (DFPN) presented in [19]. 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 natural numbers 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 the same after firing any sequences of the transition.

The Formalization of Decision-Free Petri Net

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

{"article-title":"The Formalization of Decision-Free Petri Net"}

In this article we formalize the definition of Decision-Free Petri Net (DFPN) presented in [19]. Then we formalize the concept of directed path and directed...

The Formalization of Decision-Free Petri Net

Online veröffentlicht: 30. März 2014

Seitenbereich: 29 - 35

DOI: https://doi.org/10.2478/forma-2014-0004

Schlüsselwörter
specification and verification of discrete systems, Petri net;

© by Pratima K. Shah

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

The Formalization of Decision-Free Petri Net

Online veröffentlicht: 30. März 2014

Seitenbereich: 29 - 35

DOI: https://doi.org/10.2478/forma-2014-0004

Schlüsselwörterspecification and verification of discrete systems, Petri net;

© by Pratima K. Shah

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Schlüsselwörter
specification and verification of discrete systems, Petri net;