一句话:证明保守 Petri 网的结构活性是 EXPSPACE 完全的,并给出最小活标识的双指数上界。
论文研究 Petri 网结构活性问题:是否存在初始标识使网为活。已有工作证明一般 Petri 网该问题 EXPSPACE 难。本文首先将该下界加强到保守 Petri 网这一简单子类。主要结果是:对结构活的保守网,最小活标识的取值至多关于网规模双指数;由此得到保守 Petri 网结构活性的 EXPSPACE 完全性。该结果也适用于结构有界 Petri 网,而一般情形的复杂度仍开放。作为证明工具,作者扩展了关于布尔组合的线性等式、不等式与整除约束的最小整数解上界的已知结果。
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.
@article{paperbot12622,
title = {Structural Liveness of Conservative Petri Nets},
author = {Petr Jančar and Jérôme Leroux and Jiří Valůšek},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 4},
year = {2026},
doi = {10.46298/lmcs-22(4:4)2026}
}