Journal
IEEE ACCESS
Volume 4, Issue -, Pages 4104-4118Publisher
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/ACCESS.2016.2597061
Keywords
Petri nets; soundness; branching processes; unfolding; business process model
Categories
Funding
- Alexander von Humboldt Foundation of Germany
- National Nature Science Foundation of China [61572360, 91218301]
- Shanghai Education Development Foundation
- Shanghai Municipal Education Commission through the Shuguang Program
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available