On Halting vs Converging in Recurrent Graph Neural Networks

TL;DR

This paper analyzes the expressiveness of various Recurrent Graph Neural Network models, establishing their relationships and showing that certain models can express complex logical properties even with convergence constraints.

Contribution

It formally compares the expressiveness of converging, output-converging, and halting RGNNs, proving their equivalences and differences in logical expressiveness, and introduces a coordination protocol for asynchronous halting.

Findings

Converging RGNNs are as expressive as graded-bisimulation-invariant halting RGNNs.

Output-converging RGNNs are at least as expressive as converging RGNNs.

RGNNs can express the full $ ext{μGML}$ logic even under convergence constraints.

Abstract

Recurrent Graph Neural Networks (RGNNs) extend standard GNNs by iterating message-passing until some stopping condition is met. Various RGNN models have been proposed in the literature. In this paper, we study three such models: converging RGNNs, where all vertex representations must stabilise; output-converging RGNNs, where only the output classifications must stabilise; and halting RGNNs, where a per-vertex halting classifier determines when to stop. We establish expressiveness relationships between these models: over undirected graphs, converging RGNNs are equally expressive as graded-bisimulation-invariant halting RGNNs, while output-converging RGNNs are at least as expressive. Combined with prior results on halting RGNNs, this shows that, relative to the classifiers expressible in monadic second-order logic (MSO), converging RGNNs express exactly the graded modal $\mu$-calculus ($\mu$GML), and output-converging RGNNs express at least $\mu$GML. These results hold even when restricting to ReLU networks with sum aggregation. The main technical challenge is simulating halting RGNNs by converging ones: without a global halting classifier, vertices may locally decide to halt at different times, causing desynchronisation. We develop a "traffic-light" protocol that enables vertices to coordinate despite this asynchrony. Our results answer an open question from Bollen et al. (2025) and show that the RGNN model of Pflueger et al. (2024) retains full $\mu$GML expressiveness even when convergence is guaranteed.