Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Separators in Continuous Petri Nets

Michael Blondin, Javier Esparza

TL;DR

This work shows that continuous Petri nets admit compact, efficiently verifiable witnesses for unreachability in the form of locally closed bi-separators. These separators can be computed in polynomial time and verified in NC, addressing the size and verification bottlenecks of Leroux's Presburger separators. The authors develop a complete characterization of unreachability via linear exclusion functions and siphon/trap witnesses, and extend the certificate framework to set-to-set unreachability using an altered Petri net that encodes the target polytopes. The results yield practical, explainable certificates and open avenues for parallel verification and CEGAR-inspired verification workflows in continuous Petri nets.

Abstract

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.

Separators in Continuous Petri Nets

TL;DR

This work shows that continuous Petri nets admit compact, efficiently verifiable witnesses for unreachability in the form of locally closed bi-separators. These separators can be computed in polynomial time and verified in NC, addressing the size and verification bottlenecks of Leroux's Presburger separators. The authors develop a complete characterization of unreachability via linear exclusion functions and siphon/trap witnesses, and extend the certificate framework to set-to-set unreachability using an altered Petri net that encodes the target polytopes. The results yield practical, explainable certificates and open avenues for parallel verification and CEGAR-inspired verification workflows in continuous Petri nets.

Abstract

Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking cannot reach a marking , then there is a formula of Presburger arithmetic such that: holds; is forward invariant, i.e., and imply ); and 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.
Paper Structure (15 sections, 21 theorems, 35 equations, 3 figures, 1 algorithm)

This paper contains 15 sections, 21 theorems, 35 equations, 3 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Separators and bi-separators
  4. A characterization of unreachability
  5. The predicates $B_2(Q)$ and $B_3(R)$
  6. The predicate $B_1(\mathbf{y})$
  7. Separators as certificates
  8. Locally closed bi-separators
  9. Constructing locally closed bi-separators
  10. Checking locally closed bi-separators is in NC
  11. Bi-separators for set-to-set unreachability
  12. Hardness of checking set-to-set bi-separators
  13. Certifying set-to-set unreachability
  14. Conclusion
  15. Missing proofs

Key Result

Lemma 2.1

Let $\mathbf{A} \in \mathbb{R}^{m \times n}$ and $\bm{b} \in \mathbb{R}^m$. The formula $\mathbf{A}\bm{x} \leq \bm{b}$ has no solution iff $\mathbf{A}^\mathsf{T} \bm{y} = \bm{0} \land \bm{b}^\mathsf{T} \bm{y} < 0 \land \bm{y} \geq \bm{0}$ has a solution.

Figures (3)

  • Figure 1: A Petri net and two markings $\bm{m}_\text{src} = \{p_1 \mapsto 2, p_2 \mapsto 0, p_3 \mapsto 0, p_4 \mapsto 0\}$ (black circles) and $\bm{m}_\text{tgt} = \{p_1 \mapsto 0, p_2 \mapsto 0, p_3 \mapsto 0, p_4 \mapsto 1\}$ (colored squares).
  • Figure 2: Petri net for $\psi(\bm{x}) = (a_1 \cdot x_1 + \cdots + a_n\cdot x_n > c)$ where $a_1, a_2, c > 0$ and $a_n < 0$.
  • Figure 3: Reduction from set-to-set reachability to (marking-to-marking) reachability.

Theorems & Definitions (46)

  • Lemma 2.1: Farkas' lemma
  • Definition 2.2
  • Definition 2.3
  • Proposition 2.4
  • proof
  • Theorem 3.1: FH15
  • Proposition 3.2: FH15
  • Definition 3.3
  • Lemma 3.4
  • proof
  • ...and 36 more