TY - JOUR
T1 - Soundness-preserving reduction rules for reset workflow nets
AU - Wynn, M.T.
AU - Verbeek, H.M.W.
AU - Aalst, van der, W.M.P.
AU - Hofstede, ter, A.H.M.
AU - Edmond, D.
PY - 2009
Y1 - 2009
N2 - The application of reduction rules to any Petri net may assist in its analysis as its reduced
version may be significantly smaller while still retaining the original net’s essential properties.
Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove
all tokens from a certain place. Such nets have a natural application in business process
modelling where possible cancellation of activities need to be modelled explicitly and in
workflow management where such process models with cancellation behaviours should
be enacted correctly. As cancelling the entire workflow or even cancelling certain activities
in a workflow has serious implications during execution (for instance, a workflow can
deadlock because of cancellation), such workflows should be thoroughly tested before
deployment. However, verification of large workflows with cancellation behaviour is time
consuming and can become intractable due to the state space explosion problem. One way
of speeding up verification of workflows based on reset nets is to apply reduction rules.
Even though reduction rules exist for Petri nets and some of its subclasses and extensions,
there are no documented reduction rules for reset nets. This paper systematically presents
such reduction rules. Because we want to apply the results to the workflow domain, this
paper focusses on reset workflow nets (RWF-nets), i.e. a subclass tailored to the modelling
of workflows. The approach has been implemented in the context of the workflow system
YAWL.
AB - The application of reduction rules to any Petri net may assist in its analysis as its reduced
version may be significantly smaller while still retaining the original net’s essential properties.
Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove
all tokens from a certain place. Such nets have a natural application in business process
modelling where possible cancellation of activities need to be modelled explicitly and in
workflow management where such process models with cancellation behaviours should
be enacted correctly. As cancelling the entire workflow or even cancelling certain activities
in a workflow has serious implications during execution (for instance, a workflow can
deadlock because of cancellation), such workflows should be thoroughly tested before
deployment. However, verification of large workflows with cancellation behaviour is time
consuming and can become intractable due to the state space explosion problem. One way
of speeding up verification of workflows based on reset nets is to apply reduction rules.
Even though reduction rules exist for Petri nets and some of its subclasses and extensions,
there are no documented reduction rules for reset nets. This paper systematically presents
such reduction rules. Because we want to apply the results to the workflow domain, this
paper focusses on reset workflow nets (RWF-nets), i.e. a subclass tailored to the modelling
of workflows. The approach has been implemented in the context of the workflow system
YAWL.
U2 - 10.1016/j.ins.2008.10.033
DO - 10.1016/j.ins.2008.10.033
M3 - Article
SN - 0020-0255
VL - 179
SP - 769
EP - 790
JO - Information Sciences
JF - Information Sciences
IS - 6
ER -