Representations and properties of infinite structures
Représentations et propriétés de structures infinies
Résumé
This work is dedicated to the study of infinite structures --- and graphs --- which admit a finite presentation, to the equivalences between those presentations, and to the geometrical and decidability properties of those structures. General families of structures can be described. We concentrate ourselves --- following the approach of Courcelle --- to their definition as solutions of equational systems.
We first introduce a notion of deterministic transducers (top-down with rational lookahead) suitable for infinite trees. This tool allows us to uniformly reason about equational systems.
We then start our study of infinite structures by stack-based structures (Muller and Schupp, Courcelle, Caucal). We pay particular attention to prefix recognizable structures. We generalize Barthelmann's equivalences describing those structures as solutions of equational systems, by transformation of the binary tree and by rewriting of words. We also establish that an extra operator which merges several elements together can be added to the equational systems without changing the family described.
We then study term-automatic structures (Dauchet and Tison, Blumensath and Grädel). We show that a triple equivalence of presentations similar to the case of prefix recognizable structures also holds in this case. In particular, we give a new desription of this family in terms of equational systems. We also briefly present how those result can be translated to the sub-family of automatic structures (Sénizergues, Khoussainov and Nerode).
Finally, we study the graphs described by ground term rewriting (Dauchet and Tison, Löding). We introduce a new family of such graphs. We show that those graphs admit a presentation as solutions of equational systems and that
they have a decidable first-order theory with reachability. We then show that the graphs of this family which are of bounded tree-width are equational. We conclude by showing that an extension of this result to graph of bounded clique-width does not hold.
Ce travail est dédié à l'étude de structures (et de graphes) infinies admettant une représentation finie, aux équivalences entre ces représentations et aux propriétés géométriques et de décidabilité les concernant. Des familles générales de structures peuvent être dégagées, et nous nous attachons, en suivant l'approche de Courcelle, à leur définition en terme de systèmes d'équations.
Nous introduisons tout d'abord la notion de transducteur déterministe (descendant avec anticipation reconnaissable de termes infinis). Cet outil permet un traitement systématique et uniforme des systèmes d'équations.
Nous commençons notre étude par les familles de structures à base de pile (Muller, Schupp, Courcelle, Caucal) et principalement des structures préfixe reconnaissables. Nous généralisons les équivalences de Barthelmann décrivant ces structures comme solutions de systèmes d'équations, par transformations de l'arbre binaire et par récriture de mots. Nous établissons qu'un opérateur sur les structures fusionnant certains éléments de l'univers peut être ajouté à la représentation équationnelle sans changer la famille décrite.
Nous étudions ensuite les structures terme-automatiques (Dauchet et Tison, Blumensath et Grädel). Nous montrons une triple équivalence de représentations pour ces structures, similaires à celles des graphes préfixe reconnaissables. En particulier, nous en donnons une nouvelle caractérisation en terme de système d'équations. Nous précisons aussi comment ces résultats s'adaptent à la sous-famille des graphes automatiques (Sénizergues, Khoussainov, Nerode).
Enfin, nous étudions les graphes décrits par réécriture suffixe de termes (Dauchet et Tison, Löding). Nous introduisons une nouvelle famille de tels graphes. Nous montrons que ces graphes admettent une représentation sous forme de solutions de systèmes d'équations et établissons qu'ils possèdent une théorie au premier ordre avec accessibilité décidable. Nous montrons ensuite que les graphes de cette famille dont la largeur arborescente est bornée sont les graphes équationnels. Nous montrons enfin qu'une extension de ce résultat, précisant que les graphes de cette famille de largeur de clique bornée sont préfixe reconnaissables, n'est pas vérifiée.
Origine : Fichiers produits par l'(les) auteur(s)
