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.

翻译：我们研究了谢苗诺夫算术（结构$(\mathbb{N}, +, 2^x)$的一阶理论）的扩展。众所周知，当该理论通过数串元组上的正则谓词（如Büchi $V_2$谓词）扩展时，其可判定性将丧失。因此，我们将研究范围限定于谢苗诺夫算术的存在性理论，并证明当该理论通过数串元组上的任意正则谓词扩展时，其可判定性属于EXPSPACE复杂度类。我们的方法依赖于将问题归约为某类受限仿射向量加法系统（带状态）的语言空性判定问题，而后者被证明可在EXPSPACE中判定。作为应用，我们解决了文献中的一个开放问题，证明了一类涉及长度约束的字符串约束的可判定性。