Reduction rules for YAWL workflow nets with cancellation regions and OR-joins

Abstract

A reduction rule can transform a large net into a smaller and simple\nnet while preserving certain interesting properties and it is usually applied before\nverication to reduce the complexity and to prevent state space explosion.\nReset nets have been proposed to formally describe workows with cancellation\nbehaviour. In our previous work, we have presented a set of reduction rules for\nReset Workow Net (RWF-net), which is a subclass of reset nets. In this paper,\nwe will present a set of reduction rules for YAWL nets with cancellation regions\nand OR-joins. The reduction rules for RWF-nets combined with the formal mappings\nfrom YAWL nets provide us with the means to dene a set of reduction\nrules for YAWL nets. We will also demonstrate how these reduction rules can be\nused for efcient verication of YAWL nets these features.\nKeywords: Petri nets with reset arcs, reset nets, reduction rules, workow veri-\ncation, Yet Another Workow Language, soundness property, cancellation regions,\nOR-joins.