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})$成立。尽管这些分隔符可作为不可达性的解释和形式化凭证，但因其最坏情况规模至少为阿克曼函数级，且验证公式是否为分隔符的复杂度至少为指数级（相对于公式规模），这一方法尚未得到应用。我们证明，在连续Petri网中，这两个问题可以被克服。我们引入局部闭分隔符，并证明：(a) 不可达性可由可在多项式时间内计算的局部闭分隔符验证；(b) 验证公式是否为局部闭分隔符属于NC复杂度类（因此比P完全的不可达性问题更简单）。我们进一步考虑更一般的（存在性）集合到集合可达性问题，其中两组标记由凸多面体给出。我们表明，尽管我们的方法无法直接扩展，但可通过修改后的Petri网高效验证不可达性。