
12. Petrinets
Werner Van Belle^{1}  werner@yellowcouch.org, werner.van.belle@gmail.com
1 Programming Technology Lab (PROG)
Department of Computer Science (DINF)
Vrije Universiteit Brussel (VUB); Pleinlaan 2; 1050 Brussel; Belgium
Abstract
:
Investigates the use of Petrinets in distributed open systems, which also happen to be concurrent systems. This exercise was given in 20022003
Reference:
Werner Van Belle; Petrinets;

Programming distributed systems is not easy because
 distributed systems are inherent concurrent systems, in which all
too often multiple sessions have to be managed.
 one has to take into account the possibility of failures at virtually
every possible moment.
This makes the use of thread based models and semitransparent calling
models very difficult. However, the other possibility, event based
models (presented in the previous lesson) don't solve these problems
either. Luckily, concurrency, session management and partial failures
are no longer hidden from the programmer. In this lesson we will see
how Petrinets can be used as a modeling technique that can help in
designing distributed applications.
A Petrinet is a drawing that formally and statically describes the
possibilities and impossibilities of a system at runtime. In comparison
to MSC's they fully describe the behavior which makes them perfectly
suitable to do all kinds of static checking. For instance, can the
system deadlock, will it stay running, what can happen if an error
occurs and other questions can be answered automatically.
There are a lot of varieties of Petrinets. For all practical purposes
colored Petrinets should be used, however, because it might be too
much at once, we will first introduce elementary Petrinets. Elementary
nets offer a formalism that is relatively easy to explain and naturally
extends to colored Petrinets. A second reason why we introduce elementary
nets is that all existing Petrinet formalisms are based upon the
elementary ones.
Figure 1:
A Petrinet describing
a nonnested locking strategy.

Petrinets are drawn as box/circle diagrams. Figure 1
is a Petrinet describing the behavior of a noncounting semaphore.
Petrinets have a number of concepts:
 Places: places represent the state of a system. In our example,
these are the circles. The places are unlocked, unlocking, locking, locked
and acting. It is perfectly possible to have a Petrinet
in which multiple places contain a token. Token can be moved from
one place to another by transitions, however some rules should be
considered:
 Tokens: A place can have zero, one or more tokens. Simple Petrinets
only have boolean tokens. A token is either there or is not there.
In our example only the unlocked place contains a token.
Tokens which contain values will be discussed when we describe colored
Petrinets.
 Transitions: A transition specifies how a token is replaced
from one place to another. In our example, we have the transitions:
UnlockDone, Lock, LockFalse, LockTrue,
Unlock, ActDone and Act. A transition
can be either enabled or disabled. If all the arcs coming into a transition
offer a token the transition is enabled. In our case only the transition
Lock is enabled because the only incoming arc from Unlocked
offers a token. The transition Unlock is not enabled since
there is no token at Locked. When a transition is executed
all offered tokens are taken away from their place and transferred
to all the places which receive an arc from this transition. If we
would execute the transition Lock the token would be replaced
from Unlocked to Locking. Afterward the transition
LockFalse and LockTrue will be enabled. A
transition of a P/T net is enabled
only when all of its inputplaces offer a token and all its
output places are empty.
 Marking: The marking of a Petrinet contains all the places
that contain a certain token. The marking is in fact the global state
of a Petrinet.
The design of the locking strategy presented above, has transitions
that are executed by the actor automatically §transitions such as
returnLockFalse and transitions that can be executed by
others (transitions such as
lock). A Petrinet doesn't
distinguish between them. Every transition will bring a Petrinet
from one state to another. The question we must ask ourselves now
is whether there exist a sequence of transitions that will bring the
Petrinet in a state where nothing can be done anymore. In our example
this is not the case because every transition will remove 1 token
and place 1 token somewhere else (such Petrinets are called conservative).
Therefore the Petrinet will never be in a state where there is no
transition enabled, hence there is no deadlock. Moreover, because
every place in the net can reach any other place, the Petrinet will
never be in a place that locks out part of the Petrinet in the future,
hence we can always reach every possible marking. This is called liveness
of the Petrinet. So we are no only sure that the system is
deadlockfree,
we are also sure that it is
alive. So the implementation of
the concurrency strategy is OK, with respect to concurrency behavior.
Figure 2:
A typical producer consumer Petrinet.

Figure 2 is another P/T net. It describes
the behavior of two actors. The first actor is a producer of data,
the second is a consumer of data. In the above example, the only two
enabled transitions are produce and receive.
The above Petrinet is an illustration of how well Petrinets can
be combined.
To analyze the concurrency behavior of the above system, we can say
that the consumer is only alive when the receive operation is alive.
This is the case, only when the producer is alive and since this is
also the case, the Petrinet in general is alive. The same counts
for deadlockfreedom. The producer is deadlockfree if the place buffer
filled can contain a token in all possible futures. This is again
the case because the producer is alive and does not depend on anybody
else.
Petrinets can be implemented on controlflow machines, that is, machines
with a 'fetch', 'execute', 'store', architecture. To do so one needs
to keep a marking in working memory, to which all current transition
are tested to make a step. The current marking in the working memory
is then replaced by the new marking.^{1} However fast in execution, a typical control flow machine suffers
from one enormous bottleneck: the memory access: since every single
Petrinet step has to fetch and store data in the main working memory,
Petrinets are difficult to map efficiently to commonly used hardware.
Nevertheless, in the past, dataflow machines have been build which
are much more efficient in executing Petrinets. A dataflow machine
consists of a number of registers that holds tokens, a token is transferred
from operation to operation. In a typical dataflow machine an operation
has at most two inputregisters and at most two output operations.
The input registers are filled in by other instructions that wants
to pass a token to this operation. The destination registers contain
the addresses where to put the result. These addresses refer to the
input registers of other operations. Every operation has also two
signaling registers which are used to schedule the passing of tokens.
[Moo96] contains a description of a number of existing
dataflow machines. Not so strangely the evolution of dataflow machines
follows very closely the evolution of formal Petrinet models.
Figure 3:
Two Philosophers

Figure 3 shows two processes. The left process
tries two lock two resources. The right process tries to do the same.
 Can you point out how a deadlock can arise ?
 How would you solve the problem?
 Draw a Petrinet of a regular call.
 How would you verify its behavior if one of both processes
resets ?
 Draw a Petrinet of the behavior of the server, down
to the socket level. Make sure that at least two connections can
be accepted
The previous description describes elementary place/transition Petrinets
(elementary PTNets). Although enough to describe the basic operation
of a Petrinet they are barely useful in real life situations, unless
we add some syntactical sugar. We will now explain how Petrinets
have been extended to be more practically useful. One of the first
limitations one encounters is the lacks of values. Assume we want
to extend the Petrinet in figure 1
to a nested locking strategy using an elementary PTNet.
To do so, with an elementary PTNet we would need to specify for every
possible value of the lockcount variable a specific state,
(e.g: we would have states 1, 2, 3, 4, 5, ...) and transitions in
between them. This of course is a) no longer readable and as such
not suitable as a specification language and is b) from a programmers
point of view, not performant since we have a state explosion where
it deems not necessary.
Another similar problem is the impossibility to easily replicate states.
Consider the situation where we want to describe the interface behavior
of a binary semaphore playfield. It is very simple to describe the
behavior of a binary locking strategy for only a single square (see
figure 1). The problem that
now arises is how we should specify the same behavior for all squares
on the playing field ? Without extensions the only thing we can do
is write down a full exploded Petrinet, something that is clearly
not manageable.
Therefore low level P/T nets were extended with the concept of colored
tokens. Now instead of having only true/false tokens one can have
tokens which contain a specific value (or color).
This small extension to Petrinets complicates the formalism a lot.
It is not clear when a certain transition is enabled: can we specifically
check the color of a token or do we only check its presence. It is
also not clear what should happen when a transition is executed, what
color/value will the outgoing token(s) have ? Is it possible to send
different tokens to different places ? Below we will explain how colored
Petrinets are defined.
Figure 4:
A colored Petrinet illustrating a nested
locking strategy for a playing field of 32x32 squares.

From an informal point of view a colored Petrinet consists of places,
transitions, a relation in between them and expressions which are
used to verify incoming tokens/values and create new tokens/values.
The Petrinet in figure
4 illustrates how
an easy to understand colored Petrinet looks like for a nested locking
strategy in a playing field containing 32x32 squares. A number of
additional properties can be observed:
 First, every place has a type associated with it, a color set. This
type declares which possible values can be present at the given place.
For instance the Locking place has a type/color
.
is the set of possible X values, is the set of possible
Y values and is the set of possible lockcounts, an infinite
set indeed. The possible colors of the tokens, or values for short,
at the locking place are tuples which belong to the set
.
The values , are valid tokens, while the values
, are invalid tokens.
 Second, places can contain more than one token.
 Third, all arcs contain an expression which either describes the tokens
generated or the tokens to be matched. From the point of view of a
transition
 every incoming arc describes which tokens are looked for. For example,
the incoming arc on the 'Lock_True' transition needs a 3tuple,
if one is available, such as the variables ,
and will be bound to the values present in the token/tuple. So,
.
 every outgoing arc describes how new tokens are generated. If the
Lock_True transition is executed all incoming tokens are removed
from the input places and the output places receive newly created
tokens. For example, the outgoing arc of the Lock_True transition
contains the expression . Since the variables ,
and were bound to , and , the new token will be
. This token will be put in the place LockCount.
 Fourth, some transitions can contain guards. A guard is an expression
which verifies whether the transition is enabled given a number of
input tokens. A guard is also an expression in some sort of language,
which will be described later. A guard should evaluate to true or
false. When a guard evaluates to true the transition is enabled, when
the guard evaluates to false but still all tokens are present the
transition is not enabled. For example, the transition Unlock has
a guard . Intuitively this means that a lock cannot be released
if the lock is not held. The outgoing arc of the UnlockDone transition
has an expression which decreases the lock counter with
one. Because we are sure that the incoming token has a lockcount
larger than , the resulting token will always be in the set
.
 Fifth, the expressions used within guards and on arcs can be chosen.
However if one chooses a language too rigorous a lot of analyzing
power is lost. The language we will choose will be described below.
Figure 5:
A nested locking strategy upon
a squared playing field with only one place.

Given this, we can now clearly see the expressive power of Petrinets.
We can choose how much detail we include in our Petrinet. The Petrinet
given in figure 4 only covers the locking
of a single square with a lockcount. If we want we could add a session
ID to check whether the incoming lock request is from the same one
who already has obtained a lock. The fact that we do not need
to specify this, without losing the ability to reflect over the behavior
of the system is one of the greatest strengths of Petrinets.
It is even possible to describe the same behavior with only one place.
Therefore we need to add another color which describes whether
a certain position is in busy locking (busyL), busy unlocking (busyU)
or available (avail). The associated Petrinet, without acting logic
for the sake of simplicity is pictured in 5.
On the other hand if we need to use this Petrinet in a larger context,
in which we only need to know whether a place is locked or unlocked
we can split the LockCount state of figure 4
in two as depicted in figure 6.
Figure 6:
A large Petrinet describing the
behavior of a nested locking strategy on a playing field consisting
of 32 x 32 squares. There are separate states for 'unlocked' and 'locked'.
When locked a lock counter is kept.

The formal definition of a colored Petrinet given earlier handled
expressions as if they can be anything. Therefore we need to define
what kind of expressions we will use. The expression language we will
use has a syntax and semantics comparable to an enormously reduced
variant of Scheme [SJ75]. The syntax:
Semantically speaking those expressions are straight forward. In the
end everything evaluates to either a token or an integer. There are
no other values to work with. If a compound statement is found, the
arguments are evaluated in applicative order: they are all evaluated
recursively, after that the operator is applied to the given values.
 , respectively adds, multiplies all given arguments.
 , respectively subtracts, divides all arguments
results in . results in .
results in .
 , , are logic operations. Something is considered to
be true if it is not zero.

are comparison operators. They are not defined on
tokens.
Implementing an evaluator of CPNets seems trivial: instead of checking
whether a token is present and moving the token from the input places
to the output places we also have to check a guard. Unfortunately
it isn't that simple. Remember the formula 3,
if we want to know which transitions are enabled we must be able to
evaluate the right hand side of that expression. This means that we
must find a binding for which the guard (and accompanying expressions)
is satisfied. In contrast to an elementary net where we simply have
to check whether a token is present we now have to find out which
combination of tokens is suitable to satisfy the guard. Luckily,
when searching a suitable combination we only need to take into account
the set of all tokens present at places local to the transition under
investigation. This means that we don't have to check combinations
of tokens in places which are not immediately linked to the current
transition. This can be easily seen if we look at the two expressions
within formula 3. The first requirement,
there should be a , does not necessarily guarantee that
the values are present at the places local to t. In fact nothing says
where the values have to come from. It only guarantees that there
is a binding which satisfies the guard and which binds all necessary
values. The second part of the expression on the other hand
guarantees that all the values necessary to satisfy the guard are
present at the incoming places.
Practically this means that, when a transition has tokens in
total over all its input places (this set is called and there
are free variables (this set is called we must try out
all permutations over X. If there are many tokens this number grows
fast. Hence we cannot check whether a transition is enabled in .
A second aspect to evaluating a Petrinet is knowing which transitions
have a chance to be enabled. If we start with an initial marking
we know that we only have to check the transitions immediately bound
to the places containing tokens. So we only need to check out
.
If a certain transition is selected to be executed we need to change
the marking from to as specified in formula 4.
In human terms this equation transfers a certain amount of tokens
from the input place(s) to the output place(s). Thereby changing the
local states of all the input places and all the output places, formally
changing the state of
. The transitions
connected to these places:
are the only ones who can possible change from disabled to enabled
(or vice versa).
Because of this, it is important to have Petrinets with enough distinct
places: the amount of incoming tokens at a transition will be likely
smaller if we have more places in a Petrinet. Also, evaluating the
Petrinet can be much more oriented to a set of changed places as
specified earlier. For example, a Petrinet as in figure 5
is very small, with only one place. Given the fact that the net is
conservative^{2} and that we start with 3072 tokens, and there are 5 possible enabled
transitions, we need to check out 15360 possibilities. This number
rises exponentially with the number of input tokens taken by one transition.
In comparison, consider the Petrinet in figure 4,
we start with a token count of 1024 at place 'LockCount'. There are
3 possible output places so we need to check 3072 permutations.
Given the fact that we need to try out all permutations of incoming
tokens we might start thinking of using something like a logic engine
to evaluate a Petrinet. Indeed, it is very easy to write a Petrinet
evaluator in something like Prolog. To do so one simply needs to translate
the formal definition of a Petrinet to Prolog rules.
 Look at the producer/consumer Petrinet given earlier.
If we would interpret this as a colored Petrinet what would be the
difference ? How could we solve this problem ? Remember: a P/Tnet
only enables a transition if the outputplaces are empty. A CPNet
does not impose this requirement.
 Draw the Petrinets of the two dining philosophers as
a colored Petrinet.
 Draw the Java RMI call as a colored Petrinet. Make
sure that the same semantics are followed !
So, what is all this fuzz about Petrinets ? It's a nice formalism
and people like it, that's true, but why do a certain kind of people
spend so many nights studying them ? To know how to answer these questions,
and increase the universal IQ of the human race a tiny little bit,
continue reading our intriguing saga, in which we introduce a number
of very appealing properties of Petrinets. Properties that those
nightspending people like to call decidable, because they
define a problem for which an answer can be calculated in some automatic
way. In comparison to the answers given by mathematicians this is
a tremendous improvement since they often end up simply proving that
an answer exists to a certain problem without actually giving a way
to find it. On the other hand, this so called decidability,
often requires an exponential time to decide what they are supposed
to decide... even if it is a simple question. This, given the fact
that baretothemetal programmers doesn't like exponential solutions
to decide short answers, such as 'yes' or 'no', to not so large questions,
such as for instance 'will this thing never stop ?', diminishes the
fun a bit.
Luckily the past couple of decades, modelchecking specialists came
up with much better upper bounds to decide certain properties of Petrinets...
of course, only if the Petrinets follows certain rules, which most
computer scientists don't care about, they just like to think Petrinets
are easy to validate... :
 Boundedness: A Petrinet is bounded if the set of all possible
markings generated by a petrinet is finite. This property
is decidable, it is even possible to check whether the maximum amount
of tokens arriving at one place doesn't become larger than . In
this case a petrinet is called bounded.
 Reachability: A marking is reachable from marking
under Petrinet if there exists a sequence of transitions leading
from to :
.
This is a very important property because it allows us to decide whether
a certain error condition can be met or not. Recursively we can define
this as follows:

(1) 
 Deadlockfreedom: A Petrinet is deadlock free if every reachable
marking enables some transition. This property is decidable because
it can be reduced to the reachability problem.
 Liveness: A Petrinet is alive if every transition can always
occur again. Whether this is decidable or not is still an open question.
This will turn out to be an important property, because it tells us
that a certain concurrency strategy does not close any doors that
shouldn't be closed.
 Homestateproblem: A Petrinet has a home state if this
marking can be reached from every other marking. The question to decide
now is whether a given marking is a homestate for a certain Petrinet.
This problem has shown to be decidable.
 NonTermination: The question whether a Petrinet will never
terminate is generally speaking undecidable.
For a survey on the decidability of Petrinets see [
EN94].
All the above properties are valid on elementary nets and certain
colored petrinets, depending on the expression language chosen within
the colored net. However, a lot of petrinet variants exists which
introduce somehow a check for the absence of a token. In such petrinets
a transition can be enabled if there is
no token at a certain
place. If such a construction is added to a petrinet one loses all
decidability as is shown in chapter 7 of [
Pet81].
A reachability analysis of a Petrinet gives an answer how whether
we can reach a certain marking or not, often information is included
how this marking can be reached. Reachability is decidable [EN94].
However it might take a look time. Generally, it is NPcomplete.
However for a lot of Petrinet classes better results exist. For instance:
 If the petrinet is symmetric then the reachability problem
is EXPTIMEcomplete (see glossary). A petrinet is symmetric when
for every transition there is a transition that undoes
the effect of the first transition and returns back to the original
marking. This is a property which is often found in concurrency interfaces.
Once a lock is obtained it is possible to release it again. However,
aside from this intuition nothing guarantees that the petrinet also
exhibits this behavior.
 If the petrinet is conflictfree and bounded
then reachability is decidable in P. (see glossary) A Petrinet is
bounded when there is a maximum to the number of possible tokens present
at a certain place. A Petrinet is conflictfree if for every possible
marking the net is persistent. A petrinet is persistent if for every
place with more than one enabled output transition, the execution
of one transition does not disable the other transition. In the case
of concurrency interfaces this is highly likely because normally multiple
transitions will not be enabled at once and the amount of resources
remains fixed.
Other extensions to petrinets may harm these relatively positive
results. For instance:
 Reachability in timed petrinets is NPcomplete [LLPY97,BP96]).
 Our expression language is no standard language so we don't exactly
know whether all these proofs holds with the given language. I assume
it does, because the language does not allow destructive operations,
nor does it have access to a memory, nevertheless we cannot be sure
of this.
 Colored petrinets makes all these formal approaches a bit problematic.
Expanding a colored petrinet to a simple petrinet may require an
infinite explosion, hence all these decidability criteria needs to
be investigated again.
The reachability of marking
from marking
is often
decided by creating a reachabilitygraph. Hereby the nodes of the
graph contain a marking and the arcs contain the transition that brings
one from marking a to marking b. Reachability is then decided by creating
a matrix containing on the X/Yaxis all possible nodes/markings. The
values within the matrix declare whether X is reachable from Y. If
it is a 1 is placed, if it isn't a zero is placed. With every step
more 1's are filled in by taking the transitive closure of the reachability
graph. This approach is formally very nice, drawback is that it takes
too much times since often we only want to know whether A is reachable
from B and not whether all possible A 's are reachable from all possible
B 's.
Another approach is the construction of an unfolding of a Petrinet
[ERV96]. An unfolding of a Petrinet is a new
petrinet, usually with an infinite but simpler structure. McMillan
proposed an algorithm for the construction of a finite initial prefix
of the petrinet, which contains full reachability information. However,
this information is difficult to generate, and can take a long time.
Therefore we didn't investigate this track further.
To ease the pain of deciding reachability, other tools are possible.
For instance it is possible to exploit symmetry between states by
only looking at one side of the symmetry. To feed the reader's intuition:
within a dining philosopher petrinet there is a 4 way symmetry. There
is no need in trying out every philosopher, which reduces the state
explosion drastically. how this can be done in practice is described
in detail in [Jør].
We will now formally define what a Petrinet is. This definition is
loosely based upon [Rei00]. Formally speaking, an
elementary PTNet is a triple whereby contains all
the states, contains all the transitions and contains the
flow relation, that is the linkage between states and transitions.
, and are finite sets.



whereby
and
For future reference we define
 the places of Petrinet
 the transitions of Petrinet
 the flow relation of Petrinet

as the union of places and transitions of
Petrinet .
The above formal definition of a Petrinet describes only the static
structure of a Petrinet. It doesn't contain any dynamic properties.
To add these we extend the definition with a dynamic aspect: the places
that contain a token, or in other words: the marking. A Petrinet
extended with a marking is called an elementary Petrinet.
An elementary Petrinet is a 4tuple
whereby
describes the underlying Petrinet and defines the marking (which
tokens are where). is the initial marking, or the startup
tokens of the Petrinet. To define the transition from one Marking
to another (or from one elementary Petrinet to another elementary
Petrinet) we need to define pre and postconditions of a single
transition:
Informally, the above definition states that the precondition of
is the set of all elements, either places or transitions, which have
a link toward . The postcondition of is the set of all places
or transitions that have an outgoing link toward . We can easily
extend this pre, postcondition definition of a transition to a
set of transitions.
A transition is enabled, given marking if and only
if all preconditions of hold for and no postcondition of
holds for . We will write this down formally as:
The notation
can be read as: transition
from Petrinet is enabled under marking .
When an enabled transition is executed the precondition of
the transition is removed from the marking and the postcondition of
the transition is added to the marking. We write this down as
This notation can be read as: under marking the transition
of Petrinet give rise to marking
A marking does not often gives rise to another uniquely defined marking.
Depending on the executed transition other markings could be the result.
Formally,
This can be read as: Given marking and Petrinet , then
contains all the possible markings after one
transition.
Some properties of elementary Petrinets are:
 Every place can contain at most one token. No duplicates are
allowed.
 Tokens represent boolean values: true or false, no content can be
passed from one place to another
 Given a certain transition, the time necessary to check the preconditions
and postconditions is known:
.
This is a nice property since it allows us to execute an elementary
Petrinet at a fixed rate.
We will now define Colored Petrinets formally. The definition given
below is, to a large extent, based on the well known work of [Jen94].
However, other and often older definitions exists such as referenced
in [EK98].
Before we can explain the nitty gritty detail of colored Petrinets
we need the ability to describe multiple tokens at the same place.
Since this is something that cannot be easily expressed with mathematical
sets, one resorts to multisets:
A multiset is a set in which every element can occur multiple
times. Formally a multiset is defined over a certain underlying
set as a function that maps every element of S to a natural number:
. The domain of the multiset: the occurrence
counts of every possible element of are called the coefficients
of . All possible multisets associated with a certain set
will be denoted as . This should not be compared
to the powerset, denoted which is the set of all possible
subsets.
A second preliminary before we can explain the formal side of colored
Petrinets are expressions. The guards and actions work on
values. The way in which these are represented is currently left open,
any type of expression can be inserted into a colored Petrinet. For
example, one can use expressions, or simple algebraic expressions.
One can choose whatever fits best. Of course, certain formal analysis
will no longer be possible if one chooses a language too expressive.
On the other hand, since we are not interested in model checking at
this stage we can safely choose expressions. Once one has
chosen an expression language one cannot change this anymore within
the same Petrinet. In the following definitions we will refer to
an expression as . (with a capital) refers to all possible
expressions. For every expression it should be possible
to obtain the type and free variables. We should also be able to evaluate
it under a certain binding of values to variables:
 A type is a set of possible values, e.g; a type can be something like
or it can be something like
.
A type is not necessarily infinite. The boolean type:
will be referenced to as 'bool'.
 returns the set of unbound variables within .
 returns the set of possible values the expression can
return.
 A binding of a set variables which associates with each element
an element out of . So
 The value of an expression under a certain binding is
written down as
. The expression is evaluated
similarly to calculus by substituting every variable
with the value .
We are now ready to define a colored Petrinet formally: A CPNet is
a tuple
whereby
 is a non empty set of types, called color sets.
 , , are, similarly to low level Petrinets, the places,
transitions and the flow relation between places and
transitions.
. The flow relation A
contains tuples from
. This is in contrast
to the definition given in [Jen94], in which a nodefunction
is added to the Petrinet which maps an arc to such a tuple. This
little change however doesn't change any semantics associated with
the net as explained in [Jen94].
 is a color function,
. This function associates
a type with every place. All tokens present at a place must be
of type .
 is a guard function,
such that
.
Informally speaking, we associate with every transition an expression
(the set of all expression is called ). This expression should
result in a boolean type and all variables used within the expression
should be known, hence be part of .
 is an arc expression, or action:
such
that
whereby the place of is. The arc expression associates with
every arc an expression, which will be used to verify or create new
tokenvalues. Every arc expression should evaluate to a set of tokens
(a multiset over the different types allowed by the place).
contains input expressions as well as outgoing actions.
 is an initialization function:
such that
has no free variables and
The above describes the static structure of a CPNet. To describe the
dynamic behavior of a CPNet we will do similar things as with the
low level elementary PTNets. First, describe what a marking is, then
describe when a transition is enabled and what happens when a transition
is executed. But before we do so, some syntactical sugar:

which returns the arcs
associated with the transition t.

A binding of a transition
is a function
such that
The set of all bindings for
is called
. A token element
is a couple
with
and
. A binding elements
is a couple
with
and
. The set of all
possible token elements is called
, the set of all possible binding
elements is called BE. Now we can define a marking:
A marking is a multiset over . The initial marking
is obtained from as follows

(2) 
When is a transition
enabled ?

(3) 
This means that there must exist a binding satisfying the guard ()
and all expressions placed on the incoming arcs result in something
of the correct type. When an enabled transition is executed the
marking changes to as follows :

(4) 
 [coNP] A problem is coNP if is NP. coNP
problems often seem harder than NP problems, however it is still
an open question whether coNP = NP.
 [EXPTIME] A problem of size is EXPTIME if there is a constant
and the time to solve the problem takes at most .
 [EXPTIMEcomplete] A problem is EXPTIMEcomplete if it is in EXPTIME
and other problems within EXPTIME are reducible to it. Essentially
this declares a class of problems which can be solved within exponential
time. It is known that EXPTIME PTIME.
 [Nondeterministic] A machine is nondeterministic if it may execute
different branches parallel on the same input.
 [NP] A problem is NP if it can be solved in polynomial time by
a nondeterministic machine.
 [NPcomplete] A problem is NPcomplete if other NPcomplete
problems can be reduced to it.
 [P] A problem of size is P if there is a constant and
the time to solve the problem is at most .
 [Pcomplete] A problem is Pcomplete if it is in P and other problems
are reducible to it.
 [Phard] A problem is Phard if itself is not necessarily in P
but other Pproblems may reduce to it.
Petrinets have a number of very appealing properties. For an indepth
discussion of all these properties of Petrinets, see [KCJ98].
 They are specified by means of a graphical representation.
A representation that is intuitive and covers in one drawing enough
detail to understand what the represented model is about.
 Petrinets have a description of both states and actions, this
in contrast to state diagrams or transition diagrams, which cover
only part of the behavior of a system.
 Colored Petrinets even include data manipulation within the
Petrinet. A colored Petrinet covers state transition, state of a
system and data manipulation in one drawing.
 Petrinets are a formalism that can describe a system at any
level of abstraction. Petrinets can be used to describe the interaction
between high level modules as well as the full interaction within
these modules. Petrinets can be described to specify a large variety
of different systems. This can be illustrated by pointing out the
number of practical situations in which Petrinets have helped.
 The basic building blocks of Petrinets are places, transitions
(and tokens for colored Petrinets). These primitives are easy to
understand and very powerful.
 Petrinets allows modularization of systems by means of hierarchical
decomposition. Petrinets can be combined using certain operators,
which we will not discuss here. See [BFF^{+}95] for
more information.
 For real time systems, Petrinets can be extended with a time
concept. [PM93,BMAPY97]
 Petrinets are stable toward minor changes of the modeled system.
This is proved by many practical experiences. It means that small
modifications of the modeled system does not require a complete rewrite
of the Petrinet. In many other description languages this is not
the case (e.g.: finite automaton).
 Petrinets have a large number of formal analysis, by which
properties of the modeled system can be verified. This includes: construction
of occurrence graphs (which global states are reachable), calculation
of invariants (pre and post conditions checking), reductions
(shrink down a Petrinet but still preserve a number of properties)
and checking of structural properties (such as starvation).
 BFF^{+}95

Eike Best, Hans Fleischack, Wojciech Fraczak, Richard P. Hopkins, Hanna
Klaudel, and Elisabeth Pelz.
A Class of Composable High Level Petri Nets with an Application
to the Semantics of .
In Giorgia De Michelis and Michel Diaz, editors, Application
and Theory of Petri Nets, volume 935 of Lecture Notes in Computer
Science, pages 103120. Springer Verlag, 1995.
Describes a set of high level operations to compose
petrinets.
 BMAPY97

Marius Bozga, Oded Maler, Amir Pnueli, and Sergio Yovine.
Some Progress in the Symbolic Verification of Timed Automata.
In O. Grumberg, editor, Proc. 9th International Conference on
Computer Aided Verification (CAV'97), volume 1254, pages 179190.
Springer Verlag, 1997.
Describes how BDD (Binary Decission Diagrams) can be used in
certain domains for a faster timing verification of large Petri Nets.
 BP96

Eike Best and Ctuscia Palamidessi.
Linear Constraint Systems as HighLevel Nets.
In Ugo Montanari and Vladimiro Sassone, editors, CONCUR, volume
1119, pages 498513. Springer Verlag, 1996.
Makes the mapping from linear programming to timed
Petrinets. Also proves that constructing a reachability graph of timed
PetriNets is NPcomplete.
 EK98

Mohammed Elkoutbi and Rudolf K. Keller.
Modelling Interactive Systems with Hierarchical Coloured Petri
Nets.
Proceedings of the Conference on High Performance Computing,
April 69 Boston 1998.
Given a set of UML usage scenarios, a Petrinet is
generated.
 EN94

Javier Esparza and M. Nielsen.
Decidability Issues for Petri Nets.
In Bulletin of the EATCS, volume 52, pages 115129, February
1994.
A good introduction to the decidability issues of
Petrinets.
 ERV96

Javier Esparza, Stefan Romer, and Walter Vogler.
An Improvement of McMillan's Unfolding Algorithm.
In Int'l Proceedings of Tools and Algorithms for Construction
and Analysis of Systems, volume 1055 of Lecture Notes in Computer
Science, pages 87106. Springer Verlag, 1996.
Explains the reason behind Petrinet unfolding, their
limitations and improves McMillans original algorithm.
 Jen94

K. Jensen.
An Introduction to the Theoretical Aspects of Coloured Petri
Nets.
In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency, volume 803 of Lecture Notes In Computer
Science, pages 230272. Springer Verlag, 1994.
Very good introduction to coloured petri nets. A must read
for everyone involved with petrinets. Also covers formal analysis of Petri
Nets.
 Jør

Jens Bæk Jørgensen.
Construction of Occurrence Graphs with Permutation Symmetries
Aided by the Backtrack Method.
Technical report, Computer Science Department, University of
Aarhus, Ny Munkegade, Bldg. 540, DK8000 Aarhus C, Denmark.
Explains how to detect selfsymmetries during reachability
analysis by means of backtracking. However, not a published paper, it is a
very interesting read.
 KCJ98

Lars M. Kristensen, Soren Christensen, and Kurt Jensen.
The Practitioner's Guide to Coloured Petrinets.
International Journal on Software Tools for Technology
Transfer, pages 98132, 1998.
This paper provides a comprehensive road map to the
practical use of CPNets and the Design/CPN tool. The paper is selfcontained
and does not assume any prior knowledge of Petri nets.
 LLPY97

K. Larsen, F. Larson, P. Pettersson, and W. Yi.
Efficient Verification of RealTime Systems: Compact Data Structure
and StateSpace Reduction.
In Presented at 18th IEEE RealTime Systems Symposium. San
Francisca, California, USA, pages 1424, December 1997.
Tries to solve the memoryrequirements of reachability
checks of timed automata.
 Moo96

Simon W. Moore.
Dataflow machines.
University of Cambridge,
http://www.cl.cam.ac.uk/users/swm11/dataflowlecture/dataflowlecture.html
#compare, 25 April 1996.
Historically interesting pages. It is surprising to see how
the evolution of dataflow machines follows closely the evolution of Petri
nets.
 Pet81

James L. Peterson.
Petri Net Theory and the Modeling of Systems.
PrenticeHall, Englewood Cliffs, New Jersey, April 1981.
Chapter 7 describes how a number of extensions to Petrinets
break certain decidability issues.
 PM93

P.Altenbernd and R. Milczewski.
Description of Timing Problems Using Petri Nets for
LevelIndependent Timing Verification.
Int'l Proceeding ACM/SIGDA Workshop on Timing Issues in the
Specification and Synthesis of Digital Systems (TAU), August 1993.
Describes a number of complementary techniques to verify the
dynamic and static aspects of timed petri nets.
 Rei00

W. Reisig.
An Informal Introduction To Petri Nets.
Proc. 21st Int'l Conf on Application and Theory of Petri Nets,
Aarhus, Denmark, Humboldt University of Berlin, June 2630 2000.
Although a difficult read, it's a good introduction to the
formal aspects of elementary Petrinets.
 SJ75

G. J. Sussman and G. L. Steele Jr.
Scheme, an Interpreter for Extended Lambda Calculus.
December 1975.
The original paper that introduces Scheme. The paper itself
is written on a good old fashioned typewriter, and some nostalgy can be found
between the lines. A must read.
Footnotes
 ...^{1}
 Instead of testing all transitions to a certain marking it would be
more useful to check only all postconditions of a marking.
 ...
conservative^{2}
 A Petrinet is said to be conservative if the total amount of tokens
present doesn't change over time.