Information Technology Reference
In-Depth Information
Definition 2.4. (Soundness)
[81] AWF-net
PN
ΒΌ
(
P
,
T
,
F
) is sound if
and only if
1. For every marking
M
reachable from marking
i
, there exists a
firing sequence leading from
M
to state
o
. Note that
i
and
o
represent the marking where only places
i
and
o
contain one
token, respectively, and all other places are empty;
2. Marking
o
is the only one reachable frommarking
i
with at least
one token in place
o
; and
3. There are no dead transitions in (
PN
,
i
).
Here we explain the three requirements of a sound workflow net
using some simple examples. Figure 2.2 shows some WF-nets and their
i
and
o
places are explicitly highlighted.
Requirement 1 says that once a workflow starts from initial state
i
,
no matter which intermediate state it goes to, it is always possible to
reach a final state
o
. Figure 2.2a illustrates a workflow net that does
not fulfill this requirement. Let us think about a travel request
approval process in some company. A request needs to be approved
by either the line manager (activity
t
1
) or the comptroller (activity
t
2
),
and then archived for later reference (activity
t
3
). The WF-net in
p
2
p
2
t
1
t
2
p
4
p
4
p
5
p
1
p
1
t
1
(
i
)
(
o
)
(
o
)
(
i
)
t
3
t
4
p
3
p
t
2
t
3
3
(a) Deadlock
(b) Lack-of-synchronization
p
4
p
2
t
1
t
2
p
2
p
4
p
5
p
1
p
1
t
1
(
i
)
(
o
)
(
i
)
(
o
)
t
3
t
4
p
3
t
2
t
3
p
6
(c) Correction of (a)
(d) Correction of (b)
Figure 2.2
Two workflow nets that are not sound and their corrections.
