Speakers
Description
Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti
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 P for the powers of 2.
The latter theory, denoted as PA(Pow), was introduced by Buchi as a
first attempt at characterising the sets of tuples of numbers that
can be expressed using finite automata; Buchi's method does not give
an elementary upper bound, and the complexity of this theory has been
open. The former theory, denoted as PA(Exp), was shown decidable by
Semenov; while the decision procedure for this theory differs
radically from the automata-based method proposed by Buchi, the 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 Buchi's approaches yield non-elementary blow-ups for PA(Pow),
the theory is in fact decidable in triply exponential time,
similar to the best known quantifier-elimination algorithm for PA.
We also provide a NEXPTIME upper bound for the existential fragment of
PA(Exp), a step towards a finer-grained analysis of its complexity.
Both these results are established by analysing a single parameterized
satisfiability algorithm for PA(Exp), which can be specialized to either
the setting of PA(Pow) or the existential theory of PA(Exp).
Besides the new upper bounds for the existential theory of PA(Exp) and
PA(Pow), we believe our algorithm provides new intuition for the decidability
of these theories, and for the features that lead to non-elementary blow-ups.