arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2310.01992cs.FLcs.LO
收藏

带重置的无环Petri网与工作流网

Acyclic Petri and Workflow Nets with Resets

Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, Henry Sinclair-Banks

AI总结:

本文提出两类带重置的无环Petri网新子类,证明其可覆盖性或可达性问题复杂度从Ackermann难/不可判定降至PSPACE完全,为相关问题求解提供了可处理的网类。

摘要:

本文提出两类带重置Petri网的新子类,其可达性与可覆盖性问题变为可处理的。具体而言,我们添加了一条仅适用于消耗与产生行为、不适用于重置行为的无环条件。第一类是带重置的无环Petri网,我们证明其可覆盖性问题是PSPACE完全的,这与已知的(非必然无环的)带重置Petri网可覆盖性问题的Ackermann难度形成对比;同时我们证明该类网的可达性问题仍不可判定。第二类涉及工作流网——一种具有实际动机的自然Petri网子类,我们证明带重置的无环工作流网的可覆盖性与可达性问题均为PSPACE完全的。若无无环条件,带重置工作流网的可达性与可覆盖性问题已知与带重置Petri网的难度相当,即分别为Ackermann难和不可判定。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑