Paper deep dive
Unifying approach to uniform expressivity of graph neural networks
Huan Luo, Jonni Virtema
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 7/20/2026, 9:51:23 PM
Summary
The paper introduces Template Graph Neural Networks (T-GNNs), a generalized framework where node features are updated by aggregating over valid template embeddings from a specified set of graph templates. It establishes an equivalence between the expressive power of T-GNNs and Graded Template Modal Logic (GML(T)), providing a unifying approach to analyze GNN expressivity by showing how standard AC-GNNs and variants are instantiations of this framework.
Entities (5)
Relation Signals (4)
Template GNNs → uses → Template
confidence 96% · node features are updated by aggregating over valid template embeddings from a specified set of graph templates.
Graded Template Modal Logic → characterizes → Template GNNs
confidence 95% · establish an equivalence between the expressive power of T-GNNs and GML(T)
Template GNNs → correspondsto → Graded Template Modal Logic
confidence 95% · We establish an equivalence between the expressive power of T-GNNs and GML(T)
Template GNNs → generalizes → AC-GNNs
confidence 90% · we show how standard AC-GNNs and its recent variants can be interpreted as instantiations of T-GNNs.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:The expressive power of Graph Neural Networks (GNNs) is often analysed via correspondence to the Weisfeiler-Leman (WL) algorithm and fragments of first-order logic. Standard GNNs are limited to performing aggregation over immediate neighbourhoods or over global read-outs. To increase their expressivity, recent attempts have been made to incorporate substructural information (e.g. cycle counts and subgraph properties). In this paper, we formalize this architectural trend by introducing Template GNNs (T-GNNs), a generalized framework where node features are updated by aggregating over valid template embeddings from a specified set of graph templates. We propose a corresponding logic, Graded template modal logic (GML(T)), and generalized notions of template-based bisimulation and WL algorithm. We establish an equivalence between the expressive power of T-GNNs and GML(T), and provide a unifying approach for analysing GNN expressivity: we show how standard AC-GNNs and its recent variants can be interpreted as instantiations of T-GNNs.
Tags
Links
- Source: https://arxiv.org/abs/2602.18409v1
- Canonical: https://arxiv.org/abs/2602.18409v1
Trouble viewing inline? Open PDF directly →
Full Text
74,434 characters extracted from source content.
Expand or collapse full text
Unifying approach to uniform expressivity of graph neural networks Huan Luo Jonni Virtema of Computer Science, University of Sheffield, UK School of Computing Science, University of Glasgow, UK jonni.virtema, huan.luo@glasgow.ac.uk Abstract The expressive power of Graph Neural Networks (GNNs) is often analysed via correspondence to the Weisfeiler-Leman (WL) algorithm and fragments of first-order logic. Standard GNNs are limited to performing aggregation over immediate neighbourhoods or over global read-outs. To increase their expressivity, recent attempts have been made to incorporate substructural information (e.g. cycle counts and subgraph properties). In this paper, we formalize this architectural trend by introducing Template GNNs (T-GNNs), a generalized framework where node features are updated by aggregating over valid template embeddings from a specified set of graph templates. We propose a corresponding logic, Graded template-modal logic (GML()GML(T)), and generalized notions of template-based bisimulation and WL algorithm. We establish an equivalence between the expressive power of T-GNNs and GML()GML(T), and provide a unifying approach for analysing GNN expressivity: we show how standard AC-GNNs and its recent variants can be interpreted as instantiations of T-GNNs. 1 Introduction The proliferation of structured data such as graphs and relational structures, and rapid development in the area of neural network machine learning in the past two decades, has led to the development of bespoke machine learning architectures for structured data, most notably Graph Neural Networks (GNNs) (Scarselli et al., 2009). Various extensions and variations of this model have been introduced and studied—however, from a high level perspective, a GNN iteratively and synchronously updates a vector of numerical features in every node of a graph by combining the node’s own feature vector with those of its neighbours (Gilmer et al., 2017). In this level of abstraction, the GNN model is a variation of the local model of distributed computing of Linial (1992). Given an input graph, we want the GNN to output something meaningful. For example, this could be a property of the graph itself (e.g., decide whether the graph is Eulerian), a node property (e.g., inclusion to a dominating set), or a link prediction (e.g., predict whether any two nodes are path-connected). In this paper, we focus on the task of node classification where in the end a boolean-valued classification function is applied to the feature vector of each node. In this framework, GNNs express unary (i.e., node-selecting) queries on graphs, which in the area of graph learning are known as node classifiers. Due to intimate connections between the capabilities of GNNs, expressivity of query languages over graph data, modal logics, and methods related to the graph isomorphism problem, a growing community of researchers have revealed deep and precise connections between these seemingly disparate topics. The (1-dimensional) Weisfeiler and Leman algorithm (Weisfeiler and Leman, 1968)—a.k.a. colour refinement—is a well-known non-complete heuristic for deciding whether two graphs are isomorphic that is known to have the same (non-uniform) expressivity as message-passing GNNs (Morris et al., 2019; Xu et al., 2019). In the modal logic community, de Rijke (2000) developed the notion of graded bisimulation—relation between pointed labelled graphs—in order to characterise the expressivity of graded modal logic. It is not hard to see that the notions of graded bisimulation and colour refinement are two sides of the same coin; two points in a graph are graded (k-)bisimilar if and only if the points are in the same colour class after applying the 1-WL algorithm (k rounds). Hella et al. (2015) discovered that there is a strong connection between the local model of distributed computing and graded modal logics. They established—utilising the notion of bisimulation—a one-to-one correspondence between local distributed algorithms and formulae of graded modal logic (in a non-uniform setting). Sato, Yamada, and Kashima (2019) further developed ideas from Hella et al. and applied them to the GNN-setting. The aforementioned characterisations of the expressivity of message passing models are all in some sense non-uniform. The connections to 1-WL relate to indistinguishability (with respect to any GNN of the given architecture), and the correspondence between local distributed algorithms and graded modal logic is formulated over degree bounded graphs. On the other hand, the uniform expressivity of a GNN architecture relates to studying the class of node classifiers that can be expressed by that GNN architecture (with respect to a full range of inputs that can be reasonably expected). The first characterisation of this kind was established by Barceló et al. (2020)—they established that a logical classier (i.e., one definable in first-order logic) is captured by an aggregate-combine-GNN (AC-GNN) if and only if it can be expressed in graded modal logic. They also established that each classifier definable in the two-variable fragment of first-order logic with counting quantifiers (C2C^2) can be captured by a simple homogeneous aggregate-combine-readout-GNN (ACR-GNN)—leaving the converse, relative to logical classifiers, open. Since the seminal result of Barceló et al. (2020), a plethora of similar results have been shown for different GNN architectures. The connection between graded modal logic and AC-GNNs was further extended from logical classifiers to complete one-to-one correspondences by introducing mild forms of arithmetic to the logical side. Benedikt et al. (2024) utilised logics with so-called Presburger quantifiers, while Grohe (2024) utilised counting terms and built-in relations. Cuenca Grau, Feng, and Wałęga (2026) gave a comprehensive picture of correspondences between AC(R)-GNNs and various modal logics—the main differentiator of their approach to that of Barceló et al. is the idea to replace the restriction to logical classifiers with the notion of bounded-GNNs (in the bounded setting, the ability of GNNs to differentiate multiplicities of elements in a multiset is limited to some constant). Hauke and Wałęga (2026) discovered that, actually, ACR-GNNs are strictly more expressive than C2C^2, even when restricted to logical classifiers, solving an open problem from (Barceló et al., 2020). Their result indicates that, in general, when relating capabilities of GNNs to logics that are unable to do arithmetic, invariance under some bounded version of bisimulation is more appropriate restriction than restricting to logical classifiers. E.g., in the case of AC-GNNs, where a precise characterisation has been obtained in restriction to logical classifiers, invariance under graded bisimulation and FO-definability is equivalent to being invariant under bounded graded bisimulation (Otto, 2019). The provable limitations of the expressivity of aggregate-combine GNNs have led to various extensions of the GNN paradigm, as very simple tasks such as deciding graph-reachability or cycle detection are already beyond their capabilities. Incorporating some form of recursion to the GNN formalism allows properties such as graph-reachability be expressible—typically non-uniform expressivity of GNN models of this type remain restricted to 1-WL, but their uniform expressivity is highly related to that of fixed-point logics such as the graded μ-calculus (Bollen et al., 2025; Pflueger, Tena Cucala, and Kostylev, 2024; Ahvonen et al., 2024). Two prominent paradigms for lifting GNN-expressivity beyond 1-WL relate to enriching the graph features with subgraph counts (Bouritsas et al., 2023; Bevilacqua et al., 2022; Frasca et al., 2022) or homomorphism pattern counts (Barceló et al., 2021; Jin et al., 2024)—a simple example here would be counting short cycles or paths, or homomorphisms to the complete graph of three vertices. Yet, another branch of works has considered weaker GNN models; e.g, Tena Cucala et al. (2023; 2024) related Max and Max-Sum GNNs to datalog. Many of the characterisations of expressivity of various GNN-architectures use a similar recipe following the seminal result of Barceló et al. (2020): First, propose an extension or variation of the AC-GNN model, define a variant of the WL-algorithm (or bisimulation) that corresponds to that GNN-model, and a modal logic that has modalities corresponding to the extension. One then needs to show that the bisimulation yields an upper bound for the expressivity of the GNN-model, and that every neural network yields a parameter p such that p-bounded bisimulation is still an upper bound for its expressivity and has only finitely many p-bisimulation equivalence classes. Finally, one needs to show that every p-bisimulation equivalence class is definable in the newly defined logic and that every logical formula can be simulated by a GNN—the latter is often done by computing the truth value of each subformula recursively in the elements of the feature vectors. While the recipe is simple to summarise, it does not mean that the generalisations are always easy to find or prove—sometimes only parts of the recipe can be applied. Some papers omit the logical counterpart completely and sometimes one gets a connection to a logic only by allowing infinitary connectives—this is the case when one cannot prove that the number of relevant bisimulation equivalence classes is finite. Particular examples utilising parts of the above recipe include (Bollen et al., 2025; Pflueger, Tena Cucala, and Kostylev, 2024; Cuenca Grau, Feng, and Wałęga, 2026; Soeteman and ten Cate, 2025; Chen, Zhang, and Wang, 2025). Our contributions. In this paper, we introduce an abstract general model of graph neural networks that utilises aggregation over templates. Templates are small patterns (i.e., graphs) that govern the form of message passing taking place in the GNN-computation. In standard AC-GNNs, messages are passed from a direct neighbour to another—hence the template here is an edge. If on the other hand, messages are only allowed to be passed within triangles, the template would be a triangle. Roughly speaking, aggregation in a template GNN using a template T is over the multiset of ways to embed the template T into the graph (having the node that aggregates mapped to a specified node in the template). A template GNN can have one or many templates that are used to aggregate simultaneously. For example, an AC-GNN that is enriched with triangle count information can be seen as a template GNN with two templates—an edge and a triangle. After introducing T-GNNs, we define the corresponding notions of T-WL-algorithm, graded T-bisimulation, and graded template modal logic GML()GML(T). We then establish that the expressivity of T-GNNs is bounded by the graded T-bisimulation, which also bounds the expressivity of GML()GML(T). Following the recipe of Barceló et al. (2020), we show that every GML()GML(T)-formula can be simulated by a T-GNN. Finally, we establish a one-to-one correspondence between the uniform expressivity of T-GNNs and GML()GML(T), in the bounded counting case introduced by Cuenca Grau, Feng, and Wałęga (2026) (here, in GNN-aggregation, multiplicities in multisets are capped with some constant). Our main contribution is the formalisation of a general GNN-framework which can incorporate many of the modern paradigms for developing new expressive GNN-architectures. Our main technical contribution, is a meta theorem yielding a family of theorems characterising the expressive power of GNNs. If one formalises their favourite GNN-model as a template GNN, our results give direct definitions for the corresponding WL-algorithm and logic that provably characterise the expressivity of the GNN model. 2 Preliminaries Graphs. A labelled directed graph is a tuple G=(V,E,λ)G=(V,E,λ), where V is a finite set of nodes, E⊆V×VE V× V is the edge relation, and λ:V→ℝdλ:V ^d assigns to each node a vector of real numbers of dimension d, for some fixed d∈ℕd . We call d as the dimension of G. (G,v)(G,v) is a pointed graph given a graph G and a node v∈Vv∈ V. Two pointed graphs are isomorphic (written as (G,v)≅(G′,v′)(G,v) (G ,v )) if there exists a bijection f:V→V′f:V→ V such that f(v)=v′f(v)=v , λ(v)=λ′(f(v))λ(v)=λ (f(v)), for every v∈Vv∈ V, and (v,u)∈E(v,u)∈ E iff (f(v),f(u))∈E′(f(v),f(u))∈ E . For a tuple t=(a1,…an)t=(a_1,… a_n), tit_i denotes its iith element aia_i. We identify assignments of type λ:V→0,1dλ:V→\0,1\^d with propositional assignments λ′:V→2p1,…,pdλ :V→ 2^\p_1,…,p_d\, in the obvious way. That is, pi∈λ′(v)p_i∈λ (v) if and only if λ(v)i=1λ(v)_i=1. Such labelled directed graphs can be treated as Kripke structures with the set of propositions p1,…,pd\p_1,…,p_d\, and vice versa. For a set S, we set S-GraphsS-Graphs to be the class of labelled directed graphs that are labelled with elements from S. Graph classifiers and transformations. Let S and C be sets. A node C-classifier for S-GraphsS-Graphs is a function f:S-Graphs→C-Graphsf S-Graphs→ C-Graphs that maintains the underlying graph structure (i.e., G and f(G)f(G) may differ only on λ). If C=0,1C=\0,1\, this function is called a Boolean node classifier. If C=SC=S, we call this function as S-graph transformation. GNN node classifiers. A standard aggregate-combine graph neural network (AC-GNN) consists of L AC layers and a classification function clscls, for L∈ℕL . Intuitively, each GNN-layer of input dimension d computes an ℝdR^d-graph transformation, while the classification function computes a node C-classifier, for a finite set of classes C. The node classifier computed by the GNN is the composition of these functions. Formally, an AC layer of input dimension d is a pair (agg,comb)(agg,comb), where aggagg is an aggregation function mapping multisets of vectors of dimension d to a vector of dimension d, and comb:ℝ2d→ℝdcomb ^2d ^d is a combination function mapping two vectors of dimension d to a vector of dimension d. At the l-th layer, the node label vector λl(v)λ^l(v) is updated via comb(λl−1(v),agg(λl−1(u)u∈N(v)))comb (λ^l-1(v),agg(\ -6.0mu\λ^l-1(u)\ -6.0mu\_u∈ N(v)) ), where N(v)=u∣(v,u)∈EN(v)=\u (v,u)∈ E\ is the set of neighbours of v. Each node v∈Vv∈ V is classified according to a classification function cls:ℝd→Ccls ^d→ C applied to the final node label λL(u)λ^L(u). An application (G,v)N(G,v) of an AC-GNN N to a pointed labelled graph (G,v)(G,v) is the value cls(λL(v))cls(λ^L(v)). Logical classifiers. Consider a finite set of propositions APAP.111We restrict to finite APAP to obtain a correspondence between APAP and feature vectors of finite dimension |AP| . Formulae of basic modal logic (ML) are given by φ:=p∣¬φ∣φ∧φ∣◇φ,where p∈AP. :=p , $p∈ AP$. Formulae are evaluated over pointed 0,1|AP|\0,1\ -labelled graphs (G,v)(G,v) in the usual manner. Graded modal logic (GML) extends ML with graded modalities ◇≥c ^≥ c, for positive integers c, where (G,v)⊧◇≥cφ iff |u∣(v,u)∈Eand(G,u)⊧φ|≥c.(G,v) ^≥ c iff \u (v,u)∈ E~and~(G,u) \ ≥ c. A (Boolean) GNN classifier N captures a logical classifier φ if for every graph G and node v in G, it holds that (G,v)=1N(G,v)=1 if and only if (G,v)⊧φ(G,v) . Weisfeiler-Leman (WL) algorithm. The WL algorithm is an efficient heuristic originally introduced for checking graph isomorphism (Weisfeiler and Leman, 1968). Given a graph and a countably infinite set of colours C, the 1-dimensional WL (1-WL) test is a colour refinement algorithm that updates node colouring according to the following rule: Cl(v)=HASH(Cl−1(v),Cl−1(u)u∈N(v))C^l(v)=HASH (C^l-1(v),\ -6.0mu\C^l-1(u)\ -6.0mu\_u∈ N(v) ), where HASHHASH is assumed to be a perfect hash function. The algorithm terminates when the colouring is stable or the pre-specified number of iterations is exceeded. Two pointed graphs are said to be WL-indistinguishable if their final colour multisets match. It has been proven that GNNs and 1-WL have the same distinguishing power in the sense that a GNN can distinguish two nodes of a graph if and only if the colour refinement procedure assigns different colours to the two nodes (Xu et al., 2019; Morris et al., 2019). 3 Template GNNs In this section, we define our new model—template graph neural networks—and discuss how existing GNN-models can be interpreted as template GNNs. We start by introducing the notion of a template. Definition 1 (Template). A template is a structure T=(V,E+,E−,r)T=(V,E^+,E^-,r) such that • V is a finite set of vertices, • E+⊆V×VE^+ V× V is a set of edges, where (u,v)∈E+(u,v)∈ E^+ is interpreted to mean that there is an edge from u to v, • E−⊆V×VE^- V× V is a set of non-edges such that E+∩E−=∅E^+∩ E^-= , • r∈Vr∈ V is a node called the root of the template. Note that, we do not presume that E+∪E−=V×VE^+∪ E^-=V× V. A labelled template is a pair (T,λ)(T,λ), where T=(V,E+,E−,r)T=(V,E^+,E^-,r) is a template and λ:V→ℝnλ:V ^n is a labelling. Definition 2 (Template embedding). A template embedding of T=(V,E+,E−,r)T=(V,E^+,E^-,r) into a pointed graph (G,w)=(VG,EG,w)(G,w)=(V_G,E_G,w) is an injective homomorphism f:V→VGf V→ V_G where f(r)=wf(r)=w and for all u,v∈Vu,v∈ V it holds that: 1. if (u,v)∈E+(u,v)∈ E^+ then (f(u),f(v))∈EG(f(u),f(v))∈ E_G, 2. if (u,v)∈E−(u,v)∈ E^- then (f(u),f(v))∉EG(f(u),f(v))∉ E_G. Note that, if E+∪E−=V×VE^+∪ E^-=V× V, a template embedding is simply an injective strong homomorphism from (V,E+,r)(V,E^+,r) to (G,w)(G,w). We write emb(T,(G,w))emb(T,(G,w)) for the set of all template embeddings of T into (G,w)(G,w). A (multiset) aggregation function is any function mapping multisets of real numbers to a real number. Definition 3 (Template isomorphism). Two labelled templates (V1,E1+,E1−,r1,λ1)(V_1,E_1^+,E_1^-,r_1, _1) and (V2,E2+,E2−,r2,λ2)(V_2,E_2^+,E_2^-,r_2, _2) are template isomorphic if there is a bijection f:V1→V2f V_1→ V_2 s.t. 1. f(r1)=r2f(r_1)=r_2, 2. (u,v)∈E1+(u,v)∈ E_1^+ if and only if (f(u),f(v))∈E2+(f(u),f(v))∈ E_2^+, 3. (u,v)∈E1−(u,v)∈ E_1^- if and only if (f(u),f(v))∈E2−(f(u),f(v))∈ E_2^-, 4. λ1(u)=λ2(f(u)) _1(u)= _2(f(u)), for every u∈V1∖r1u∈ V_1 \r_1\. Definition 4 (Template aggregation function). Let T=(V,E+,E−,r)T=(V,E^+,E^-,r) be a template and d∈ℕd . A function aggT:(T,λ)→ℝdagg_T (T,λ) ^d that maps labelled T-templates to ℝdR^d is a T-aggregate function if the function is invariant under template automorphisms. That is, aggT(T,λ1)=aggT(T,λ2),agg_T(T, _1)=agg_T(T, _2), whenever (T,λ1)(T, _1) and (T,λ2)(T, _2) are template isomorphic. Intuitively, a template GNN is a message passing GNN, where messages are not passed via edges, but instead via template embeddings. For a fixed template T, the multiset of messages that a node v receives, is the multiset of labelled graphs obtained via template embeddings. The multiset of labelled graphs is then transformed into a multiset of feature vectors by the template aggregate function. This multiset of feature vectors is then combined with the feature vector of v as in standard AC-GNNs—via further aggregate/combine functions. The formal definition is given below. Definition 5 (Unary Template GNN). Fix L,d∈ℕL,d and a set of templates T. A unary L-layer T-GNN (with feature dimension d) is a tuple =(aggTlll≤L,aggll≤L,combll≤L,cls),N=(\agg^l_T^l\_l≤ L,\agg^l\_l≤ L,\comb^l\_l≤ L,cls), where, for each layer 1≤l≤L1≤ l≤ L, Tl∈T^l is a template, aggTllagg^l_T^l is a TlT^l-aggregate function, agglagg^l is an aggregate function, comblcomb^l is a combination function, and cls:ℝd→0,1cls:R^d→\0,1\ is a final Boolean classification function. At the l-th layer, the node feature vector (of dimension d) of a node v is updated by λl(v)≔combl(λl−1(v),agglaggTll(Tl,λfl−1)∣f∈emb(Tl,(G,v))),λ^l(v) ^l (λ^l-1(v),\\ agg^l\ -6.0mu\agg^l_T^l(T^l,λ^l-1_f) f (T^l,(G,v))\ -6.0mu\ ), where λfl−1(u):=λl−1(f(u))λ^l-1_f(u):=λ^l-1(f(u)), for u∈Tlu∈ T^l. Finally, each node v is classified by applying clscls to the final node label λL(u)λ^L(u). When =TT=\T\, we write T-GNN instead of T-GNN. If N is a T-GNN for some T, we call it a template GNN. We also consider template GNNs that aggregate over multiple templates simultaneously. We call these GNNs n-ary. Definition 6 (n-ary Template GNN). Fix L,d∈ℕL,d and a set of templates T. An n-ary L-layer T-GNN (with feature dimension d) is a tuple =(aggTjlll≤Lj≤n,aggjll≤L,j≤n,combll≤L,cls),N=(\agg^l_T_j^l\_ subarraycl≤ L\\ j≤ n subarray,\agg_j^l\_ subarraycl≤ L,\\ j≤ n subarray,\comb^l\_l≤ L,cls), where, for each layer 1≤l≤L1≤ l≤ L and 1≤j≤n1≤ j≤ n, Tjl∈T_j^l is a template, aggTjllagg^l_T_j^l is a TjlT_j^l-aggregate function, aggjlagg_j^l is an aggregate function, comblcomb^l is a combination function, and cls:ℝd→0,1cls:R^d→\0,1\ is a final Boolean classification function. At the l-th layer, the feature vector of node v is updated by λl(v)≔combl(λl−1(v),agg1laggT1l(T1l,λfl−1)∣f∈emb(T1l,(G,v)),⋮aggnlaggTnll(Tnl,λfl−1)∣f∈emb(Tnl,(G,v))),λ^l(v) ^l (λ^l-1(v),\\ agg_1^l\ -6.0mu\agg^l_T_1^l(T_1^l,λ^l-1_f) f (T_1^l,(G,v))\ -6.0mu\,\\ \\ agg_n^l\ -6.0mu\agg^l_T_n^l(T_n^l,λ^l-1_f) f (T_n^l,(G,v))\ -6.0mu\ ), where λfl−1λ^l-1_f is defined as in the unary case. For c≥1c≥ 1, we call a function f whose parameters are (tuples of) multisets c-bounded, if f(A)=f(A↾c)f(A)=f(A c), where A↾cA c is obtained from A by changing multiplicities larger than c to c. We call a T-GNN N c-bounded, if all its outer aggregate functions222Template aggregate functions are trivially c-bounded, since their input is a single labelled graph. are c-bounded, and we call N bounded, if it is c-bounded for some c. For multisets A and B and c≥1c≥ 1, we write A=cBA=_cB if A↾c=B↾cA c=B c. Families of GNNs interpreted as template GNNs. A standard AC-GNN (see e.g. Barceló et al. (2020)) can be interpreted as a unary template GNN with the template T1T_1, as shown in Figure 1(1(a)), which has vertex set V=r1,aV=\r_1,a\, edge set E1+=(r1,a)E_1^+=\(r_1,a)\, and non-edge set E1−=∅E_1^-= . The number of valid template embeddings at node v is the same as the number of neighbouring nodes of v. When aggTagg_T projects to the feature vector of a and the outer aggregation function is the same as the one used in the AC-GNN, the update rules of node feature vectors for T-GNNs and AC-GNNs coincide. Cuenca Grau, Feng, and Wałęga (2026) introduced the family of bounded GNNs, where aggregation (and readout) functions are restricted to bounded functions. The paper established that bounded GNNs with AC+ layers (defined below) have the same expressive power as the two variable fragment of first-order logic with counting quantifiers. For an AC+ layer, the node feature vectors λl(v)λ^l(v) is updated via comb(λl−1(v),aggλl−1(u)u∈N(v),aggλl−1(u)u∈N¯(v)),comb (λ^l-1(v),\\ agg\ -6.0mu\λ^l-1(u)\ -6.0mu\_u∈ N(v),agg\ -6.0mu\λ^l-1(u)\ -6.0mu\_u∈ N(v)), where N¯(v)=u∣(v,u)∉E∖v N(v)=\u (v,u)∉ E\ \v\ is the set of non-neighbours of v excluding v itself. Bounded AC+-GNNs can be interpreted as a binary template GNNs with =T1,T2T=\T_1,T_2\ for each layer, where T1T_1 is the same as above, and T2T_2 as shown in Figure 1(1(b)), has vertex set V=r2,aV=\r_2,a\, edge set E2+=∅E_2^+= , and non-edge set E2−=(r2,a)E_2^-=\(r_2,a)\. When aggT1agg_T_1 and aggT2agg_T_2 project to the feature vector of a, and the outer aggregation functions for T1T_1 and T2T_2 match the two aggregation functions used in AC+ layers, the update rules of node feature vectors for T-GNNs and AC+-GNNs coincide. r1r_1a (a) T1T_1 r2r_2a (b) T2T_2 Figure 1: Templates T1T_1 and T2T_2 used to capture AC-GNNs and AC+-GNNs. The solid arrow represents an element of E+E^+, while the dashed arrow represents an element of E−E^-. Another line of work that can be directly interpreted as T-GNNs are the ones that enrich the standard GNNs with local graph structural information. For instance, Chen, Zhang, and Wang (2025) proposed k-hop subgraph GNNs, where every node is updated by incorporating information extracted from subgraphs induced by the set of nodes reachable within k steps from the node. Specifically, the k-hop neighbourhood of a node v can be defined as Nk(v)≔u∣d(v,u)≤kN_k(v) \u d(v,u)≤ k\ where d(v,u)d(v,u) is the shortest path distance between v and u. We write GvkG_v^k for the k-hop subgraph structure rooted at v. Instead of aggregating over immediate neighbourhood as in standard GNNs, k-hop subgraph GNNs aggregate over (Gvk,λ(u)(l−1)u∈Nk(v))(G_v^k,\ -6.0mu\λ(u)^(l-1)\ -6.0mu\_u∈ N_k(v)) when updating the node feature vectors. k-hop subgraph GNNs can be interpreted as T-GNNs where T is the set of all rooted graphs of radius k. The radius of a template T is defined by rd(T)≔maxv∈Vd(r,v)rd(T) _v∈ Vd(r,v), where d(r,v)d(r,v) is the shortest E+E^+-path distance from r to v. If there is no E+E^+-path from r to v, we set d(r,v):=∞d(r,v):=∞. We provide a concrete example in the next section. 4 Weisfeiler-Leman Test and Bisimulation Next, we define the new notions of template WL-algorithm and graded template bisimulation, and show that the notions coincide and bound the expressive power of template GNNs. We also discuss how existing WL-variants can be interpreted in our framework. Fix a countable set of colours C. A node colouring of a labelled graph G=(V,E,λ)G=(V,E,λ) is a function col:V→Ccol V→ C. Intuitively, template WL algorithm generalises the standard 1-WL algorithm by replacing, in the colour refinement rounds, the multisets of colours of neighbours of a given node by multisets of coloured graphs obtained via template embeddings (or tuples of multisets, when several templates are used). Definition 7 (T-WL algorithm). An L-round T-WL algorithm takes as an input a labelled graph G=(V,E,λ)G=(V,E,λ), a finite set of templates =T1,…,TnT=\T_1,…,T_n\, and L∈ℕL . Initial node colours are given by node labels of the graph, col0(v)≔HASH(λ(v))col^0(v) (λ(v)) for every v∈Vv∈ V. For 1≤l≤L1≤ l≤ L, node colours are repeatedly refined at each round by coll(v)≔HASH(coll−1(v),(T1,colfl−1)∣f∈emb(T1,(G,v)),⋮(Tn,colfl−1)∣f∈emb(Tn,(G,v))),col^l(v) (col^l-1(v),\\ \ -6.0mu\(T_1,col^l-1_f) f (T_1,(G,v))\ -6.0mu\,\\ \\ \ -6.0mu\(T_n,col^l-1_f) f (T_n,(G,v))\ -6.0mu\ ), where colfl−1(u):=coll−1(f(u))col^l-1_f(u):=col^l-1(f(u)), for each u∈Tiu∈ T_i. The procedure terminates after L rounds, and colL(v)col^L(v) is the final node colour. Here HASHHASH is assumed to be an injective function with co-domain C. When the T-WL algorithm is run on a pair of graphs, it is run with the same injective HASHHASH function. The standard 1-WL algorithm updates a node’s colour based on its own label and the multiset of its neighbours’ colours. T-WL with a single edge template, as shown in Figure 1(1(a)), is equivalent to 1-WL. The update rule coll(v)≔HASH(coll−1(v),(T,colfl−1)∣f∈emb(T,(G,v))col^l(v) (col^l-1(v),\ -6.0mu\(T,col^l-1_f) f (T,(G,v))\ -6.0mu\ is informationally equivalent to the standard 1-WL update rule: coll(v)≔HASH(coll−1(v),(coll−1(u))∣u∈N(v))col^l(v) (col^l-1(v),\ -6.0mu\(col^l-1(u)) u∈ N(v)\ -6.0mu\ ). To increase the expressive power of standard GNNs (from 1-WL), Chen, Zhang, and Wang (2025) proposed k-hop subgraph GNNs and the corresponding k-hop subgraph WL algorithm. As discussed in the previous section, k-hop subgraph GNNs can be interpreted as T-GNNs, when T is the set of all rooted graphs of radius k. Using the same set of templates, T-WL algorithm corresponds to the k-hop subgraph WL algorithm of Chen, Zhang, and Wang. For illustrative purposes, the following example shows how 2-hop subgraph WL and T-WL achieve the same result, on a pair of non-isomorphic graphs that cannot be distinguished by standard 1-WL. Example 8. Consider a triangle template T△T_ with vertex set V=r,a,bV=\r,a,b\, edge set E+=(r,a),(a,b),(b,r)E^+=\(r,a),(a,b),(b,r)\, and non-edge set E−=∅E^-= , and a path template TpT_p with vertex set V=r,a,bV=\r,a,b\, edge set E+=(r,a),(a,b)E^+=\(r,a),(a,b)\, and non-edge set E−=(b,r)E^-=\(b,r)\. Figure 2 shows how 22-hop subgraph WL and T-WL with =T△,TpT=\T_ ,T_p\ distinguish a pair of non-isomorphic graphs, respectively. 2-hop subgraph WLInduced subgraphInduced subgraphG1G_1vvG2G_2vT-WLT△T_ TpT_pG1G_1vvG2G_2v Figure 2: Top: 22-hop subgraph WL extracts subgraphs rooted at node v. Bottom: T-WL arrives at the same colouring by matching node v against =T△,TpT=\T_ ,T_p\. Next, we introduce the notion of graded template bisimulation and connect it to the T-WL algorithm. Definition 9 (Graded T-bisimulation). Let G=(V,E,λ)G=(V,E,λ) and G′=(V′,E′,λ′)G =(V ,E ,λ ) be labelled graphs and T a set of templates. A relation Z0⊆V×V′Z_0 V× V is a graded 0-T-bisimulation if for every (v,v′)∈Z0(v,v )∈ Z_0, λ(v)=λ′(v′)λ(v)=λ (v ). For l≥1l≥ 1, a relation Zl⊆V×V′Z_l V× V is a graded l-T-bisimulation if there exists a graded (l-11)-T-bisimulation Zl−1Z_l-1 s.t. for every (v,v′)∈Zl(v,v )∈ Z_l: 1. (v,v′)∈Zl−1(v,v )∈ Z_l-1, 2. for every T∈T , and every k≥1k≥ 1: • for pairwise distinct f1,…fk∈emb(T,(G,v))f_1,… f_k (T,(G,v)) there exists pairwise distinct f1′,…fk′∈emb(T,(G′,v′))f _1,… f _k (T,(G ,v )) s.t. for all 1≤i≤k1≤ i≤ k, u∈Tu∈ T, (fi(u),fi′(u))∈Zl−1(f_i(u),f_i (u))∈ Z_l-1, • for pairwise distinct f1′,…fk′∈emb(T,(G′,v′))f _1,… f _k (T,(G ,v )) there exists pairwise distinct f1,…fk∈emb(T,(G,v))f_1,… f_k (T,(G,v)) s.t. for all 1≤i≤k1≤ i≤ k, u∈Tu∈ T, (fi(u),fi′(u))∈Zl−1(f_i(u),f_i (u))∈ Z_l-1. We say that (v,v′)(v,v ) are graded l-T-bisimilar—and write (G′,v′)∼l(G,v)(G ,v ) ^l_T(G,v)—if there is a graded l-T-bisimulation ZlZ_l such that (v,v′)∈Zl(v,v )∈ Z_l. For a counting bound c≥1c≥ 1, we define l-c-T-bisimulation by restricting k≤ck≤ c in item 2, and write (G′,v′)∼l,c(G,v)(G ,v ) ^l,c_T(G,v) when v and v′v are l-c-T-bisimilar. We obtain the notion of graded T-bisimulation (graded T-bisimilarity, resp.) from the above definitions in the obvious way by replacing all occurrences of Z0Z_0, ZlZ_l, and Zl−1Z_l-1 by Z. For the cases of graded T-bisimulation and graded l-T-bisimulation, we may the use the following alternative formulation of item 2: 2’. for every template T∈T , there exists a bijection g:emb(T,(G,v))→emb(T,(G′,v′))g:emb(T,(G,v)) (T,(G ,v )) such that for all f∈emb(T,(G,v))f (T,(G,v)), for all u∈Tu∈ T, (f(u),g(f)(u))∈Zl−1(f(u),g(f)(u))∈ Z_l-1. T-WL algorithm and graded T-bisimulation are different sides of the same coin, as the following proposition shows. Proposition 10. Let G=(V,E,λ)G=(V,E,λ) and G′=(V′,E′,λ′)G =(V ,E ,λ ) be labelled graphs, T a finite set of templates, and l∈ℕl . Then (G′,v′)∼l(G,v)(G ,v ) ^l_T(G,v) if and only if coll(v)=coll(v′)col^l(v)=col^l(v ). Proof. The proof is by induction on l. For the base case, by definition of initial colouring, col0(v)=HASH(λ(v))col^0(v)=HASH(λ(v)) and col0(v′)=HASH(λ′(v′))col^0(v )=HASH(λ (v )). Since the hash function is injective, col0(v)=col0(v′)col^0(v)=col^0(v ) if and only if λ(v)=λ′(v′)λ(v)=λ (v ). By definition of graded 0-T-bisimulation, (v,v′)∈Z0(v,v )∈ Z_0 if and only if λ(v)=λ′(v′)λ(v)=λ (v ). For the inductive step, assume the proposition holds for l−1l-1. (⇐ ): Since the hash function is injective, coll(v)=coll(v′)col^l(v)=col^l(v ) holds if and only if the arguments to the hash function are identical, as follows 1. coll−1(v)=coll−1(v′)col^l-1(v)=col^l-1(v ), 2. for every T∈T , (T,colfl−1)∣f∈emb(T,(G,v))=(T,colf′l−1)∣f′∈emb(T,(G′,v′))\ -6.0mu\(T,col^l-1_f) f (T,(G,v))\ -6.0mu\=\ -6.0mu\(T,col^l-1_f ) f (T,(G ,v ))\ -6.0mu\ By induction hypothesis, 1. implies (v,v′)∈Zl−1(v,v )∈ Z_l-1. The multisets are equal in 2. implies for every T∈T , there exists a bijection g:emb(T,(G,v))→emb(T,(G′,v′))g:emb(T,(G,v)) (T,(G ,v )) such that for all f∈emb(T,(G,v))f (T,(G,v)), (T,colfl−1)=(T,colg(f)l−1)(T,col^l-1_f)=(T,col^l-1_g(f)), which implies colfl−1=colg(f)l−1col^l-1_f=col^l-1_g(f), which means for all u∈Tu∈ T, coll−1(f(u))=coll−1(g(f)(u))col^l-1(f(u))=col^l-1(g(f)(u)) by definition. By induction hypothesis, it follows that for all u∈Tu∈ T, (f(u),g(f)(u))∈Zl−1(f(u),g(f)(u))∈ Z_l-1. Since λ(v)=λ′(v′)λ(v)=λ (v ) is implied by initial colouring, (v,v′)∈Zl−1(v,v )∈ Z_l-1 is implied by 1., and the existence of bijection g for all T∈T is implied by 2., the definition of graded l-T-bisimulation is satisfied. Therefore, (v,v′)∈Zl(v,v )∈ Z_l. (⇒ ): Assume (v,v′)∈Zl(v,v )∈ Z_l. Then (v,v′)∈Zl−1(v,v )∈ Z_l-1 by definition. By induction hypothesis, (v,v′)∈Zl−1(v,v )∈ Z_l-1 implies coll−1(v)=coll−1(v′)col^l-1(v)=col^l-1(v ), matching the first argument of the hash function. Since (v,v′)∈Zl(v,v )∈ Z_l, for every T∈T , there exists a bijection g:emb(T,(G,v))→emb(T,(G′,v′))g:emb(T,(G,v)) (T,(G ,v )) such that for all f∈embf , for all u∈Tu∈ T, (f(u),g(f)(u))∈Zl−1(f(u),g(f)(u))∈ Z_l-1 by definition. Applying induction hypothesis to all pairs (f(u),g(f)(u))∈Zl−1(f(u),g(f)(u))∈ Z_l-1, we have coll−1(f(u))=coll−1(g(f)(u))col^l-1(f(u))=col^l-1(g(f)(u)), which means colfl−1=colg(f)l−1col^l-1_f=col^l-1_g(f). Since for every T∈T a bijection g exists mapping f to g(f)g(f), (T,colfl−1)∣f∈emb(T,(G,v))=(T,colf′l−1)∣f′∈emb(T,(G′,v′))\ -6.0mu\(T,col^l-1_f) f (T,(G,v))\ -6.0mu\=\ -6.0mu\(T,col^l-1_f ) f (T,(G ,v ))\ -6.0mu\, matching the other arguments of the hash function. Therefore, coll(v)=coll(v′)col^l(v)=col^l(v ). ∎ It is not difficult too see that the above proof gives an analogous connection between the bounded variants of T-WL-algorithm and bounded T-bisimulation. For c≥1c≥ 1, a c-bounded T-WL algorithm is obtained from Definition 7 by stipulating that HASHHASH cannot differentiate between multiplicities c from larger multiplicities (i.e., HASHHASH is a c-bounded function). Hence, Proposition 10 can be reformulated to state that (v,v′)(v,v ) are l-c-T-bisimilar if and only if coll(v)=coll(v′)col^l(v)=col^l(v ) using a c-bounded HASHHASH-function. Proposition 11. Let G and G′G be labelled graphs, T be a finite set of templates, N a c-bounded L-layer T-GNN, and l≤Ll≤ L. If (v,v′)∈V×V′(v,v )∈ V× V are l-c-T-bisimilar, then they have the same feature vectors at the l-th layer of N. The result remains true also for non-bounded T-GNN, if l-c-T-bisimilarity is replaced with graded l-T-bisimilarity. Proof. The proof is by induction on l. For the base case, by definition of 0-c-T-bisimulation, (v,v′)∈Z0(v,v )∈ Z_0 if and only if λ(v)=λ(v′)λ(v)=λ(v ). T-GNN N initializes node feature vectors based on the initial node labels λ(v)λ(v) and λ(v′)λ(v ) of the graphs. For the inductive step, assume the statement holds for l−1l-1. Consider the update rule for a c-bounded T-GNN classifier. Independent of choices of aggagg, aggTagg_T, and combcomb functions, λl(v)=λl(v′)λ^l(v)=λ^l(v ) holds if 1. λl−1(v)=λl−1(v′)λ^l-1(v)=λ^l-1(v ), 2. for every T∈T1l,…,TnlT∈\T_1^l,…,T_n^l\, (T,λfl−1)∣f∈emb(T,(G,v))=c(T,λf′l−1)∣f′∈emb(T,(G′,v′)).\ -6.0mu\(T,λ^l-1_f) f∈ emb(T,(G,v))\ -6.0mu\\\ =_c\ -6.0mu\(T,λ^l-1_f ) f ∈ emb(T,(G ,v ))\ -6.0mu\. Assume (v,v′)∈Zl(v,v )∈ Z_l. Then (v,v′)∈Zl−1(v,v )∈ Z_l-1 by definition. By induction hypothesis (v,v′)∈Zl−1(v,v )∈ Z_l-1 implies λl−1(v)=λl−1(v′)λ^l-1(v)=λ^l-1(v ). By definition of l-c-T-bisimulation, we have for every T∈T , k≤ck≤ c, for pairwise distinct f1,…fk∈emb(T,(G,v))f_1,… f_k (T,(G,v)) there exists pairwise distinct f1′,…fk′∈emb(T,(G′,v′))f _1,… f _k (T,(G ,v )) s.t. for all 1≤i≤k1≤ i≤ k, u∈Tu∈ T, (fi(u),fi′(u))∈Zl−1(f_i(u),f_i (u))∈ Z_l-1. Applying induction hypothesis to all pairs (fi(u),fi′(u))∈Zl−1(f_i(u),f _i(u))∈ Z_l-1, we have for all 1≤i≤k1≤ i≤ k, u∈Tu∈ T, λl−1(fi(u))=λl−1(fi′(u))λ^l-1(f_i(u))=λ^l-1(f _i(u)), which means λfl−1=λf′l−1λ^l-1_f=λ^l-1_f . The same arguments apply to the back condition symmetrically. The back and forth conditions ensure that the number of embeddings mapping to any tuple of equivalent classes in Zl−1Z_l-1 is preserved between (G,v)(G,v) and (G′,v′)(G ,v ) for k≤ck≤ c. Hence, for every T∈T1l,…,TnlT∈\T_1^l,…,T_n^l\, (T,λfl−1)∣f∈emb(T,(G,v))=c(T,λf′l−1)∣f′∈emb(T,(G′,v′))\ -6.0mu\(T,λ^l-1_f) f (T,(G,v))\ -6.0mu\=_c\ -6.0mu\(T,λ^l-1_f ) f (T,(G ,v ))\ -6.0mu\. Therefore, λl(v)=λl(v′)λ^l(v)=λ^l(v ). The proof for non-bounded case follows in verbatim, once all references to the counting bound c are removed. ∎ 5 Graded Modal Logic and Template GNNs Next, we define our new logic—graded template modal logic GML()GML(T) and prove the main technical result of the paper: for any finite set of templates T, GML()GML(T) captures the uniform expressivity of bounded counting T-GNNs. 5.1 Graded Template Modal Logic We define a logic that has a modality ⟨T⟩≥j(φ1,…,φn) T ^≥ j( _1,…, _n) for each template T of cardinality n+1n+1 and positive j∈ℕj . From now on, we stipulate that the domain of a template of cardinality n+1n+1 is the set [n+1]≔0,1,…,n[n+1] \0,1,…,n\ and that 0 is the root of the template. GML(T). Let T be a finite set of templates. The syntax of GML(T) is given by the following grammar: φ:=p∣¬φ∣φ∧φ∣⟨T⟩≥j(φ1,φ2,…,φnT), :=p T ^≥ j( _1, _2,…, _n_T), where j≥1j≥ 1 is a natural number, T=(V,E+,E−,r)∈T=(V,E^+,E^-,r) is a template, and nT=|V|−1n_T= V -1. The semantics extends that of GML with the following clause for formulae of the form ⟨T⟩≥j(φ1,φ2,…,φnT) T ^≥ j( _1, _2,…, _n_T): (G,v)⊧⟨T⟩≥j(φ1,φ2,…,φnT)(G,v) T ^≥ j( _1, _2,…, _n_T) if and only if |f∈emb(T,(G,v))∣(G,f(i))⊧φi, for 1≤i≤nT|≥j. \f (T,(G,v))\\ (G,f(i)) _i, for 1≤ i≤ n_T\ ≥ j. The modal depth md(φ)md( ) of a GML()GML(T)-formula is defined as usual, with the following additional case: md(⟨T⟩≥j(φ1,φ2,…,φn))≔1+max1≤i≤n(md(φi)).md( T ^≥ j( _1, _2,…, _n)) 1+ _1≤ i≤ n(md( _i)). The depth of the syntactic tree sd(φ)sd( ) of φ is defined similarly as md(φ)md( ), except that all logical connectives add 1 to the depth. We define the counting bound cb(φ)cb( ) of a formula φ∈GML() (T) to be the smallest natural number c∈ℕc such that if ⟨T⟩≥j T ^≥ j occurs in φ , then j≤cj≤ c. Proposition 12. Every GML(T)-formula of modal depth at most l and counting bound at most c is invariant under l-c-T-bisimulation. Proof. The proof is by induction on the structure of φ . For the base case, let φ=p =p be a proposition symbol. By definition, if (G,v)(G,v) and (G′,v′)(G ,v ) are l-c-T-bisimilar, then λ(v)=λ(v′)λ(v)=λ(v ). Hence (G,v)⊧p⇔p∈λ(v)⇔p∈λ′(v′)⇔(G′,v′)⊧p.(G,v) p p∈λ(v) p∈λ (v ) (G ,v ) p. For the inductive step, let φ be a formula with md(φ)≤lmd( )≤ l and cb≤ccb≤ c. The Boolean cases follow immediately from the induction hypothesis. Consider the case where φ=⟨T⟩≥j(φ1,…,φn) = T ^≥ j( _1,…, _n). Since md(φ)≤lmd( )≤ l, we have md(φi)≤l−1md( _i)≤ l-1, for 1≤i≤n1≤ i≤ n. By definition of counting bound, j≤cj≤ c. Let S be the set f∈emb(T,(G,v))∣(G,f(i))⊧φi, for 1≤i≤n\f (T,(G,v)) (G,f(i)) _i, for 1≤ i≤ n\ and S′S be the corresponding set f′∈emb(T,(G′,v′))∣(G′,f′(i))⊧φi, for 1≤i≤n.\f (T,(G ,v )) (G ,f (i)) _i, for 1≤ i≤ n\. By the forth condition in the definition of l-c-T-bisimulation, for pairwise distinct f1,…fj∈emb(T,(G,v))f_1,… f_j (T,(G,v)) there exists pairwise distinct f1′,…fj′∈emb(T,(G′,v′))f _1,… f _j (T,(G ,v )) s.t. for all 1≤m≤j1≤ m≤ j, u∈Tu∈ T, (fm(u),fm′(u))∈Zl−1(f_m(u),f_m (u))∈ Z_l-1. Symmetrically, by the back condition in the definition of l-c-T-bisimulation, we have for pairwise distinct f1′,…fj′∈emb(T,(G′,v′))f _1,… f _j (T,(G ,v )) there exists pairwise distinct f1,…fj∈emb(T,(G,v))f_1,… f_j (T,(G,v)) s.t. for all 1≤m≤j1≤ m≤ j, u∈Tu∈ T, (fm(u),fm′(u))∈Zl−1(f_m(u),f_m (u))∈ Z_l-1. Since (fm(u),fm′(u))∈Zl−1(f_m(u),f_m (u))∈ Z_l-1 and md(φi)≤l−1md( _i)≤ l-1, by induction hypothesis, we have (G,f(i))⊧φi⇔(G′,f′(i))⊧φi(G,f(i)) _i (G ,f (i)) _i, for 1≤i≤n1≤ i≤ n. Therefore, (G,v)⊧φ⇔|S|≥j⇔|S′|≥j⇔(G′,v′)⊧φ.(G,v) \, \,|S|≥ j\, \,|S |≥ j\, \,(G ,v ) . ∎ Next we define two variants of characteristic formulae χ(G,v)lχ^l_(G,v) and χ(G,v)l,cχ^l,c_(G,v) for GML()GML(T), where l,c∈ℕl,c and (G,v)(G,v) is a finite pointed graph. The goal of these formulae is to satisfy the following two properties (G′,v′)⊧χ(G,v)l (G ,v ) χ^l_(G,v)\, ⇔(G′,v′)∼l(G,v) \,(G ,v ) ^l_T(G,v) (G′,v′)⊧χ(G,v)l,c (G ,v ) χ^l,c_(G,v)\, ⇔(G′,v′)∼l,c(G,v). \,(G ,v ) ^l,c_T(G,v). Since we are interested in connections to neural networks, we restrict the consideration to finite graphs. In the case of infinite graphs, χ(G,v)lχ^l_(G,v) would not always be a finite formula. For a template T of cardinality n+1n+1, an n-tuple of GMLGML-formulae φ→ , and a pointed graph (G,v)(G,v), we define ST,φ→(G,v)S^(G,v)_T, to be the following set of template embeddings: f∈emb(T,(G,v))∣(G,f(i))⊧φi for 1≤i≤n.\f (T,(G,v)) (G,f(i)) _i for 1≤ i≤ n\. Definition 13 (Characteristic formulae for GMLGML). Let (G,v)(G,v) be a pointed labelled graph. We define the l-characteristic formula χ(G,v)lχ^l_(G,v) of (G,v)(G,v) by induction on l∈ℕl as follows: χ(G,v)0≔⋀p∣p∈λ(v)∧⋀¬p∣p∉λ(v). _(G,v)^0 \p p∈λ(v)\ \ p p∉λ(v)\. For l≥1l≥ 1, the characteristic formula χ(G,v)l _(G,v)^l is defined as χ(G,v)l:=χ(G,v)l−1∧⋀T∈(⋀f∈emb(T,(G,v))⟨T⟩≥k(φ1f,…,φnf)where k=|ST,φ→(G,v)|∧¬⟨T⟩≥|ST,⊤→(G,v)|+1(⊤→)), _(G,v)^l:= _(G,v)^l-1\\ _T ( -5.69054pt _f (T,(G,v)) -19.91692pt T ^≥ k( ^f_1,…, ^f_n)\,\,\,where k=|S^(G,v)_T, \\ T ^≥ S^(G,v)_T, +1( ) ), where φ→=(φ1f,…,φnf)=(χ(G,f(1))l−1,…,χ(G,f(n))l−1) =( ^f_1,…, ^f_n)=( _(G,f(1))^l-1,…, _(G,f(n))^l-1) and ⊤→=(⊤,…,⊤) =( ,…, ). Next, we define the bounded variants of l-characteristic formulae. We first require the following proposition, whose proof is standard. We say that an equivalence relation ∼ has a finite index, if it has finitely many equivalence classes. We write [∼][ ] for the set of all ∼ equivalence classes. Proposition 14. For every l,c∈ℕl,c and a finite set of templates T, the relation ∼l,c ^l,c_T has a finite index. For the next definition, we need a representative for each equivalence class C∈[∼l,c]C∈[ ^l,c_T]; we may pick, e.g., the first in the alphabetical ordering obtained via some encoding. We write (G,v)∈[∼l,c](G,v)∈[ ^l,c_T] when ranging over such representatives. Definition 15 (Bounded characteristic formulae for GMLGML). Let c≥1c≥ 1 be a natural number, T a finite set of templates, and (G,v)(G,v) a pointed labelled graph. We define the l-c-characteristic formula χ(G,v)l,cχ^l,c_(G,v) of (G,v)(G,v) by induction on l∈ℕl as follows: χ(G,v)0,c≔⋀p∣p∈λ(v)∧⋀¬p∣p∉λ(v). _(G,v)^0,c \p p∈λ(v)\ \ p p∉λ(v)\. For l≥1l≥ 1, the characteristic formula χ(G,v)l,c _(G,v)^l,c is defined as χ(G,v)l,c:=χ(G,v)l−1,c∧⋀T∈(⋀f∈emb(T,(G,v))⟨T⟩≥k(φ→)where k=minc,|ST,φ→(G,v)|∧⋀(Gi,vi)∈[∼l−1,c]1≤i≤n|ST,ψ→(G,v)|+1≤c¬⟨T⟩≥|ST,ψ→(G,v)|+1(ψ1,…,ψn)), _(G,v)^l,c:= _(G,v)^l-1,c\\ _T ( -8.53581pt _f (T,(G,v)) -22.76219pt T ^≥ k( ) k= \c, S^(G,v)_T, \\\ -8.53581pt _ subarrayc\(G_i,v_i)∈[ ^l-1,c_T]\_1≤ i≤ n\\ S^(G,v)_T, ψ +1≤ c subarray -22.76219pt T ^≥ S^(G,v)_T, ψ +1( _1,…, _n) ), where φ→=(φ1f,…,φnf)=(χ(G,f(1))l−1,c,…,χ(G,f(n))l−1,c) =( ^f_1,…, ^f_n)=( _(G,f(1))^l-1,c,…, _(G,f(n))^l-1,c), ψ→=(ψ1,…,ψn)=(χ(G1,v1)l−1,c,…,χ(Gn,vn)l−1,c) ψ=( _1,…, _n)=( _(G_1,v_1)^l-1,c,…, _(G_n,v_n)^l-1,c). The following proposition follows directly from the construction of the characteristic formulae. Proposition 16. Every pointed graph (G,v)(G,v) satisfies its own l-c-T-characteristic formula χ(G,v)l,cχ^l,c_(G,v), for every l,c∈ℕl,c . We are now ready to prove the desired property that a characteristic formula of a pointed graph characterises the corresponding bisimulation equivalence class. Proposition 17. Let c≥1c≥ 1 and l∈ℕl be natural numbers and T a finite set of templates. Then (G′,v′)⊧χ(G,v)l,c⇔(G′,v′)∼l,c(G,v).(G ,v ) χ^l,c_(G,v) (G ,v ) ^l,c_T(G,v). Hence, every ∼l,c ^l,c_T equivalence class is definable by a GML(T) formula of modal depth l and counting bound c. Proof. (⇐)( ): Assume (G′,v′)∼l,c(G,v)(G ,v ) ^l,c_T(G,v). By Prop. 16, (G,v)⊧χ(G,v)l,c(G,v) χ^l,c_(G,v). By Prop. 12, therefore, (G′,v′)⊧χ(G,v)l,c(G ,v ) χ^l,c_(G,v). (⇒)( ): The proof proceeds by induction on l. For the base case, by definition of χ(G,v)0,cχ^0,c_(G,v), (G′,v′)⊧χ(G,v)0,c(G ,v ) χ^0,c_(G,v) iff λ(v′)=λ(v)λ(v )=λ(v), matching the definition of (G′,v′)∼0,c(G,v)(G ,v ) ^0,c_T(G,v). For the inductive step, assume the proposition holds for l−1l-1. Assume (G′,v′)⊧χ(G,v)l,c(G ,v ) χ^l,c_(G,v). By definition of χ(G,v)l,cχ^l,c_(G,v), (G′,v′)⊧χ(G,v)l−1,c(G ,v ) χ^l-1,c_(G,v). By induction hypothesis, (G′,v′)∼l−1,c(G,v)(G ,v ) ^l-1,c_T(G,v), matching the first condition in the definition of ∼l,c ^l,c_T. For any T∈T , let C→=(C1,…,Cn) C=(C_1,…,C_n) be any tuple of representatives of the equivalence classes of ∼l−1,c ^l-1,c_T, and ψ→C→ ψ_ C be the tuple of corresponding characteristic formulae. Let n=|ST,ψ→C→(G,v)|n=|S^(G,v)_T, ψ_ C| and m=|ST,ψ→C→(G′,v′)|m=|S^(G ,v )_T, ψ_ C|. In the case of n≥cn≥ c, the second conjunct in the definition of χ(G,v)l,cχ^l,c_(G,v) requires ⟨T⟩≥cψ→ T ^≥ c ψ, which implies m≥cm≥ c. The third conjunct does not apply as n+1≤cn+1≤ c is not met. Hence, min(c,n)=c=min(c,m) (c,n)=c= (c,m). In the case of n<cn<c, the second conjunct requires ⟨T⟩≥nψ→ T ^≥ n ψ, which implies m≥nm≥ n. As n+1≤cn+1≤ c, the third conjunct applies and requires ¬⟨T⟩≥n+1ψ→ T ^≥ n+1 ψ, which implies m≤nm≤ n. Taken together, m=nm=n. Hence, min(c,n)=n=m=min(c,m) (c,n)=n=m= (c,m). Let f1,…,fk∈emb(T,(G,v))f_1,…,f_k (T,(G,v)) be pairwise distinct embeddings, k≤ck≤ c. Group them by the characteristic formulae ψ→C→ ψ_ C satisfied by the image of template nodes. For any specific group of size k′≤k≤ck ≤ k≤ c, k′≤nk ≤ n. Hence, k′≤min(c,n)=min(c,m)k ≤ (c,n)= (c,m). This implies G′G contains at least k′k distinct embeddings where the image of template nodes satisfy ψ→C→ ψ_ C. By induction hypothesis, nodes satisfying the same characteristic formulae are ((l−-1))-c-T-bisimilar. Symmetric arguments apply to the back condition in the definition of ∼l,c ^l,c_T. Therefore, (G′,v′)∼l,c(G,v)(G ,v ) ^l,c_T(G,v). ∎ Now, since there are only finitely many bounded bisimulation classes for any fixed parameters, we obtain that every l-c-T invariant class of pointed graphs is definable in GML()GML(T). Proposition 18. Every l-c-T invariant class of pointed graphs is definable by GML()GML(T) formula of modal depth l and counting bound c. Proof. Every l-c-T invariant class of pointed graphs is a union of ∼l,c ^l,c_T equivalence classes. Every ∼l,c ^l,c_T equivalence class is definable by a l-c-characteristic formula by Proposition 17, and there is a finite number of such equivalence classes by Proposition 14. Thus, every l-c-T invariant class of pointed graphs is definable by a finite disjunction of l-c-characteristic formulae, one for each equivalence class. ∎ 5.2 From GNNs to logic and back We are now ready to prove our main technical results connecting the uniform expressivity of T-GNNs with expressivity of GML()GML(T). Combining our results on T-GNN invariance under bounded graded bisimulation and Proposition 18 allows us to establish the following result of the uniform expressivity of T-GNNs. Recall that a logical classifier φ captures a (Boolean) GNN classifier N if for every graph G and node v in G, it holds that (G,v)=1N(G,v)=1 if and only if (G,v)⊧φ(G,v) . Theorem 19. Let T be a finite set of templates and N a c-bounded T-GNN with l layers. Then there exists a φ∈GML() (T) of modal depth l and counting bound c that captures N. Proof. The class of pointed graphs that a c-bounded T-GNN N with l layers accepts is invariant under l-c-T bisimulation by Proposition 11. Every such class of pointed graphs is definable by a GML()GML(T) formula of modal depth l and counting bound c by Proposition 18. ∎ Theorem 20. Let T be a finite set of templates, φ∈GML() (T), cmax=cb(φ)c_max=cb( ) and l=sd(φ)l=sd( ). Then there exists a (bounded) T-GNN N with l layers that captures φ . Proof. Let sub(φ)=(φ1,…,φd)sub( )=( _1,…, _d) be the set of all subformulae of φ , such that if φk _k is a subformula of φl _l, then k≤lk≤ l. In particular, φ=φd = _d. We construct a (bounded) l layer T-GNN N of dimension d. The final classification function is cls(λl(v)d)cls(λ^l(v)_d), where λl(v)dλ^l(v)_d is the d-th component of λl(v)λ^l(v). Let J⊆1,…,dJ \1,…,d\ be the set of indices such that for all k∈Jk∈ J, φk _k is the modal formula of the form ⟨T⟩≥c(φ1,φ2,…,φn) T ^≥ c( _1, _2,…, _n). Let m=|J|m=|J| be the number of modal subformulae in sub(φ)sub( ). We define a bijection ι:1,…,m→J :\1,…,m\→ J such that for each j∈1,…,mj∈\1,…,m\, let the corresponding subformula be: φι(j)=⟨T(j)⟩≥cj(ψj,1,…,ψj,nj). _ (j)= T^(j) ^≥ c_j( _j,1,…, _j,n_j). Layer 0 initializes all feature vectors to ℝdR^d to represent truth values of propositions, such that if φk _k is a proposition, then λ0(v)k=1λ^0(v)_k=1 iff (G,v)⊧φk(G,v) _k, all other entries are set to 0. Layers 1,…,l1,…,l are homogeneous, with activation function being truncated ReLU, defined as σ(x)=min(max(0,x),1)σ(x)= ( (0,x),1). Aggregation function is the max-n-sum where n is the counting bound of φ . For each layer l and each j∈1,…,mj∈\1,…,m\, assign the template Tjl=T(j)T_j^l=T^(j), corresponding to φι(j)=⟨T(j)⟩≥cj(ψj,1,…,ψj,nj) _ (j)= T^(j) ^≥ c_j( _j,1,…, _j,n_j), let id(j,i)id(j,i) be the index of the subformula ψj,i _j,i in sub(φ)sub( ). The template aggregation function is defined as follows: aggT(j)l(T(j),λfl−1)≔σ(∑i=1njλl−1(f(i))id(j,i)−nj+1) -8.53581ptagg^l_T^(j)(T^(j),λ^l-1_f) σ ( _i=1^n_jλ^l-1(f(i))_id(j,i)-n_j+1 ) (1) The combination function is defined as comb(,z1,…,zm)=σ(++),comb(x,z_1,…,z_m)=σ(xC+zA+b), where ∈ℝdx ^d is λl−1(v)λ^l-1(v), =(z1,…,zm)∈ℝmz=(z_1,…,z_m) ^m are obtained from template aggregations, and matrices ∈ℝd×d,∈ℝm×d,∈ℝdC ^d× d,A ^m× d,b ^d are defined based on sub(φ)sub( ) as follows: 1. If φk _k is a proposition, then Ckk=1C_k=1, 2. If φk=¬φp _k= _p, then Cpk=−1C_pk=-1 and bk=1b_k=1, 3. If φk=φp∧φq _k= _p _q, then Cpk=Cqk=1C_pk=C_qk=1, and bk=−1b_k=-1, 4. If φk=φι(j) _k= _ (j) corresponds to a modal formula of the form ⟨T(j)⟩≥cj(ψj,1,…,ψj,nj) T^(j) ^≥ c_j( _j,1,…, _j,n_j), then Ajk=1A_jk=1 and bk=−cj+1b_k=-c_j+1, and all other entries are 0. Next we show by induction on the structure of subformula φk _k that for every graph G, every node v, and any layer l≥sd(φk)l ( _k), λl(v)k=1λ^l(v)_k=1 iff (G,v)⊧φk(G,v) _k. For the base case, if φk _k is a proposition, sd(φk)=0sd( _k)=0. By design of layer 0, λ0(v)k=1λ^0(v)_k=1 iff (G,v)⊧φk(G,v) _k, and λl(v)k=0λ^l(v)_k=0 otherwise. As Ckk=1C_k=1 preserves identity, λl(v)k=1λ^l(v)_k=1 iff (G,v)⊧φk(G,v) _k for all l≥0l≥ 0. For the inductive step, assume the statement holds for all subformulae of syntactic depth less than φk _k. • Case 1: φk=¬φp _k= _p. By construction, Cpk=−1C_pk=-1 and bk=1b_k=1, we have λl(v)k=σ(−λl−1(v)p+1)λ^l(v)_k=σ(-λ^l-1(v)_p+1). By induction hypothesis, λl−1(v)p=1λ^l-1(v)_p=1 iff (G,v)⊧φp(G,v) _p, then λl(v)k=σ(0)=0λ^l(v)_k=σ(0)=0. Similarly, λl−1(v)p=0λ^l-1(v)_p=0 iff (G,v)⊧̸φp(G,v) _p, then λl(v)k=σ(1)=1λ^l(v)_k=σ(1)=1. Hence, λl(v)kλ^l(v)_k captures ¬φp _p. • Case 2: φk=φp∧φq _k= _p _q. By construction, Cpk=Cqk=1C_pk=C_qk=1 and bk=−1b_k=-1, we have λl(v)k=σ(λl−1(v)p+λl−1(v)q−1)λ^l(v)_k=σ(λ^l-1(v)_p+λ^l-1(v)_q-1). By induction hypothesis, λl−1(v)p=1λ^l-1(v)_p=1 iff (G,v)⊧φp(G,v) _p, and λl−1(v)q=1λ^l-1(v)_q=1 iff (G,v)⊧φq(G,v) _q. Hence, λl(v)k=1λ^l(v)_k=1 iff (G,v)⊧φp∧φq(G,v) _p _q, and λl(v)k=0λ^l(v)_k=0 otherwise. • Case 3: φk=φι(j)=⟨T(j)⟩≥cj(ψj,1,…,ψj,nj) _k= _ (j)= T^(j) ^≥ c_j( _j,1,…, _j,n_j). Consider first the template aggregation function. By inductive hypothesis, λl−1(f(i))id(j,i)=1λ^l-1(f(i))_id(j,i)=1 iff (G,f(i))⊧ψi(G,f(i)) _i. The sum in (1) equals to n iff all subformulae (ψj,1,…,ψj,nj)( _j,1,…, _j,n_j) are satisfied, in which case σ(n−n+1)=1σ(n-n+1)=1. The sum is ≤n−1≤ n-1 otherwise, in which case σ returns 0. Next consider the max-n-sum aggregation function bounded by cmaxc_max. Let N be the number of valid embeddings. By construction, Aj,k=1A_j,k=1 and bk=−c+1b_k=-c+1, we have λl(v)k=σ(min(cmax,N)−c+1)λ^l(v)_k=σ( (c_max,N)-c+1). Since c≤cmaxc≤ c_max, if N≥cN≥ c, then min(cmax,N)≥c (c_max,N)≥ c, λl(v)k=1λ^l(v)_k=1. If N<cN<c, λl(v)k=0λ^l(v)_k=0. Hence, λl(v)k=1λ^l(v)_k=1 iff N≥cN≥ c iff (G,v)⊧φk(G,v) _k, and λl(v)k=0λ^l(v)_k=0 otherwise. ∎ By combining Theorems 19 and 20 we obtain that Boolean bounded T-GNN node classifiers are exactly those that are definable in GML()GML(T). 6 Conclusions and Future Work In this paper, we introduced template GNNs as a framework to study the (uniform) expressivity of different graph neural networks in a unified manner. In addition, we introduced the accompanying notions of T-WL algorithm, graded T-bisimulation, and graded modal logic GML()GML(T). We showed how various existing approaches to extend the expressivity of GNNs utilising diverse subgraph information can be formalised in our framework. The main technical result of our paper is a metatheorem stating that, for any finite set of templates T, GML()GML(T) captures the uniform expressivity of bounded counting T-GNNs. Several existing characterisations, such as the ones by Barceló et al. (2020) and Cuenca Grau, Feng, and Wałęga (2026) can be seen as special cases of our metatheorem. Similarly, our metatheorem is directly applicable to the k-hop subgraph GNNs of Chen, Zhang, and Wang (2025) and their version of the 1-WL algorithm. A recent result by Hauke and Wałęga (2026) (discussed in the introduction) implies that, in general, our logical characterisation does not transfer to the case of non-bounded T-GNNs and GML()GML(T), even if restricted to logical classifier definable in first-order logic. However, since trivially T-GNNs and bounded T-GNNs have the same separation power—on any given graph, T-GNNs aggregate over multisets of bounded cardinality—two graphs are separable by a T-GNN if they are separable by the T-WL algorithm, or equivalently, by a GML()GML(T)-formula. Open questions and future work. We conclude by discussing directions for future research. • Our framework is closely connected to the local graph parameter enabled GNNs of Barceló et al. (2021). Their ℱF-MPNNs and ℱF-WL algorithm obtain graph pattern information as our model does, but restricts to standard graph neighbour message passing. What is the precise relationship between these models? • Can we extend our framework to cover the Hierarchical Ego Graph Neural Networks (Soeteman and ten Cate, 2025) by some kind of hybrid extension of our logic. • Can we extend our logical characterisations to cover non-bounded T-GNNs by adding similar counting features to our logic as in (Benedikt et al., 2024; Grohe, 2024). • Can we extend our results to cover recursive neural networks using a form of μ-calculus as in (Bollen et al., 2025). References Ahvonen et al. (2024) 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 Zhan, C., eds., Advances in Neural Information Processing Systems, volume 37, 104205–104249. Barceló et al. (2020) 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 8th International Conference on Learning Representations, ICLR 2020 Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net. Barceló et al. (2021) Barceló, P.; Geerts, F.; Reutter, J. L.; and Ryschkov, M. 2021. Graph neural networks with local graph parameters. In Ranzato, M.; Beygelzimer, A.; Dauphin, Y. N.; Liang, P.; and Vaughan, J. W., eds., Advances in Neural Information Processing Systems, volume 34, 25280–25293. Benedikt et al. (2024) Benedikt, M.; Lu, C.; Motik, B.; and Tan, T. 2024. Decidability of graph neural networks via logical characterizations. In Bringmann, K.; Grohe, M.; Puppis, G.; and Svensson, O., eds., 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, Tallinn, Estonia, July 8-12, 2024, volume 297 of LIPIcs, 127:1–127:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Bevilacqua et al. (2022) Bevilacqua, B.; Frasca, F.; Lim, D.; Srinivasan, B.; Cai, C.; Balamurugan, G.; Bronstein, M. M.; and Maron, H. 2022. Equivariant subgraph aggregation networks. In 10th International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net. Bollen et al. (2025) Bollen, J.; Van den Bussche, J.; Vansummeren, S.; and Virtema, J. 2025. Halting Recurrent GNNs and the Graded μ-Calculus. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning, 175–184. Bouritsas et al. (2023) Bouritsas, G.; Frasca, F.; Zafeiriou, S.; and Bronstein, M. M. 2023. Improving graph neural network expressivity via subgraph isomorphism counting. IEEE Transactions on Pattern Analysis and Machine Intelligence 45(1):657–668. Chen, Zhang, and Wang (2025) Chen, Z.; Zhang, Q.; and Wang, R. 2025. On the expressive power of subgraph graph neural networks for graphs with bounded cycles. arXiv preprint arXiv:2502.03703. Cuenca Grau, Feng, and Wałęga (2026) Cuenca Grau, B.; Feng, E.; and Wałęga, P. A. 2026. The correspondence between bounded graph neural networks and fragments of first-order logic. arXiv preprint arXiv:2505.08021. In AAAI 2026. de Rijke (2000) de Rijke, M. 2000. A note on graded modal logic. Studia Logica 64(2):271–283. Frasca et al. (2022) Frasca, F.; Bevilacqua, B.; Bronstein, M. M.; and Maron, H. 2022. Understanding and extending subgraph gnns by rethinking their symmetries. In Koyejo, S.; Mohamed, S.; Agarwal, A.; Belgrave, D.; Cho, K.; and Oh, A., eds., Advances in Neural Information Processing Systems, volume 35, 31376–31390. Gilmer et al. (2017) 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, 1263–1272. Grohe (2024) Grohe, M. 2024. The descriptive complexity of graph neural networks. TheoretiCS 3. Hauke and Wałęga (2026) Hauke, S. P., and Wałęga, P. A. 2026. Aggregate-combine-readout gnns are more expressive than logic C2C^2. arXiv preprint arXiv:2508.06091. In AAAI 2026. Hella et al. (2015) Hella, L.; Järvisalo, M.; Kuusisto, A.; Laurinharju, J.; Lempiäinen, T.; Luosto, K.; Suomela, J.; and Virtema, J. 2015. Weak models of distributed computing, with connections to modal logic. Distributed Computing 28(1):31–53. Jin et al. (2024) Jin, E.; Bronstein, M. M.; Ceylan, İ. İ.; and Lanzinger, M. 2024. Homomorphism counts for graph neural networks: All about that basis. In Proceedings of the 41st International Conference on Machine Learning, 22075–22098. Linial (1992) Linial, N. 1992. Locality in distributed graph algorithms. SIAM Journal on Computing 21(1):193–201. Morris et al. (2019) 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. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, 4602–4609. Otto (2019) Otto, M. 2019. Graded modal logic and counting bisimulation. arXiv preprint arXiv:1910.00039. Pflueger, Tena Cucala, and Kostylev (2024) Pflueger, M.; Tena Cucala, D.; and Kostylev, E. V. 2024. Recurrent graph neural networks and their connections to bisimulation and logic. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, 14608–14616. Sato, Yamada, and Kashima (2019) Sato, R.; Yamada, M.; and Kashima, H. 2019. Approximation ratios of graph neural networks for combinatorial problems. In Wallach, H. M.; Larochelle, H.; Beygelzimer, A.; d’Alché-Buc, F.; Fox, E. B.; and Garnett, R., eds., Advances in Neural Information Processing Systems, volume 32, 4083–4092. Scarselli et al. (2009) 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. Soeteman and ten Cate (2025) Soeteman, A., and ten Cate, B. 2025. Logical expressiveness of graph neural networks with hierarchical node individualization. arXiv preprint arXiv:2506.13911. In NeurIPS 2025. Tena Cucala and Cuenca Grau (2024) Tena Cucala, D. J., and Cuenca Grau, B. 2024. Bridging max graph neural networks and datalog with negation. In Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, 950–961. Tena Cucala et al. (2023) Tena Cucala, D. J.; Cuenca Grau, B.; Motik, B.; and Kostylev, E. V. 2023. On the correspondence between monotonic max-sum gnns and datalog. In Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, 658–667. Weisfeiler and Leman (1968) Weisfeiler, B., and Leman, A. 1968. A reduction of a graph to a canonical form and an algebra arising during this reduction. Nauchno-Technicheskaya Informatsiya 2(9):12–16. Xu et al. (2019) Xu, K.; Hu, W.; Leskovec, J.; and Jegelka, S. 2019. How powerful are graph neural networks? In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net.