We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jančar and Purser, 2019] holds even for a simple subclass of conservative nets. As the main result we then show that for structurally live conservative nets the values of the least live markings are at most double exponential in the size of the nets, which entails the EXPSPACE-completeness of structural liveness for conservative Petri nets; the complexity of the general case remains unclear. As a proof ingredient with a potential of wider applicability, we present an extension of the known results bounding the smallest integer solutions of boolean combinations of linear (in)equations and divisibility constraints.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Structural Liveness of Conservative Petri Nets

  • Petr Jančar,
  • Jérôme Leroux,
  • Jiří Valůšek

摘要

We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jančar and Purser, 2019] holds even for a simple subclass of conservative nets. As the main result we then show that for structurally live conservative nets the values of the least live markings are at most double exponential in the size of the nets, which entails the EXPSPACE-completeness of structural liveness for conservative Petri nets; the complexity of the general case remains unclear. As a proof ingredient with a potential of wider applicability, we present an extension of the known results bounding the smallest integer solutions of boolean combinations of linear (in)equations and divisibility constraints.