Cet article étudie les réseaux de neurones graphes (GNN), un modèle d'apprentissage automatique qui traite des données structurées en graphes. Plus précisément, nous proposons un nouveau mécanisme de terminaison pour résoudre le problème de terminaison garantie des GNN récurrents. Les GNN récurrents existants présentent le problème de fournir la taille du graphe au modèle ou de ne pas garantir la terminaison. Dans cet article, nous proposons et prouvons un modèle de terminaison capable de représenter tous les classificateurs de nœuds définis par le mu-calcul modal gradué, même dans une variante standard de GNN qui ignore la taille du graphe. Pour y parvenir, nous développons une nouvelle sémantique d'approximation pour le mu-calcul gradué et, sur cette base, proposons un nouvel algorithme de vérification de modèle (algorithme de comptage) qui ne prend pas en compte la taille du graphe. Enfin, nous démontrons que l'algorithme de comptage peut être implémenté dans un GNN récurrent terminal.
