Acyclic Petri and Workflow Nets with Resets

TL;DR

This paper introduces two new subclasses of Petri nets with resets, demonstrating that certain problems become more tractable under specific acyclicity conditions, with implications for reachability and coverability analysis.

Contribution

It defines acyclic Petri and workflow nets with resets and establishes their reachability and coverability complexities, contrasting with known hardness results.

Findings

Coverability is PSPACE-complete for acyclic Petri nets with resets.

Reachability remains undecidable for acyclic Petri nets with resets.

Both coverability and reachability are PSPACE-complete for acyclic workflow nets with resets.

Abstract

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.