TY - JOUR

T1 - SEPARATORS IN CONTINUOUS PETRI NETS

AU - Blondin, Michael

AU - Esparza, Javier

N1 - Publisher Copyright:
© M. Blondin and J. Esparza.

PY - 2024

Y1 - 2024

N2 - Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking msrc cannot reach a marking mtgt, then there is a formula φ of Presburger arithmetic such that: φ(msrc) holds; φ is forward invariant, i.e., φ(m) and m → m′ imply φ(m′); and ¬φ(mtgt) 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.

AB - Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking msrc cannot reach a marking mtgt, then there is a formula φ of Presburger arithmetic such that: φ(msrc) holds; φ is forward invariant, i.e., φ(m) and m → m′ imply φ(m′); and ¬φ(mtgt) 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.

KW - Petri net and continuous reachability and separators and certificates

UR - http://www.scopus.com/inward/record.url?scp=85186421579&partnerID=8YFLogxK

U2 - 10.46298/lmcs-20(1:15)2024

DO - 10.46298/lmcs-20(1:15)2024

M3 - Article

AN - SCOPUS:85186421579

SN - 1860-5974

VL - 20

SP - 15:1-15:24

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 1

ER -