Complexity of the soundness problem of workflow nets

• Main Authors: LIU, Guan Jun, SUN, Jun, LIU, Yang, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2014
• Subjects: Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4979; https://ink.library.smu.edu.sg/context/sis_research/article/5982/viewcontent/pn12.pdf
• Institution: Singapore Management University

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.