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.

翻译：Leroux已证明，Petri网中的不可达性可通过Presburger分离子来验证，即若标记$\vec{m}_\text{src}$无法到达标记$\vec{m}_\text{tgt}$，则存在一个Presburger算术公式$\varphi$满足：$\varphi(\vec{m}_\text{src})$成立；$\varphi$是前向不变的，即若$\varphi(\vec{m})$且$\vec{m} \rightarrow \vec{m}'$，则$\varphi(\vec{m}')$成立；且$\neg \varphi(\vec{m}_\text{tgt})$成立。尽管这些分离子可作为不可达性的解释和形式化证书，但由于其最坏情况规模至少为Ackermann级别，且验证公式是否为分离子的复杂度至少为指数级（相对于公式规模），此前尚未得到实际应用。本文证明，在连续Petri网中，这两个问题均可被克服。我们引入局部闭分离子，并证明：(a) 不可达性可由一个多项式时间可计算的局部闭分离子验证；(b) 验证一个公式是否为局部闭分离子的复杂度属于NC类（因此比不可达性更简单，后者为P完全问题）。我们进一步考虑更一般的（存在性）集合到集合可达性问题，其中两组标记由凸多面体给出。研究表明，虽然我们的方法无法直接扩展，但可通过修改后的Petri网高效地验证不可达性。