Deciding structural liveness of Petri nets

TL;DR

This paper proves that determining whether a Petri net can be initially configured to be live (structurally live) is a decidable problem, resolving an open question in Petri net theory.

Contribution

It establishes the decidability of the structural liveness problem for Petri nets, a long-standing open problem in the field.

Findings

Decidability of structural liveness for Petri nets is proven.

Finite Presburger descriptions of reachability sets can be computed.

Addresses an open problem highlighted by recent research.

Abstract

Place/transition Petri nets are a standard model for a class of distributed systems whose reachability spaces might be infinite. One of well-studied topics is the verification of safety and liveness properties in this model; despite the extensive research effort, some basic problems remain open, which is exemplified by the open complexity status of the reachability problem. The liveness problems are known to be closely related to the reachability problem, and many structural properties of nets that are related to liveness have been studied. Somewhat surprisingly, the decidability status of the problem if a net is structurally live, i.e. if there is an initial marking for which it is live, has remained open, as also a recent paper (Best and Esparza, 2016) emphasizes. Here we show that the structural liveness problem for Petri nets is decidable. A crucial ingredient of the proof is the result by Leroux (LiCS 2013) showing that we can compute a finite (Presburger) description of the reachability set for a marked Petri net if this set is semilinear.