Information Technology Reference
In-Depth Information
them may fire, but does not have to. Simultaneous firing of multiple
enabled transitions is not allowed in the original Petri net definition.
This semantics make Petri nets well-suited to model the concurrent
behavior of distributed systems. Here we give the formal definition of
the execution rules of Petri nets.
Definition 2.2. (Execution Rule of a Petri Net)
1. A transition
t
is said to be
enabled
if each of its input place is
marked with at least
W
(
p
,
t
) tokens, where
W
(
p
,
t
) is the weight
of the arc from
p
to
t
. Mathematically,
W
(
p
,
t
).
2. An enabled transition may or may not fire in a given state
transition step.
3. A firing of an enabled transition
t
removes
W
(
p
,
t
) tokens from
each input place
p
of
t
, and adds
W
(
t
,
p
) tokens to each output
place
p
of
t
,where
W
(
t
,
p
) is the weight of the arc from
t
to
p
.
Mathematically,
M
0
(
p
)
8
p
2
P
,
M
(
p
)
¼
M
(
p
)
W
(
p
,
t
)
þ
W
(
t
,
p
), for any
p
in
P
.
Typical properties one might analyze by using Petri nets are
illustrated as follows. For brevity we only give an intuitive explanation;
please refer to [78-80] for formal definitions and more details.
Reachability
. Starting from an initial marking, firing transitions
will lead a Petri net to different markings. This property con-
siders, given an initial marking, whether or not a target marking
can be reached, after a sequence of firings. All markings given a
Petri net and initial marking
M
0
constitute the reachability set
denoted by
R
(N,
M
0
) and sometimes
R
(
M
0
).
Boundedness
. This property considers whether or not the num-
ber of tokens in each place does not exceed a finite number, in any
reachable marking.
Liveness
. This property considers whether or not a given transi-
tion, or any transition, can be fired ultimately, given any marking
in
R
(PN,
M
0
).
There are mainly three types of analysis approaches [78], that is,
reachability graph, matrix equation, and reduction and decomposi-
tion. The reachability graph method relies on building the state space
