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