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

This example shows that liveness, being an eventuality property, does not
extend smoothly from a PN model to a priority PN model with the same
structure. However, as long as we accept that we have to build the complete
RG, we don't have problems in checking any kind of property of priority
PN systems. Observe that even for PN models structural liveness is not
proved simply by applying an automatic algorithm (except for some simple
subclasses of PN models) but rather it is proved by the modeller on a case
by case basis, using the net structure and some information from P and
T-invariants. Hence the addition of priority only adds one more constraint
to be taken into account by the modeller when devising the proof.

Reversibility and home states — These are eventuality properties,
hence the addition of a priority structure may change drastically the be-
haviour of a PN model. As for the other properties in this class, the con-
struction of the RG allows them to be checked on a particular PN system.
Also in this case proofs performed on the model can take advantage of the
information coming from the P and T-invariants computation.

4.4 Structural Analysis Techniques

4.4.1 Linear algebraic techniques

Structural results based on the incidence matrix apply to PN models with
priority in the same way as for PN models without priority. Transition
priorities are not taken into account in the incidence matrix, like inhibitor
and test arcs. This may result in the loss of some invariance relations, but
never in the computation of wrong relations. For example, in the PN model
in Fig. 4.3, the relation M(p 1 ) ≤ max(1,M 0 (p 1 )) cannot be derived from
the incidence matrix since it is enforced by priority.

P- and T-semiflows — P- and T-semiflows define marking-independent
invariance relations for which it makes no sense trying to take priority into
account. Hence, P- and T-semiflows can be defined, computed and exploited
in exactly the same way as for PN models without priority.
The addition of a priority structure may introduce new parametric invariant
relations that do not hold true in the corresponding PN model without
priority. Fig. 4.3 provides an example of the existence of such cases. Indeed,
in the example, the marking of place p 1 is less than or equal to one, due
to the fact that its output transition t 2 has higher priority than its input
transition t 1 , that O(t 2 ) = I(t 1 ) = 1, and that M 0 (p 1 ) = 0.
Another example is provided by the priority PN model of Fig. 4.6. It is
covered by a unique P-semiflow comprising all the places. Hence the model
has one P-invariant:
M(p 1 ) + M(p 2 ) + M(p 3 ) = K.