# Reachability in 2-dimensional Branching Vector Addition Systems with States

- Speaker(s)
**Clotilde Biziere**- Affiliation
- University of Warsaw / ENS Paris
- Date
- April 10, 2024, 2:15 p.m.
- Room
- room 5050
- Seminar
- Seminar Automata Theory

Vector addition systems with states (VASS) are finite-state machines

equipped with a finite number of counters ranging over nonnegative

integers. Operations on counters are limited to incrementation and

decrementation. Their central algorithmic problem is reachability: given

a VASS, decide whether there exists an execution from an initial

configuration to a final one. This problem was shown decidable in 1981

by a complex proof.

Hopcroft and Pansiot were among the first to address the VASS

reachability problem. They showed in 1979 that the set of reachable

configurations of a VASS (for a given initial configuration) is

semi-linear in dimension 2, and proposed a specific algorithm, simpler

than the general approach, to compute it. Unfortunately, this approach

no longer works in higher dimensions: already in dimension 3, there are

VASS whose reachability set is not semi-linear.

Branching VASS (BVASS) are one popular extension of VASS. Their

reachability problem is well understood in dimension 1, but the general

case is still open. In this talk, I will present an algorithm extending

the approach of Hopcroft and Pansiot to BVASS, thus proving that

reachability is decidable in 2-dimensional BVASS. I did this work during

an internship at the University of Bordeaux (France) supervised by

Jérôme Leroux, Grégoire Sutre and Thibaut Hilaire.