La réécriture de graphes est un cadre formel qui décrit comment des graphes peuvent être transformés en appliquant un ensemble de règles, appelé système de réécriture de graphes. Nous nous intéressons à la preuve automatique de la terminaison de ces systèmes, c'est-à-dire aux techniques permettant de montrer que, pour tout graphe, l'application des règles de transformation d'un système donné ne peut se répéter indéfiniment. Nous contribuons au développement de techniques automatiques d'analyse de la terminaison des systèmes de réécriture de graphes avec double pushout (DPO), en proposant quatre apports.

Premièrement, nous étendons une technique existante, reposant sur des graphes de type. Cette méthode attribue des poids à des morphismes ciblant un graphe de type; le poids d'un graphe sujet à transformation est défini comme la somme des poids de tous les morphismes depuis ce graphe vers le graphe de type. La terminaison est alors établie en montrant que le poids du graphe diminue strictement à chaque application d'une règle de transformation, à condition que l'ensemble des poids soit bien fondé. Exiger que les poids soient bien fondés peut, cependant, se révéler limitant en pratique, car la recherche d'un graphe de type adapté est extrêmement difficile. Notre extension rend cette recherche beaucoup plus facile en autorisant des poids issus d'ensembles non bien fondés.

Deuxièmement, nous développons une nouvelle condition suffisante, appelée comptage de morphismes. Cette méthode s'applique aux systèmes de réécriture de graphes avec DPO à règles injectives sur des multigraphes orientés dont les arêtes sont étiquetées. Elle repose sur l'idée que la réécriture ne peut pas durer indéfiniment si le nombre de morphismes ayant un sous-graphe donné comme domaine diminue strictement à chaque transformation.

Troisièmement, nous étendons notre méthode de comptage de morphismes pour une analyse plus fine. Plus particulièrement, nous considérons les morphismes ayant un sous-graphe spécifique comme domaine et dont l'image n'est pas incluse dans un contexte interdit.

Nous mettons enfin en œuvre ces techniques en les implantant au sein d'un nouvel outil logiciel : LyonParallel. Dédié à la transformation avec DPO des multigraphes orientés étiquetés sur les arêtes, cet outil permet d'exhiber automatiquement la terminaison d'exemples que les approches antérieures ne pouvaient pas traiter.