Contraintes d'ordre et automates d'arbres pour les preuves de terminaison

Non disponible/Not availableLes systèmes de réécriture sont des systèmes de calcul simples et lisibles dont l'expressivité est suffisante pour le codage des programmes ou la spécification de processus automatiques. En exprimant les programmes ou processus sous la forme de systèmes de réécriture, on dispose, en outre, d'outils de vérification puissants basés sur les méthodes de preuve de la réécriture. La terminaison assure l'achèvement des calculs en un temps fini et elle est une prémisse indispensable à d'autres méthodes de preuve telle la preuve par récurrence. Classiquement, la preuve de terminaison d'un système de réécriture utilise la recherche d'un ordre bien fondé assurant la décroissance de chaque étape de réécriture. La recherche manuelle d'un tel ordre n'est envisageable que sur des petits systèmes. C'est pourquoi l'automatisation des preuves de terminaison est un élément crucial pour l'exploitation des outils de preuve de la réécriture sur des programmes ou des processus de taille réelle. Dans cette thèse nous présentons deux approches pour l'automatisation des preuves de terminaison des systèmes de réécriture. Dans la première approche, la recherche de l'ordre de terminaison - une instance de l'ordre général sur les chemins (GPO) - est effectuée a l'aide d'un mécanisme de résolution de contraintes d'ordre (sur des graphes orientés) tendant à rendre la recherche efficace et automatique. La deuxième approche est modulaire ; le système est divisé en sous-systèmes et les preuves de terminaison sont réalisées indépendamment pour chaque sous-système. La terminaison du système complet est assurée, pour une certaine stratégie d'application des sous-systèmes, par un critère basé sur le calcul d'une approximation de l'ensemble des formes normales en utilisant des techniques d'automates d'arbres. D'autres applications de cette approximation sont également présentées, parmi lesquelles la complétude suffisante, le test d'atteignabilité, et la preuve de non-terminaison forte