2026-07-23T12:54:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19739 2024-03-12T12:14:47Z ddc:004 open_access

Semënov Arithmetic, Affine {VASS}, and String Constraints Draghici, Andrei Haase, Christoph Manea, Florin arithmetic theories Büchi arithmetic exponentiation vector addition systems with states string constraints We study extensions of Semënov arithmetic, the first-order theory of the structure ⟨ℕ,+,2^x⟩. It is well-known that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the Büchi V₂-predicate. We therefore restrict ourselves to the existential theory of Semënov 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrei Draghici and Christoph Haase and Florin Manea 2024 Is Part Of LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2024.29 urn:nbn:de:0030-drops-197393 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.29 eng https://creativecommons.org/licenses/by/4.0/legalcode