Prelegent: Michael Blondin

In this talk, we will consider Petri nets: a well-established formalism for the analysis of concurrent systems. Testing whether a target Petri net configuration cannot be reached often amounts to proving the absence of bugs in a system. Thus, formally certifying unreachability is practically (and theoretically) interesting. It is known that unreachability certificates always exist in the form of Presburger-definable formulas known as separators. Unfortunately, such separators have (super-)Ackermannian worst-case size. Moreover, checking whether a given formula is a separator has (super-)exponential complexity. We will see 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 (and hence simpler than unreachablity, which is P-complete).