English

Structural Liveness of Conservative Petri Nets

Logic in Computer Science 2026-04-22 v2

Abstract

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.

Keywords

Cite

@article{arxiv.2503.11590,
  title  = {Structural Liveness of Conservative Petri Nets},
  author = {Petr Jančar and Jérôme Leroux and Jiří Valůšek},
  journal= {arXiv preprint arXiv:2503.11590},
  year   = {2026}
}

Comments

Extended and modified version of the paper presented at FoSSaCS 2025

R2 v1 2026-06-28T22:20:54.185Z