| Summary: | 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.
|
|---|