Document Open Access Logo

A Forward-Only Construction of Semilinear Inductive Invariants for VAS

Authors Clotilde Bizière , Jérôme Leroux , Grégoire Sutre

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.9.pdf
  • Filesize: 0.78 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Vector addition systems
  • Inductive invariants
  • Semilinear sets
  • Verification

Metrics

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.

Cite As Get BibTex

Clotilde Bizière, Jérôme Leroux, and Grégoire Sutre. A Forward-Only Construction of Semilinear Inductive Invariants for VAS. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.9

Author Details

Clotilde Bizière
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
  • University of Warsaw, Poland
Jérôme Leroux
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Grégoire Sutre
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France

Funding

This work was supported by the grant ANR-25-CE48-6933 of the French National Research Agency (project CoqoPetri).
  • Bizière, Clotilde: Supported by Polish National Science Centre SONATA BIS-12 grant number 2022/46/E/ST6/00230.

Acknowledgements

We are grateful to Jean Goubault-Larrecq and Philippe Schnoebelen for drawing our attention to Ramsey’s Theorem and connections with almost-full relations.

References

  1. Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. In 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-299. ACM, 2004. URL: https://doi.org/10.1145/1011767.1011810.
  2. Clotilde Bizière, Jérôme Leroux, and Grégoire Sutre. Bridging the gap between plain VASS and branching VASS. In Foundations of Software Science and Computation Structures - 29th International Conference, FoSSaCS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, volume 16503 of Lecture Notes in Computer Science, pages 65-87. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22730-0_4.
  3. Clotilde Bizière, Jérôme Leroux, and Grégoire Sutre. A forward-only construction of semilinear inductive invariants for VAS, 2026. URL: https://arxiv.org/abs/2606.27166.
  4. Wojciech Czerwiński and Łukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), pages 1229-1240, 2022. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  5. Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. Vector addition tree automata. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 64-73. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319601.
  6. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, July 1992. URL: https://doi.org/10.1145/146637.146681.
  7. S. Ginsburg and E. H. Spanier. Semigroups, Presburger formulas, and languages. Pacific J. Math., 16(2):285-296, 1966. URL: https://doi.org/10.2140/pjm.1966.16.285.
  8. Roland Guttenberg, Wojciech Czerwiński, and Sławomir Lasota. Reachability and related problems in vector addition systems with nested zero tests. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 581-593, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00050.
  9. Roland Guttenberg, Eren Keskin, and Roland Meyer. PVASS reachability is decidable. In 41st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2026, Lisbon, 20-23 July, 2026, LIPIcs, pages 53:1-53:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. URL: https://doi.org/10.4230/LIPIcs.LICS.2026.53.
  10. Petr Jančar. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science, 74(1):71-93, 1990. URL: https://doi.org/10.1016/0304-3975(90)90006-4.
  11. Richard M. Karp and Raymond E. Miller. Parallel Program Schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  12. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC '82, pages 267-281, New York, NY, USA, 1982. Association for Computing Machinery. URL: https://doi.org/10.1145/800070.802201.
  13. 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, 2008. URL: https://dl.acm.org/doi/10.5555/1497079.1497082.
  14. Jérôme Leroux. The general vector addition system reachability problem by presburger inductive invariants. In Proceedings 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. URL: https://doi.org/10.1109/LICS.2009.10.
  15. Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 307-316. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926421.
  16. Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. URL: https://doi.org/10.29007/BNX2.
  17. Jérôme Leroux. Presburger vector addition systems. In 28th 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. URL: https://doi.org/10.1109/LICS.2013.7.
  18. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  19. Jerome Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS '15, pages 56-67, USA, 2015. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2015.16.
  20. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  21. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. URL: https://doi.org/10.1137/0213029.
  22. Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electronic Notes in Theoretical Computer Science, 223:239-264, 2008. Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008). URL: https://doi.org/10.1016/j.entcs.2008.12.042.
  23. Wim Veldman and Marc Bezem. Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society, s2-47(2):193-211, 1993. URL: https://doi.org/10.1112/jlms/s2-47.2.193.
  24. 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. URL: https://doi.org/10.46298/DMTCS.350.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact