Affiliations: Department of Computer Science and Technology, Tongji University, Shanghai 201804, China. [email protected] | ISTD, Singapore University of Technology and Design, Singapore 138682, Singapore. [email protected] | School of Computer Engineering, Nanyang Technological University, Singapore 639798, Singapore. [email protected] | School of Computing, National University of Singapore, Singapore 117417, Singapore. [email protected]
Note: [] Address for correspondence: Department of Computer Science and Technology, Tongji University, Shanghai 201804, China
Abstract: Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for bounded WF-nets with reset or inhibitor arcs (ReWF-nets and InWF-nets for short, resp.). ReWF- and InWF-nets are two extensions to WF-nets and their soundness problems were proven by Aalst et al. to be undecidable. Additionally, we prove that the soundness problem is co-NP-hard for asymmetric-choice WF-nets that are a larger class and can model more cases of interaction and resource allocation than free-choice ones.
