Presburger Arithmetic: From Automata to Formulas

Presburger arithmetic is the first-order theory of the integers with addition and ordering, but without multiplication. This theory is decidable and the sets it definesadmit several different representations, including formulas, generators, and finiteautomata, the latter being the focus of this thesis. Finite-automata representations of Presburger sets work by encoding numbers as words and sets by automata-defined languages. With this representation, set operations are easily computableas automata operations, and minimized deterministic automata are a canonicalrepresentation of Presburger sets. However, automata-based representations are somewhat opaque and do not allow all operations to be performed efficiently. Anideal situation would be to be able to move easily between formula-based andautomata-based representations but, while building an automaton from a formulais a well understood process, moving the other way is a much more difcult problem that has only attracted attention fairly recently.The main results of this thesis are new algorithms for extracting informationabout Presburger-definable sets represented by finite automata. More precisely, we present algorithms that take as input a finite-automaton representing a Presburgerdefinable set S and compute in polynomial time the affine hull over Qor over Z of the set S, i.e., the smallest set defined by a conjunction of linearequations (and congruence relations in Z) which includes S. Also, we presentan algorithm that takes as input a deterministic finite-automaton representing theinteger elements of a polyhedron P and computes a quantifier-free formula correspondingto this set.The algorithms rely on a very detailed analysis of the scheme used for encodinginteger vectors and this analysis sheds light on some structural properties offinite-automata representing Presburger definable sets.The algorithms presented have been implemented and the results are encouraging: automata with more than 100000 states are handled in seconds.