On Halting vs Converging in Recurrent Graph Neural Networks Jeroen Bollen , Stijn Vansummeren , Hasselt University [email protected], [email protected]
arXiv:2604.25551v1 [cs.LG] 28 Apr 2026
Abstract
refer to GNNs, we mean AC-GNNs. A natural question is: what can these networks compute? The expressiveness of a GNN architecture refers to the class of vertex classifiers it can express. Understanding expressiveness reveals fundamental capabilities and limitations of an architecture, and provides a basis for comparing different architectures. A fundamental property of AC-GNNs is their invariance under graded bisimulation (Morris et al. 2019; Xu et al. 2019), which has enabled a productive line of research characterising GNN expressiveness through modal logics.
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 µ-calculus (µGML), and output-converging RGNNs express at least µ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 “trafficlight” 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 µGML expressiveness even when convergence is guaranteed.
For fixed-depth GNNs, this expressiveness is well understood. Barceló et al. (2020) showed that the classifiers expressible by both fixed-depth GNNs and firstorder logic are precisely those definable in graded modal logic. For recurrent GNNs (RGNNs), which repeatedly apply a single layer to produce a sequence of increasingly refined feature vectors, the expressiveness is less understood, and is tightly linked to the question of how and especially when should the output be read. In this paper, we study three output semantics inspired by existing work and study their relative expressiveness: converging RGNNs, where the entire feature vector of every vertex must stabilise (Scarselli et al. 2009) (Definition 6); output-converging RGNNs, where only the classification must stabilise (Pflueger, Tena Cucala, and Kostylev 2024) (Definition 7); and halting RGNNs, where an explicit halting classifier determines when to stop (Bollen et al. 2025) (Definition 8). Our formalisations differ from these references in some respects; we give precise definitions in Section 3 and discuss the differences. Our main result is that, over undirected graphs, converging RGNNs have exactly the same expressive power as gradedbisimulation-invariant halting RGNNs (Theorem 1). This resolves an open question posed by Bollen et al. (2025), who asked whether it is possible to achieve fully convergent termination.
1 Introduction Graph Neural Networks (GNNs) are a class of machine-learning models operating on graphs. The most common GNN architecture is the aggregatecombine GNN (AC-GNN) (Gilmer et al. 2017; Hamilton 2020). In each layer of an AC-GNN, every vertex first aggregates the feature vectors of its neighbours into a single summary, and then combines this summary with its own feature vector to produce an updated feature vector. This simple message-passing scheme underlies most practical AC-GNN variants, including Graph Convolutional Networks (Kipf and Welling 2017), GraphSAGE (Hamilton, Ying, and Leskovec 2017), Graph Isomorphism Networks (Xu et al. 2019), and Principal Neighbourhood Aggregation (Corso et al. 2020). Throughout this paper, when we
The equivalence follows from two constructions that simulate one model with the other (Propositions 2 and 3). The halting-to-converging direction proves especially challenging: in a halting RGNN, the computation stops only when all vertices satisfy the halting classifier simultaneously, providing a global synchronisation mechanism. A converging RGNN has no 1
such mechanism, so vertices must coordinate among themselves when to stop. We solve this using a local coordination scheme detailed in Section 6. We also consider “simple” RGNNs, which use only standard neural network components; the converging-tohalting construction works even for simple RGNNs, while the halting-to-converging construction requires mild restrictions on the halting RGNN.
G, and define the neighbourhood of v as nbrG (v) := {u ∈ V | (v, u) ∈ E}. We write G[X] for the set of all finite undirected X-labelled graphs. Vertex Label Transformers. Our primary objects of study are functions that transform the labels of a graph while preserving its structure. Definition 1 (Label transformer). A label transformer from X to Y is a function f : G[X] → G[Y ] that, given an X-labelled graph G = (V, E, λ1 ), produces a Y -labelled graph f (G) = (V, E, λ2 ) . In other words, f preserves the vertex set and edge relation of the input graph, modifying only the vertex labels.
Since every converging RGNN is trivially also an output-converging RGNN, our equivalence implies that output-converging RGNNs are at least as expressive as graded-bisimulation-invariant halting RGNNs. Combined with a recent result of Bollen et al. (2025), we obtain that every vertex classifier definable in the graded modal µ-calculus (µGML) is expressible by a simple converging RGNN, and hence also by a simple output-converging RGNN. In the converse direction, converging and output-converging RGNNs are both invariant under graded bisimulation. Colcombet et al. (2025) recently proved the finitary JaninWalukiewicz theorem for standard bisimulation; if this extends to graded bisimulation, it follows that every MSO-definable classifier expressible by a converging or output-converging RGNN is also expressible in µGML. Ahvonen et al. (2025) claim this characterisation in a preprint, proceeding via distributed messagepassing automata; their work also relies on this extension, has not yet been published, and does not establish the characterisation for simple RGNNs. Our main contribution, the structural equivalence (Theorem 1), is independent of this open question.
Given a function h : X → Y , its lifting h↑ : G[X] → G[Y ] is the label transformer h↑ (G) = (V, E, h ◦ λ) that applies h to each vertex label of G. Definition 2 (Vertex classifier). A vertex classifier on X is a label transformer f : G[X] → G[B]. Vertex classifiers are the central notion of expressiveness for GNNs: we say that a GNN expresses a vertex classifier f if, on every input graph G, the GNN produces the same Boolean labelling as f . For a finite label set X, write E for the edge relation and, for each q ∈ X, write Pq for the set of vertices with label q. A monadic second-order logic (MSO) formula φ(x) with one free vertex variable, or a µGML formula φ, over these predicates defines a vertex classifier on X, where vertex v is classified as true precisely when G |= φ(v). We say a vertex classifier is MSO-definable, respectively definable in µGML, if it is defined by such a formula.
Section 2 introduces notation and AC-layers. Section 3 defines recurrent GNNs and their three output semantics. Section 4 states the main results. Sections 5 and 6 prove the two directions of Theorem 1. Section 7 discusses related work, and Section 8 discusses limitations and open questions.
GNN Layers. The basic computational unit of a graph neural network is the aggregate-combine layer, which updates vertex labels by combining each vertex’s current label with an aggregated summary of its neighbours’ labels. Definition 3 (Aggregate-combine layer). An aggregate-combine layer (AC-layer) of input dimension p and output dimension q is a label transformer L : G[Rp ] → G[Rq ] of the form ( L(G)(v) = CMB G(v), ( )) AGG {{G(u) | u ∈ nbrG (v)}} ,
2 Preliminaries We denote the booleans, natural numbers including zero, and real numbers by B, N, and R, respectively. For the booleans B = {0, 1}, we interpret 0 as false and 1 as true. Given a set X, we write |X| for its cardinality. A finite multiset over a set X is a function M : X → N with support supp(M ) := {x ∈ X | M (x) > 0}. Intuitively, M (x) denotes the multiplicity of x in M . We use double curly braces {{...}} to denote multisets.
(1) where AGG : M(R ) → R is its aggregation function and CMB : Rp × Rp → Rq is its combination function. p
We denote the concatenation of two vectors x and y by x|y. We write [x]i for the i-th component of a vector x. ∑d The L1 norm of a vector x ∈ Rd is ∥x∥1 = i=1 |[x]i |.
p
While in their full generality, the AGG and CMB functions of an AC-layer can be arbitrary, in practice they are often instantiated to be of the following simple form. A function f : Rp → Rq is called simple if it is expressible as a feedforward neural network with ReLU activations, i.e., if f is of the form Aℓ ◦ ReLU ◦ Aℓ−1 ◦ · · · ◦ ReLU ◦ A1 , with each Ai an affine transformation and [ReLU(x)]i = max(0, [x]i ). A simple aggregation function ∑ is the summation of its inputs, i.e., AGG(M ) = x∈supp(M ) M (x) · x. A simple combination function is one of the form CMB(x, y) = f (x | y)
Graphs. A labelled graph over a set of labels X is a triple G = (V, E, λ) where V is a finite set of vertices, E ⊆ V × V is the edge relation, and λ : V → X is the vertex labelling function. We say G is undirected if E is symmetric. Throughout, we will always assume graphs are undirected. We write G(v) for the label of vertex v in 2
for some simple function f : R2p → Rq . A simple AClayer is an AC-layer whose aggregation function is a simple aggregation function and whose combination function is a simple combination function.
simple if the underlying RGNN is simple. A halting RGNN is simple if the underlying RGNN is simple and its halting classifier is a simple classifier. Converging RGNNs are inspired by the model of Scarselli et al. (2009), who required the update function to be a contraction mapping. By the Banach fixed-point theorem, iterating a contraction guarantees asymptotic convergence to a unique fixed point, but the fixed point need not be reached in finitely many steps. In practice, Scarselli et al. stop when the change between successive iterations falls below a threshold, which corresponds to a halting RGNN in our framework. Our converging RGNNs instead require exact stabilisation in finitely many steps, without imposing the contraction condition.
3 Recurrent Graph Neural Networks A recurrent GNN iterates a single AC-layer, producing a sequence of feature graphs. Definition 4 (Recurrent GNN). A recurrent graph neural network (RGNN) over a label set X is a tuple R = (In, L, Out) where: • In : X → Rd is the initialisation function; • L : G[Rd ] → G[Rd ] is an AC-layer, called the update function; and
Output-converging RGNNs are inspired by the model of Pflueger et al. (2024), who define the output of a vertex to be the stabilised classification if one exists, and false otherwise. Their semantics assigns an output to every vertex on every graph, but their constructions do not guarantee that stabilisation occurs. We require that output-convergence is guaranteed for all inputs.
• Out : R → B is the readout function. d
We call d the dimension of R. Definition 5 (Run). The infinite run of an RGNN R = (In, L, Out) on an input graph G ∈ G[X] is the sequence H0 , H1 , . . . of Rd -labelled graphs where H0 = In↑ (G) and Hi+1 = L(Hi ) for all i ≥ 0. A run is any finite prefix H0 , . . . , Hk of the infinite run. The output of a run H0 , . . . , Hk is the B-labelled graph Out↑ (Hk ).
Halting RGNNs correspond to the model introduced by Bollen et al. (2025). Their notion of simplicity differs slightly from ours: they require the halting classifier to be a projection Hlt(x) = 1 iff [x]i > 0 for some fixed index i, whereas we allow any simple function with a ≥ 0 threshold. Since their constructions produce feature vectors where the halting and readout components are boolean, the strict inequality [x]i > 0 is equivalent to [x]i − 21 ≥ 0, which fits our definition.
Different output semantics yield different architectures with different expressiveness. Throughout the following definitions, let R = (In, L, Out) be a fixed RGNN of dimension d. Definition 6 (Converging RGNN). A run H0 , . . . , Hk converges if L(Hk ) = Hk . A converging RGNN is an RGNN such that for every input graph, some run converges. The output on input G is C(G) := Out↑ (Hk ),
Graded Bisimulation. Graded bisimulation is a notion of structural equivalence for graphs that respects neighbourhood multiplicities. It characterises the distinguishing power of GNNs: two pointed graphs are indistinguishable by any GNN if and only if they are graded bisimilar (Grohe (2021)). Definition 9 (Graded bisimulation). Let G and H be X-labelled graphs. A relation Z ⊆ VG × VH is a graded bisimulation between G and H if for every (u, v) ∈ Z:
(2)
where H0 , . . . , Hk is any converging run. Note that all converging runs on the same input yield the same output. Definition 7 (Output-converging RGNN). An infinite run H0 , H1 , . . . output-converges if there exists k ∈ N such that Out↑ (Hi ) = Out↑ (Hk ) for all i ≥ k. An output-converging RGNN is an RGNN such that for every input graph, the infinite run output-converges. The output on input G is O(G) := Out↑ (Hk ).
1. G(u) = H(v); and
(3)
2. there exists a bijection f : nbrG (u) → nbrH (v) such that (w, f (w)) ∈ Z for every w ∈ nbrG (u).
Definition 8 (Halting RGNN). A run H0 , . . . , Hk is complete under halting classifier Hlt : Rd → B if k is the smallest index at which Hlt(Hk (v)) = 1 for every vertex v. A halting RGNN is a pair H = (R, Hlt) such that for every input graph, a complete run exists. The output on input G is H(G) := Out↑ (Hk ),
A graded bisimulation is total if its domain is the entire vertex set of the first graph G, and surjective if its range is the entire vertex set of the second graph H.
(4)
The bijection requirement in condition (2) ensures that neighbours are matched one-to-one, preserving multiplicities. In ordinary bisimulation, multiple neighbours can be matched to the same neighbour, ignoring multiplicities. Definition 10 (Invariance under graded-bisimulation). A label transformer f : G[X] → G[Y ] is invariant under graded-bisimulation if for every pair of X-labelled
where H0 , . . . , Hk is the complete run. A simple classifier is a function c : Rd → B for which there exists a simple function f : Rd → R such that c(x) = 1 iff f (x) ≥ 0. We say an RGNN is simple if its update function is a simple AC-layer and its readout function is a simple classifier. A converging RGNN is 3
graphs G and H and every graded-bisimulation Z between G and H, the relation Z is also a gradedbisimulation between f (G) and f (H). Proposition 1. Every vertex classifier definable by a converging RGNN or an output-converging RGNN is invariant under graded bisimulation. Every vertex classifier definable by a halting RGNN is invariant under total surjective graded bisimulations.
iterations i of every run; and 3. there exists B ≥ 0 such that |[Hi+1 (v)]j − [Hi (v)]j | ≤ B for all feature vector components j, vertices v, and iterations i of every run. We refer to the second condition as the range condition and the third condition as the bounded-change condition. Bollen et al. (2025) showed that every µGML formula is expressible by a graded-bisimulation-invariant simple halting RGNN whose halting classifier satisfies the range condition of Proposition 3. Their constructions have per-component changes in {−1, 0, 1}, so the bounded-change condition is satisfied with B = 1. Combined with Proposition 3, we obtain: Corollary 1. Every vertex classifier definable in µGML is expressible by a simple converging RGNN, and hence also by a simple output-converging RGNN.
Proof. Every AC-layer preserves gradedbisimulations, as does every lifted function, and any composition thereof. As runs of RGNNs are precisely such compositions, a graded-bisimulation between input graphs remains one after any number of iterations. For converging RGNNs, this implies that gradedbisimilar vertices converge at the same iteration with equal labels: if one has stabilised, so has the other. The output-converging case was proven by Pflueger et al. (2024).
For the converse direction, converging RGNNs and output-converging RGNNs are both invariant under graded bisimulation as per Proposition 1. Colcombet et al. (2025) recently proved the finitary Janin-Walukiewicz theorem (Janin and Lenzi 2001; Walukiewicz 2002): over finite graphs, bisimulationinvariant MSO formulas are expressible in the µcalculus. Whether this result extends to graded bisimulation is, to our knowledge, open; if it does, every MSO-definable vertex classifier expressible by a converging or output-converging RGNN is also expressible in µGML.
For halting RGNNs, the situation is more delicate. Halting depends on a global condition: all vertices must satisfy the halting classifier. Totality and surjectivity ensure that if all vertices halt in one graph, so do all vertices in the other. The full proof is given by Bollen et al. (2025). Clearly, invariance under graded bisimulation implies invariance under total-surjective graded bisimulation, but the converse is not true. Consequently, any vertex classifier that is definable by a halting RGNN and that is only invariant under total surjective graded bisimulation, but not under graded bisimulation, cannot equivalently be defined by a (output-) converging RGNN. Therefore, in the following we necessarily compare converging RGNNs with halting RGNNs on the class of vertex classifiers that are invariant under graded bisimulation.
5 From Converging to Halting We begin with the simpler direction: every converging RGNN can be simulated by a halting RGNN. Proof of Proposition 2. Let C = (In, L, Out) be a converging RGNN of dimension d, and let H0 , H1 , . . . denote the infinite run of C on an input graph G. Since C converges, there exists some k ∈ N such that Hk−1 = Hk .
4 Main Results Our main contribution is establishing the equivalence between converging RGNNs and graded-bisimulationinvariant halting RGNNs. Theorem 1. Over undirected graphs, converging RGNNs and graded-bisimulation-invariant halting RGNNs express exactly the same vertex classifiers.
The idea is to construct a halting RGNN H whose run H0′ , H1′ , . . . satisfies Hi′ (v) = Hi (v) | Hi−1 (v) for all i ≥ 1. By storing both the current and previous feature vectors, each vertex can locally detect whether its feature has stabilised. When Hk−1 = Hk , all vertices will simultaneously detect stabilisation, triggering the system to halt.
This theorem follows from two constructions, detailed in Sections 5 and 6: Proposition 2. For every converging RGNN C, there exists a halting RGNN H such that C(G) = H(G) for all graphs G. If C is simple, then so is H. Proposition 3. For every graded-bisimulationinvariant halting RGNN H, there exists a converging RGNN C such that H(G) = C(G) for all undirected graphs G. Furthermore, if H satisfies the following conditions, then C is simple:
We construct H = ((In′ , L′ , Out′ ), Hlt) of dimension 2d as follows: • In′ (x) := In(x) | (In(x) + 1d ), where 1d ∈ Rd is the all-ones vector. This ensures the two components are initially distinct, so no vertex signals halting before the first iteration.
1. H is simple;
• L′ is an AC-layer that, given a feature vector y|y ′ ∈ R2d , computes L(y) | y.
2. the simple function f defining H’s halting classifier satisfies f (Hi (v)) ∈ {−1, 1} for all vertices v and
• Hlt(y | y ′ ) := 1 iff h(y | y ′ ) ≥ 0, where h(y | y ′ ) := −∥y − y ′ ∥1 . 4
• Out′ (y | y ′ ) := Out(y).
vertices satisfy the halting classifier, at which point the entire system halts all at once. In a converging RGNN, vertices cannot simply keep computing while waiting for the system to halt: the act of continuing the computation prevents the feature vectors from stabilising, which is precisely the condition required for convergence.
We verify that L′ is indeed an AC-layer. Since L has aggregation function AGG and combination function CMB, we define: ′
AGG′ (M ) := AGG(π1 (M )) | 0d ,
(5)
′
(6)
′
CMB ((y | y ), (a | a )) := CMB(y, a) | y,
A natural strategy is to have each vertex step through H’s halting states one at a time. A vertex pauses at Hi once it locally satisfies the halting classifier, and resumes when it discovers that a neighbour is already simulating Hi+1 . This causes vertices to desynchronise: different vertices may be simulating different halting states at the same time. The difficulty is that to advance, a vertex needs its neighbours’ snapshots from the halting state it is currently simulating, but a neighbour that has already advanced no longer holds that snapshot.
where π1 (M ) denotes the multiset obtained by projecting each element of M onto its first d components. By construction, the run H0′ , H1′ , . . . of H on G satisfies Hi′ (v) = Hi (v) | Hi−1 (v) for all i ≥ 1 and all vertices v. At iteration k, every vertex v has Hk′ (v) = Hk (v) | Hk−1 (v), and since Hk−1 = Hk , we have h(Hk′ (v)) = −∥Hk (v) − Hk−1 (v)∥1 = 0 ≥ 0, so all vertices satisfy the halting condition. Thus H halts, and the outputs agree: H(G) = Out′↑ (Hk′ ) = Out↑ (Hk ) = C(G).
(7)
We solve this by having each vertex advertise its previous snapshot when it advances, so that neighbours who stayed behind can catch up. However, neighbours that advanced simultaneously receive this previous snapshot too, even though they no longer need it. Each vertex therefore signals both which halting state it is currently simulating and which halting state its advertised snapshot represents. This enables two things:
Now suppose C is simple. The construction above does not preserve simplicity, since AGG′ involves projection rather than plain summation. We give an alternative construction of L′ that preserves simplicity. Since AGG is summation over Rd , we define AGG′ to be summation over R2d . Since summation distributes over concatenation, the first d components of the result equal AGG(π1 (M )); the remaining components are ignored by CMB′ . We define ′
′
′
CMB ((y | y ), (a | a )) := f (y | a) | y,
• A vertex can detect when a neighbour has moved ahead, triggering it to catch up.
(8)
• A vertex can determine whether a neighbour’s advertised snapshot is the one it needs or an outdated one.
where f is the simple function such that CMB(y, a) = f (y | a). This layer computes the same function as the general construction. Now AGG′ is summation, hence simple, and CMB′ is simple since it selects y and a from the input via an affine transformation, applies f , and concatenates y. The function h(y | ∑d y ′ ) = −∥y − y ′ ∥1 = − i=1 |[y]i − [y ′ ]i | is simple, since |z| = ReLU(z) + ReLU(−z). If Out is a simple classifier, then so is Out′ .
To make this precise, we first introduce a formal notion of which halting state each vertex is simulating.
6.2 Correspondence To relate the converging run to the halting run, we introduce a correspondence: a function that maps, for each converging state, each vertex to a halting state. Definition 11 (Correspondence). A correspondence between these runs is a function Φ : V × N → {0, . . . , k} satisfying, for all vertices v and all j ≥ 0:
6 From Halting to Converging The converse direction is more challenging. Given a graded-bisimulation-invariant halting RGNN H, we must construct a converging RGNN C that computes the same classifier.
Φ(v, j + 1) ∈ {Φ(v, j), Φ(v, j) + 1}.
Throughout this section, let H be a halting RGNN with complete run H0 , . . . , Hk on input graph G, where k is the index at which the run completes, and let C0 , C1 , . . . be the infinite run of a converging RGNN C on the same input. We refer to each graph Hi in the halting run as a halting state, and each graph Cj in the converging run as a converging state. A vertex’s feature vector in a halting state, Hi (v), is called a snapshot, and a vertex’s feature vector in a converging state, Cj (v), is called a configuration.
(9)
Given a converging state Cj , we say that vertex v is simulating halting state HΦ(v,j) . The monotonicity condition ensures that vertices only move forward through the halting run, advancing by at most one halting state per converging step. Given a correspondence Φ, we say vertex v is behind at converging state Cj if there exists a neighbour u with Φ(u, j) > Φ(v, j). A vertex is eager at Cj if it is behind or if Hlt(HΦ(v,j) (v)) = 0. A vertex is aligned at Cj when it receives from each neighbour the information about HΦ(v,j) needed to advance. We will construct C so that a vertex advances precisely when it is both eager and aligned. Lemma 6 will show that these properties can be tested locally.
6.1 The Synchronisation Problem The difficulty lies in coordination. In a halting RGNN, vertices can continue computing indefinitely until all 5
6.3 Configurations
6.5 Construction
Assume that H has dimension d. Each configuration Cj (v) ∈ R2d+6 has the form: ( ) m Cj (v) = κcj (v), τjc (v), κm (10) j (v), τj (v) ,
We construct C = (In′ , L′ , Out′ ) as follows. The initialisation function sets both snapshots to the initial halting state and both traffic lights to enc3 (0): In′ (x) := (In(x), enc3 (0), In(x), enc3 (0)) .
d where κcj (v), κm j (v) ∈ R are the current and advertised snapshot respectively, and τjc (v), τjm (v) ∈ R3 are the current and advertised traffic light, defined next.
The update function L is an AC-layer with aggregation function AGG′ and combination function CMB′ . The aggregation function AGG′ applies H’s aggregation to each snapshot component independently and summation to each traffic light component. If H is simple, this reduces to summation over the full configuration.
The advertised components store information transmitted to neighbours; the traffic lights, defined next, encode which halting state a vertex is simulating, allowing neighbours to determine their relative positions in the halting run. Definition 12 (Traffic light). A traffic light is an element of T := {(1, 0, 0), (0, 1, 0), (0, 0, 1)}.
(12)
′
Since Coherence 4 guarantees that neighbours differ by at most one halting state, comparing traffic lights determines their relative positions. Writing ⊙ for componentwise product, we define the following predicates on two configurations κ = (κc , τ c , κm , τ m ) and κ̂ = (κˆc , τˆc , κˆm , τˆm ):
(11)
The encoding enc3 : N → T maps i to (1, 0, 0) if i ≡ 0 (mod 3), to (0, 1, 0) if i ≡ 1 (mod 3), and to (0, 0, 1) if i ≡ 2 (mod 3). The successor and predecessor operations are adv(g, y, r) := (r, g, y) and ret(g, y, r) := (y, r, g), so that enc3 (i + 1) = adv(enc3 (i)) and enc3 (i − 1) = ret(enc3 (i)) for i ≥ 1.
behind(κ, κ̂) := ∥adv(τ c ) ⊙ τˆc ∥1 > 0, aligned(κ, κ̂) := ∥τ c ⊙ τˆm ∥1 = ∥τˆm ∥1 , eager(κ, κ̂) := behind(κ, κ̂) ∨ ¬Hlt(κc ).
(13) (14) (15)
When κ is the configuration of a vertex in some state Cj and κ̂ is the aggregated configurations from its neighbours, these predicates detect whether a vertex is behind, aligned, and eager, using only the traffic lights and the halting classifier. In particular, every vertex that is behind is eager.
6.4 Coherence A correspondence is coherent when the configurations genuinely reflect the halting states being simulated. Definition 13 (Coherence). A correspondence Φ is coherent if for every converging state Cj and every vertex v:
The combination function CMB′ distinguishes two cases: a vertex is advancing if aligned(κ, κ̂) ∧ eager(κ, κ̂), and waiting otherwise.
1. κcj (v) = HΦ(v,j) (v);
Writing κ′ := CMB(κc , κˆm ) for the next snapshot and τ ′ := adv(τ c ) for the next traffic light: { ′ ′ c c (κ , τ , κ , τ ) if advancing, (16a) ′ CMB (κ, κ̂) := (κc , τ c , κc , τ c ) if waiting. (16b)
2. τjc (v) = enc3 (Φ(v, j)); c m 3. if j ≥ 1, then κm j (v) = κj−1 (v) and τj (v) = c τj−1 (v); and
4. for every neighbour u of v, |Φ(v, j) − Φ(u, j)| ≤ 1.
Note that both cases set τ m to the current traffic light τ c.
We say Φ is coherent until step n if Coherence 1–4 hold for all j ≤ n.
Finally, the readout function is:
Coherence items 1 and 2 require that each vertex’s current snapshot and traffic light faithfully reflect the halting state being simulated. Coherence 3 requires the advertised components to equal the previous current components, and Coherence 4 bounds the desynchronisation between neighbours to at most one halting state.
If the correspondence is coherent and Φ(v, j) = k, then κc = Hk (v), so Out′ always returns the same value as Out at the corresponding halting step: Out′ (Cj (v)) = Out(Hk (v)). In particular, once Φ(v, j) = k for all v, this holds simultaneously.
Out′ (κ) := Out(κc ).
(17)
In the following lemma we argue formally that C is simple if H satisfies the three conditions of Proposition 3. Intuitively, the range condition is needed because C applies Boolean-valued logic to the result of H’s halting classifier Hlt. If the simple function defining Hlt is arbitrary, then we cannot do this required boolean logic using simple functions only. By contrast, if it always produces values in {−1, 1}, then these can easily be transformed to the range {0, 1}, which allows us to do boolean logic using simple functions.
The choice of encoding Φ(v, j) as a traffic light may seem odd, but storing it as a natural number would not suffice due to the aggregation mechanism of GNNs. In a simple GNN, each vertex receives only the sum of its neighbours’ messages, not individual values. If vertices sent their Φ-values directly, the sum would reveal only the total, making it impossible to determine whether any particular neighbour is behind. The same holds for most aggregation functions, such as mean and max. 6
The bounded-change condition is needed because conditionally applying a simple function, i.e., multiplying a branch by a {0, 1} indicator of the same input, is not itself simple. Instead, we implement the case distinction using a ReLU identity that requires the percomponent changes to be bounded. Lemma 1. If H is simple, the simple function f defining Hlt has range {−1, 1} on all feature vectors encountered during runs of H, and there exists B ≥ 0 such that |[Hi+1 (v)]j − [Hi (v)]j | ≤ B for all components j, vertices v, and iterations i of every run, then C is also simple.
For the other three lemmas, fix a connected component Γ of G with vertex set NΓ , and let kΓ be the first index at which Hlt(HkΓ (v)) = 1 for all v ∈ NΓ . By definition of a complete run, kΓ ≤ k. Note kΓ < k is possible when all vertices with Hlt(HkΓ (v)) = 0 lie outside NΓ . The remaining three key lemmas, called Completeness, Convergence, and Correctness, intuitively show that C’s configurations on NΓ converge to their state at HkΓ , and that for all v ∈ NΓ , Out(HkΓ (v)) = Out(Hk (v)) . To obtain the latter equality invariance of H under graded-bisimulation is crucial: it implies that the computation of H at any vertex depends only on its connected component, so vertices from different components cannot influence each other.
Proof. Since H is simple, AGG′ is summation and hence simple. Writing |z| := ReLU(z) + ReLU(−z), ∑ the norm ∥x∥1 = i |[x]i | is simple. During runs, the norms in behind and aligned evaluate to non-negative integers, and min(x, 1) = x − ReLU(x − 1) maps them to {0, 1} indicators, returning 0 if the comparisons in (13) and (14) return False, and 1 otherwise. Since the simple function f defining Hlt has range {−1, 1}, the simple function (1 − f )/2 gives a {0, 1} indicator for ¬Hlt, so eager is also simple.
In the remaining lemmas, let Φ denote the coherent correspondence given by Lemma 2. Lemma 3 (Completeness). There exists a j ′ ∈ N such that Φ(v, j ′ ) = kΓ for all v ∈ NΓ . Lemma 4 (Convergence). For all j ≥ j ′ + 1 and all v ∈ NΓ , Cj+1 (v) = Cj (v). Lemma 5 (Correctness). For all j ≥ j ′ and all v ∈ NΓ , Out′ (Cj (v)) = H(G)(v).
It remains to show that CMB′ is simple. Let a and e denote the {0, 1}-valued aligned and eager predicates above, and let s := ReLU(a + e − 1), so that s = 1 when advancing and s = 0 when waiting.
We next prove Lemmas 2–5. We begin with a lemma confirming that, given a coherent correspondence the predicates behind, aligned, and eager coincide with the definitions of behind, aligned, and eager from Section 6.2. Lemma 6. Write behindj (v), alignedj (v), and eagerj (v) for the predicates behind, aligned, and eager evaluated at vertex v in state Cj . Let Φ be a correspondence coherent until step j. Then:
Both branches of (16) set the advertised components to (κc , τ c ), so these require no conditional logic. For the current-snapshot components, define the percomponent delta δi := [CMB(κc , κˆm )]i − [κc ]i and the function φ(δ, s′ ) := ReLU(δ + s′ ) − ReLU(δ) ′
− ReLU(−δ + s ) + ReLU(−δ).
1. behindj (v) holds if and only if some neighbour u of v satisfies Φ(u, j) > Φ(v, j). In that case, Φ(u, j) = Φ(v, j) + 1.
(18)
It is straightforward to verify that φ(δ, 0) = 0 and φ(δ, s′ ) = δ whenever s′ ≥ |δ|. The bounded-change condition ensures |δi | ≤ B on coherent inputs, so setting s′ := B · s makes [κc ]i + φ(δi , B · s) equal [κc ]i when waiting (s = 0) and [CMB(κc , κˆm )]i when advancing (s = 1). The traffic-light components are handled identically with B = 1. All operations are compositions of affine transformations and ReLU, so CMB′ is simple; note it agrees with (16) only on coherent inputs. Finally, Out′ projects onto κc and applies Out, so it is also simple.
2. alignedj (v) holds if and only if κm j (u) = HΦ(v,j) (u) and τjm (u) = enc3 (Φ(v, j)) for every neighbour u of v. 3. eagerj (v) holds if and only if v is behind or Hlt(HΦ(v,j) (v)) = 0. Proof. We prove the three statements in order. 1. By Coherence 4, every neighbour u has Φ(u, j) ∈ {Φ(v, j) − 1, Φ(v, j), Φ(v, j) + 1}. By Coherence 2, τjc (u) = enc3 (Φ(u, j)). Since enc3 (i + 1) = adv(enc3 (i)) and enc3 (i − 1) = ret(enc3 (i)), the three possible traffic lights are ret(τjc (v)), τjc (v), and adv(τjc (v)). These are three distinct one-hot vectors, so each is uniquely identifiable in the componentwise sum τˆjc (v), and ∥adv(τjc (v))⊙ τˆjc (v)∥1 > 0 precisely when some neighbour has Φ(u, j) = Φ(v, j) + 1.
6.6 Correctness It remains to show that C is a converging RGNN computing the same classifier as H. To this end, throughout the section, fix input graph G, the complete run H0 , . . . , Hk of H on G, and the infinite run C0 , C1 , . . . of C on G. The correctness argument relies on four key lemmas, which we first state before turning to their proof. The first lemma is Coherence, which provides an invariance relating C’s infinite run to H’s halting run. Lemma 2 (Coherence). There exists a coherent correspondence Φ between the halting run of H and the converging run of C.
2. By Coherence 2, τjc (v) = enc3 (Φ(v, j)). Since traffic lights are one-hot, alignedj (v) holds precisely when τjm (u) = enc3 (Φ(v, j)) for every neighbour u. At j = 0, the definition of In′ gives m κm 0 (u) = H0 (u) and τ0 (u) = enc3 (0), so the 7
claim is immediate. For j ≥ 1, by Coherence 3, c m c κm j (u) = κj−1 (u) and τj (u) = τj−1 (u), so by m Coherence 1 and 2, κj (u) = HΦ(u,j−1) (u) and τjm (u) = enc3 (Φ(u, j − 1)). Since |Φ(u, j − 1) − Φ(u, j)| ≤ 1 and |Φ(u, j) − Φ(v, j)| ≤ 1 by Coherence 4, we have |Φ(u, j − 1) − Φ(v, j)| ≤ 2, so τjm (u) = enc3 (Φ(v, j)) forces Φ(u, j − 1) = Φ(v, j) and hence κm j (u) = HΦ(v,j) (u). Since the trafficlight condition already implies the snapshot condition, both conditions hold if and only if alignedj (v) holds.
Coherence 3 at Cj+1 holds in both cases since both c m branches of (16) set κm j+1 (v) = κj (v) and τj+1 (v) = c τj (v). It remains to verify Coherence 4. For any edge (v, w), if both endpoints advance or neither does, the gap is unchanged. Suppose exactly one advances; call it a and the other b. Then |Φ(a, j + 1) − Φ(b, j + 1)| = |Φ(a, j)+1−Φ(b, j)|, which exceeds 1 only if Φ(b, j) = Φ(a, j)−1. At Cj , a advances and is therefore aligned, so by Lemma 6, τjm (b) = enc3 (Φ(a, j)). By Coherc (b) = enc3 (Φ(b, j − 1)), ence 3 and 2, τjm (b) = τj−1 and Φ(b, j − 1) ∈ {Φ(b, j) − 1, Φ(b, j)} = {Φ(a, j) − 2, Φ(a, j) − 1}. Since |Φ(b, j − 1) − Φ(a, j)| ≤ 2 < 3, we have enc3 (Φ(b, j − 1)) ̸= enc3 (Φ(a, j)), a contradiction.
3. By Coherence 1, κcj (v) = HΦ(v,j) (v), so ¬Hlt(κcj (v)) holds if and only if Hlt(HΦ(v,j) (v)) = 0. The claim follows from the definition of eager and item 1. To prove the coherence lemma we establish a helper lemma: when a vertex is aligned, applying CMB correctly produces the next snapshot. Lemma 7. Let Φ be a correspondence coherent until step j. If v is aligned at Cj , then CMB(κcj (v), κˆm (v)) = HΦ(v,j)+1 (v). j
The completeness proof relies on two further helper lemmas. Lemma 8 shows that behind vertices are always aligned and therefore advance immediately. Lemma 9 shows that no vertex simulates beyond kΓ . Lemma 8. For every j ∈ N and every vertex v, if v is behind at Cj , then v is aligned at Cj .
Proof. Since v is aligned at Cj , Lemma 6 gives κm j (u) = HΦ(v,j) (u) for every neighbour u. Substituting into the definition of κˆm j (v) gives ({ }) κˆm j (v) = AGG {HΦ(v,j) (u) | u ∈ nbrG (v)} . (19)
Proof. We proceed by strong induction on j. At j = 0, Φ(u, 0) = 0 for every vertex u, so no vertex is behind. For j ≥ 1, suppose v is behind at converging state Cj with Φ(v, j) = m. Some neighbour u has Φ(u, j) = m + 1 by Lemma 6. We show that Φ(w, j − 1) = m for every neighbour w of v, which implies that v is aligned at Cj .
By Coherence 1, κcj (v) = HΦ(v,j) (v). Substituting both equalities into the definition of H’s layer L gives CMB(κcj (v), κˆm j (v)) = L(HΦ(v,j) )(v)
(20)
= HΦ(v,j)+1 (v),
(21)
First, we show that Φ(v, j − 1) = m. Since Φ(u, ·) increases by at most 1 per step, Φ(u, j −1) ∈ {m, m+1}. If Φ(u, j − 1) = m + 1, then Coherence 4 and Φ(v, j) = m give Φ(v, j − 1) = m, so v is behind at Cj−1 . Since v is behind, by the inductive hypothesis v is aligned, and by the definition of eagerness, v is eager. Hence v advances, so Φ(v, j) = m + 1, a contradiction. Hence Φ(u, j − 1) = m, and since Φ(u, j) = m + 1, vertex u advanced from Cj−1 to Cj , requiring that u is aligned at Cj−1 . Since u is aligned at Cj−1 and v is a neighbour of u, we have m τj−1 (v) = enc3 (m). For j = 1, the definition of In′ gives τ0m (v) = enc3 (0), so m = 0 and Φ(v, 0) = 0 = m. m c For j ≥ 2, Coherence 3 gives τj−1 (v) = τj−2 (v), so c τj−2 (v) = enc3 (m). By Coherence 2, Φ(v, j − 2) = m, and since m = Φ(v, j −2) ≤ Φ(v, j −1) ≤ Φ(v, j) = m, we get Φ(v, j − 1) = m.
where the last equality is by definition of the halting run. Proof of Lemma 2. We proceed by induction on j. Define Φ(v, 0) := 0 for all v. By the definition of In′ , C0 (v) = (H0 (v), enc3 (0), H0 (v), enc3 (0)), so Coherence 1–4 hold at j = 0. For the inductive step, suppose Φ is coherent until step j and set Φ(v, j + 1) := Φ(v, j) + 1 if v advances at Cj , and Φ(v, j + 1) := Φ(v, j) otherwise. We verify Coherence 1–4 at Cj+1 . For Coherence 1 and 2 we distinguish two cases.
Second, we show that Φ(w, j − 1) = m for every neighbour w of v. For any neighbour w of v, Coherence 4 at converging state Cj−1 gives Φ(w, j − 1) ∈ {m − 1, m, m + 1}. We show Φ(w, j − 1) = m by eliminating the other two possibilities.
1. If v advances (16a), then v is aligned at Cj and Φ(v, j + 1) = Φ(v, j) + 1. By Lemma 7 and Coherence 2 at Cj , κcj+1 (v) = CMB(κcj (v), κˆm j (v)) = HΦ(v,j)+1 (v), (22) c τj+1 (v) = adv(τjc (v)) = enc3 (Φ(v, j) + 1).
1. If Φ(w, j − 1) = m + 1, then v is behind at Cj−1 . Since v is behind, by the inductive hypothesis v is aligned, and by the definition of eagerness, v is eager. Hence v advances, contradicting Φ(v, j) = m.
(23)
2. If v waits (16b), then Φ(v, j + 1) = Φ(v, j). By Coherence 1 and 2 at Cj , κcj+1 (v) = HΦ(v,j) (v),
(24)
c τj+1 (v) = enc3 (Φ(v, j)).
(25)
2. If Φ(w, j−1) = m−1, then m ≥ 1. By its definition, j ≥ Φ(v, j), so j ≥ Φ(u, j) = m + 1 ≥ 2. Coher8
ence 4 at converging state Cj−2 with Φ(v, j − 2) = m gives Φ(w, j − 2) ∈ {m − 1, m, m + 1}, and since Φ(w, j − 2) ≤ Φ(w, j − 1) = m − 1 by definition, Φ(w, j − 2) = m − 1. Hence w is behind at Cj−2 . Since w is behind, by the inductive hypothesis w is aligned, and by the definition of eagerness, w is eager. Hence w advances, so Φ(w, j − 1) ≥ m, a contradiction.
HkΓ (v), and Hlt(HkΓ (v)) holds by definition of kΓ , so no vertex is eager. Since advancing (16a) requires eagerness, every vertex waits (16b) at Cj for every j ≥ j ′ , which preserves κc and τ c . By Coherence 3, c m c ′ κm j (v) = κj−1 (v) and τj (v) = τj−1 (v) for j ≥ j + 1, c c m and since κ and τ are preserved, κj (v) = κcj (v) and τjm (v) = τjc (v). All four components of Cj+1 (v) therefore equal those of Cj (v).
Hence Φ(w, j − 1) = m for all neighbours w. By c (w) = enc3 (m), and by Coherence 3, Coherence 2, τj−1 m c τj (w) = τj−1 (w) = enc3 (m) = τjc (v). Therefore v is aligned at Cj .
The correctness proof connects the converging run’s output to the halting RGNN’s output via Coherence 1 and invariance under graded bisimulation.
Lemma 9. For every vertex v ∈ NΓ and every j ∈ N, Φ(v, j) ≤ kΓ .
Proof of Lemma 5. By Lemma 3 and Coherence 1, κcj′ (v) = HkΓ (v). By Lemma 4, Cj+1 (v) = Cj (v) for j ≥ j ′ + 1. Since all vertices share index kΓ at Cj ′ , no vertex is behind by Lemma 6, and Hlt(HkΓ (v)) holds by definition of kΓ , so no vertex is eager and none advances. Hence κcj′ +1 (v) = κcj′ (v), and κcj (v) = HkΓ (v) for all j ≥ j ′ , and hence Out′ (Cj (v)) = Out(HkΓ (v)).
Proof. Suppose for contradiction that Φ(v, j) > kΓ for some vertex v and some j ∈ N, and let j be minimal. Then Φ(v, j − 1) = kΓ and v advances at Cj−1 , which requires v to be eager. By Coherence 1, κcj−1 (v) = HkΓ (v), and Hlt(HkΓ (v)) holds by definition of kΓ , so v is eager only if it is behind. By Lemma 6, being behind requires a neighbour u with Φ(u, j − 1) > kΓ , but Φ(u, j − 1) ≤ kΓ for all u by the choice of j, a contradiction.
It remains to show that Out(HkΓ (v)) = H(G)(v). As Γ is a connected component, the relation Z = {(v, v) | v ∈ NΓ } is a graded bisimulation between G and Γ. Writing HjΓ (v) for the feature vectors of the run on Γ, AC-layers preserve graded bisimulations, so Hj (v) = HjΓ (v) for all j. In particular, Hlt(HkΓΓ (v)) holds for all v ∈ NΓ , so by definition H(Γ)(v) = Out(HkΓΓ (v)) = Out(HkΓ (v)). As H is invariant under graded bisimulation, H(G)(v) = H(Γ)(v) = Out(HkΓ (v)).
Proof of Lemma 3. We show that if Φ(v, j) < kΓ for some v ∈ NΓ , then some vertex advances at Cj or Cj+1 . Let m = min{Φ(v, j) : v ∈ NΓ } < kΓ . We identify a vertex v with Φ(v, j) = m that is eager. If every vertex in NΓ has index m, then m < kΓ implies some v satisfies Hlt(Hm (v)) = 0, so v is eager by Lemma 6. Otherwise, connectedness and Coherence 4 yield a vertex v at index m with a neighbour at m + 1, so v is behind and hence eager by Lemma 6.
Proof of Proposition 3. Let C be the RGNN constructed in Section 6.5. By Lemma 4, the configuration of every vertex stabilises, so C is a converging RGNN. By Lemma 5, the converged output at each vertex v equals H(G)(v). The simplicity claim follows from Lemma 1.
If v is behind at Cj , Lemma 8 gives that v is aligned at Cj , so v advances at Cj . Otherwise, every vertex has index m, and v is eager because Hlt(Hm (v)) = 0. If v is aligned at Cj , then v advances at Cj . Suppose v is not aligned at Cj . Since v does not adc vance, τj+1 (v) = enc3 (m) and κcj+1 (v) = κcj (v). Since every neighbour w has Φ(w, j) = m, Coherence 2 gives τjc (w) = enc3 (m), and by Coherence 3, m τj+1 (w) = τjc (w) = enc3 (m), so v is aligned at Cj+1 . Since κcj+1 (v) = κcj (v), Hlt(Hm (v)) = 0 persists, so v is eager at Cj+1 and advances at Cj+1 .
7 Related Work The recurrent models of Scarselli et al. (2009), Pflueger et al. (2024), and Bollen et al. (2025) are discussed in Section 3. Here we discuss two additional recurrent models with different output semantics. Ahvonen et al. (2024) study a visiting-acceptance semantics: a vertex is classified as true if its feature vector visits a designated accepting set at least once during the infinite run. They show that their RGNNs over reals capture countable disjunctions of GML formulas (ωGML), while their RGNNs over floats capture the graded modal substitution calculus. As noted by Ahvonen et al., ωGML and µGML are orthogonal in expressivity: visiting-acceptance can express properties not in µGML, such as the centre-point property, while µGML can express properties not in ωGML, such as the non-reachability property (Kuusisto 2013).
By Lemma 9, Φ(v, j) ≤ kΓ for all v ∈ NΓ and j ∈ N. Since Φ is non-decreasing per vertex, and some vertex advances whenever Φ(v, j) < kΓ for some v, we obtain Φ(v, j ′ ) = kΓ for all v ∈ NΓ after finitely many steps. Once Φ(v, j ′ ) = kΓ for all v, no vertex is behind or eager, so every vertex waits and the configuration stabilises after one additional step. Proof of Lemma 4. By Lemma 3, Φ(v, j ′ ) = kΓ for all v. By Lemma 9, Φ(v, j) ≤ kΓ for all j. Since Φ is also non-decreasing, Φ(v, j) = kΓ for all j ≥ j ′ . Since no neighbour has a different index, no vertex is behind by Lemma 6. By Coherence 1, κcj (v) =
Rosenbluth and Grohe (2025) study RGNNs where each vertex has a completion bit; the output is determined by the first feature vector where this bit 9
is set. If given the graph size as input, these networks can compute any computable vertex function invariant under colour refinement. Since their model receives the graph size as additional input, it operates under different assumptions and is not directly comparable to ours.
that value. If one were to redefine simple RGNNs with a different aggregation function, however, the simplicity proof becomes more sensitive. The proof converts aggregated traffic light norms into {0, 1} indicators via min(x, 1) = x−ReLU(x−1), which requires these values to be positive integers. Summation yields neighbour counts, so this holds; componentwise maximum on one-hot vectors produces values in {0, 1} directly, so the same argument applies. Mean aggregation, however, produces rationals: a single ahead neighbour among three yields 1/3, not 1. Since no fixed simple function maps every positive real to 1 and 0 to 0, the thresholding step fails. Whether the simplicity result can be recovered for mean aggregation remains open.
8 Discussion We have shown that, over undirected graphs, converging RGNNs and graded-bisimulation-invariant halting RGNNs express exactly the same vertex classifiers. Combined with the result of Bollen et al. that every µGML formula is expressible by a halting RGNN, yielding Corollary 1, and assuming the finitary JaninWalukiewicz theorem extends to graded bisimulation, this would give a tight characterisation within MSO: the µGML-definable classifiers are exactly those that are both MSO-definable and expressible by a converging or output-converging RGNN.
References Ahvonen, V.; Heiman, D.; Kuusisto, A.; and Lutz, C. 2024. Logical characterizations of recurrent graph neural networks with reals and floats. In Globerson, A.; Mackey, L.; Belgrave, D.; Fan, A.; Paquet, U.; Tomczak, J.; and Zhang, C., eds., Advances in Neural Information Processing Systems, volume 37, 104205– 104249. Curran Associates, Inc. Ahvonen, V.; Heiman, D.; and Kuusisto, A. 2025. Graph neural networks and mso. Barceló, P.; Kostylev, E. V.; Monet, M.; Pérez, J.; Reutter, J.; and Silva, J. P. 2020. The logical expressiveness of graph neural networks. In International Conference on Learning Representations. Bollen, J.; Van den Bussche, J.; Vansummeren, S.; and Virtema, J. 2025. Halting Recurrent GNNs and the Graded mu-Calculus. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning, 175–184. Colcombet, T.; Doumane, A.; and Kuperberg, D. 2025. Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs. In Censor-Hillel, K.; Grandoni, F.; Ouaknine, J.; and Puppis, G., eds., 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025), volume 334 of Leibniz International Proceedings in Informatics (LIPIcs), 152:1–152:16. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. Corso, G.; Cavalleri, L.; Beaini, D.; Liò, P.; and Veličković, P. 2020. Principal neighbourhood aggregation for graph nets. In Larochelle, H.; Ranzato, M.; Hadsell, R.; Balcan, M.; and Lin, H., eds., Advances in Neural Information Processing Systems, volume 33, 13260–13271. Curran Associates, Inc. Gilmer, J.; Schoenholz, S. S.; Riley, P. F.; Vinyals, O.; and Dahl, G. E. 2017. Neural message passing for quantum chemistry. In Proceedings of the 34th International Conference on Machine Learning - Volume 70, ICML’17, 1263–1272. JMLR.org. Grohe, M. 2021. The logic of graph neural networks. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–17. Hamilton, W.; Ying, Z.; and Leskovec, J. 2017. Inductive representation learning on large graphs. In Guyon, I.; Luxburg, U. V.; Bengio, S.; Wallach, H.;
The restriction to MSO in this characterisation is necessary. For instance, the classifier that checks whether a vertex has equally many green neighbours as red neighbours is invariant under graded bisimulation and expressible by a converging RGNN (in a single iteration), but is not MSO-definable. A full logical characterisation of converging RGNN classifiers, beyond the MSO-definable fragment, remains open. Our equivalence is stated for undirected graphs. Given a halting RGNN with complete run H0 , . . . , Hk on input G, each connected component Γ converges independently: writing kΓ for the first index at which all vertices in Γ satisfy Hlt, we may have kΓ < k, in which case no vertex in Γ ever simulates the halting states Hi for kΓ < i ≤ k. The correctness argument relies on two properties: because our graphs are undirected, all vertices within a component converge at the same step kΓ , and because our RGNNs are invariant under graded bisimulation, Out(HkΓ (v)) = Out(Hk (v)) for all vertices v in Γ. On directed graphs, the first property does not hold. A vertex v can converge at some earlier state Hk′ , and vertices that still depend on it have no way to communicate to v that it has fallen behind. Even if Out(Hk′ (v)) = Out(Hk (v)), vertices that v sends messages to will never receive a message from v that reflects the halting state Hk′ +1 or later. By Lemma 7, they will need these intermediate states to calculate the correct next snapshot, so the simulation will fail. Hence, whether some halting RGNNs can be faithfully simulated by converging RGNNs on directed graphs remains open. The halting-to-converging construction uses summation for the traffic light components, but this choice is not essential. Any aggregation function that preserves the support of the multiset of neighbours’ traffic lights suffices, since this is all that behind and aligned require. Both mean and componentwise maximum satisfy this property: with one-hot traffic light vectors, each component of the aggregated result is nonzero if and only if at least one neighbour holds 10
Fergus, R.; Vishwanathan, S.; and Garnett, R., eds., Advances in Neural Information Processing Systems, volume 30. Curran Associates, Inc. Hamilton, W. L. 2020. Graph representation learning. Synthesis Lectures on Artificial Intelligence and Machine Learning 14(3):1–159. Janin, D., and Lenzi, G. 2001. Relating levels of the mu-calculus hierarchy and levels of the monadic hierarchy. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, 347–356. IEEE Computer Society. Kipf, T. N., and Welling, M. 2017. Semi-supervised classification with graph convolutional networks. In International Conference on Learning Representations. Kuusisto, A. 2013. Modal Logic and Distributed Message Passing Automata. In Ronchi Della Rocca, S., ed., Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), 452–468. Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. Morris, C.; Ritzert, M.; Fey, M.; Hamilton, W. L.; Lenssen, J. E.; Rattan, G.; and Grohe, M. 2019. Weisfeiler and leman go neural: Higher-order graph neural networks. Proceedings of the AAAI Conference on Artificial Intelligence 33(01):4602–4609. Pflueger, M.; Tena Cucala, D.; and Kostylev, E. V. 2024. Recurrent graph neural networks and their connections to bisimulation and logic. Proceedings of the AAAI Conference on Artificial Intelligence 38(13):14608–14616. Rosenbluth, E., and Grohe, M. 2025. Repetition makes perfect: Recurrent graph neural networks match message-passing limit. Scarselli, F.; Gori, M.; Tsoi, A. C.; Hagenbuchner, M.; and Monfardini, G. 2009. The graph neural network model. IEEE Transactions on Neural Networks 20(1):61–80. Walukiewicz, I. 2002. Monadic second-order logic on tree-like structures. Theor. Comput. Sci. 275(1– 2):311–346. Xu, K.; Hu, W.; Leskovec, J.; and Jegelka, S. 2019. How powerful are graph neural networks? In International Conference on Learning Representations.
11