Sem\"enov Arithmetic, Affine VASS, and String Constraints

TL;DR

This paper proves the decidability of an existential fragment of Sem"enov arithmetic extended with regular predicates, by reducing it to affine VASS emptiness, and applies this to string length constraints.

Contribution

It establishes decidability of the existential theory of Sem"enov arithmetic with regular predicates via a reduction to affine VASS emptiness, solving an open problem.

Findings

Existential Sem"enov arithmetic with regular predicates is decidable in EXPSPACE.

Reduction to affine VASS emptiness is effective for this theory.

Decidability of certain string length constraints is achieved.

Abstract

We study extensions of Sem\"enov arithmetic, the first-order theory of the structure $(\mathbb{N}, +, 2^x)$. It is well-knonw that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the B\"uchi $V_2$-predicate. We therefore restrict ourselves to the existential theory of Sem\"enov 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 results, we settle an open problem from the literature and show decidability of a class of string constraints involving length constraints.