Graphics Programs Reference
In-Depth Information
that the PN marking is intrinsically “distributed”.
2.3.2
Reachability set and reachability graph
The firing rule defines the dynamics of PN models. Starting from the initial
marking it is possible to compute the set of all markings reachable from it
(the state space of the PN system) and all the paths that the system may
follow to move from state to state. Observe that the initial state must be
completely specified (specific values should be assigned to all parameters) for
the computation of the set of reachable markings, so that this computation
is possible only for PN systems.
Definition 2.3.3 The Reachability Set of a PN system with initial marking
M
0
is denoted RS(M
0
), and it is defined as the smallest set of markings
such that
•
M
0
∈
RS(M
0
)
•
M
1
∈
RS(M
0
)
∧∃
t
∈
T : M
1
[t
i
M
2
⇒
M
2
∈
RS(M
0
)
When there is no possibility of confusion we indicate with RS the set
RS(M
0
). We also indicate with RS(M) the set of markings reachable from
a generic marking M.
The structure of the algorithm for the computation of the RS of a given
PN system is simple: the RS is built incrementally starting from the set
containing only M
0
. New markings are then iteratively added into the RS
by selecting a marking M that is already present in the RS and by inserting
all the new markings that are directly reachable from M. Once a marking M
has been considered in an iteration, it must not be considered in successive
iterations. Moreover, if a marking is reachable by many markings it is
obviously added only once in the RS. The algorithm does terminate only if
the reachability set is finite.
Fig.
2.3
shows the RS of the readers & writers PN system obtained from
the PN model in Fig.
2.1
by setting K = 2.
The RS contains no information about the transition sequences fired to reach
each marking. This information is contained in the reachability graph, where
each node represents a reachable state, and there is an arc from M
1
to M
2
if the marking M
2
is directly reachable from M
1
. If M
1
[t
i
M
2
, the arc is
labelled with t. Note that more than one arc can connect two nodes (it is
indeed possible for two transitions to be enabled in the same marking and
to produce the same state change), so that the reachability graph is actually
a multigraph.
Definition 2.3.4 Given a PN system, and its reachability set RS, we call
Reachability Graph RG(M
0
) the labelled directed multigraph whose set of
Search WWH ::
Custom Search