A central decision problem in Petri net theory is reachability asking whether a given marking can be reached from the initial marking. Related is the covering problem (or sub-marking reachbility), which decides whether there is a reachable marking covering at least the tokens in the given marking. For live and bounded free-choice nets as well as for sound free-choice workflow nets, both problems are polynomial in their computational complexity. This paper refines this complexity for the class of sound acyclic free-choice workflow nets to a quadratic polynomial, more specifically to $O(P^2 + T^2)$. Furthermore, this paper shows the feasibility of accurately explaining why a given marking is or is not reachable. This can be achieved by 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 marked 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. In this paper, we provide algorithms for all these concepts and explain their computation in detail by basing them on the concepts of concurrency and post-dominance frontiers - a well known concept from compiler construction. In doing this, we present straight-forward implementations for solving (sub-marking) reachability.
翻译:Petri网理论中的一个核心判定问题是可达性问题,即询问给定标识是否可以从初始标识到达。与之相关的是覆盖问题(或称子标识可达性问题),它判定是否存在一个可达标识,其至少覆盖给定标识中的所有令牌。对于活且有界的自由选择网以及合理的自由选择工作流网,这两个问题的计算复杂度均为多项式级别。本文针对合理的无环自由选择工作流网类,将该复杂度进一步细化为二次多项式,具体为$O(P^2 + T^2)$。此外,本文展示了精确解释为何给定标识可达或不可达的可行性。这可以通过三个新概念实现:可容许性、最大可容许性以及发散变迁。可容许性要求给定标识中的所有库所两两并发。最大可容许性则指在可容许标识中添加一个已标记库所将使其变为不可容许。发散变迁是指最初“产生”导致给定标识的并发令牌的变迁。本文为所有这些概念提供了算法,并通过基于并发性和后支配边界——编译器构造中的一个著名概念——详细解释了它们的计算过程。在此过程中,我们提出了解决(子标识)可达性问题的直接实现方法。