Page 68 -

2 The Language: Rationale and Fundamentals 55

Definition 8. (Sound). A procedure modeled in the form of a WF-net PN D
.P;T;F/ is sound if and only if:
For every state M reachable from state i, there exists a firing sequence leading
from state M to state o. Formally:
h i
8 M .i ! M/ ) .M ! o/

State o is the only state reachable from state i with at least one token in place o.
Formally:
h i
8 M .i ! M ^ M o/ ) .M D o/

There are no dead transitions in .PN; i/. Formally:

t
h i
8 t2T 9 M;M 0 i ! M ! M 0

The format of workflow nets is essentially the same as for Petri nets, although there
are some notational enhancements (often termed “syntactic sugar”) for split and join
constructs that simplify the specification of a workflow net. Figure 2.16 illustrates
the range of workflow-net constructs.
A key aspect of a workflow net is that it identifies the way in which a task is
initiated. This can occur in one of the four ways: (1) automatic tasks execute as
soon as they are enabled, (2) user tasks are passed to human resources for execution
once enabled, (3) external tasks only proceed once they are enabled and a required
message or signal is received from the operating environment, and (4) time tasks
only proceed once they are enabled and a specified (time-based) deadline occurs.
Figure 2.17 illustrates the order fulfillment process shown earlier in the form of
a workflow net. In this model, the split and join constructs are explicitly identified.
Also the manner in which tasks are triggered is shown. Most are undertaken by
human resources (i.e., staff); however, the take order task is externally triggered
when an order request is received and the decline order task runs automatically
with the customer receiving a notification either by email or fax.
While Petri nets and workflow nets provide an effective means of modeling a
business process, they are not able to capture the notion of cancelation. This is a

place automatic task user task explicit OR join explicit OR split

arc
external task time task AND split AND join
Fig. 2.16 Workflow net constructs