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

siderably reduce the state space size, hence the time and space required
to generate the RG of the priority model are usually less than the space
and time required to generate the RG of the corresponding model without
priority.
Since enabling is more restricted than in the corresponding PN model with-
out priority, reachability is not preserved in general by the addition of a
priority structure. However, a marking M 0 is reachable from a marking M
in a PN model with priority only if it is reachable in the corresponding PN
model without priority. For example, in the priority PN model representing
the readers & writers system, the marking M 0 = p 5 +Kp 6 remains reachable
after the introduction of priority, while the marking M 00 = Kp 2 + p 5 that
was reachable in the PN model without priority, is not reachable after the
introduction of priority, if K > 1.
Boundedness — Boundedness is preserved by the introduction of a pri-
ority structure in the sense that a bounded PN model remains bounded
after the introduction of a priority specification. This implies that the use
of P-semiflows to study the boundedness of a PN model can be applied to
the model without priority M associated with a priority PN model M π and
if the former model is shown to be structurally bounded, the conclusion can
be extended to the latter model. In the examples that will be presented in
later chapters of this topic we shall use P-invariants to check boundedness
of GSPN models exploiting this observation.
Observe that an unbounded PN model may become bounded after the spec-
ification of an appropriate priority structure. Consider for example the PN
model depicted in Fig. 4.3. The structure is typical of an unbounded PN
model, in which the marking of place p 1 can grow indefinitely due to the re-
peated firing of transition t 1 . If we add the priority specification π 1 = 0 and
π 2 = 1, however, the PN model with priority becomes 1-bounded (provided
that M 0 (p 1 ) ≤ 1), since transition t 1 is no more enabled (although it still
has concession) after putting one token in p 1 , until the firing of t 2 removes
it. As a consequence, if we cannot show that the model without priority
M associated with a priority PN model M π is bounded, we have to devise
more powerful proof techniques that take into account priority to show the
boundedness of model M π . Observe that this kind of problem arises also
in PN models with inhibitor/test arcs: indeed the PN model depicted in
Fig. 4.4 is 1-bounded even if the P-semiflows computation doesn't allow this
property to be discovered.
Liveness and liveness degree — This property is intimately related
to the enabling and firing rules, hence it is greatly influenced by a change
in the priority specification: a live PN model may become not live after
the introduction of an inappropriate priority structure and, viceversa, a PN