In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. 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.
翻译:本文提出了两类带重置的Petri网新子类,使得其可达性与覆盖性问题变得可解。我们在消耗与生成操作上引入无环性约束,但不对重置操作施加此限制。第一类是带重置的无环Petri网,我们证明其覆盖性问题为PSPACE完全问题,这与已知的(非无环)带重置Petri网覆盖性问题的Ackermann难度形成对比。同时证明带重置的无环Petri网的可达性问题仍不可判定。第二类涉及工作流网——一类具有实际动机的Petri网自然子类。我们证明带重置的无环工作流网中覆盖性与可达性均为PSPACE完全。若无无环性约束,带重置的工作流网中可达性与覆盖性问题分别与带重置的Petri网具有同等难度,即分别为Ackermann难和不可判定。