  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.
