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.
| Identifer | oai:union.ndltd.org:BICfB/oai:ETDULg:ULgetd-05212007-145638 |
| Date | 29 November 2005 |
| Creators | Latour, Louis |
| Contributors | Gribomont, Pascal, Boigelot, Bernard, Wolper, Pierre, Rigo, Michel, Pecheur, Ch., Finkel, A, Müller-Olm, M |
| Publisher | Universite de Liege |
| Source Sets | Bibliothèque interuniversitaire de la Communauté française de Belgique |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | http://bictel.ulg.ac.be/ETD-db/collection/available/ULgetd-05212007-145638/ |
| Rights | unrestricted, Je certifie avoir complété et signé le contrat BICTEL/e remis par le gestionnaire facultaire. |
Page generated in 0.0017 seconds