Presburger Arithmetic: From Automata to Formulas

• Main Author: Latour, Louis
• Other Authors: Gribomont, Pascal
• Format: Others
• Published: Universite de Liege 2005
• Subjects: automata/automate; Presburger Arithmetic/arithmetique de Presburger; integer/entier; affine hull/enveloppe affine
• Online Access: http://bictel.ulg.ac.be/ETD-db/collection/available/ULgetd-05212007-145638/

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 defines admit several different representations, including formulas, generators, and finite automata, 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 computable as automata operations, and minimized deterministic automata are a canonical representation of Presburger sets. However, automata-based representations are somewhat opaque and do not allow all operations to be performed efficiently. An ideal situation would be to be able to move easily between formula-based and automata-based representations but, while building an automaton from a formula is 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 information about Presburger-definable sets represented by finite automata. More precisely, we present algorithms that take as input a finite-automaton representing a Presburger definable set S and compute in polynomial time the affine hull over Q or over Z of the set S, i.e., the smallest set defined by a conjunction of linear equations (and congruence relations in Z) which includes S. Also, we present an algorithm that takes as input a deterministic finite-automaton representing the integer elements of a polyhedron P and computes a quantifier-free formula corresponding to this set. The algorithms rely on a very detailed analysis of the scheme used for encoding integer vectors and this analysis sheds light on some structural properties of finite-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.