pith. sign in

arxiv: 2503.11590 · v2 · submitted 2025-03-14 · 💻 cs.LO

Structural Liveness of Conservative Petri Nets

Petr Jan\v{c}ar , J\'er\^ome Leroux , Ji\v{r}\'i Val\r{u}\v{s}ek This is my paper

Pith reviewed 2026-05-23 00:09 UTC · model grok-4.3

classification 💻 cs.LO
keywords Petri netsstructural livenessconservative netsEXPSPACEminimal markingsDiophantine constraints
0
0 comments X

The pith

For conservative Petri nets, structural liveness is EXPSPACE-complete.

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

The paper proves that structural liveness of conservative Petri nets is EXPSPACE-complete. It shows this by establishing that any minimal live marking in a structurally live conservative net has values bounded by a doubly exponential function of the net size. This bound allows deciding the property in EXPSPACE, matching the hardness result that already applies to this subclass. The result extends to structurally bounded nets as well. The proof relies on an extension of bounds for minimal solutions to systems involving linear equations, inequalities, and divisibility.

Core claim

In conservative Petri nets, if the net is structurally live then the smallest live initial markings have token counts at most doubly exponential in the size of the net description. This size bound yields an EXPSPACE decision procedure for structural liveness, which is also EXPSPACE-hard for conservative nets.

What carries the argument

An extension of bounds on the size of minimal integer solutions to Boolean combinations of linear equalities, inequalities and divisibility constraints, applied to an encoding of structural liveness.

If this is right

  • Structural liveness is decidable in EXPSPACE for conservative nets.
  • The same complexity holds for structurally bounded Petri nets.
  • Minimal live markings are bounded doubly exponentially in size.
  • The general case for arbitrary Petri nets remains open.

Where Pith is reading between the lines

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

  • The bound technique may transfer to other net properties involving reachability or liveness.
  • Similar complexity results could be sought for other restricted classes of Petri nets.
  • The result suggests that conservative nets capture much of the hardness of the general structural liveness problem.

Load-bearing premise

The known bounds on minimal solutions to linear Diophantine systems with divisibility can be extended and applied to the particular formula encoding structural liveness for conservative nets.

What would settle it

A counterexample would be a conservative Petri net that is structurally live, yet every live marking requires some place to hold more than doubly exponentially many tokens relative to the net size.

Figures

Figures reproduced from arXiv: 2503.11590 by J\'er\^ome Leroux, Ji\v{r}\'i Val\r{u}\v{s}ek, Petr Jan\v{c}ar.

Figure 1
Figure 1. Figure 1: The net A1 on the left is conservative (as evidenced by the weight vector (1, 1, 1, 2, 1)) and structurally live; x0 = (1, 0, 1, 0, 2) is a live configuration, since there is the only (infinite) execution (1, 0, 1, 0, 2) a1 −→ (0, 1, 2, 0, 1) a3 −→ (0, 1, 0, 1, 1) a2 −→ (1, 0, 0, 1, 1) a4 −→ (1, 0, 1, 0, 2) a1 −→ · · · from x0. We can verify that if a configuration x of A1 is live, then x(1) + x(2) > 0 ∧ x… view at source ↗
Figure 2
Figure 2. Figure 2: Illustration for the proof of Lemma 19. a configuration (p, x) is f-quasi-dead if x ∈ ↑(C G v=r, . . . , CG v=r) and there is (p, x) ρ −→ (q, y) where (q, y) is dead and |ρ| ≤ f(||G||, d). Now we show a crucial lemma: each nonlive configuration (p, x) of G where all components of x are large can reach a quasi-dead configuration, even one with the same state p. (The function f2 in the lemma will serve us as… view at source ↗
Figure 3
Figure 3. Figure 3: Transformation of the pair (a−, a+), (a+, a−) where ||a−||1 = ||a+||1 = 3. Proof. Let A be an ordinary strongly reversible 1-conservative net, with the set of places P. To extend A to the required PP-net A′ , we add a new (control) place run, and further (control) places as clarified by the following construction of the actions of A′ . Successively, for each pair of mutually reversed actions a = (a−, a+) a… view at source ↗
Figure 4
Figure 4. Figure 4: Construction in the proof of Lemma 28. ahinc,pi : (inc, store) → (inc, p) and ahdec,pi : (dec, p) → (dec, store); 3. a1 : inc → dec, a2 : dec → dec′ ; a R 2 : dec′ → dec, 4. a3 : (dec, dec′ ) → (dec, store); 5. ainit : dec → init and a R init : init → dec. Since A is an ordinary strongly reversible PP-net, it is clear that A′ is an ordi￾nary PP-net. We show that A′ is also (structurally) reversible: Since … view at source ↗
read the original abstract

We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As our main result, we prove that for structurally live conservative nets, the values of the minimal live markings are at most doubly exponential in the size of the net. This implies the EXPSPACE-completeness of structural liveness for conservative Petri nets. The result also applies to structurally bounded Petri nets, whereas the complexity of the general case remains open. As a proof ingredient of independent interest, we present an extension of known results on the bounds of minimal integer solutions to Boolean combinations of linear equalities, inequalities, and divisibility constraints.

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 paper shows that structural liveness remains EXPSPACE-complete when restricted to conservative Petri nets. It reuses the 2019 EXPSPACE-hardness result of Jancar and Purser and proves a new doubly exponential upper bound on the token counts in any minimal live marking of a structurally live conservative net; the bound is obtained by encoding structural liveness into a Boolean combination of linear equalities, inequalities and divisibility constraints and then extending known results on the size of minimal integer solutions to such systems. The same bound applies to structurally bounded nets. The extension itself is presented as an independent technical contribution.

Significance. If the central bound holds, the result supplies a tight complexity classification for an important and natural subclass of Petri nets and simultaneously supplies a reusable bound on minimal solutions of linear systems augmented with divisibility constraints. Both the complexity statement and the bound on integer solutions are stated in a form that is directly usable by subsequent work in verification and integer programming.

minor comments (2)
  1. [Abstract] The abstract states that the bound is 'at most doubly exponential in the size of the net' but does not specify the precise size measure (number of places, total size of the incidence matrix, etc.). Adding one sentence would remove any ambiguity for readers who wish to instantiate the bound.
  2. The manuscript should include a short self-contained statement of the precise form of the Boolean combination that arises from the structural-liveness encoding (before invoking the new bound), so that the applicability of the extension can be checked without reconstructing the encoding from the surrounding text.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the paper and the recommendation for minor revision. No major comments appear in the report, so we have no specific points requiring response or revision.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper cites the 2019 EXPSPACE-hardness result (Jancar-Purser) to establish hardness for the conservative subclass and then derives the doubly-exponential bound on minimal live markings via a new encoding into Boolean combinations of linear constraints plus an explicit extension of known solution-size bounds. This extension is presented as an independent proof ingredient rather than a self-citation or fitted parameter. No equation reduces to a prior result by definition, no uniqueness theorem is imported from the authors' own prior work to force the outcome, and the central upper-bound claim does not collapse to the input data or to the cited hardness result. The derivation chain therefore remains non-circular.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on an extension of prior bounds for minimal solutions to linear systems with divisibility constraints and on standard modeling of Petri-net liveness via such systems. No free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption Standard properties of conservative Petri nets and structural liveness
    Used to reduce structural liveness to existence of small solutions in linear systems.
  • standard math Known bounds on minimal integer solutions to linear Diophantine systems
    The paper extends these known results to include Boolean combinations and divisibility constraints.

pith-pipeline@v0.9.0 · 5663 in / 1363 out tokens · 58556 ms · 2026-05-23T00:09:39.728186+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

  • IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    We show that the EXPSPACE-hardness result for structural liveness of Petri nets holds even for a simple subclass of conservative nets. As our main result, we prove that for structurally live conservative nets, the values of the minimal live markings are at most doubly exponential in the size of the net.

  • IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    As a proof ingredient of independent interest, we present an extension of known results on the bounds of minimal integer solutions to Boolean combinations of linear equalities, inequalities, and divisibility constraints.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

30 extracted references · 30 canonical work pages

  1. [1]

    Fischer, and René Peralta

    Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Pera lta, R.: Computation in networks of passively mobile finite-state sensors. Distrib uted Comput. 18(4), 235– 253 (2006). https://doi.org/10.1007/s00446-005-0138-3

    work page doi:10.1007/s00446-005-0138-3 2006

  2. [2]

    Distributed Comput

    Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The c omputational power of population protocols. Distributed Comput. 20(4), 279–304 (2007). https://doi.org/10.1007/s00446-007-0040-2

    work page doi:10.1007/s00446-007-0040-2 2007

  3. [3]

    Birkhäuser Cha m (2024)

    Best, E., Devillers, R.: Petri Net Primer. Birkhäuser Cha m (2024). https://doi.org/10.1007/978-3-031-48278-6 , 545 pp

    work page doi:10.1007/978-3-031-48278-6 2024

  4. [4]

    Best, E., Esparza, J.: Existence of home states in Petri nets is decidable. Inf. Process. Lett. 116(6), 423–427 (2016). https://doi.org/10.1016/j.ipl.2016.01.011

    work page doi:10.1016/j.ipl.2016.01.011 2016

  5. [5]

    In: Chandra, A.K., Wotschke, D., Friedman, E.P., Harrison, M.A

    Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential Spac e Complete Problems for Petri Nets and Commutative Semigroups: Preliminary Report . In: Chandra, A.K., Wotschke, D., Friedman, E.P., Harrison, M.A. (eds.) Proceedings of the 8th Annual ACM Symposium on Theory of Computing, May 3-5, 1976, Hershey , Pennsylvania, USA. pp. 50–54. ACM (1976). https://do...

    work page doi:10.1145/800113.803630 1976

  6. [6]

    Korhonen, A single-exponential time 2-approximation algorithm for treewidth, in: IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS 2021), 2022, pp

    Czerwinski, W., Orlikowski, L.: Reachability in Vector A ddition Systems is Ackermann-complete. In: 62nd IEEE Annual Symposium on Foun dations of Com- puter Science, FOCS 2021, Denver, CO, USA, February 7-10, 20 22. pp. 1229–1240. IEEE (2021). https://doi.org/10.1109/FOCS52979.2021.00120

    work page doi:10.1109/focs52979.2021.00120 2021

  7. [7]

    Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (1995)

    Desel, J., Esparza, J.: Free Choice Petri Nets. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (1995). https://doi.org/10.1017/CBO9780511526558 Structural Liveness of Conservative Petri Nets 33

    work page doi:10.1017/cbo9780511526558 1995

  8. [8]

    In: Donatelli, S., Haar, S

    Esparza, J., Raskin, M.A., Weil-Kennedy, C.: Parameteri zed Analysis of Im- mediate Observation Petri Nets. In: Donatelli, S., Haar, S. (eds.) Applica- tion and Theory of Petri Nets and Concurrency - 40th Internat ional Confer- ence, PETRI NETS 2019, Aachen, Germany, June 23-28, 2019, Pr oceedings. Lecture Notes in Computer Science, vol. 11522, pp. 365–38...

    work page doi:10.1007/978-3-030-21571-2_20 2019

  9. [9]

    ACM SIGLOG News 5(3), 67–82 (2018)

    Haase, C.: A survival guide to Presburger arithmetic. ACM SIGLOG News 5(3), 67–82 (2018). https://doi.org/10.1145/3242953.3242964

    work page doi:10.1145/3242953.3242964 2018

  10. [10]

    In: 15th An- nual Symposium on Switching and Automata Theory, New Orlean s, Louisiana, USA, October 14-16, 1974

    Hack, M.: The Recursive Equivalence of the Reachability Problem and the Liveness Problem for Petri Nets and Vector Addition Systems . In: 15th An- nual Symposium on Switching and Automata Theory, New Orlean s, Louisiana, USA, October 14-16, 1974. pp. 156–164. IEEE Computer Societ y (1974). https://doi.org/10.1109/SWAT.1974.28

    work page doi:10.1109/swat.1974.28 1974

  11. [11]

    Hujsa, T., Devillers, R.: On Deadlockability, Liveness and Reversibility in Sub- classes of Weighted Petri Nets. Fundam. Informaticae 161(4), 383–421 (2018). https://doi.org/10.3233/FI-2018-1708

    work page doi:10.3233/fi-2018-1708 2018

  12. [12]

    In: Pérez, G.A., Raskin, J

    Jančar, P., Leroux, J.: The Semilinear Home-Space Probl em Is Ackermann- Complete for Petri Nets. In: Pérez, G.A., Raskin, J. (eds.) 3 4th International Con- ference on Concurrency Theory, CONCUR 2023, September 18-2 3, 2023, Antwerp, Belgium. LIPIcs, vol. 279, pp. 36:1–36:17. Schloss Dagstuh l - Leibniz-Zentrum für Informatik (2023). https://doi.org/10.4...

    work page doi:10.4230/lipics.concur.2023.36 2023

  13. [13]

    Jančar, P., Leroux, J.: On the Home-Space Problem for Pet ri Nets and its Ackermannian Complexity. Log. Methods Comput. Sci. 20(4) (2024). https://doi.org/10.46298/LMCS-20(4:23)2024

    work page doi:10.46298/lmcs-20(4:23)2024 2024

  14. [14]

    Acta Informatica 56(6), 537– 552 (2019)

    Jančar, P., Purser, D.: Structural liveness of Petri net s is ExpSpace-hard and decidable. Acta Informatica 56(6), 537– 552 (2019). https://doi.org/10.1007/s00236-019-00338-6 , https://doi.org/10.1007/s00236-019-00338-6

    work page doi:10.1007/s00236-019-00338-6 2019

  15. [15]

    Jančar, P., Valůšek, J.: Structural Liveness of Immedia te Obser- vation Petri Nets. Fundam. Informaticae 188(3), 179–215 (2023). https://doi.org/10.3233/FI-222146

    work page doi:10.3233/fi-222146 2023

  16. [16]

    Durations and parametric model-checking in timed automata

    Klaedtke, F.: Bounds on the automata size for Presburger arith- metic. ACM Trans. Comput. Log. 9(2), 11:1–11:34 (2008). https://doi.org/10.1145/1342991.1342995

    work page doi:10.1145/1342991.1342995 2008

  17. [17]

    In: Etessami, K., Feige, U., P uppis, G

    Künnemann, M., Mazowiecki, F., Schütze, L., Sinclair-B anks, H., Wegrzy- cki, K.: Coverability in V ASS Revisited: Improving Rackoff’ s Bound to Ob- tain Conditional Optimality. In: Etessami, K., Feige, U., P uppis, G. (eds.) 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, July 10-14, 2023, Paderborn, Germany. LIPIcs, v o...

    work page doi:10.4230/lipics.icalp.2023.131 2023

  18. [18]

    In: Chattopadhyay, A., Gastin, P

    Leroux, J.: Distance Between Mutually Reachable Petri N et Configurations. In: Chattopadhyay, A., Gastin, P. (eds.) 39th IARCS Annual C onference on Foundations of Software Technology and Theoretical Comp uter Science, FSTTCS 2019, December 11-13, 2019, Bombay, India. LIPIcs, v ol. 150, pp. 47:1–47:14. Schloss Dagstuhl - Leibniz-Zentrum für Inf ormatik (20...

    work page doi:10.4230/lipics.fsttcs.2019.47 2019

  19. [19]

    Korhonen, A single-exponential time 2-approximation algorithm for treewidth, in: IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS 2021), 2022, pp

    Leroux, J.: The Reachability Problem for Petri Nets is No t Primitive Recur- sive. In: 62nd IEEE Annual Symposium on Foundations of Compu ter Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022. pp. 1241–12 52. IEEE (2021). https://doi.org/10.1109/FOCS52979.2021.00121 34 P. Jančar, J. Leroux, J. Valůšek

    work page doi:10.1109/focs52979.2021.00121 2021

  20. [20]

    In: 34th Annual ACM/IEEE Symp osium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019

    Leroux, J., Schmitz, S.: Reachability in Vector Additio n Systems is Primitive- Recursive in Fixed Dimension. In: 34th Annual ACM/IEEE Symp osium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. pp. 1–13. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785796

    work page doi:10.1109/lics.2019.8785796 2019

  21. [21]

    Mayr, E.W.: Some Complexity Results for Polynomial Idea ls. J. Complex. 13(3), 303–325 (1997). https://doi.org/10.1006/jcom.1997.0447

    work page doi:10.1006/jcom.1997.0447 1997

  22. [22]

    Advances in mathema tics 46(3), 305–329 (1982)

    Mayr, E.W., Meyer, A.R.: The complexity of the word probl ems for commuta- tive semigroups and polynomial ideals. Advances in mathema tics 46(3), 305–329 (1982). https://doi.org/10.1016/0001-8708(82)90048-2

    work page doi:10.1016/0001-8708(82)90048-2 1982

  23. [23]

    In: Ciardo, G., K indler, E

    Mayr, E.W., Weihmann, J.: A Framework for Classical Petr i Net Problems: Conservative Petri Nets as an Application. In: Ciardo, G., K indler, E. (eds.) Application and Theory of Petri Nets and Concurrency - 35th I nternational Conference, PETRI NETS 2014, Tunis, Tunisia, June 23-27, 20 14. Proceedings. Lecture Notes in Computer Science, vol. 8489, pp. 314...

    work page doi:10.1007/978-3-319-07734-5_17 2014

  24. [24]

    In: Book, R.V

    Pottier, L.: Minimal Solutions of Linear Diophantine Sy stems: Bounds and Al- gorithms. In: Book, R.V. (ed.) Rewriting Techniques and App lications, 4th In- ternational Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings. Lecture Notes in Computer Science, vol. 488, pp. 162–173. Sp ringer (1991). https://doi.org/10.1007/3-540-53904-2_94

    work page doi:10.1007/3-540-53904-2_94 1991

  25. [25]

    Rackoff, C.: The Covering and Boundedness Problems for Ve c- tor Addition Systems. Theor. Comput. Sci. 6, 223–231 (1978). https://doi.org/10.1016/0304-3975(78)90036-1

    work page doi:10.1016/0304-3975(78)90036-1 1978

  26. [26]

    In: Reachability Problems - 14th Interna tional Con- ference, RP 2020, Paris, France, October 19-21, 2020, Proce edings

    Raskin, M., Weil-Kennedy, C.: Efficient Restrictions of I mmediate Obser- vation Petri Nets. In: Reachability Problems - 14th Interna tional Con- ference, RP 2020, Paris, France, October 19-21, 2020, Proce edings. Lec- ture Notes in Computer Science, vol. 12448, pp. 99–114. Spri nger (2020). https://doi.org/10.1007/978-3-030-61739-4_7

    work page doi:10.1007/978-3-030-61739-4_7 2020

  27. [27]

    In: 31st International Confe rence on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria ( Virtual Confer- ence)

    Raskin, M.A., Weil-Kennedy, C., Esparza, J.: Flatness a nd Complexity of Imme- diate Observation Petri Nets. In: 31st International Confe rence on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria ( Virtual Confer- ence). LIPIcs, vol. 171, pp. 45:1–45:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230...

    work page doi:10.4230/lipics.concur.2020.45 2020

  28. [28]

    Understanding Petri Nets – Modeling Techniques, Analysis Methods, Case Studies

    Reisig, W.: Understanding Petri Nets. Springer-Verlag (2013). https://doi.org/10.1007/978-3-642-33278-4 , 230 pp

    work page doi:10.1007/978-3-642-33278-4 2013

  29. [29]

    John Wiley & Sons, Inc., USA (1986)

    Schrijver, A.: Theory of Linear and Integer Programming . John Wiley & Sons, Inc., USA (1986)

    work page 1986

  30. [30]

    Weil-Kennedy, C.: Observation Petri Nets. Ph.D. the- sis, Technical University of Munich, Germany (2023), https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20230320-1691161-1-3

    work page 2023