An algebraic Petri net (APN) 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 Coloured Petri nets are a backward compatible extension of the mathematical concept of Petri nets.
Coloured Petri nets preserve useful properties of Petri nets and at the same time extend the initial formalism to allow the distinction between to ...
(CPN) in many aspects. However, in the APN case, the semantics of the data types is given by an
axiomatization
In mathematics and logic, an axiomatic system is any Set (mathematics), set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A Theory (mathematical logic), theory is a consistent, relatively-self-co ...
enabling proofs and computations on it.
Algebraic Petri nets were invented by Jacques Vautherin in 1985 in his 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 parts:
* The ''signature'' (Sort and Ops in the example below) which gives the valid constants and operations of the
term algebra.
* The ''axiomatization'' (Axioms in the example below) which gives the semantics 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
multiset (bags) of tokens. Those tokens are elements of a
term algebra 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
rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a well-formed formula, formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewr ...
[Dick, A. J. and Watson, P. 1991. Order-sorted term rewriting. Comput. J. 34, 1 (Feb. 1991), 16-19.] 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
The CO-OPN (Concurrent Object-Oriented Petri Nets) specification language is based on both algebraic specifications and algebraic Petri nets formalisms. The former formalism represent the data structures aspects, while the latter stands for the b ...
.
References
Further reading
*
*
External links
An Introduction to the Algebraic Specification of Abstract Data Types
{{DEFAULTSORT:Algebraic Petri Nets
Specification languages
Petri nets