In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-hardness for coverability in (not necessarily acyclic) Petri nets with resets. We prove that the reachability problem remains undecidable for acyclic Petri nets with resets. The second class concerns workflow nets, a practically motivated and natural subclass of Petri nets. Here, we show that both coverability and reachability in acyclic workflow nets with resets are PSPACE-complete. Without the acyclicity condition, reachability and coverability in workflow nets with resets are known to be equally hard as for Petri nets with resets, that being Ackermann-hard and undecidable, respectively.
翻译:本文提出了两类新的带重置操作的佩特里网子类,使得其可达性与覆盖性问题的可计算性变得可处理。具体而言,我们在消耗与产出(而非重置操作)上施加无环性条件。第一类是无环带重置佩特里网,我们证明其覆盖性问题是PSPACE完全的。这与已知的(非无环)带重置佩特里网覆盖性问题Ackermann不可判定性形成对比。我们进一步证明无环带重置佩特里网的可达性问题仍是不可判定的。第二类关注工作流网——一类具有实际动机的佩特里网自然子类。我们证明无环带重置工作流网的覆盖性与可达性问题均为PSPACE完全的。若无无环性条件,带重置工作流网的可达性与覆盖性已知分别具有与带重置佩特里网同等的计算复杂度,即Ackermann不可判定性与不可判定性。