Return to search

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 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.

Identiferoai:union.ndltd.org:BICfB/oai:ETDULg:ULgetd-05212007-145638
Date29 November 2005
CreatorsLatour, Louis
ContributorsGribomont, Pascal, Boigelot, Bernard, Wolper, Pierre, Rigo, Michel, Pecheur, Ch., Finkel, A, Müller-Olm, M
PublisherUniversite de Liege
Source SetsBibliothèque interuniversitaire de la Communauté française de Belgique
Detected LanguageEnglish
Typetext
Formatapplication/pdf
Sourcehttp://bictel.ulg.ac.be/ETD-db/collection/available/ULgetd-05212007-145638/
Rightsunrestricted, Je certifie avoir complété et signé le contrat BICTEL/e remis par le gestionnaire facultaire.

Page generated in 0.0015 seconds