pith. sign in

arxiv: 2606.27166 · v1 · pith:OKLHP2WEnew · submitted 2026-06-25 · 💻 cs.LO · cs.FL

A Forward-Only Construction of Semilinear Inductive Invariants for VAS

Clotilde Bizi\`ere , J\'er\^ome Leroux , Gr\'egoire Sutre This is my paper

Pith reviewed 2026-06-26 02:15 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords vector addition systemssemilinear inductive invariantsforward constructionreachabilityperiodic invariantsbranching VAS
0
0 comments X

The pith

Semilinear inductive invariants for VAS can be built forward-only from the source configuration alone.

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

The paper introduces a forward-only construction of semilinear inductive invariants for vector addition systems. This method constructs the invariants starting only from the source configuration and without any backward reasoning or dependence on the target. Previous approaches used a symmetric back-and-forth scheme that mixed source and target information. The new invariants are more canonical and better reflect the structure of the VAS. The construction also guarantees periodic invariants when the system itself is periodic, and it advances the goal of handling branching variants of the model.

Core claim

We introduce a new forward-only construction of semilinear inductive invariants for VAS. Our method builds invariants from the source configuration alone and avoids the need for backward reasoning. This yields invariants that are more canonical and better aligned with the structure of the system. In particular, our method produces periodic inductive invariants for periodic VAS. Beyond its intrinsic interest, our approach provides a step toward extending invariant-based techniques to Branching VAS.

What carries the argument

Forward-only construction of semilinear inductive invariants that enumerates runs from the source to find witnesses of non-reachability.

If this is right

  • Invariants are guaranteed to be more aligned with the VAS structure.
  • The method produces periodic invariants for periodic VAS.
  • The construction can be extended more readily to asymmetric models such as Branching VAS.
  • Non-reachability witnesses do not require target-dependent backward closure.

Where Pith is reading between the lines

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

  • This could simplify implementations by eliminating the need to compute backward closures.
  • The canonical invariants might be useful for analyzing families of targets from the same source.
  • It hints at the possibility of source-specific invariants that certify reachability properties independently of particular targets.

Load-bearing premise

A forward-only procedure is guaranteed to find a valid semilinear inductive invariant for any unreachable target without using backward reasoning or target information.

What would settle it

An example of a VAS with unreachable target where the forward-only search fails to produce any semilinear inductive invariant that proves the non-reachability.

read the original abstract

The reachability problem for Vector Addition Systems (VAS) is a central decision problem in the theory of infinite-state systems, first solved by Kosaraju and Mayr in the 1980s. An alternative, conceptually simpler approach introduced by Leroux shows that non-reachability is always witnessed by semilinear inductive invariants, yielding a decision procedure by combining an enumeration of runs with a search for such invariants. However, the construction of these invariants relies on a back-and-forth scheme that depends symmetrically on the source and the target. As a result, the invariants are not guaranteed to reflect the structural properties of the VAS, and the construction is difficult to extend to asymmetric models such as Branching VAS. We introduce a new forward-only construction of semilinear inductive invariants for VAS. Our method builds invariants from the source configuration alone and avoids the need for backward reasoning. This yields invariants that are more canonical and better aligned with the structure of the system. In particular, our method produces periodic inductive invariants for periodic VAS. Beyond its intrinsic interest, our approach provides a step toward extending invariant-based techniques to Branching VAS.

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

2 major / 2 minor

Summary. The paper claims to introduce a forward-only construction of semilinear inductive invariants for Vector Addition Systems (VAS) that starts solely from the source configuration and avoids any backward reasoning or target-dependent information. This is presented as an improvement over Leroux's symmetric back-and-forth scheme, yielding invariants that are more canonical and structurally aligned with the VAS; in particular, the method is claimed to produce periodic inductive invariants when the VAS is periodic. The construction is positioned as a step toward extending invariant-based techniques to Branching VAS.

Significance. If the forward construction is both sound and complete, the result would supply a target-independent decision procedure for VAS reachability that respects the asymmetry of the model and produces invariants with better structural properties. This could facilitate extensions to related systems such as Branching VAS and clarify the relationship between periodicity of the system and periodicity of its invariants.

major comments (2)
  1. [Construction and completeness argument (likely §4)] The central completeness claim—that the forward-only enumeration from the source is guaranteed to eventually produce a separating semilinear inductive invariant whenever the target is unreachable—requires an explicit argument that every possible separating semilinear set is eventually generated by the forward procedure. The manuscript does not appear to supply a lemma or theorem establishing this guarantee without implicit appeal to backward closure.
  2. [Periodic case (likely §5)] For periodic VAS, the claim that the forward method produces periodic invariants (stated in the abstract and presumably formalized later) is load-bearing for the 'better aligned with the structure' assertion, yet the provided development does not contain a general proof that the generated invariants inherit periodicity from the VAS without additional target-dependent filtering.
minor comments (2)
  1. [Abstract and §1] The abstract refers to 'periodic VAS' and 'periodic inductive invariants' without a preliminary definition or reference; a short definitional paragraph or citation in the introduction would improve readability.
  2. [Preliminaries] Notation for semilinear sets and the precise form of the forward enumeration operator could be illustrated with a small running example immediately after the definitions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The two major comments identify places where the completeness and periodicity arguments would benefit from more explicit development. We address each below and will revise the manuscript to incorporate the requested clarifications.

read point-by-point responses

  1. Referee: [Construction and completeness argument (likely §4)] The central completeness claim—that the forward-only enumeration from the source is guaranteed to eventually produce a separating semilinear inductive invariant whenever the target is unreachable—requires an explicit argument that every possible separating semilinear set is eventually generated by the forward procedure. The manuscript does not appear to supply a lemma or theorem establishing this guarantee without implicit appeal to backward closure.

    Authors: We agree that the completeness argument in §4 would be strengthened by an explicit lemma establishing that the forward enumeration eventually generates every separating semilinear inductive invariant. The current text sketches the enumeration but does not isolate this guarantee as a standalone statement. In the revision we will add a new lemma (and its proof) showing that any semilinear set separating an unreachable target can be obtained by forward closure operations starting from the source configuration alone, without any appeal to backward reachability. revision: yes

  2. Referee: [Periodic case (likely §5)] For periodic VAS, the claim that the forward method produces periodic invariants (stated in the abstract and presumably formalized later) is load-bearing for the 'better aligned with the structure' assertion, yet the provided development does not contain a general proof that the generated invariants inherit periodicity from the VAS without additional target-dependent filtering.

    Authors: We accept that a general proof is required to substantiate the claim that the forward construction produces periodic invariants for periodic VAS. The abstract states the property, but §5 currently illustrates it only on examples rather than proving it in full generality. We will add a theorem in the revised §5 proving that every invariant generated by the forward procedure from a periodic VAS is itself periodic, with no target-dependent filtering step. revision: yes

Circularity Check

0 steps flagged

No circularity detected in forward-only construction

full rationale

The paper presents a new algorithmic construction of semilinear inductive invariants that operates forward from the source configuration alone. The existence of semilinear invariants is cited to prior work, but the forward-only enumeration procedure, its completeness guarantee, and the production of periodic invariants are introduced as independent algorithmic contributions without any reduction of predictions to fitted inputs, self-definitional equations, or load-bearing self-citation chains. No equations or derivations in the provided abstract or description collapse to the inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract only; no free parameters, axioms, or invented entities are described.

pith-pipeline@v0.9.1-grok · 5742 in / 996 out tokens · 21903 ms · 2026-06-26T02:15:42.960203+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

12 extracted references · 11 canonical work pages

  1. [1]

    Fischer, and René Peralta

    1 Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. In Soma Chaudhuri and Shay Kutten, editors,Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Distributed Computing, PODC 2004, St. John’s, Newfoundland, Canada, July 25-28, 2004, pages 290–2...

    work page doi:10.1145/1011767.1011810 2004

  2. [2]

    2022 , volume =

    Springer Nature Switzerland. 4 Wojciech Czerwiński and Łukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), pages 1229–1240, 2022.doi:10.1109/FOCS52979.2021.00120. 5 Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. Vector addition tree automa...

    work page doi:10.1109/focs52979.2021.00120 2022

  3. [3]

    10 Michel Hack

    to appear at LICS 2026.arXiv:arXiv:2504.05015. 10 Michel Hack. The equality problem for vector addition systems is undecidable.Theor. Comput. Sci., 2(1):77–95, 1976.doi:10.1016/0304-3975(76)90008-6. 11 Petr Jančar. Undecidability of bisimilarity for Petri nets and some related problems.Theor. Comput. Sci., 148(2):281–301, 1995.doi:10.1016/0304-3975(95)000...

    work page doi:10.1016/0304-3975(76)90008-6 2026

  4. [4]

    13 Richard M

    URL:https://www.sciencedirect.com/science/article/pii/ 0304397590900064,doi:10.1016/0304-3975(90)90006-4. 13 Richard M. Karp and Raymond E. Miller. Parallel Program Schemata.J. Comput. Syst. Sci., 3(2):147–195, 1969.doi:10.1016/S0022-0000(69)80011-5. 14 S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). InProce...

    work page doi:10.1016/0304-3975(90)90006-4 1969

  5. [5]

    Association for Computing Machinery.doi: 10.1145/800070.802201. C. Bizière, J. Leroux, and G. Sutre 15 15 Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data.Fundam. Informaticae, 88(3):251–274,

    work page doi:10.1145/800070.802201

  6. [6]

    16 Jérôme Leroux

    URL: http://content.iospress.com/articles/fundamenta-informaticae/fi88-3-03. 16 Jérôme Leroux. The general vector addition system reachability problem by presburger inductive invariants. InProceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 4–13. IEEE Computer Society, 2009....

    work page doi:10.1109/lics.2009.10 2009

  7. [7]

    29007/bnx2

    URL:/publications/paper/Blr, doi:10. 29007/bnx2. 19 Jérôme Leroux. Presburger vector addition systems. In28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 23–32. IEEE Computer Society, 2013.doi:10.1109/LICS.2013.7. 20 Jérôme Leroux. The reachability problem for Petri nets is not primitive...

    work page doi:10.1109/lics.2013.7 2013

  8. [8]

    IEEE Computer Society.doi:10.1109/LICS.2015

    work page doi:10.1109/lics.2015 2015

  9. [9]

    Reachability in vector addition systems is primitive- recursive in fixed dimension

    22 Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive- recursive in fixed dimension. In34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1–13. IEEE,

    2019

  10. [10]

    25 Richard J

    doi:10.1109/LICS.2019.8785796. 23 Ernst W. Mayr. An algorithm for the general Petri net reachability problem.SIAM J. Comput., 13(3):441–460, 1984.doi:10.1137/0213029. 24 Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs.Electronic Notes in Theoretical Computer Science, 223:239–264,

    work page doi:10.1109/lics.2019.8785796 2019

  11. [11]

    URL: https://www.sciencedirect.com/ science/article/pii/S1571066108005057,doi:10.1016/j.entcs.2008.12.042

    Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008). URL: https://www.sciencedirect.com/ science/article/pii/S1571066108005057,doi:10.1016/j.entcs.2008.12.042. 25 Wim Veldman and Marc Bezem. Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics.Journal of the London Mathematical Society, s2-4...

    work page doi:10.1016/j.entcs.2008.12.042 2008

  12. [12]

    26 Kumar Neeraj Verma and Jean Goubault-Larrecq

    URL:https://londmathsoc.onlinelibrary.wiley.com/doi/abs/10.1112/jlms/ s2-47.2.193, arXiv:https://londmathsoc.onlinelibrary.wiley.com/doi/pdf/10.1112/ jlms/s2-47.2.193,doi:10.1112/jlms/s2-47.2.193. 26 Kumar Neeraj Verma and Jean Goubault-Larrecq. Karp-Miller trees for a branching extension of VASS.Discret. Math. Theor. Comput. Sci., 7(1):217–230, 2005.doi:...

    work page doi:10.1112/jlms/ 2005