Reachability in Branching Vector Addition Systems (BVAS)

Speaker(s)

Clotilde Bizière

Affiliation

University of Warsaw, University of Bordeaux

Language of the talk

English

Date

May 20, 2026, 2:15 p.m.

Room

room 5440

Title in Polish

Reachability in Branching Vector Addition Systems (BVAS)

Seminar

Seminar Automata Theory

---

The reachability problem for Vector Addition Systems (VAS) admits two fundamentally different decidability proofs. The classical KLM approach relies on a structural decomposition of runs and yields the optimal Ackermannian complexity bounds. A more recent approach due to Leroux is based instead on inductive invariants: whenever a target configuration is not reachable, there exists a semilinear set containing the source configuration, closed under the transitions of the system, and excluding the target. Decidability then follows by combining an enumeration of runs with a search for such invariants. The proof of existence of these inductive invariants itself splits into two parts. The first establishes geometric properties of VAS reachability sets, namely that they are almost semilinear. The second shows that transition systems with almost semilinear reachability sets admit semilinear inductive invariants.

Branching Vector Addition Systems (BVAS) extend VAS with branching transitions allowing two reachable configurations to be combined into a new one. As a consequence, computations are tree-shaped rather than word-shaped. Their reachability problem has remained open since the model was introduced in 2004.

Joint work with Jérôme Leroux and Grégoire Sutre aims at extending the inductive invariant approach to BVAS. We first showed that BVAS reachability sets are sections of VAS reachability sets, and therefore inherit their geometric properties (FoSSaCS 2026). However, this does not by itself yield inductive invariants. Indeed, Leroux’s argument relies crucially on VAS being symmetric (taking the opposite of every action in a VAS V yields a reversed VAS V' such that runs from s to t in V correspond to runs from t to s in V'). This symmetry breaks down in the branching setting. We therefore revisited the VAS invariant argument so that it no longer depends on this symmetry property (submitted), and finally extended the construction to BVAS (currently being written up).

During the first hour, I will present the proof that BVAS reachability sets are VAS sections, together with some consequences (including a simple reachability algorithm in dimension two) and related open computability questions. The proof is lightweight and non-technical, and relies on a natural extension to BVAS of Jancar’s well-quasi-order on VAS runs. During the second hour, I will present the inductive invariant construction, which is more technical.
 

---