Graphics Programs Reference
In-Depth Information
degree k, then we are interested in the so-called k-liveness of a transition.
A transition t in a PN system is k-live if and only if from every reachable
marking M it is possible to reach a marking M 0 such that ED(t,M 0 ) = k.
Boundedness — A place p of a PN system is said to be k-bounded if and
only if, for each reachable marking M, the number of tokens in that place
is less than or equal to k. A PN system is said to be k-bounded if and only
if all places p P are k-bounded.
A PN model is said to be k-bounded if every PN system obtainable through
a suitable instantiation of the parametric initial marking is k-bounded.
PN models and PN systems that are 1-bounded are said to be safe.
Pn models and PN systems that are K-bounded for some k are said to be
bounded.
A very important consequence of boundedness is that it implies the finiteness
of the state space. In particular, if a PN model comprising N places is k-
bounded, the number of states cannot exceed (k + 1) N .
Boundedness can also be defined at the net level (structural boundedness) as
we shall see in the next section. A Petri net is said to be bounded if and only
if for every finite initial marking M 0 the resulting PN system is bounded.
It is interesting to note that boundedness, liveness and reversibility are in-
dependent properties. The interested reader can find in [ 53] eight examples
of nets that present all possible combinations of the three properties.
Mutual exclusion — Two mutual exclusion properties are of interest:
one among places and one among transitions. Two places p and q are mutu-
ally exclusive in a PN system if their token counts cannot be both positive
in the same marking, i.e., M RS M(p) · M(q) = 0. Two transitions in
a PN system are mutually exclusive if they cannot be both enabled in any
marking. Two places (or two transitions) are mutually exclusive in a PN
model if they are mutually exclusive in any PN system that can be obtained
by instantiating the model parameters.
The properties introduced so far are generic. Their interpretation heavily
depends on the specific system being studied. For example, if a PN system
describes the behaviour of a distributed program, it is important for the
correctness of the program that the PN system has no deadlock states.
Viceversa, if the model describes a program that is supposed to terminate,
then it is not only desirable to have a deadlock in the system, but the
deadlock state must also be reachable from all markings, thus ensuring that
the program will eventually terminate.
2.5
Structural Analysis Techniques

Search WWH ::

Custom Search