Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

TL;DR

This work tackles the scalability challenge of checking generalized reachability in Petri nets by combining polyhedral reductions with a fast, tailored projection procedure. It introduces Token Flow Graphs to perform linear-time variable elimination on $E\land F$ into a projected formula $F_2$ on the reduced net, preserving verdicts under $E$-equivalence and often achieving exactness. Implemented as the open-source pre-processor Octantoctant, the method accelerates mainstream model-checkers and delivers substantial speedups on MCC benchmarks, including challenging queries, while outperforming general-purpose quantifier-elimination tools like Redlog and isl on projection tasks. The results demonstrate that polyhedral reductions can be deployed transparently to improve reachability verification in practice, motivating further refinement of projection precision and polarization criteria.

Abstract

We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net. Our projection is defined as a variable elimination procedure for linear integer arithmetic tailored to the specific kind of constraints we handle. It has linear complexity, is guaranteed to return a sound property, and makes use of a simple condition to detect when the result is exact. Experimental results show that our approach works well in practice and that it can be useful even when there is only a limited amount of reductions.

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

TL;DR

This work tackles the scalability challenge of checking generalized reachability in Petri nets by combining polyhedral reductions with a fast, tailored projection procedure. It introduces Token Flow Graphs to perform linear-time variable elimination on into a projected formula on the reduced net, preserving verdicts under -equivalence and often achieving exactness. Implemented as the open-source pre-processor Octantoctant, the method accelerates mainstream model-checkers and delivers substantial speedups on MCC benchmarks, including challenging queries, while outperforming general-purpose quantifier-elimination tools like Redlog and isl on projection tasks. The results demonstrate that polyhedral reductions can be deployed transparently to improve reachability verification in practice, motivating further refinement of projection precision and polarization criteria.

Abstract

We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net. Our projection is defined as a variable elimination procedure for linear integer arithmetic tailored to the specific kind of constraints we handle. It has linear complexity, is guaranteed to return a sound property, and makes use of a simple condition to detect when the result is exact. Experimental results show that our approach works well in practice and that it can be useful even when there is only a limited amount of reductions.
Paper Structure (7 sections, 6 theorems, 6 equations, 7 figures)

This paper contains 7 sections, 6 theorems, 6 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Petri Nets and Polyhedral Abstraction
  3. Combining Polyhedral Abstraction with Reachability
  4. Projecting Formulas Using Token Flow Graphs
  5. Formal Procedure and Proof of Correctness
  6. Experimental Results
  7. Discussion and Related Works

Key Result

Theorem 3.1

Assume $(N_1, m_1) \equiv_E (N_2, m_2)$ and $F_2 \mathop{\sqsubseteq_{E}}F_1$, and take a marking $m'_2$ reachable in $(N_2, m_2)$ such that $m'_2 \models F_2$. Then there exists $m'_1 \in R(N_1, m_1)$ such that $m'_1 \mathop{\equiv_{E}\,}m'_2$ and $m'_1 \models F_1$.

Figures (7)

  • Figure 1: An example of Petri net, $M_1$ (left), and one of its polyhedral abstractions, $M_2$ (right), with $E \triangleq (p_1 = p_4 + 4096) \wedge (p_6 = p_0 + p_2 + p_3 + p_5 + p_7) \wedge (a_1 = p_7 + p_8) \wedge (a_2 = a_1 + p_5)$. Colors are used to emphasize places that are either removed or added.
  • Figure 2: Equations from our example in Fig. \ref{['fig:stahl']} and the associated TFG.
  • Figure 3: Random walk w/wo reductions.
  • Figure 4: $k$-induction w/wo reductions.
  • Figure 5: Impact of projections on the challenging queries.
  • ...and 2 more figures

Theorems & Definitions (15)

  • Definition 2.1: $E$-equivalence
  • Definition 3.1: Equivalence between formulas
  • Theorem 3.1: Finding Witnesses
  • proof
  • Corollary 3.1.1
  • Definition 4.1: Token Flow Graph
  • Definition 4.2: Polarized Set of Constraints
  • Definition 5.1: Well-formed TFG
  • Theorem 5.1: Projection Equivalence
  • Lemma 5.2: Soundness
  • ...and 5 more