Abstract FR:

Cette thèse s'inscrit dans l'étude de familles de graphes infinis de présentation finie, de leurs propriétés structurelles, ainsi que des comparaisons entre ces familles. Après un survol du domaine, nous nous intéressons à trois problèmes. Premièrement, nous définissons trois familles de systèmes de réécriture de termes dont nous démontrons que la relation de dérivation peut être représentée de façon finie. Il en découle plusieurs questions sur les familles de graphes infinis correspondantes. Dans un second temps, nous étudions deux familles de graphes dont les traces sont les langages contextuels, à savoir les graphes rationnels et les graphes linéairement bornés. Nous nous intéressons en particulier au cas des langages contextuels déterministes, ainsi qu'à la comparaison structurelle de ces deux familles. Enfin, d'un point de vue plus proche de la vérification, nous proposons un algorithme de calcul des prédécesseurs pour une famille d'automates à pile d'ordre supérieur.