Structural Liveness of Conservative Petri Nets
For researchers in Petri net theory, this resolves the complexity of structural liveness for conservative nets, a long-standing open problem, though the general case remains open.
The paper proves that structural liveness for conservative Petri nets is EXPSPACE-complete, showing that minimal live markings are at most doubly exponential in net size. This extends previous EXPSPACE-hardness results to a simple subclass of conservative nets.
We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As our main result, we prove that for structurally live conservative nets, the values of the minimal live markings are at most doubly exponential in the size of the net. This implies the EXPSPACE-completeness of structural liveness for conservative Petri nets. The result also applies to structurally bounded Petri nets, whereas the complexity of the general case remains open. As a proof ingredient of independent interest, we present an extension of known results on the bounds of minimal integer solutions to Boolean combinations of linear equalities, inequalities, and divisibility constraints.