PETRI NETS AND THEIR PROPERTIES - Modelling with Generalised Stochastic Petri Nets - page 44

It is possible to visualize the T-semiflows above as paths in the graph rep-
resentation of the net, as shown in Fig. 2.14.
It may be possible in some cases to prove that a PN system (or model) is
not live using structural techniques: since the covering by T-semiflows is a
necessary condition for liveness of bounded nets, if at least one transition
is not included in any T-semiflow, while the net is covered by P-semiflows
(hence being structurally bounded), the net is not live (as well as any PN
system or model with that same structure).

2.5.2 Graph-based structural techniques

In this section we define deadlocks and traps [ 54, 25] which are particular
configurations of a Petri net useful to study the liveness of PN systems.
Furthermore, some structural relations between transitions are defined, that
allow the definition of necessary conditions for the occurrence of situations
such as conflict, mutual exclusion and confusion in PN systems.

Deadlocks and traps — The following definitions of deadlocks and traps
are restricted to PNs without inhibitor arcs and in which all arc weights are
either zero or one (ordinary nets).

Definition 2.5.2 A deadlock is a subset of places P D ⊆ P such that the set
of its input transitions is a subset of the set of its output transitions; that is:
[ [

{ • p }⊆ { p • }

p∈P D p∈P D

Definition 2.5.3 A trap is a subset of places P T ⊆ P such that the set of
its output transitions is a subset of the set of its input transitions; that is:
[ [

{ p • }⊆ { • p }

p∈P T p∈P T

Deadlocks and traps can be used to study the liveness of systems by exploit-
ing the following properties:

• there is no way of increasing the total marking of an empty deadlock
P D : once a deadlock has lost all its tokens, all transitions that have
an input place in P D cannot fire; as a consequence the system is not
live.

• if a trap is marked in the initial marking, then it will never lose all its
tokens; hence a good way to ensure that a deadlock will not lose all
its tokens is to make sure that it contains a trap marked in the initial
marking.