Rencontre,
15 October 2026
Clotilde Bizière (LABRI, Bordeaux), Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants
Résumé
In this talk, I will present a proof of decidability for the reachability problem in branching vector addition systems (BVAS), a long-standing open problem that is equivalent to provability in the multiplicative exponential fragment of linear logic (MELL). 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.



