Business Process Management (Part-2 Business Process Modelling[Chapter VI Properties Of Business Processes ] ) Sec D -- By Mathias Weske

Soundness Theorem

Reachability analysis based on reachability graphs is a simple method to characterize
the cases that comply with a given workflow net. However, reachability
analysis only works well for small examples. The reachability graphs of
real world business processes involving dozens of activities suffer from state
explosion, which renders reachability graph analysis inappropriate in these
settings.
Besides manually creating a reachability graph and checking for the
three properties of workflow nets that collectively define soundness, there
are computer-supported ways to determine soundness. The first class of approaches
creates the reachability graph automatically and checks the soundness
property. Due to the state explosion problem, this approach suffers from
exponential run time behaviour. As a result, the creation of the reachability
graph might not be feasible for real-world applications.
But there are other options that take advantage of the rich set of tools
that have been developed by the Petri net community. In the reminder of this
section, one of these approaches is discussed. It is based on a theorem that boundedness.
The general idea is deriving a Petri net from the workflow net to be checked
for soundness, as sketched in Figure 6.10: By adding a transition t to a
workflow net PN, and linking the final place o to t and t to the initial place
i, a Petri net PN0 is created.
We can show that PN0 is live and bounded if and only if PN is sound. As
a consequence, existing techniques to analyze liveness and boundedness for
Petri nets can be used to check a workflow net for the soundness property.
For an important subclass of Petri nets, there are efficient analysis techniques
for liveness and boundedness. This renders the check for soundness of
workflow nets an efficient task, even for large workflow nets, which can be
found in real-world scenarios.
Theorem 6.1 A Workflow net PN = (P, T, F) is sound if and only if
(PN0, i), such that PN0 = (P0, T0, F0), P0 = P, T0 = T [ {t }, and
F0 = F [ {(o, t ), (t , i)}, is live and bounded.
To prove this theorem, we first show that if PN0 is live and bounded, then PN
is a sound workflow net. Then, it is shown that from the soundness property
of the workflow net, liveness and boundedness properties of the Petri net PN0
follow. The proof is illustrated in Figure 6.10.
Since PN0 is live, for each transition there is a firing sequence starting
in the initial state i that activates it. This is especially true for the added
transition t . Since o is the only input place of t , we can conclude that there
is a state M reachable from i with at least one token in o, i.e., M o.
When t fires, a token is put on the initial place i. Again, there is a firing
sequence that leads to a state in which there is a token in o. Since PN0 is
bounded, M = o, because otherwise tokens would aggregate in a place of the
Petri net.
Now we show that if PN is sound, PN0 is bounded. This is shown by
contradiction. Assume that PN is sound, but that PN0 is unbounded. Since
PN is sound and (by assumption) PN0 is unbounded, there exist states M,M0
such that i ! M ! M0 and M0 M, allowing the aggregation of tokens in
a place of PN0.
Since PN is a sound workflow net, there exists a firing sequence such
that i ! M ! o. Applying the same firing sequence to state M0 leads to
a state M00 > o. This means that in M00 there is a token in o; but there is
at least one additional token in the net! This is a violation of the soundness
property of PN and shows the contradiction.
Finally, we have to show that if PN is sound then PN0 is live. Soundness
implies that each transition can participate in a firing sequence leading from
the initial state i to the final state o. By firing t , the initial state i can be
reached, so that liveness of PN0 follows. For arbitrary Petri nets, liveness and boundedness are still complex to
compute, so that exponential run time behaviour can be expected. However, for an important subclass of Petri nets, liveness and boundedness can be
computed in polynomial time. This subclass is free choice nets. Free choice
nets have the property that the sets of input places of two transitions are
either disjoint or identical.