Reachability for BoBrVASS

Bounded Vector Addition Systems with States (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ński proved that the reachability problem in this model is PSPACE-complete even in dimension 1. In the talk we will discuss the complexity of the reachability problem when the model is further extended with branching transitions; we call this new model BoBrVASS, which stands for Bounded Branching VASS. We will sketch the proof that the problem is EXPTIME-complete when the dimension is 2 or larger, leaving the case of dimension 1 as an interesting open problem. The talk will be based on a manuscript co-authored with Filip Mazowiecki (LaBRI, Université de Bordeaux), available as a pre-print on arxiv: https://arxiv.org/abs/1904.10226

Authors

• Michał Pilipczuk.

Keywords

No keywords are indexed for this paper.