Place/transition Petri nets are a standard model for a class of distributed systems whose reachability spaces might be infinite. One of well-studied topics is the verification of safety and liveness properties in this model; despite the extensive research effort, some basic problems remain open, which is exemplified by the open complexity status of the reachability problem. The liveness problems are known to be closely related to the reachability problem, and many structural properties of nets that are related to liveness have been studied. Somewhat surprisingly, the decidability status of the problem if a net is structurally live, i.e. if there is an initial marking for which it is live, has remained open, as also a recent paper (Best and Esparza, 2016) emphasizes. Here we show that the structural liveness problem for Petri nets is decidable. A crucial ingredient of the proof is the result by Leroux (LiCS 2013) showing that we can compute a finite (Presburger) description of the reachability set for a marked Petri net if this set is semilinear.
展开▼
机译：放置/转移Petri网是其可达性空间可能是无限的一类分布式系统的标准模型。一个经过充分研究的主题是在此模型中安全性和活动性的验证。尽管进行了广泛的研究，但仍存在一些基本问题，以可达性问题的开放复杂性状态为例。已知活动性问题与可达性问题密切相关，并且已经研究了许多与活动性相关的网的结构特性。令人惊讶的是，正如最近的一篇论文（Best and Esparza，2016）所强调的那样，如果一个网在结构上是有生命的，即是否有一个有生命的初始标记，该问题的可判定性状态仍然是开放的。在这里，我们证明Petri网的结构活度问题是可以确定的。证明的关键要素是Leroux（LiCS 2013）的结果，该结果表明，如果标记Petri网是半线性的，我们可以计算出该集合的有限性（Presburger）描述。
展开▼
