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

Reachability — To check whether a marking M 0 is reachable from a
marking M in a given PN system, it is only necessary to check if RG com-
prises a directed path connecting M to M 0 . The concatenation of the la-
bels of the arcs forming the path gives the transition sequence σ such that
M[σ i M 0 .

Reversibility — To check whether a given marking M is a home state,
it is su cient to build the set of all the markings that can be reached by
following backwards in the RG any path entering M, and to verify that this
set is RS(M).
A PN system is reversible if and only if its initial marking is a home state.
This is true if and only if the RG has a unique strongly connected component
that contains M 0 .

Absence of deadlock — The presence of a deadlock can be checked on
the RG by looking for a dead marking, i.e. a node with no output arcs. The
absence of such a node is su cient to guarantee the absence of deadlock.

Liveness — Transition t of a PN system is live if and only if from every
marking M ∈ RS it is possible to reach a new marking M 0 such that t ∈
E(M 0 ). In [64] the following characterization of the liveness property in
terms of the RG structure is given:

t is live if and only if

• the RG contains no dead marking;

• t labels some arc of every strongly connected component of RG.

It is easy to check on the RG of Fig. 2.4 that t 5 is live: the RG has no dead
marking, it has a unique strongly connected component, and t 5 labels, for
example, the arc connecting M 4 and M 8 .

A place p ∈ P of a PN system is k-bounded iff Boundedness —

k = max

M∈RS M(p)

Of course this can be computed only for finite reachability sets.

Mutual exclusion — Mutual exclusion between places p and p 0 in a
given PN system is checked by verifying that

∀ M ∈ RS : M(p) · M(p 0 ) = 0