Reachability in 2-dimensional Branching Vector Addition Systems with States

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.