Résumé de rapport du LIF

Téléchargement / Download : pdf 164k , ps.gz 164k , bibtex

Abstract

Following Semenov, Muchnik [Muc03] solves the problem of deciding whether an automaton working on the representation of tuples of numbers in some basis is definable in Presburger arithmetic, or equivalently is a semilinear set. His solution yields a formula characterizing the semilinear sets, that can be decided in elementary time if dynamic programming techniques are used. But there is no easy way to extract from this formula the representation of semilinear sets with bases and periods, which is useful in applications to program verification. We give a solution to this problem when the semilinear sets corresponds to a conjunction of equalities, inequalities and moduli equations which corresponds to semilinears sets that have the same periods. Our approach relies on a logical characterization of these sets and yields doubly exponential bounds.

Keywords

Automata, Presburger Arithmetic, Semilinear Set.

Résumé

Après Semenov, Muchnik [Muc03] résoud le problème de décider si le langage reconnu par un automate qui fonctionne sur les représentations (dans une certaine base) de n-uplet d'entiers est définissable dans l'arithmétique de Presburger, ou de manière équivalente si c'est un ensemble semilinéaire. Sa solution donne une formule logique qui caractérise les ensembles semilinéaires, qui peut être décidée en temps élémentaire si on utilise la programmation dynamique. Mais il n'y a pas de technique simple permettant d'extraire de la formule la représentation des semilinéaires sous la forme base et périodes, ce qui est utile dans certaines applications pour la vérification de programmes. Nous donnons une solution à ce problème quand les semilinéaires correspondent à une conjonction d'égalités, d'inégalités et d'équations modulo, ce qui correspond à des semilinéaires qui ont les mêmes périodes. Notre solution utilise une caractérisation logique de ces semilinéaires et donne une borne doublement exponentielle.

Mots clés

Automates, Arithmétique de Presburger, Ensembles Semilinéaires.

Bibtex

@TECHREPORT{21-2004,
    AUTHOR	= {Denis Lugiez},
    TITLE	= {{From Automata to Semilinear Sets: a  Solution for Polyhedra and Even More General  Sets}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {21-2004},
    MONTH	= {april},
    YEAR	= {2004},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/21-2004.html},
}