The Library
The complexity of Presburger arithmetic with power or powers
Tools
Benedikt, Michael, Chistikov, Dmitry and Mansutti, Alessio (2023) The complexity of Presburger arithmetic with power or powers. In: 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), Paderborn, Germany, 10-14 Jul 2023. Published in: Leibniz International Proceedings in Informatics (LIPIcs), 261 112:1-112:18. ISBN 9783959772785. doi:10.4230/LIPIcs.ICALP.2023.112 ISSN 1868-8969.
|
PDF
LIPIcs-ICALP-2023-112.pdf - Published Version - Requires a PDF viewer. Available under License Creative Commons Attribution 4.0. Download (821Kb) | Preview |
Official URL: https://drops.dagstuhl.de/opus/volltexte/2023/1816...
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.
Item Type: | Conference Item (Paper) | ||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software |
||||||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||||||||
Library of Congress Subject Headings (LCSH): | Arithmetic, Exponents (Algebra), Decision making -- Mathematical models, Logic, Symbolic and mathematical | ||||||||||||
Series Name: | Leibniz International Proceedings in Informatics (LIPIcs) | ||||||||||||
Journal or Publication Title: | Leibniz International Proceedings in Informatics (LIPIcs) | ||||||||||||
Publisher: | Schloss Dagstuhl — Leibniz-Zentrum für Informatik | ||||||||||||
Place of Publication: | Dagstuhl, Germany | ||||||||||||
ISBN: | 9783959772785 | ||||||||||||
ISSN: | 1868-8969 | ||||||||||||
Official Date: | 5 July 2023 | ||||||||||||
Dates: |
|
||||||||||||
Volume: | 261 | ||||||||||||
Page Range: | 112:1-112:18 | ||||||||||||
DOI: | 10.4230/LIPIcs.ICALP.2023.112 | ||||||||||||
Status: | Peer Reviewed | ||||||||||||
Publication Status: | Published | ||||||||||||
Access rights to Published version: | Open Access (Creative Commons) | ||||||||||||
Date of first compliant deposit: | 7 July 2023 | ||||||||||||
Date of first compliant Open Access: | 7 July 2023 | ||||||||||||
RIOXX Funder/Project Grant: |
|
||||||||||||
Conference Paper Type: | Paper | ||||||||||||
Title of Event: | 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) | ||||||||||||
Type of Event: | Conference | ||||||||||||
Location of Event: | Paderborn, Germany | ||||||||||||
Date(s) of Event: | 10-14 Jul 2023 |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year