Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Complexity of Proving Polyhedral Reductions

Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

TL;DR

This paper proposes an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets by encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds.

Abstract

We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples.

On the Complexity of Proving Polyhedral Reductions

TL;DR

This paper proposes an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets by encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds.

Abstract

We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples.
Paper Structure (23 sections, 22 theorems, 23 equations, 10 figures, 1 table)

This paper contains 23 sections, 22 theorems, 23 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Petri nets and polyhedral abstraction
  3. Petri nets
  4. Polyhedral abstraction
  5. Basic properties of polyhedral reduction
  6. Parametric reduction rules and equivalence
  7. Coherency constraints
  8. Instantiation law
  9. Automated proof procedure
  10. Presburger encoding of Petri net semantics
  11. Core requirements: parametric $E$-abstraction encoding
  12. Verifying that a net is coherent.
  13. Coherent solvability
  14. Silent constraints
  15. Reachability
  16. ...and 8 more sections

Key Result

Theorem 2.2

The problem of checking whether a statement $(N_1, m_1) \equiv_E (N_2, m_2)$ is valid is undecidable.

Figures (10)

  • Figure 1: Equivalence rule (concat), $(N_1, C_1) \approxeq_E (N_2, C_2)$, between nets $N_1$ (left) and $N_2$ (right), for the relation $E \triangleq (x = y_1 + y_2)$.
  • Figure 2: Equivalence rule (magic).
  • Figure 3: Illustration of Lemma \ref{['lemma:reachability']}.
  • Figure 4: Illustration of Lemma \ref{['lemma:invariance']}.
  • Figure 5: Detailed dependency relations.
  • ...and 5 more figures

Theorems & Definitions (29)

  • Definition 2.1: E-Abstraction
  • Theorem 2.2: Undecidability of the E-Equivalence Checking
  • Lemma 2.3: Reachability Checking pn2021fi2022
  • Lemma 2.4: Invariance Checking pn2021fi2022
  • Definition 2.5: $E$-Transform Formula
  • Theorem 2.6: Reachability Conservation pn2021fi2022
  • Corollary 2.7: Invariant Conservation
  • Definition 3.1: Coherent Net
  • Definition 3.2: Parametric Reduction Rule
  • Definition 3.3: Parametric $E$-Abstraction
  • ...and 19 more