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.

Subscribe to:
Posts (Atom)