Technical Report No. 186 - Abstract

Felix Klaedtke
On the Automata Size for Presburger Arithmetic

We prove that the number of states of the minimal automaton for a Presburger arithmetic formula is triple exponentially bounded in the length of the formula and we show that this triple exponential bound is tight. Furthermore, we improve the automata constructions for linear (in)equations found in the literature and show that our constructions are optimal.