Graphics Programs Reference

In-Depth Information

It is possible to visualize the T-semiflows above as paths in the graph rep-

resentation of the net, as shown in Fig.
2.14.

It may be possible in some cases to prove that a PN system (or model) is

not live using structural techniques: since the covering by T-semiflows is a

necessary condition for liveness of bounded nets, if at least one transition

is not included in any T-semiflow, while the net is covered by P-semiflows

(hence being structurally bounded), the net is not live (as well as any PN

system or model with that same structure).

2.5.2

Graph-based structural techniques

configurations of a Petri net useful to study the liveness of PN systems.

Furthermore, some structural relations between transitions are defined, that

allow the definition of necessary conditions for the occurrence of situations

such as conflict, mutual exclusion and confusion in PN systems.

Deadlocks and traps — The following definitions of deadlocks and traps

are restricted to PNs without inhibitor arcs and in which all arc weights are

either zero or one (ordinary nets).

Definition 2.5.2 A deadlock is a subset of places P
D
⊆
P such that the set

of its input transitions is a subset of the set of its output transitions; that is:

[

[

{
•
p
}⊆

{
p
•
}

p∈P
D

p∈P
D

Definition 2.5.3 A trap is a subset of places P
T
⊆
P such that the set of

its output transitions is a subset of the set of its input transitions; that is:

[

[

{
p
•
}⊆

{
•
p
}

p∈P
T

p∈P
T

Deadlocks and traps can be used to study the liveness of systems by exploit-

ing the following properties:

•
there is no way of increasing the total marking of an empty deadlock

P
D
: once a deadlock has lost all its tokens, all transitions that have

an input place in P
D
cannot fire; as a consequence the system is not

live.

•
if a trap is marked in the initial marking, then it will never lose all its

tokens; hence a good way to ensure that a deadlock will not lose all

its tokens is to make sure that it contains a trap marked in the initial

marking.

Search WWH ::

Custom Search