pith. sign in

arxiv: 2306.01466 · v4 · submitted 2023-06-02 · 💻 cs.LO

On the Complexity of Proving Polyhedral Reductions

Nicolas Amat (IMDEA Software Institute) , Silvano Dal Zilio (LAAS-VERTICS , LAAS) , Didier Le Botlan (LAAS-VERTICS This is my paper

Pith reviewed 2026-05-24 08:20 UTC · model grok-4.3

classification 💻 cs.LO
keywords polyhedral abstractionPetri netsSMT formulasflat netsPresburger arithmeticreachabilitystate space equivalenceautomated verification
0
0 comments X

The pith

An SMT encoding automatically proves when one Petri net is a polyhedral abstraction of another.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents an automated procedure to verify polyhedral abstractions between Petri nets. These abstractions equate two nets when their markings satisfy a set of linear integer constraints. The procedure encodes the equivalence question as a collection of SMT formulas; if the formulas are satisfiable then the abstraction holds. Completeness of the method is obtained by restricting attention to flat nets, whose reachable markings are known to be definable in Presburger arithmetic. The result supplies both a practical proof technique and a clearer account of how polyhedral reductions can simplify reachability questions.

Core claim

The authors show that the problem of checking whether one Petri net is a polyhedral abstraction of another can be reduced to the satisfiability of a finite set of SMT formulas. Satisfaction of these formulas is sufficient to establish the equivalence. When both nets belong to the class of flat nets, the procedure is also complete because the reachability sets of flat nets are Presburger-definable. This encoding therefore yields an automated proof method for a new form of state-space equivalence and clarifies its use on reachability problems.

What carries the argument

Encoding the polyhedral-equivalence question between two Petri nets as a set of SMT formulas, with completeness supplied by the Presburger-definable reachability sets of flat nets.

If this is right

  • Reachability questions on a large net can be transferred to a smaller net once the polyhedral abstraction is proven.
  • Infinite-state systems modeled by Petri nets become amenable to automated equivalence proofs via existing SMT solvers.
  • Polyhedral reductions can be validated without manual intervention for any pair of nets whose equivalence reduces to the SMT conditions.
  • The method supplies a concrete characterization of valid polyhedral abstractions in terms of linear constraints on markings.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The SMT encoding may be reusable for other forms of state-space equivalence that can be expressed with linear constraints.
  • Integration of the procedure into existing Petri-net analysis tools would allow automatic discovery of useful abstractions during verification.
  • Advances in SMT solvers for Presburger arithmetic would directly improve the practical reach of the completeness result.

Load-bearing premise

The procedure is complete only when the nets are flat, because only then are the reachable markings guaranteed to be Presburger-definable.

What would settle it

Exhibit two flat Petri nets together with a candidate linear constraint such that the SMT formulas are satisfiable yet there exist reachable markings in the first net that violate the constraint when transferred to the second net.

Figures

Figures reproduced from arXiv: 2306.01466 by Didier Le Botlan (LAAS-VERTICS, LAAS), Nicolas Amat (IMDEA Software Institute), Silvano Dal Zilio (LAAS-VERTICS.

Figure 1
Figure 1. Figure 1: Equivalence rule (CONCAT), (N1, C1) ≊E (N2, C2), between nets N1 (left) and N2 (right), for the relation E ≜ (x = y1 + y2). y1 a b τ τ τ y3 τ τ y4 c y2 c ′ C1 ≜ (y2 + y3 + y4 = 0) x = y1 + y2 + y3 + y4 x a b c ′ c C2 ≜ True [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Equivalence rule (MAGIC). we prove that this equivalence is sound when no transition can input a token directly into place y2 of N1. This means that the rule is correct in the absence of the “dashed” transition (with label d), but that our procedure should flag the rule as unsound when transition d is present. The results presented in this paper provide an automated technique for proving the correctness of… view at source ↗
Figure 3
Figure 3. Figure 3: Illustration of Lemma 2.3. m1 m′ 1 m2 m′ 2 m1 ≡E m2 ∃m′ 2 . m′ 1 ≡E m′ 2 [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Detailed dependency relations. as LIA in SMT-LIB [29]. We illustrate the results given in this section using a diagram ( [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Illustration of (Core 0) [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Illustration of (Core 1). Condition (S1) is depicted in [PITH_FULL_IMAGE:figures/full_fig_p017_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Illustration of (Core 2). C1 R(N1, C1) C2 R(N2, C2) m1 m′ a 1 m2 E m′ 2 a E 1 [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 10
Figure 10. Figure 10: A Petri net modeling users in a swimming pool, see e.g. [22]. [PITH_FULL_IMAGE:figures/full_fig_p029_10.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript proposes an automated procedure to prove polyhedral abstractions (polyhedral reductions) between Petri nets. The core method encodes the equivalence problem as a finite set of SMT formulas such that satisfiability entails equivalence; the approach is claimed to handle infinite-state systems. For completeness the paper invokes a connection to flat nets whose reachability sets are Presburger-definable. The work also aims to characterize polyhedral reductions and their use on reachability problems, and reports an implementation together with illustrative examples.

Significance. If the encoding is sound, the result supplies a practical, automated technique for establishing a new form of state-space equivalence on infinite-state Petri nets. The explicit restriction of the completeness claim to flat nets is a clear strength that avoids over-generalization. The implementation and examples provide concrete evidence of usability, and the link to Presburger-definable reachability sets supplies a useful theoretical anchor.

minor comments (2)
  1. The title emphasizes complexity yet the abstract and high-level description focus on the existence of the encoding and its completeness restriction; a short paragraph in the introduction clarifying what complexity results (if any) are proved would improve alignment between title and content.
  2. The abstract states that the procedure has been implemented but supplies no information on the SMT solver, the input language for nets, or the size of the examples; adding these details would aid reproducibility.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. No major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines an encoding of polyhedral equivalence checking into a finite set of SMT formulas, with the claim that satisfiability entails equivalence. Completeness is explicitly restricted to the subclass of flat nets whose reachability sets are Presburger-definable. No self-definitional steps, fitted parameters renamed as predictions, load-bearing self-citations, or ansatz smuggling appear in the stated procedure. The derivation reduces the problem to an external SMT solver without internal circular reduction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The method rests on standard decidability properties of Presburger arithmetic and SMT solvers without introducing new free parameters or entities.

axioms (1)
  • domain assumption Reachability sets of flat nets are Presburger-definable
    Invoked to guarantee completeness of the SMT encoding for infinite-state systems.

pith-pipeline@v0.9.0 · 5695 in / 915 out tokens · 20791 ms · 2026-05-24T08:20:13.277493+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    Petri net Reductions for Counting Markings

    Berthomieu B, Le Botlan D, Dal Zilio S. Petri net Reductions for Counting Markings. In: Model Checking Software (SPIN), volume 10869 of Lecture Notes in Computer Science . Springer, 2018 doi: 10.1007/978-3-319-94111-0_4

    work page doi:10.1007/978-3-319-94111-0_4 2018

  2. [2]

    Counting Petri net markings from reduction equations

    Berthomieu B, Le Botlan D, Dal Zilio S. Counting Petri net markings from reduction equations. In- ternational Journal on Software Tools for Technology Transfer , 2019. 22(2):163–181. doi:10.1007/ s10009-019-00519-1

    work page 2019

  3. [3]

    Checking properties of nets using transformations

    Berthelot G, Lri-Iie. Checking properties of nets using transformations. In: Advances in Petri Nets (APN), volume 222 of Lecture Notes in Computer Science. Springer, 1985 doi:10.1007/BFb0016204

    work page doi:10.1007/bfb0016204 1985

  4. [4]

    Transformations and Decompositions of Nets

    Berthelot G. Transformations and Decompositions of Nets. In: Petri Nets: Central Models and Their Properties (ACPN), volume 254 of Lecture Notes in Computer Science. Springer, 1987 doi:10.1007/ 978- 3-540-47919-2_13

    work page 1987

  5. [5]

    A Polyhedral Abstraction for Petri Nets and its Application to SMT- Based Model Checking

    Amat N, Berthomieu B, Dal Zilio S. A Polyhedral Abstraction for Petri Nets and its Application to SMT- Based Model Checking. Fundamenta Informaticae, 2022. 187(2-4):103–138. doi:10.3233/FI-222134

    work page doi:10.3233/fi-222134 2022

  6. [6]

    Leveraging polyhedral reductions for solving Petri net reachability problems

    Amat N, Dal Zilio S, Le Botlan D. Leveraging polyhedral reductions for solving Petri net reachability problems. International Journal on Software Tools for Technology Transfer , 2023. 25(1):95–114. doi: 10.1007/s10009-022-00694-8

    work page doi:10.1007/s10009-022-00694-8 2023

  7. [7]

    Polyhedral Analysis for Synchronous Languages

    Besson F, Jensen T, Talpin JP. Polyhedral Analysis for Synchronous Languages. In: Static Analysis (SAS), volume 1694 of Lecture Notes in Computer Science. Springer, 1999 doi:10.1007/3-540-48294-6_4

    work page doi:10.1007/3-540-48294-6_4 1999

  8. [8]

    Automatic parallelization in the polytope model

    Feautrier P. Automatic parallelization in the polytope model. In: The Data Parallel Programming Model, volume 1132 of Lecture Notes in Computer Science. Springer, 1996. doi:10.1007/3-540-61736-1_44

    work page doi:10.1007/3-540-61736-1_44 1996

  9. [9]

    Hierarchical Set Decision Diagrams and Regular Models

    Thierry-Mieg Y , Poitrenaud D, Hamez A, Kordon F. Hierarchical Set Decision Diagrams and Regular Models. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of Lecture Notes in Computer Science. Springer, 2009 doi:10.1007/978-3-642-00768-2_1

    work page doi:10.1007/978-3-642-00768-2_1 2009

  10. [10]

    Tina Toolbox, 2023

    LAAS-CNRS. Tina Toolbox, 2023. URL http://projects.laas.fr/tina

    work page 2023

  11. [11]

    SMPT: The Satisfiability Modulo Petri Nets Model Checker

    Amat N. SMPT: The Satisfiability Modulo Petri Nets Model Checker. An SMT-based model checker for Petri nets focused on reachability problems that takes advantage of polyhedral reduction., 2020. URL https://github.com/nicolasAmat/SMPT. N. Amat et al. / On the Complexity of Proving Polyhedral Reductions 393

    work page 2020

  12. [12]

    SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets

    Amat N, Dal Zilio S. SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets. In: Formal Methods (FM), volume 14000 of Lecture Notes in Computer Science . Springer, 2023 doi: 10.1007/978-3-031-27481-7_25

    work page doi:10.1007/978-3-031-27481-7_25 2023

  13. [13]

    Property Directed Reachability for Generalized Petri Nets

    Amat N, Dal Zilio S, Hujsa T. Property Directed Reachability for Generalized Petri Nets. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 13243 of Lecture Notes in Computer Science. Springer, 2022 doi:10.1007/978-3-030-99524-9_28

    work page doi:10.1007/978-3-030-99524-9_28 2022

  14. [14]

    Presentation of the 9th Edition of the Model Checking Contest

    Amparore E, Berthomieu B, Ciardo G, Dal Zilio S, Gallà F, Hillah LM, Hulin-Hubard F, Jensen PG, Jezequel L, Kordon F, Le Botlan D, Liebke T, Meijer J, Miner A, Paviot-Adet E, Srba J, Thierry-Mieg Y , van Dijk T, Wolf K. Presentation of the 9th Edition of the Model Checking Contest. In: Tools and Algorithms for the Construction and Analysis of Systems (TAC...

    work page 2019

  15. [15]

    Decidability issues for Petri nets

    Esparza J, Nielsen M. Decidability issues for Petri nets. BRICS Report Series, 1994. 1(8). doi:10.7146/ brics.v1i8.21662

    work page 1994

  16. [16]

    Decidability and complexity of Petri net problems — An introduction

    Esparza J. Decidability and complexity of Petri net problems — An introduction. In: Lectures on Petri Nets I: Basic Models (ACPN), volume 1491 of Lecture Notes in Computer Science . Springer, 1998 doi: 10.1007/3-540-65306-6_20

    work page doi:10.1007/3-540-65306-6_20 1998

  17. [17]

    Decidability Questions for Petri Nets

    Hack MHT. Decidability Questions for Petri Nets. PhD Thesis, 1976

    work page 1976

  18. [18]

    Petri nets and the equivalence problem

    Hirshfeld Y . Petri nets and the equivalence problem. In: Computer Science Logic (CSL), volume 832 of Lecture Notes in Computer Science. Springer, 1994 doi:10.1007/BFb0049331

    work page doi:10.1007/bfb0049331 1994

  19. [19]

    On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets

    Amat N, Berthomieu B, Dal Zilio S. On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets. In: Application and Theory of Petri Nets and Concurrency (PETRI NETS), volume 12734 of Lecture Notes in Computer Science. Springer, 2021 doi:10.1007/978-3-030-76983-3_9

    work page doi:10.1007/978-3-030-76983-3_9 2021

  20. [20]

    Checking marking reachability with the state equation in Petri net subclasses

    Hujsa T, Berthomieu B, Dal Zilio S, Le Botlan D. Checking marking reachability with the state equation in Petri net subclasses. CoRR, 2020. abs/2006.05600

    work page arXiv 2020

  21. [21]

    On the Petri Nets with a Single Shared Place and Beyond

    Hujsa T, Berthomieu B, Dal Zilio S, Le Botlan D. On the Petri Nets with a Single Shared Place and Beyond. CoRR, 2020. abs/2005.04818. 2005.04818

    work page arXiv 2020

  22. [22]

    Reachability Analysis of (Timed) Petri Nets Using Real Arithmetic

    Bérard B, Fribourg L. Reachability Analysis of (Timed) Petri Nets Using Real Arithmetic. In: Con- currency Theory (CONCUR), volume 1664 of Lecture Notes in Computer Science . Springer, 1999 doi: 10.1007/3-540-48320-9_14

    work page doi:10.1007/3-540-48320-9_14 1999

  23. [23]

    FAST: Fast Acceleration of Symbolic Transition Systems

    Bardin S, Finkel A, Leroux J, Petrucci L. FAST: Fast Acceleration of Symbolic Transition Systems. In: Computer Aided Verification (CA V), volume 2725 ofLecture Notes in Computer Science. Springer, 2003 doi:10.1007/978-3-540-45069-6_12

    work page doi:10.1007/978-3-540-45069-6_12 2003

  24. [24]

    FAST: acceleration from theory to practice

    Bardin S, Finkel A, Leroux J, Petrucci L. FAST: acceleration from theory to practice. International Jour- nal on Software Tools for Technology Transfer, 2008. 10(5):401–424. doi:10.1007/s10009-008-0064-3

    work page doi:10.1007/s10009-008-0064-3 2008

  25. [25]

    Presburger Vector Addition Systems

    Leroux J. Presburger Vector Addition Systems. In: Logic in Computer Science (LICS). IEEE, 2013 doi:10.1109/LICS.2013.7

    work page doi:10.1109/lics.2013.7 2013

  26. [26]

    Automated Polyhedral Abstraction Proving

    Amat N, Dal Zilio S, Le Botlan D. Automated Polyhedral Abstraction Proving. In: Application and Theory of Petri Nets and Concurrency (PETRI NETS), volume 13929 of Lecture Notes in Computer Science. Springer, 2023 doi:10.1007/978-3-031-33620-1_18. 394 N. Amat et al. / On the Complexity of Proving Polyhedral Reductions

    work page doi:10.1007/978-3-031-33620-1_18 2023

  27. [27]

    Accelerating the Computation of Dead and Concurrent Places Using Reductions

    Amat N, Dal Zilio S, Le Botlan D. Accelerating the Computation of Dead and Concurrent Places Using Reductions. In: Model Checking Software (SPIN), volume 12864 of Lecture Notes in Computer Science. Springer, 2021 doi:10.1007/978-3-030-84629-9_3

    work page doi:10.1007/978-3-030-84629-9_3 2021

  28. [28]

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

    Amat N, Dal Zilio S, Le Botlan D. Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability. In: Verification, Model Checking, and Abstract Interpretation (VMCAI), Lecture Notes in Computer Science. Springer, 2024 doi:10.1007/978-3-031-50524-9_5

    work page doi:10.1007/978-3-031-50524-9_5 2024

  29. [29]

    The SMT-LIB Standard: Version 2.6

    Barrett C, Fontaine P, Tinelli C. The SMT-LIB Standard: Version 2.6. Standard, University of Iowa, 2017

    work page 2017

  30. [30]

    On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation

    Presburger M, Jacquette D. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation. History and Philosophy of Logic , 1991. 12(2):225–233. doi:10.1080/014453409108837187

    work page doi:10.1080/014453409108837187 1991

  31. [31]

    Semigroups, Presburger formulas, and languages

    Ginsburg S, Spanier E. Semigroups, Presburger formulas, and languages. Pacific journal of Mathematics,

    work page

  32. [32]

    doi:10.2140/pjm.1966.16.285

    16(2):285–296. doi:10.2140/pjm.1966.16.285

    work page doi:10.2140/pjm.1966.16.285 1966

  33. [33]

    Semilinearity of the reachability set is decidable for Petri nets

    Hauschildt D. Semilinearity of the reachability set is decidable for Petri nets. PhD Thesis, University of Hamburg, Germany, 1990

    work page 1990

  34. [34]

    Vector addition systems and semi-linearity

    Lambert JL. Vector addition systems and semi-linearity. Université Paris-Nord. Centre Scientifique et Polytechnique [CSP], 1990

    work page 1990

  35. [35]

    How to Compose Presburger-Accelerations: Applications to Broadcast Protocols

    Finkel A, Leroux J. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 2556 of Lecture Notes in Computer Science. Springer, 2002 doi:10.1007/3-540-36206-1_14

    work page doi:10.1007/3-540-36206-1_14 2002

  36. [36]

    Reductron: The Polyhedral Abstraction Prover

    Amat N. Reductron: The Polyhedral Abstraction Prover. A tool to automatically prove the correctness of polyhedral equivalences for Petri nets., 2023. URL https://github.com/nicolasAmat/Reductron

    work page 2023

  37. [37]

    File formats of the Tina Toolbox

    LAAS-CNRS. File formats of the Tina Toolbox. URL http://projects.laas.fr/tina//manuals/ formats.html/

    work page

  38. [38]

    Z3: An Efficient SMT Solver

    De Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science . Springer, 2008 doi:10.1007/978-3-540-78800-3_24

    work page doi:10.1007/978-3-540-78800-3_24 2008