# Reachability for Bounded Branching VASS

## TL;DR

This paper studies the reachability problem in bounded branching VASS, showing that it is EXPTIME-complete for dimensions two or higher, extending previous results on simpler models.

## Contribution

It establishes the complexity of reachability in bounded branching VASS, demonstrating EXPTIME-completeness for dimensions two and above, which was previously unknown.

## Key findings

- Reachability in bounded branching VASS is EXPTIME-complete for dimension ≥ 2.
- The model extends classic VASS with branching transitions and bounded configurations.
- Previous PSPACE-complete results for dimension 1 do not extend to higher dimensions.

## Abstract

In this paper we consider the reachability problem for bounded branching VASS. Bounded VASS are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. This model gained a lot of attention in 2012 when Haase et al. showed its connections with timed automata. Later in 2013 Fearnley and Jurdzi\'{n}ski proved that the reachability problem in this model is PSPACE-complete even in dimension 1. Here, we investigate the complexity of the reachability problem when the model is extended with branching transitions, and we prove that the problem is EXPTIME-complete when the dimension is 2 or larger.