PSPACE-Completeness of the Soundness Problem of Safe Asymmetric-Choice Workflow Nets

Asymmetric-choice workflow nets (ACWF-nets) are an important subclass of workflow nets (WF-nets) that can model and analyse business processes of many systems, especially the interactions among multiple processes. Soundness of WF-nets is a basic property guaranteeing that these business processes are deadlock-/livelock-free and each designed action has a potential chance to be executed. Aalst et al. proved that the soundness problem is decidable for general WF-nets and proposed a polynomial algorithm to check the soundness for free-choice workflow nets (FCWF-nets) that are a special subclass of ACWF-nets. Tiplea et al. proved that for safe acyclic WF-nets the soundness problem is co-NP-complete, and we proved that for safe WF-nets the soundness problem is PSPACE-complete. We also proved that for safe ACWF-nets the soundness problem is co-NP-hard, but this paper sharpens this result by proving that for safe ACWF-nets this problem is PSPACE-complete actually. This paper provides a polynomial-time reduction from the acceptance problem of linear bounded automata (LBA) to the soundness problem of safe ACWF-nets. The kernel of the reduction is to guarantee that an LBA with an input string does not accept the input string if and only if the constructed safe ACWF-net is sound. Based on our reduction, we easily prove that the liveness problem of safe AC-nets is also PSPACE-complete, but the best result on this problem was NP-hardness provided by Ohta and Tsuji. Therefore, we also strengthen their result.