paperbot · PL 论文追踪

全部论文 待读 收藏

Structural Liveness of Conservative Petri Nets

保守 Petri 网的结构活性
LMCS vol.Volume 22, Issue 42026引用 0 inbox
Petr Jančar, Jérôme Leroux, Jiří Valůšek
crossref: 2026-10-10

AI 速览

一句话:证明保守 Petri 网的结构活性是 EXPSPACE 完全的,并给出最小活标识的双指数上界。

论文研究 Petri 网结构活性问题:是否存在初始标识使网为活。已有工作证明一般 Petri 网该问题 EXPSPACE 难。本文首先将该下界加强到保守 Petri 网这一简单子类。主要结果是:对结构活的保守网,最小活标识的取值至多关于网规模双指数;由此得到保守 Petri 网结构活性的 EXPSPACE 完全性。该结果也适用于结构有界 Petri 网,而一般情形的复杂度仍开放。作为证明工具,作者扩展了关于布尔组合的线性等式、不等式与整除约束的最小整数解上界的已知结果。

问题
判定保守 Petri 网(及更一般网)的结构活性,即是否存在使网为活的初始标识,并确定其复杂度。
方法
将 EXPSPACE-hardness 加强到保守子类,证明结构活保守网的最小活标识大小至多双指数,并扩展线性/整除约束布尔组合的最小整数解界。
评估
通过复杂度下界归约与上界分析,证明保守和结构有界 Petri 网的结构活性为 EXPSPACE 完全,一般情形仍开放。
原文摘要(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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}