Page 66 -

2 The Language: Rationale and Fundamentals 53

A state M n is called reachable from state M 1 (denoted M 1 ! M n ) if and only if
t 1 t 2
there is a firing sequence D t 1 t 2 t 3 ::: t n 1 such that M 1 ! M 2 ! :::
t n 1
! M n .
We use .PN; M / to denote a Petri net PN with an initial state M. On the basis of
this, we can define some additional properties for Petri nets.

Definition 3. (Live).APetri net .PN; M / is live if and only if, for every reach-
able state M and every transition t, there is a state M reachable from M ,which
0
00
0
enables t.
The notion of liveness is important as a Petri net which demonstrates that at least
one transition can fire in every reachable state is deadlock free. Being deadlock free
is a desirable property for a Petri net. Another important property is boundedness,
which ensures that the number of tokens in a net cannot grow arbitrarily.

Definition 4. (Bounded).A Petri net .PN; M / is bounded if and only if, for every
reachable state and every place p, the number of tokens in p is bounded.

Another useful and related property is coverability, which allows two states to be
compared.

Definition 5. (Coverable):A marking M in Petri net .PN; M / is said to be
0
coverable if there exists a reachable marking M such that M M :
00
00
0
A final property of Petri nets that proves to be useful when reasoning about them is
that of strong connectivity, defined as follows.
Definition 6. (Strongly connected). A Petri net is strongly connected if and only
if, for every pair of nodes (i.e., places and transitions) x and y, there is a directed
path leading from x to y.

Figure 2.15 provides an example of a Petri net used for modeling a business process.
In this case it shows an order fulfillment process. This proceeds first with a take
order task and then the pack order and check account tasks execute in parallel.
When they have both completed, the credit check task executes, and if the customer
has sufficient credit remaining, the order is despatched. If not, the decline order task
runs and the customer is advised and finally the return stock task ensures that the
items from the order are returned to the warehouse.

check account decline return
order stock
take order credit
check
pack order despatch
Fig. 2.15 Petri net example: order fulfillment process