Structural Presburger-definable Digit Vector Automata

Les automates finis permettent de représenter symboliquement des ensembles infinis de vecteurs d'entiers décomposés comme des mots de vecteurs de chiffres. On montre que l'automate minimal représentant un ensemble Presburger-définissable est structurellement Presburger-définissable: c'est à dire, que les automates obtenus en changeant l'état initial et les états finaux représentent des ensembles Presburger-définissables./ Digit Vector Automata (DVA) provide a natural symbolic representation for regular sets of integer vectors encoded as strings of digit vectors (least significant digit first). We prove that the minimal DVA that represents a Presburger-definable set is structurally Presburger-definable: that means, the DVA obtained by modifying the initial state and the set of final states represents a Presburger-definable set