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

An important reachability property is reversibility: a PN system is said to
be reversible if and only if from any state reachable from M 0 , it is possible
to come back to M 0 itself. In more formal terms, a PN system with initial
marking M 0 is reversible if and only if ∀ M ∈ RS(M 0 ),M 0 ∈ RS(M). Re-
versibility expresses the possibility for a PN system to come back infinitely
often to its initial marking.
It is however possible that the state to which we want to be always able
to come back is not the initial marking of the PN system. We say that
M ∈ RS(M 0 ) is a home state for the PN system if and only if ∀ M 0 ∈
RS(M 0 ),M ∈ RS(M 0 ).
Absence of deadlock — A PN system contains a deadlock if it can reach
a state in which no transition can be fired. A PN model is deadlock-free
if all PN systems that can be obtained by instantiation of its parametric
initial marking are deadlock-free.
There is no definition of deadlock-freeness for Petri nets. As we shall see in
a later section it is instead possible to determine whether a Petri net can
potentially have a deadlock, depending on its graph structure.
Liveness — A transition t is said to be live in a PN system if and only if,
for each marking M reachable from M 0 , there exists a marking M 0 , reachable
from M, such that t ∈ E(M 0 ). A transition t is said to be live in a PN model
if it is live in all PN systems obtained from the PN model by instantiating
the parametric initial marking MP to an initial marking M 0 . A PN system
is said to be live if all t ∈ T are live in it. A PN model is said to be live if
every PN system, obtained by instantiating the parametric initial marking,
is live. Finally, a Petri net is live if there exists a live PN system obtained
from the net. Liveness of a Petri net is an existential property since in most
cases it is possible to build a corresponding PN system that is not live: just
take as initial marking one for which no transition is enabled.
The PN model of our readers & writers example in Fig. 2.1 is live for any
K ≥ 1. This means for example that from any possible marking there is at
least one evolution that allows another read or another write to take place.
A transition that is not live is said to be dead. For each dead transition t, it
is possible to find a marking M such that none of the markings in RS(M)
enables t.
A very important consequence of liveness is that, if at least one transition is
live, then the PN system cannot deadlock. However, the absence of deadlock
is not a su cient condition for a PN system to be live: a system without
deadlock states and with some dead transitions is partially live.
Liveness defines the possibility for a transition to be enabled (and to fire)
infinitely often. If instead we are interested in more detailed information,
that is whether the transition may be enabled infinitely often with enabling