Deciding Reachability and the Covering Problem with Diagnostics for Sound Acyclic Free-Choice Workflow Nets

TL;DR

The paper addresses the reachability and covering problems for a targeted Petri-net class: sound acyclic free-choice workflow nets. It advances the state of the art by achieving quadratic-time decision procedures and by providing diagnostics through the novel notions of admissibility, maximum admissibility, and diverging transitions, all grounded in concurrency and post-dominance frontiers. A central insight is that reachability can be characterized via run nets and diverging points without enumerating occurrence sequences, enabling both efficient verification and explainability. The results offer practical implications for process-model verification and diagnostics in industrial settings, with extensions to extended free-choice nets via a Murata transformation and avenues toward broader applicability.

Abstract

A central decision problem in Petri net theory is reachability asking whether a given marking can be reached from the initial marking. Related is the covering problem (or sub-marking reachbility), which decides whether there is a reachable marking covering at least the tokens in the given marking. For live and bounded free-choice nets as well as for sound free-choice workflow nets, both problems are polynomial in their computational complexity. This paper refines this complexity for the class of sound acyclic free-choice workflow nets to a quadratic polynomial, more specifically to $O(P^2 + T^2)$. Furthermore, this paper shows the feasibility of accurately explaining why a given marking is or is not reachable. This can be achieved by three new concepts: admissibility, maximum admissibility, and diverging transitions. Admissibility requires that all places in a given marking are pairwise concurrent. Maximum admissibility states that adding a marked place to an admissible marking would make it inadmissible. A diverging transition is a transition which originally "produces" the concurrent tokens that lead to a given marking. In this paper, we provide algorithms for all these concepts and explain their computation in detail by basing them on the concepts of concurrency and post-dominance frontiers - a well known concept from compiler construction. In doing this, we present straight-forward implementations for solving (sub-marking) reachability.

Figures (17)

• Figure 1: A sound acyclic free-choice workflow net focusing on a marking with tokens on $p9$, $p12$, and $p16$ (colored in pink).
• Figure 2: In sound extended free-choice workflow nets, \ref{['lemma:ConcurrentJointTransition']} does not hold without modifications as $p6$ is not a joining transition.
• Figure 4: The net of \ref{['fig:example']} with selected marking $[\,p9,p10\,]$ (highlighted in pink). The marking is admissible by \ref{['algo:CheckMaximumAdmissibility']}. At least one of the places highlighted in green will be marked at the same time as $[\,p9,p10\,]$ in a reachable marking as this is not maximum admissible.
• Figure 5: The net of \ref{['fig:example']} with selected marking $[\,p3,p5\,]$ (highlighted in pink). The marking is not admissible by \ref{['algo:CheckMaximumAdmissibility']} since $p3$ is not concurrent to $p5$ as there is a path from $p3$ to $p5$ highlighted in orange.
• Figure 6: A sound A FC- WF-net with selected marking $[\,p3,p5,p7\,]$ (highlighted in pink). The marking is not admissible by \ref{['algo:CheckMaximumAdmissibility']} since $p5$ is not concurrent to $p7$. Since both places do not have any path in-between them, they are mutually exclusive. For diagnostics, it would be of benefit to present the decision point $p4$ in the net making both places exclusive.

Theorems & Definitions (23)

• Definition 2.1: Petri Nets
• Definition 2.2: Workflow Nets, FC-WF-Nets, and AFC-WF-Nets
• Definition 2.3: Marking
• Definition 2.4: Enabledness, Firing, and Reachability
• Definition 2.5: Live, Bounded, Safe, and Dead
• Definition 2.6: Soundness
• Lemma 2.1: Safeness
• Theorem 2.1: Path-to-End Theorem
• Definition 3.1: Concurrency
• Lemma 3.1