PETRI NETS WITH sPRIORITY - Modelling with Generalised Stochastic Petri Nets - page 81

two transitions t i and t j at the same priority level and a third transition t k
causally connected to either t i or t j and such that π k = π i = π j .
Concerning indirect conflict, observe that it can never arise if π 4 = π 5 . If
instead π 4 > π 5 and either (a) π 8 = π 9 = π 5 or (b) π 2 = π 3 = π 5 , then an
indirect conflict between t 5 and t 9 or between t 5 and t 2 can be observed. A
structural necessary condition for indirect conflict is the presence of a non
free-choice conflict comprising at least two transitions t i and t j such that
π i > π j .

4.3 Properties of Priority PN Models

In this section, we discuss the impact of priority on the properties of PN
models. In particular, we are interested in observing the relation between
the properties of a priority PN model and the properties of the underlying
PN model without priority. The practical reason for studying this rela-
tion is that some of the properties can be e ciently checked using algo-
rithms that apply only to models without priority. Properties can be di-
vided into two broad classes: properties that must hold for all states in the
state space (in the literature these are called safety or invariant properties)
and properties that must hold for some state (called eventuality or progress
properties). Examples of invariant properties are absence of deadlock
( ∀ M ∈ RS(M 0 ),E(M) 6 = ∅ ), boundedness, and mutual exclusion. Examples
of eventuality properties are reachability (a given marking will be eventually
reached) and liveness (a transition will eventually become enabled).
Let M π be a PN model with priority and let M be the underlying PN
model without priority. Since the introduction of priority can only reduce
the state space, all the safety properties that can be shown to be true for M ,
surely hold also for M π . Eventuality properties instead are not preserved
in general by the introduction of a priority structure.
It is interesting to observe that P and T-invariants describe properties that
continue to hold after the addition of a priority structure. The reason is
that they are computed only taking into account the state change caused by
transition firing, without any assumption on the possibility for a transition
of ever becoming enabled.
Let us consider the properties of PN models of general interest and discuss
their extension to priority PN models.

Reachability — The reachability property for PN models with priority
is defined in terms of enabling and firing, as was already the case for PN
models without priority. If we check reachability by generating the complete
reachability set, there is no problem in computing the RS for the PN system
with priority since precise enabling and firing rules have been defined for
the extended formalism.

Moreover, the introduction of priority may con-