Bounds on the automata size for Presburger arithmetic

Automata provide a decision procedure for Presburger arithmetic. However, until now only crude lower and upper bounds were known on the sizes of the automata produced by the automata-based approach for Presburger arithmetic. In this article, we give an upper bound on the number of states of the minimal deterministic automaton for a Presburger arithmetic formula. This bound depends on the length of the formula and the quantifiers occurring in it. We establish the upper bound by comparing the automata for Presburger arithmetic formulas with the formulas produced by a quantifier-elimination method. We show that our bound is tight, also for nondeterministic automata. Moreover, we provide automata constructions for atomic formulas and establish lower bounds for the automata for linear equations and inequations.