A reduction rule can transform a large net into a smaller and simple
net while preserving certain interesting properties and it is usually applied before
verication to reduce the complexity and to prevent state space explosion.
Reset nets have been proposed to formally describe workows with cancellation
behaviour. In our previous work, we have presented a set of reduction rules for
Reset Workow Net (RWF-net), which is a subclass of reset nets. In this paper,
we will present a set of reduction rules for YAWL nets with cancellation regions
and OR-joins. The reduction rules for RWF-nets combined with the formal mappings
from YAWL nets provide us with the means to dene a set of reduction
rules for YAWL nets. We will also demonstrate how these reduction rules can be
used for efcient verication of YAWL nets these features.
Keywords: Petri nets with reset arcs, reset nets, reduction rules, workow veri-
cation, Yet Another Workow Language, soundness property, cancellation regions,
|Place of Publication||Eindhoven|
|Number of pages||37|
|Publication status||Published - 2006|