Separators in Continuous Petri Nets
share
Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking m⃗_src cannot reach a marking m⃗_tgt, then there is a formula φ of Presburger arithmetic such that: φ(m⃗_src) holds; φ is forward invariant, i.e., φ(m⃗) and m⃗→m⃗' imply φ(m⃗'); and φ(m⃗_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 (super-)Ackermannian worst-case size and the (super-)exponential complexity of checking that a formula is a separator. 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 unreachablity, 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 still efficiently certify unreachability via an altered Petri.
READ FULL TEXT