Document Open Access Logo

Semënov Arithmetic, Affine {VASS}, and String Constraints

Authors Andrei Draghici , Christoph Haase , Florin Manea

PDF
Thumbnail PDF

File

LIPIcs.STACS.2024.29.pdf
  • Filesize: 0.95 MB
  • 19 pages

Document Identifiers

Author Details

Andrei Draghici
  • Department of Computer Science, University of Oxford, UK
Christoph Haase
  • Department of Computer Science, University of Oxford, UK
Florin Manea
  • Computer Science Department and Campus-Institut Data Science, Göttingen University, Germany

Funding

This work is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT). Florin Manea’s work was supported by a Heisenberg Grant, funded by the Deutsche Forschungsgemeinschaft (DFG, project 466789228).

Cite AsGet BibTex

Andrei Draghici, Christoph Haase, and Florin Manea. Semënov Arithmetic, Affine {VASS}, and String Constraints. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.STACS.2024.29

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • arithmetic theories
  • Büchi arithmetic
  • exponentiation
  • vector addition systems with states
  • string constraints

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. Norn: An SMT solver for string constraints. In Proc. Computer Aided Verification, CAV, volume 9206 of Lect. Notes Comp. Sci., pages 462-469, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_29.
  2. Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The Complexity of Presburger Arithmetic with Power or Powers. In International Colloquium on Automata, Languages, and Programming, ICALP, volume 261 of Leibniz International Proceedings in Informatics (LIPIcs), pages 112:1-112:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.112.
  3. Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, and Dirk Nowotka. Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci., 943:50-72, 2023. URL: https://doi.org/10.1016/j.tcs.2022.12.009.
  4. Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, and Vijay Ganesh. An SMT solver for regular expressions and linear arithmetic over string length. In Computer Aided Verification, CAV, volume 12760 of Lect. Notes Comp. Sci., pages 289-312, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_14.
  5. Achim Blumensath and Erich Grädel. Automatic structures. In Logic in Computer Science, LICS, pages 51-62. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/LICS.2000.855755.
  6. Véronique Bruyère, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin, 1(2):191-238, 1994. URL: https://doi.org/10.36045/bbms/1103408547.
  7. Gregory Cherlin and Françoise Point. On extensions of Presburger arithmetic. In Proc. 4th Easter Model Theory conference, Gross Köris, pages 17-34, 1986. Google Scholar
  8. Alain Finkel, Stefan Göller, and Christoph Haase. Reachability in register machines with polynomial updates. In Proc. Mathematical Foundations of Computer Science, MFCS, volume 8087 of Lect. Notes Comp. Sci., pages 409-420. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40313-2_37.
  9. Florent Guépin, Christoph Haase, and James Worrell. On the existential theories of Büchi arithmetic and linear p-adic fields. In Proc. Symposium on Logic in Computer Science, LICS, pages 1-10, 2019. URL: https://doi.org/10.1109/LICS.2019.8785681.
  10. Bakhadyr Khoussainov and Anil Nerode. Automatic presentations of structures. In Logical and Computational Complexity, LCC, volume 960 of Lect. Notes Comp. Sci., pages 367-392. Springer, 1995. URL: https://doi.org/10.1007/3-540-60178-3_93.
  11. Françoise Point. On the expansion of (ℕ,+,2^x) of Presburger arithmetic. Unpublished manuscript, 2010. URL: https://u.osu.edu/friedman.8/files/2014/01/0AppB072710-1mnlwyn.pdf.
  12. Julien Reichert. Reachability games with counters: decidability and algorithms. PhD thesis, École normale supérieure de Cachan-ENS Cachan, 2015. Google Scholar
  13. A. L. Semënov. On certain extensions of the arithmetic of addition of natural numbers. Mathematics of the USSR-Izvestiya, 15(2):401, 1980. URL: https://doi.org/10.1070/IM1980v015n02ABEH001252.
  14. Pierre Wolper and Bernard Boigelot. On the construction of automata from linear arithmetic constraints. In Proc. Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pages 1-19, 2000. URL: https://doi.org/10.1007/3-540-46419-0_1.
  15. Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, and Naijun Zhan. A decision procedure for string constraints with string/integer conversion and flat regular constraints. Acta Informatica, October 2023. URL: https://doi.org/10.1007/s00236-023-00446-4.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact