Reduction of Workflow Nets for Generalised Soundness Verification

This paper proposes a reduction method to verify the generalised soundness of large workflows described as workflow nets-a suited class of Petri nets. The proposed static analysis method is based on the application of six novel reduction transformations that transform a workflow net into a smaller one while preserving generalised soundness. The soundness of the method is proved. As practical contributions, this paper presents convincing experimental results obtained using a dedicated tool, developed to validate and demonstrate the effectiveness, efficiency and scalability of this method over a large set of industrial workflow nets.