A Branching-Process-Based Method to Check Soundness of Workflow Systems

作者：Liu, Guanjun^*; Reisig, Wolfgang; Jiang, Changjun; Zhou, Mengchu

来源：IEEE Access, 2016, 4: 4104-4118.

DOI：10.1109/ACCESS.2016.2597061

• Petri nets
• soundness
• branching processes
• unfolding
• business process model

Workflow nets (WF-nets) as a class of Petri nets are widely used to model and analyze workflow systems. Soundness is an important property of WF-nets, which guarantees that the systems are deadlock and livelock-free and each task has a chance to be performed. Van der Aalst has proven that the soundness problem is decidable for WF-nets and we have also shown that it is PSPACE-complete for bounded ones. Since the definition of soundness is based on reachability and Van der Aalst has proven that a sound WF-net must be bounded, the soundness detection can be carried out via the reachability graph analysis. However, the state explosion problem is a big obstacle to this technique. The unfolding technique of Petri nets can effectively avoid/alleviate this problem. This paper proposes an algorithm to generate a finite prefix of the unfolding of a WF-net, called basic unfolding. Furthermore, a necessary and sufficient condition is proposed to decide soundness based on basic unfolding. In addition, some examples illustrate that the unfolding technique can save the storage space effectively.

• 出版日期2016
• 单位同济大学