Soundness-preserving reduction rules for reset workflow nets

M.T. Wynn, H.M.W. Verbeek, W.M.P. Aalst, van der, A.H.M. Hofstede, ter, D. Edmond

Research output: Contribution to journalArticleAcademicpeer-review

26 Citations (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)769-790
Number of pages22
JournalInformation Sciences
Volume179
Issue number6
DOIs
Publication statusPublished - 2009

Fingerprint

Dive into the research topics of 'Soundness-preserving reduction rules for reset workflow nets'. Together they form a unique fingerprint.

Cite this