Document Open Access Logo

The Complexity of Presburger Arithmetic with Power or Powers

Authors Michael Benedikt , Dmitry Chistikov , Alessio Mansutti

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.112.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Michael Benedikt
  • Department of Computer Science, University of Oxford, UK
Dmitry Chistikov
  • Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Alessio Mansutti
  • IMDEA Software Institute, Madrid, Spain

Funding

  • Benedikt, Michael: funded in part by EPSRC grant EP/T022124/1.
  • Chistikov, Dmitry: acknowledges the support of IMDEA Software Institute.
  • Mansutti, Alessio: funded in part by ERC grant No. 852769 (ARiAT).

Cite AsGet BibTex

Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The Complexity of Presburger Arithmetic with Power or Powers. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 112:1-112:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.112

Abstract

We investigate expansions of Presburger arithmetic (Pa), i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function that takes a number to the power of 2, or a predicate 2^ℕ for the powers of 2. The latter theory, denoted Pa(2^ℕ(·)), was introduced by Büchi as a first attempt at characterizing the sets of tuples of numbers that can be expressed using finite automata; Büchi’s method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as Pa(λx.2^|x|), was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by Büchi, Semenov’s method is also non-elementary. And in fact, the theory with the power function has a non-elementary lower bound. In this paper, we show that while Semenov’s and Büchi’s approaches yield non-elementary blow-ups for Pa(2^ℕ(·)), the theory is in fact decidable in triply exponential time, similarly to the best known quantifier-elimination algorithm for Pa. We also provide a NExpTime upper bound for the existential fragment of Pa(λx.2^|x|), a step towards a finer-grained analysis of its complexity. Both these results are established by analyzing a single parameterized satisfiability algorithm for Pa(λx.2^|x|), which can be specialized to either the setting of Pa(2^ℕ(·)) or the existential theory of Pa(λx.2^|x|). Besides the new upper bounds for the existential theory of Pa(λx.2^|x|) and Pa(2^ℕ(·)), we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • arithmetic theories
  • exponentiation
  • decision procedures

Metrics

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

Related Versions

References

  1. Leonard Berman. The complexity of logical theories. Theor. Comput. Sci., 11(1):71-77, 1980. Google Scholar
  2. Alexis Bès. A survey of arithmetic definability. Soc. Math. Belgique, pages 1-54, 2002. Google Scholar
  3. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Springer, 1997. Google Scholar
  4. Gregory Cherlin and Françoise Point. On extensions of Presburger arithmetic. In 4th Easter Conference on Model Theory, volume 86 of Humboldt-Univ. Berlin Seminarberichte, pages 17-34, 1986. URL: https://webusers.imj-prg.fr/~francoise.point/papiers/cherlin_point86.pdf.
  5. Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. In LICS, 2022. Google Scholar
  6. Kevin J. Compton and C. Ward Henson. A uniform method for proving lower bounds on the computational complexity of logical theories. APAL, 48(1):1-79, 1990. Google Scholar
  7. Antoine Durand-Gasselin and Peter Habermehl. On the use of non-deterministic automata for Presburger arithmetic. In CONCUR, 2010. Google Scholar
  8. Jeanne Ferrante and Charles Rackoff. A decision procedure for the first order theory of real addition with order. SIAM J. Comput., 4(1):69-76, 1975. Google Scholar
  9. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. Google Scholar
  10. Robert Givan, David McAllester, Carl Witty, and Dexter Kozen. Tarskian set constraints. Information and Computation, 174(2):105-131, 2002. Google Scholar
  11. Florent Guépin, Christoph Haase, and James Worrell. On the existential theories of Büchi arithmetic and linear p-adic fields. In LICS, 2019. Google Scholar
  12. Philipp Hieronymi and Christian Schulz. A strong version of Cobham’s theorem. In STOC, 2022. Google Scholar
  13. Deepak Kapur, Zhihai Zhang, Matthias Horbach, Hengjun Zhao, Qi Lu, and ThanhVu Nguyen. Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariants. In Automated Reasoning and Mathematics - Essays in Memory of William W. McCune, volume 7788 of LNCS, pages 189-228. Springer, 2013. Google Scholar
  14. Felix Klaedtke. Bounds on the automata size for Presburger arithmetic. ACM Trans. Comput. Log., 9(2):11:1-11:34, 2008. Google Scholar
  15. Antonia Lechner, Joël Ouaknine, and James Worrell. On the complexity of linear arithmetic with divisibility. In LICS, 2015. Google Scholar
  16. Antoine Miné. The octagon abstract domain. High. Order Symb. Comput., 19(1):31-100, 2006. Google Scholar
  17. Derek C. Oppen. A 2^2^2^pn upper bound on the complexity of Presburger arithmetic. JCSS, 16(3):323-332, 1978. Google Scholar
  18. Rohit J. Parikh. On context-free languages. J. ACM, 13(4):570-581, 1966. Google Scholar
  19. Françoise Point. On decidable extensions of Presburger arithmetic: from A. Bertrand numeration systems to Pisot numbers. JSL, 65(3):1347-1374, 2000. Google Scholar
  20. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, 1929. In Comptes Rendus du I Congrès des Mathématiciens des Pays Slaves, pages 92-101. Google Scholar
  21. Rodrigo Raya, Jad Hamza, and Viktor Kunčak. On the complexity of convex and reverse convex prequadratic constraints. In LPAR, 2023. Google Scholar
  22. C. R. Reddy and D. W. Loveland. Presburger arithmetic with bounded quantifier alternation. In STOC, 1978. Google Scholar
  23. Aleksei L. Semenov. On certain extensions of the arithmetic of addition of natural numbers. Math. USSR Izv., 15(2):401-418, 1980. Google Scholar
  24. Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv., 22(3):587-618, 1984. Google Scholar
  25. Volker Weispfenning. The Complexity of Almost Linear Diophantine Problems. J. Symb. Comput., 10(5):395-404, 1990. Google Scholar
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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact