PSPACE-Completeness of the Soundness Problem of Safe Asymmetric-Choice Workflow Nets
- 30 June 2020
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC
- Vol. 12152, 196-216
- https://doi.org/10.1007/978-3-030-51831-8_10
Abstract
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.Keywords
This publication has 30 references indexed in Scilit:
- The reachability problem for Petri nets is not elementaryPublished by Association for Computing Machinery (ACM) ,2019
- Polynomial analysis algorithms for free choice Probabilistic Workflow NetsPerformance Evaluation, 2017
- Soundness of workflow nets: classification, decidability, and analysisFormal Aspects of Computing, 2010
- On liveness and boundedness of asymmetric choice netsTheoretical Computer Science, 2004
- Decidability and complexity of Petri net problems — An introductionLecture Notes in Computer Science, 1998
- On liveness and controlled siphons in Petri netsLecture Notes in Computer Science, 1996
- Complexity results for 1-safe netsTheoretical Computer Science, 1995
- Free Choice Petri NetsPublished by Cambridge University Press (CUP) ,1995
- Structure Theory of Petri Nets: the Free Choice HiatusLecture Notes in Computer Science, 1987
- Free choice systems have home statesActa Informatica, 1984