Université de Liège Réseau des Bibliothèques

BICTEL/e - ULg
Serveur institutionnel des thèses de doctorat



Nouvelles thèses
dans BICTEL/e - ULg
  • Wislez, Arnaud - Molecular interactions of bioadhesive-inspired species with inorganic surfaces/Interactions moléculaires de composés bio-inspirés avec des surfaces inorganiques
  • Esser, Céline - Regularity of functions: Genericity and multifractal analysis
  • Dupont, Josselin - "L’émergence d’une politique foncière régionale en Bretagne : de l’identification des enjeux à la création d’un Etablissement public foncier d’Etat/The emergence of a regional land policy in Brittany: from issues identification to the creation of a State Établissement public foncier".
Présentation Recherche thèse Dépôt thèse Accès
gestionnaires
 
Page de résumé pour ULgetd-05212007-145638

Auteur : Latour, Louis
E-mail de l'auteur : Louis.Latour@gmail.com
URN : ULgetd-05212007-145638
Langue : Anglais/English
Titre : Presburger Arithmetic: From Automata to Formulas
Intitulé du diplôme : Doctorat en sciences de l'ingénieur
Département : FSA - Département d'électricité, électronique et informatique
Jury :
Nom : Titre :
Finkel, A Membre du jury/Committee Member
Müller-Olm, M Membre du jury/Committee Member
Pecheur, Ch. Membre du jury/Committee Member
Rigo, Michel Membre du jury/Committee Member
Gribomont, Pascal Président du jury/Committee Chair
Boigelot, Bernard Promoteur/Director
Wolper, Pierre Promoteur/Director
Mots-clés :
  • automata/automate
  • Presburger Arithmetic/arithmetique de Presburger
  • integer/entier
  • affine hull/enveloppe affine
Date de soutenance : 2005-11-29
Type d'accès : Public/Internet
Résumé :

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.

Autre version :
Fichiers :
Nom du fichier Taille Temps de chargement évalué (HH:MI:SS)
Modem 56K ADSL
[Public/Internet] thesis_louis_latour.pdf 1.43 Mb 00:03:23 00:00:07

Bien que le maximum ait été fait pour que les droits des ayants-droits soient respectés, si un de ceux-ci constatait qu'une oeuvre sur laquelle il a des droits a été utilisée dans BICTEL/e ULg sans son autorisation explicite, il est invité à prendre contact le plus rapidement possible avec la Direction du Réseau des Bibliothèques.


Parcourir BICTEL/e par Auteur|Département | Rechercher dans BICTEL/e


© Réseau des Bibliothèques de l'ULg, Grande traverse, 12 B37 4000 LIEGE