Graphics Programs Reference
In-Depth Information
Mutual exclusion — When PN models are used for the validation or
verification of systems, it is important to know whether two transitions can
never be enabled in the same marking, i.e., whether two transitions are
mutually exclusive. In formulae:
Definition 2.3.9 (Mutual exclusion) For any PN system
S
, transitions
t
l
and t
m
are mutually exclusive iff
6∃
M
∈
RS(M
0
) : t
l
∈
E(M) and t
m
∈
E(M)
(2.8)
Observe that while conflict, concurrency, confusion and causal connection
are properties of a single marking, mutual exclusion is a property of two
transitions in a given system, and needs therefore to be proved by cheking
every reachable marking, at least in principle.
2.4
Properties of Petri Nets
Several important properties of PN models, PN systems and Petri nets, can
be defined and proved with suitable analysis tools. Proving properties is a
key step in the analysis of PN models, since it allows statements to be made
about the modelled system behaviour in an objective manner.
We introduce several of the most useful properties below, and we comment
on their usefulness with respect to the modelling and analysis process. We
discuss in the next section what analysis methods can be used to prove these
properties, while we shall present examples of proofs in the chapters devoted
to applications.
Reachability and reversibility — As defined in the previous sections,
a marking M
0
is reachable from M if there exists a sequence σ
M
such that
initial marking M = 2p
1
+ p
5
; the transition sequence σ
M
= t
1
,t
1
,t
2
,t
3
,t
4
is fireable in M and M[σ
M
i
M
0
where M
0
= p
4
+ p
6
. Observe that also the
following holds: M[σ
0
M
i
M
0
where σ
0
M
= t
1
,t
3
,t
1
,t
2
,t
4
; we can thus conclude
that there are at least two different sequences fireable in M that lead to the
same marking M
0
.
Reachability can be used to answer questions concerning the possibility for
the modelled system of being in a given marking M. Returning to our basic
example in Fig.
2.1,
suppose we want to know whether it is possible for all
the processes to execute a read at the same time. In terms of reachability
analysis this is equivalent to asking whether the marking M
0
with K tokens
in place p
6
is reachable from the initial marking. If the number of markings
in the reachability set is finite, and a maximum value for K is fixed, this
question can be answered in finite time by inspecting the different reachabil-
ity sets (one for each value of K). The parametric proof valid for arbitrary
values of K may instead be nontrivial to carry out.
Search WWH ::
Custom Search