Structural Liveness of Conservative Petri Nets

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Jančar, Petr, Leroux, Jérôme, Valůšek, Jiří
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866908981344075776
author Jančar, Petr
Leroux, Jérôme
Valůšek, Jiří
author_facet Jančar, Petr
Leroux, Jérôme
Valůšek, Jiří
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2503_11590
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Structural Liveness of Conservative Petri Nets
Jančar, Petr
Leroux, Jérôme
Valůšek, Jiří
Logic in Computer Science
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.
title Structural Liveness of Conservative Petri Nets
topic Logic in Computer Science
url https://arxiv.org/abs/2503.11590