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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Deciding (Sub-Marking) Reachability in  \(\pmb {O(P^2 + T^2)}\) for Sound Acyclic Free-Choice Workflow Nets

  • Thomas M. Prinz,
  • Christopher T. Schwanen,
  • Wil M. P. van der Aalst

摘要

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.