Algebraic Petri nets
Encyclopedia
Algebraic Petri Net is an evolution of the well known Petri net
in which elements of User Defined Data Types (called Algebraic Abstract Data Types (AADT)) replace black tokens. This formalism can be compared to Coloured Petri Nets CPN
in many aspects. However, in the APN case, the
semantics of the data types is given by an axiomatization enabling proofs and computations on it.
Algebraic Petri Nets were invented by Jacques Vautherin in 85 in is PhD thesis and later improved by Wolfang Reisig.
The formalism has two aspects :
AADT can be themselves split in two part :
The following picture describes an Algebraic Petri Net model of the Dining Philosophers problem. There are two AADT in this model, one for the forks algebra, one for the philosophers algebra. Please note that the philosophers AADT uses the fork AADT. Since all philosophers can take their left fork without taking their right fork, executing this model can result in a deadlock.
The control part is composed of :
In the example below only transition goEat is firable at the beginning. One goEat has been fired, takeL and takeR are also enabled and thus can also be fired.
Algebraic Petri Nets are the basic formalism of more advanced ones such as CO-OPN.
Petri net
A Petri net is one of several mathematical modeling languages for the description of distributed systems. A Petri net is a directed bipartite graph, in which the nodes represent transitions and places...
in which elements of User Defined Data Types (called Algebraic Abstract Data Types (AADT)) replace black tokens. This formalism can be compared to Coloured Petri Nets CPN
CPN
CPN may stand for:*Called party number*Calpine Corporation, New York Stock Exchange symbol CPN*Canadian Perinatal Network*Carnivorous Plant Newsletter*Carpinteria , California, Amtrak station code CPN...
in many aspects. However, in the APN case, the
semantics of the data types is given by an axiomatization enabling proofs and computations on it.
Algebraic Petri Nets were invented by Jacques Vautherin in 85 in is PhD thesis and later improved by Wolfang Reisig.
The formalism has two aspects :
- The control part which is handled by a Petri Net.
- The data part which is handled by one or many AADTs.
AADT can be themselves split in two part :
- The signature (Sort and Ops in the example below) which gives the valid constants and operations of the term algebraTerm algebraIn universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X...
. - The axiomatization (Axioms in the example below) which gives the semantic of the operations described in the signature part.
The following picture describes an Algebraic Petri Net model of the Dining Philosophers problem. There are two AADT in this model, one for the forks algebra, one for the philosophers algebra. Please note that the philosophers AADT uses the fork AADT. Since all philosophers can take their left fork without taking their right fork, executing this model can result in a deadlock.
The control part is composed of :
- Places contain MultisetMultisetIn mathematics, the notion of multiset is a generalization of the notion of set in which members are allowed to appear more than once...
(bags) of tokens. Those tokens are elements of a term algebraTerm algebraIn universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X...
built upon the signature of the AADT(in the example, terms that represent either a philosopher or a fork). Each place contains one and only one multiset of terms, the place is typed by its multiset. - Arcs can be labeled with multisets of either closed or free terms. Again terms are built from the AADT signature.
- Transitions are events that can be fired whenever there are enough resources (namely enough tokens in the input places to satisfy all the input arcs) and the guard (firing conditions) of the transition holds. Then the produced tokens are put in the target places of the output arcs. Usually Term RewritingRewritingIn mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
is used for the operational semantics in order to check if conditions hold and to compute output terms.
In the example below only transition goEat is firable at the beginning. One goEat has been fired, takeL and takeR are also enabled and thus can also be fired.
Algebraic Petri Nets are the basic formalism of more advanced ones such as CO-OPN.