On the Reachability Problem for Two-Dimensional Branching VASS
Abstract
Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there exists a run from an initial configuration to a final one. This problem has been known to be decidable for over forty years, and its complexity has recently been precisely characterized. Our work concerns the reachability problem for BVASS, a branching generalization of VASS. In dimension one, the exact complexity of this problem is known. In this paper, we prove that the reachability problem for 2-dimensional BVASS is decidable. In fact, we even show that the reachability set admits a computable semilinear presentation. The decidability status of the reachability problem for BVASS remains open in higher dimensions.
Keywords
Cite
@article{arxiv.2506.22561,
title = {On the Reachability Problem for Two-Dimensional Branching VASS},
author = {Clotilde Bizière and Thibault Hilaire and Jérôme Leroux and Grégoire Sutre},
journal= {arXiv preprint arXiv:2506.22561},
year = {2025}
}
Comments
Full version of the paper with the same title and authors to appear in the proceedings of MFCS 2025