. . . . . . . . . ( end of section Computation Graphs) <<Contents | End>>
Petri Nets are a way to model many kinds of systems that are both non-determinstic and/or concurrent. When many things can happen independently, and these event also tend to control what happens next to some extent, then a Petri Net may provide a good model.
Petri nets do not necessarily evolve in a deterministic way. Several different events(Transitions) are possible(Enabled) at any given time. One of the enabled transitions occurs. The state of the system is represented by the marks(Marking) made by putting special objects (Tokens) in special icons called places(Places).
Here is a list of the different kinds of Petri Net defined here. You can, if you wish, jump to the more specific models and return to the general ones, top-down by following links.
Source: ElstobEtAl74, WooEtAl98
Each place is a node that models a property of the system or a component of the system's state. Places are normally shown by circles, sometimes with a label next to the circle. The circle doesn't have a label inside because its state is shown by "marking" the inside of the circle.
Transitions model the dynamics of the system, the possible changes. Transitions are shown as a thin rectangle. If labeled the label is written beside them.
Nodes are partitioned into Places and Transitions:
To save space and typing many mathematicians use P for Places and T for Transitions and the variable p always refers to a place, and t refers to a Transition:
The above declaration needs a defence because when you write A | B you must know that A and B are sets of the same type. In the above declaration Places and Transitions are of type @Nodes and so the type of Arcs is @(Nodes><Nodes).
To save space and time, a will always represent an arc:
Arcs are drawn as lines with arrow heads. Notice that an arc can go from a place to a transition or from a transition to a place but never from a place to a place or a transition to a transition. It is possible for an arc to go from place p to transition t and also another arc can go from t to p. In this case an arrowhead is drawn at both ends of a single arc.
When an arrow goes from a place p to a transition t it is said to be an input to t.
When an arrow goes from a transition t to a place p it is said to be an output from t.
The following are short hand notations allowing us to write about the behavior of transitions.
We define the relationship between a transition t and a place p as being None, In, Out, and Inout arcs:
Notice that in the MATHS notation relations can be used as follows:
Tokens are used to mark the places and so record their state. If a Petri net models a computer system then these tokens tend associated with threads of execution. In a model of a physical system (for example making coffee) the tokens tend to be associated with physical resources like (for example) beans, pots, cups, water, boiler, ... However in some models one token can stand for several (combined) resources: for example a cup of hot black coffee might be a single token cup_black_coffee even through you might argue that it is a cup+hot water+coffee combination. Tokens can also be the two possible values for a condition: true and false.
The following is my personal abstraction from several common models of Petri nets. See [ Special Versions ] below for some specialized and so more applicable kinds of Petri nets -- nets with conditions on the places, nets which keep a count of the number of tokens, etc..
There is a special value for Tokens called empty. This is shown as a place with nothing inside it -- a blank circular icon. It is also a value that doesn't get listed when describing a marking in a net.
Associated with every transition and place there is an operation that describes the effect of the transition on that place. If there is no arc then the transition has no effect. If there is an output arc is then the operation the puts tokens onto it. Each input needs an operation that takes tokens. By changing the effect of input and output we create different versions of a Petri Net.
These operations are always one-to-one operations. Sometimes operations can not be carried out -- for example taking a token from an empty place:
Note. If the input was not one-to-one then the operation has a choice about what is consumed. This complicates the analysis of the net's behavior. It alloes it to model more complex systems. If empty is some thing that can be input then we have an optional input. A normal PN can simulate actions with choices by having one action for each possible combination of choices instead.
Petri nets evolve by taking tokens from places and putting them on places. In some versions can destroy and create tokens. Some versions only allow tokens to be put on places that don't have tokens. These differences are set up by changing the operations on the arcs(op).
I extend the op so that it doesn't do anything to places that have no connection to a transtion:
I choose to allow the effect of putting and taking to be allways possible, and to alows do nothing:
Notice that op is well-defined. When these operations are
carried out they have a well-determined effect -- removing a bean
from a non-empty can reduces the number of beans in the can by one.
Table
Arc | Operation |
---|---|
None | do nothing |
In | given |
Out | given |
Inout | do nothing |
Notice that these operations can not always be carried out -- you can't
get a bean from an empty coffee can. If a place is
empty then you can not take a token from it, and you can certainly
put a token on it:
Notice that Initial is only a partial map. This makes it easier to describe typical Petri nets. Normally most places are empty so this allows a net to described by just listing the non_empty (marked) places. So the initial (lower case) map is defined as Initial (Upper Case) plus the empty Places.
(The "f|+>x" notation for completing a partial map is in STANDARD)
We will use m to indicate a marking:
Now a given transition t can sometimes fire depending on the marking m. The effect depends on the operations placed on the arcs as tabulated in the op mapping. The result is a new value ( m'(p) ) represented by the element in the set
We write
So if the effect of a transition t is described by changing m to m' then the relation between a current state and a possible next state as m becomes m' ::= for some t:Enabled(m), all p ( m'(p) = the ((t,p).op)(m(p)) ).
If | then |
---|---|
(t,p) in In | m'(p) = the ((t,p).op)(m(p)) |
(t,p) in Out | m'(p) = the ((t,p).op)(m(p)) |
(t,p) in Inout | m'(p) = m(p) |
(t,p) in None | m'(p) = m(p) |
This is then repeated to generate a sequence of new markings:
We have defined a state determined mechanism:
Notice that when a place has a token, and several arcs going to transitions, that token can only fire one transition. There is an implicit choice point in every place. However, unlike flowcharts and start charts there is no explicit condition determining which happens. This introduces non-determinacy. It is useful because it can model users making choices. For example, if you telephone someone their phone starts ringing. They may answer, or you may hang up. This is not a choice made by the telephone system and so is naturally shown as a place with two outgoing arcs.
On the other hand, when a transition has two or more outgoing arcs all the place that they go to get a token. This means that transitions can create concurrent threads of control. Similarly they can absorb or join two or more threads.
On the other hand when a Place has more than outgoing arrow then more than one transition can be enabled. The system can choose one or the other. Places embody choices and decisions in the net.
Places with no outgoing transitions:
In modeling requirements Sources and Sinks are rare.
We start by defining the two functions:
Now use them to make the net:
Define the folowing terms:
The following properties follow:
A SIMPLE_PETRI_NET with single place can exhibit complex behaviors. For example
We can never fire a transition that outputs true onto true.
Notice that the following formula
is not correct because put is not one-to-one and so take is not definable. I'll leave as an exercise [click here if you can fill this hole] the rewriting of SIMPLE_PETRI_NET so that the following become valid:
The resulting assumptions model a situation where tokens are destroyed as they enter places. It shouldn't be possible to destroy a token on a place by adding another token. In a simple PN this is still possible. Here is an example:
A neat formulation of this is to make sure that put doesn't
lead to a fewer number of tokens, or that the sequence t, put(t), put^2(t),...
never repeats itself:
For example:
Exercise. Show that in this model Sources can continuously generate new tokens and Sinks can continuously absorb any incoming tokens.
In a more complex model the Tokens can be items of data, the places queues, and the transitions have functions or processes that indicate how input tokens are used to produce output tokens.
A very common form puts a different weight on each arc but has the same operation.
This means that when transition t fires place p changes by the difference between the outputs from t asnd the sum of the inputs to t.
The commonest case is when
Typcially the weights are either 1 or 0 as well.
Notice that when Tokens =Nat0 it is easy to create Petri Nets where the number of tokens on a place grow without limit. An example being any net where a single input produces two outputs that in turn lead to input back into the original place.
A variation of WEIGHTED_PETRI_NET is when the weights are an action on some group or monoid. The commonest forms are
Source: CommonerHoltPnueli71
However they are are not capable of expressing conditional execution, see Conditions below.
As an example a phone can be on-hook, so we have two places: on_hook and off_hook. A couple of transitions can show that we can put the phone on_hook and take it off_hook. By only putting a token on one of them, we make sure that only one can be true at a time. This gives us a Toggle.
One can have non-boolean conditions as well.
For example, you raise a telephone and it becomes off_hook (not on_hook). Putting the phone back puts the phone on-hook and not off-hook.
. . . . . . . . . ( end of section Design Patterns) <<Contents | End>>
. . . . . . . . . ( end of section Petri Nets) <<Contents | End>>
Add a binary conflict relationship:
. . . . . . . . . ( end of section Theories of Concurrency) <<Contents | End>>
Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.
The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see [ home.html ]
For a more rigorous description of the standard notations see