Integer reachability in data VASS

Data Vector Addition Systems with States (data VASS) is an extension of plain Vector Addition Systems with States (VASS) for which the decidability status of  the reachability problem is still open. We show decidability of the integer reachability problem (the counters can drop below zero), and believe this result to be a major step towards solving proper reachability. Integer reachability in data VASS is way more complex than in plain VASS (where it is reducible to integer linear programming), mostly due to the fact that the state spaces are not finite but orbit-finite. Our solution combines an iterative decision procedure, inspired by the KLM decomposition in plain VASS, with new techniques for proving termination. As corollaries, we can deduce decidability of the nonemptiness of intersection of Parikh images of register automata, and of the reachability problem for data T-nets (a structural restriction of data Petri nets, the model equivalent to data VASS).