Semenov Arithmetic, Affine VASS, and String Constraints

We study extensions of Semenov arithmetic, the first-order theory of the structure $\langle \mathbb{N}, +, 2^x\rangle$. It is well-known that this theory becomes undecidable when extended with regular predicates over number strings, such as the Büchi $V_2$-predicate. We therefore restrict ourselves to the existential theory of Semenov arithmetic and show that this theory is decidable in 2-EXPSPACE when extended with arbitrary regular predicates over number strings. Our approach relies on a reduction to the 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. Contributed talk given by Andrei Draghici

Authors

• Andrei Draghici

Keywords

No keywords are indexed for this paper.