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

TL;DR

This paper improves the complexity bounds for reachability and covering problems in sound acyclic free-choice workflow nets and introduces new concepts and algorithms for explaining reachability status based on concurrency and post-dominance.

Contribution

It refines the complexity of reachability and covering problems to quadratic time and introduces new concepts and algorithms for explaining reachability in Petri nets.

Findings

Complexity of reachability is reduced to O(P^2 + T^2) for specific nets.

New concepts: admissibility, maximum admissibility, diverging transitions.

Algorithms for explaining reachability based on concurrency and post-dominance.

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.