Semenov Arithmetic, Affine VASS, and String Constraints

We study extensions of Semenov arithmetic, the first-order theory of the structure < N,+, 2(x)>. It is well-known that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the Buchi V-2-predicate. We therefore restrict ourselves to the existential theory of Semenov arithmetic and show that this theory is decidable in EXPSPACE when extended with arbitrary regular predicates over tuples of number strings. Our approach relies on a reduction to the language emptiness problem for a restricted class of affine vector addition systems with states, which we show decidable in EXPSPACE. As an application of our result, we settle an open problem from the literature and show decidability of a class of string constraints involving length constraints.