Deciding (Sub-Marking) Reachability in \(\pmb {O(P^2 + T^2)}\) for Sound Acyclic Free-Choice Workflow Nets
摘要
Reachability is a central decision problem in Petri net theory deciding whether a given marking can be reached from the initial marking. Sub-marking reachability (the covering problem) asks whether there is a reachable marking, which consists of at least the tokens in the given marking. The current state of the art describes the computational complexity of both problems as polynomial for live and bounded free-choice nets as well as for sound free-choice workflow nets. This paper refines this complexity on the class of sound acyclic (simple) free-choice workflow nets to \(O(P^2 + T^2)\) . The presented approach uses three new concepts: admissibility, maximum admissibility, and diverging transitions. Admissibility requires that all places in a given marking are pairwise concurrent. Maximum admissibility states that adding a place to an admissible marking would make it inadmissible. A diverging transition is a transition which originally “produces” the concurrent tokens that lead to a given marking. All three concepts can additionally provide explanations why a (sub-)marking is not reachable.