Soundness of reset workflow nets

TL;DR

This paper resolves the long-standing open question of generalised soundness for reset workflow nets by proving its undecidability via a reduction from two-counter Minsky machines. It then introduces a novel, decidable intermediate property, called $1$-in-between soundness and denoted as $\\mathcal{P}_1$, which sits between generalised soundness and $1$-soundness (generalised sound nets ⊆ $\\mathcal{P}_1$ ⊆ $1$-sound nets). The authors further develop a framework based on nonredundancy and skeleton nets to relate reset workflow nets to standard workflow nets, enabling a decidable approximation that can certify either non-generalised-soundness or $1$-soundness in a structured way. Although the decision procedures are Ackermannian in worst-case complexity, the results provide a principled approach to algorithmically analyze reset workflow nets and suggest practical heuristics. Overall, the work closes the undecidability landscape for reset nets and introduces a productive intermediate notion that could guide future automatic analysis and reductions in this domain.

Abstract

Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown decades ago, but their complexity was only identified recently. In this work, we are primarily interested in two popular variants: $1$-soundness and generalised soundness. Workflow nets have been extended with resets to model workflows that can, e.g., cancel actions. It has been known for a while that, for this extension, all variants of soundness, except possibly generalised soundness, are undecidable. We complete the picture by showing that generalised soundness is also undecidable for reset workflow nets. We then blur this undecidability landscape by identifying a property, coined ``$1$-in-between soundness'', which lies between $1$-soundness and generalised soundness. It reveals an unusual non-monotonic complexity behaviour: a decidable soundness property is in between two undecidable ones. This can be valuable in the algorithmic analysis of reset workflow nets, as our procedure yields an output of the form ``$1$-sound'' or ``not generalised sound'' which is always correct.

Figures (4)

• Figure 1: Example of a reset Petri net where circles are places, boxes are transitions, solid edges are arcs, and dotted edges are reset arcs. The small filled circle depicts a token.
• Figure 2: Example of a reset workflow net. Reset arcs are depicted implicitly by colored patterns, rather than explicitly by dotted directed edges. In words, transition $u_1$ resets place $q_2$, and transition $u_2$ resets all places from $\{p_1, p_2, q_1, q_2, q_3\}$. Formally, $R = \{(q_2, u_1)\} \cup \{(r, u_2) : r \in \{p_1, p_2, q_1, q_2, q_3\}\}$. The two filled circles within place $i$ represent two tokens.
• Figure 3: The set of markings reachable from $\{i \colon 1\}$ in the reset workflow net of \ref{['fig:example']}. Each edge $\bm{m} \xrightarrow{}^{t} \bm{m}'$ indicates that firing transition $t$ in marking $\bm{m}$ leads to marking $\bm{m}'$.
• Figure 5: Classes of reset workflow nets: generalised sound, up-to-$k$-sound, $k$-in-between sound and all reset workflow nets. Properties with lighter colors also satisfy darker colored properties. For example, the class of generalised sound reset workflow nets is the most restrictive and it is contained in all other classes. Note that "$k$-in-between sound" is a class of properties, not a single one. So, in the figure, one should think of each horizontal line as one of these properties.

Theorems & Definitions (29)

• lemma 1: FigueiraFSS11
• theorem 1
• proposition 1
• proposition 2
• theorem 2
• Remark 1
• theorem 3
• proposition 3
• Claim 3
• proposition 4