Discovery, verification and conformance of workflows with cancellation

Petri nets are frequently used for the modeling and analysis of workflows. Their graphical nature, well-defined semantics, and analysis techniques are attractive as information systems become more "process-aware". Unfortunately, the classical Petri net has problems modeling cancellation in a succinct and direct manner. Modeling cancellation regions in a classical net is impossible or results in a "spaghetti-like" net. Cancellation regions are supported by many workflow management systems, but these systems do not support advanced analysis techniques (process mining, verification, performance analysis, etc.). This paper proposes to use reset workflow nets (RWF-nets) and discusses (1) the discovery of RWF-nets (i.e., extracting information from event logs to construct such models), (2) the verification of RWF-nets (i.e., checking whether a workflow process has deadlocks, livelocks, etc.), and (3) the conformance of an event log with respect to a RWF-net (i.e., comparing real with modeled behavior)