Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants

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

Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants

Logic in Computer Science 2026-07-10 v1 Formal Languages and Automata Theory

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

Abstract

In this paper, we solve the reachability problem for branching vector addition systems (BVAS), a long standing open problem. Our approach is based on semilinear inductive invariants. More precisely, we prove that if a configuration of a BVAS is not reachable, then there exists an inductive invariant, given as a semilinear set, that does not contain this configuration. Based on this property, we deduce a very simple (enumerative) algorithm solving the reachability problem for BVAS.

Cite

@article{arxiv.2607.09558,
  title  = {Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants},
  author = {Clotilde Bizière and Jérôme Leroux and Grégoire Sutre},
  journal= {arXiv preprint arXiv:2607.09558},
  year   = {2026}
}