Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking $\vec{m}_\text{src}$ cannot reach a marking $\vec{m}_\text{tgt}$, then there is a formula $\varphi$ of Presburger arithmetic such that: $\varphi(\vec{m}_\text{src})$ holds; $\varphi$ is forward invariant, i.e., $\varphi(\vec{m})$ and $\vec{m} \rightarrow \vec{m}'$ imply $\varphi(\vec{m}'$); and $\neg \varphi(\vec{m}_\text{tgt})$ holds. While these separators could be used as explanations and as formal certificates of unreachability, this has not yet been the case due to their worst-case size, which is at least Ackermannian, and the complexity of checking that a formula is a separator, which is at least exponential (in the formula size). We show that, in continuous Petri nets, these two problems can be overcome. We introduce locally closed separators, and prove that: (a) unreachability can be witnessed by a locally closed separator computable in polynomial time; (b) checking whether a formula is a locally closed separator is in NC (so, simpler than unreachability, which is P-complete). We further consider the more general problem of (existential) set-to-set reachability, where two sets of markings are given as convex polytopes. We show that, while our approach does not extend directly, we can efficiently certify unreachability via an altered Petri net.

翻译：勒鲁已证明，佩特里网中的不可达性可由普雷斯伯格分隔符证实：若标记$\vec{m}_\text{src}$无法到达标记$\vec{m}_\text{tgt}$，则存在一个普雷斯伯格算术公式$\varphi$满足：$\varphi(\vec{m}_\text{src})$成立；$\varphi$是前向不变的，即若$\varphi(\vec{m})$且$\vec{m} \rightarrow \vec{m}'$，则$\varphi(\vec{m}')$成立；且$\neg \varphi(\vec{m}_\text{tgt})$成立。尽管这些分隔符可作为不可达性的解释与形式化证书，但由于其最坏情况规模至少为阿克曼函数级，且验证公式是否为分隔符的复杂性至少为指数级（相对于公式规模），此前尚未实现此用途。我们证明，在连续佩特里网中，这两个问题均可被解决。我们引入局部闭分隔符，并证明：(a) 不可达性可由一个多项式时间内可计算的局部闭分隔符所证实；(b) 验证一个公式是否为局部闭分隔符属于NC复杂度类（因此比不可达性更简单，后者为P完全问题）。我们进一步考虑更一般的（存在性）集合到集合可达性问题，其中两组标记以凸多面体形式给出。我们证明，尽管我们的方法无法直接扩展，但可通过修改后的佩特里网高效地认证不可达性。