Logical characterizations of recurrent graph neural networks with reals and floats

Authors: veeti  ahvonen
damian  heiman
antti  kuusisto
carsten  lutz
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-13 10:03:13

Abstract: In pioneering work from 2019, Barceló and coauthors identified logics that precisely match the expressive power of constant iteration-depth graph neural networks (GNNs) relative to properties definable in first-order logic. In this article, we give exact logical characterizations of recurrent GNNs in two scenarios: (1) in the setting with floating-point numbers and (2) with reals. For floats, the formalism matching recurrent GNNs is a rule-based modal logic with counting, while for reals we use a suitable infinitary modal logic, also with counting. These results give exact matches between logics and GNNs in the recurrent setting without relativising to a background logic in either case, but using some natural assumptions about floating-point arithmetic. Applying our characterizations, we also prove that, relative to graph properties definable in monadic second-order logic (MSO), our infinitary and rule-based logics are equally expressive. This implies that recurrent GNNs with reals and floats have the same expressive power over MSO-definable properties and shows that, for such properties, also recurrent GNNs with reals are characterized by a (finitary!) rule-based modal logic. In the general case, in contrast, the expressive power with floats is weaker than with reals. In addition to logic-oriented results, we also characterize recurrent GNNs, with both reals and floats, via distributed automata, drawing links to distributed computing models.

Main paper: 
 introduction: 
 Graph Neural Networks (GNNs) [11, 30, 34] have proven to be highly useful for processing graph data in numerous applications that span a remarkable range of disciplines including bioinformatics [35] , recommender systems [33] , traffic forecasting [21] , and a multitude of others. The success of GNNs in applications has stimulated lively research into their theoretical properties such as expressive power. A landmark result is due to Barceló et al. [5] which was among the first to characterize the expressive power of GNNs in terms of logic, see [12, 8, 6, 26] and references therein for related results. More precisely, Barceló et al. show that a basic GNN model with a constant number of iterations has exactly the same expressive power as graded modal logic GML in restriction to properties definable in first-order logic FO.In this article, we advance the analysis of the expressive power of GNNs in two directions. First, we study the relation between GNN models based on real numbers, as mostly studied in theory, and GNN models based on floating-point numbers, as mostly used in practice. And second, we focus on a family of basic recurrent GNNs while previous research has mainly considered GNNs with a constant number of iterations, with the notable exception of [26] . The GNNs studied in the current paper have a simple and natural termination (or acceptance) condition: termination is signaled via designated feature vectors and thus the GNN "decides" by itself about when to terminate. We remark that some of our results also apply to constant iteration GNNs and to recurrent GNNs with a termination condition based on fixed points, as used in the inaugural work on GNNs [11] ; see the conclusion section for further details.We provide three main results. The first one is that recurrent GNNs with floats, or GNN[F]s, have the same expressive power as the graded modal substitution calculus GMSC [24, 1, 3] . This is a rulebased modal logic that extends the modal substitution calculus MSC [24] with counting modalities. MSC has been shown to precisely correspond to distributed computation models based on automata [24] and Boolean circuits [1] . GMSC is related to the graded modal µ-calculus, but orthogonal in expressive power. The correspondence between GNN[F]s and GMSC is as follows.Theorem 3.2. The following have the same expressive power: GNN[F]s, GMSC, and R-simple aggregate-combine GNN[F]s.Here R-simple aggregate-combine GNN[F]s mean GNN [F] s that use basic aggregate-combine functions as specified by Barceló et al. [5] and the truncated ReLU as the non-linearity function, see Section 2.1 for the formalities. The theorem shows that an R-simple model of GNN[F]s suffices, and in fact GNN[F]s with a more complex architecture can be turned into equivalent R-simple ones. We emphasize that the characterization provided by Theorem 3.2 is absolute, that is, not relative to a background logic. In contrast, the characterization by Barceló et al. [5] is relative to first-order logic. Our characterization does rely, however, on an assumption about floating-point arithmetics. We believe that this assumption is entirely natural as it reflects practical implementations of floats.Our second result shows that recurrent GNNs with reals, or GNN[R]s, have the same expressive power as the infinitary modal logic ω-GML that consists of infinite disjunctions of GML-formulas. Theorem 3.4. GNN[R]s have the same expressive power as ω-GML.Again, this result is absolute. As we assume no restrictions on the arithmetics used in GNN[R]s, they are very powerful: with the infinitary logic ω-GML it is easy to define even undecidable graph properties. We regard the theorem as an interesting theoretical upper bound on the expressivity of GNNs operating in an unrestricted, recurrent message passing scenario with messages flowing to neighbouring nodes. We note that GNN[R]s can easily be shown more expressive than GNN[F]s.Our third result considers GNN[R]s and GNN[F]s relative to a very expressive background logic, probably the most natural choice in the recurrent GNN context: monadic second-order logic MSO. This result says that, remarkably, for the very significant and large class of MSO-expressible properties, using actual reals with unrestricted arithmetic gives no more expressive power than using floats, by Theorem 3.2 even in the R-simple aggregate-combine setting. Thus, for this class of properties, the theoretical analyses from the literature do not diverge from the practical implementation! Taken together, the above results also imply that in restriction to MSO-expressible properties, GNN[R]s are equivalent to the (finitary!) graded modal substitution calculus GMSC.We also develop characterizations of GNNs in terms of distributed automata. These are in fact crucial tools in our proofs, but the characterizations are also interesting in their own right as they build links between GNNs and distributed computing. We study a class of distributed automata called counting message passing automata (CMPAs) that may have a countably infinite number of states. Informally, these distributed automata update the state of each node according to the node's own state and the multiset of states received from its out-neighbours. We also study their restriction that admits only a finite number of states (FCMPAs) and, furthermore, bounded FCMPAs. In the bounded case the multiplicities of states in the received multisets are bounded by some constant k ∈ N. A summary of our main results, both absolute and relative to MSO, is given in Table 1 .Table 1 : A summary of our main results. The first row contains the results obtained without relativising to a background logic and the second row contains results relative to MSO. Here x ≡ y means that x and y have the same expressive power while x < y means that y is strictly more expressive than x. Further, "bnd." stands for "bounded" and "AC" for "aggregate-combine". Related Work. Barceló et al. [5] study aggregate-combine GNNs with a constant number of iterations. They characterize these GNNs-in restriction to properties expressible in first-order logic-in terms of graded modal logic GML and show that a global readout mechanism leads to a model equivalent to the two-variable fragment of first-order logic with counting quantifiers FOC 2 . Our work extends the former result to include recurrence in a natural way while we leave studying global readouts as future work; see the conclusion section for further details. Grohe [13] connects the guarded fragment of first-order logic with counting GFO + C and polynomial-size bounded-depth circuits, linking (non-recurrent) GNNs to the circuit complexity class TC 0 . Grohe's characterization utilises dyadic rationals rather than floating-point numbers. Benedikt et al. [6] use logics with a generalized form of counting via Presburger quantifiers to obtain characterizations for (non-recurrent) GNNs with a bounded activation function. The article also investigates questions of decidability concerning GNNs-a topic we will not study here. As a general remark on related work, it is worth mentioning that the expressive power of (basic) recurrent GNN-models is invariant under the Weisfeiler-Leman test. This link has been recently studied in numerous articles [25, 36, 12, 5] .Pfluger et al. [26] investigate recurrent GNNs with two kinds of termination conditions: one based on reaching a fixed point when iteratively generating feature vectors, and one where termination occurs after a number of rounds determined by the size of the input graph. They concentrate on the case of unrestricted aggregation and combination functions, even including all uncomputable ones. Their main result is relative to a logic LocMMFP introduced specifically for this purpose, extending first-order logic with a least fixed-point operator over unary monotone formulas. The characterization itself is given in terms of the graded two-way µ-calculus. We remark that MSO significantly generalizes LocMMFP and that the graded two-way µ-calculus is incomparable in expressive power to our GMSC. In contrast to our work and to Barcelo et al. [5] , Pfluger et al. do not discuss the case where the aggregation and combination functions of the GNNs are R-simple or restricted in any other way. We view our work as complementing yet being in the spirit of both Barceló et al. [5] and Pfluger et al. [26] .GNNs are essentially distributed systems, and logical characterizations for distributed systems have been studied widely. A related research direction begins with Hella et al. [16] , Kuusisto [24] and Hella et al. [17] by results linking distributed computation models to modal logics. The articles [16] and [17] give characterizations of constant-iteration scenarios with modal logics, and [24] lifts the approach to recurrent message-passing algorithms via showing that the modal substitution calculus MSC captures the expressivity of finite distributed message passing automata. This generalizes the result from [16] that characterized the closely related class SB(1) of local distributed algorithms with modal logic. Later Ahvonen et al. [1] showed a match between MSC and circuit-based distributed systems. Building on the work on MSC, Reiter showed in [27] that the µ-fragment of the modal µcalculus captures the expressivity of finite message passing automata in the asynchronous scenario. 
preliminaries: 
 We let N, Z + and R denote the sets of non-negative integers, positive integers, and real numbers respectively. For all n ∈ Z + , we let [n] := {1, . . . , n} and for all n ∈ N, we let [0; n] := {0, . . . , n}.With |X| we denote the cardinality of the set X, with P(X) the power set of X and with M(X) the set of multisets over X, i.e., the set of functions X → N. With M k (X) we denote the set of k-multisets over X, i.e., the set of functions X → [0; k]. Given a k-multiset M ∈ M k (X) and x ∈ X, intuitively M (x) = n < k means that there are exactly n copies of x and M (x) = k means that there are k or more copies of x.We work with node-labeled directed graphs (possibly with self-loops), and simply refer to them as graphs. Let LAB denote a countably infinite set of node label symbols, representing features. We denote finite sets of node label symbols by Π ⊆ LAB. Given any Π ⊆ LAB, a Π-labeled graph is a triple G = (V, E, λ) where V is a set of nodes, E ⊆ V × V is a set of edges and λ : V → P(Π) is a node labeling function. Note that a node can carry multiple label symbols. A pointed graph is a pair (G, v) with v ∈ V . Given a graph (V, E, λ), the set of out-neighbours of v ∈ V is { w | (v, w) ∈ E }. Unless stated otherwise, we only consider finite graphs, i.e., graphs where the set of nodes is finite. A node property over Π is a class of pointed Π-labeled graphs. A graph property over Π is a class of Π-labeled graphs. A graph property G over Π corresponds to a node property N over Π if the following holds for all Π-labeled graphs G: G ∈ G iff (G, v) ∈ N for every node v of G. Henceforth a property means a node property. We note that many of our results hold even with infinite graphs and infinite sets of node label symbols. Our results easily extend to graphs that admit labels on both nodes and edges.A graph neural network (GNN) is a neural network architecture for graph-structured data. It may be viewed as a distributed system where the nodes of the (directed, node-labeled) input graph calculate with real numbers and communicate synchronously in discrete rounds. More formally, a recurrent graph neural network GNN[R] over (Π, d), with Π ⊆ LAB and d ∈ Z + , is a tuple G = (R d , π, δ, F ). A recurrent graph neural network computes in a (node-labeled) directed graph as follows. In any Π-labeled graph (V, E, λ), the initialization function π : P(Π) → R d assigns to each node v an initial feature vector or state x 0 v = π(λ(v)). 1 In each subsequent round t = 1, 2, . . . , every node computes a new feature vector x t v using a transition function δ : R d × M(R d ) → R d , δ(x, y) = COM(x, AGG(y)), which is a composition of an aggregation function AGG : M(R d ) → R d (typically sum, min, max or average) and a combination functionCOM : R d × R d → R d such that x t v = COM x t-1 v , AGG {{ x t-1 u | (v, u) ∈ E }}where double curly brackets {{...}} denote multisets. 2 The recurrent GNN G accepts a pointed Π-labeled graph (G, v) if v visits (at least once) a state in the set F ⊆ R d of accepting feature vectors, i.e., x t v ∈ F for some t ∈ N. When we do not need to specify d, we may refer to aGNN[R] over (Π, d) as a GNN[R] over Π. A constant-iteration GNN[R] is a pair (G, N ) where G is a GNN[R] and N ∈ N. It accepts a pointed graph (G, v) if x N v ∈ F .Informally, we simply run a GNN[R] for N iterations and accept (or do not accept) based on the last iteration. We say that G (resp., (G, N )) expresses a node property P over Π, if for each pointed Π-labeled graph (G, w):(G, w) ∈ P iff G (resp., (G, N )) accepts (G, w). A node property P over Π is expressible as a GNN[R] (resp. as a constant-iteration GNN[R]) if there is a GNN[R] (resp. constant-iteration GNN[R]) expressing P.One common, useful and simple possibility for the aggregation and combination functions, which is also used by Barceló et al. (see [5] , and also the papers [25, 15] ) is defined byCOM x t-1 v , AGG {{ x t-1 u | (v, u) ∈ E }} = f (x t-1 v • C + (v,u)∈E x t-1 u • A + b), where f : R d → R d is a non-linearity function (such as the truncated ReLU also used by Barceló et al. in [5] , defined by ReLU * (x) = min(max(0, x), 1) and applied separately to each vector element), C, A ∈ R d×d are matrices and b ∈ R d is a bias vector. We refer to GNNs that use aggregation and combination functions of this form and ReLU * as the non-linearity function as R-simple aggregate-combine GNNs (here 'R' stands for ReLU * ).Example 2.1. Given Π and p ∈ Π, reachability of node label symbol p is the property P over Π that contains those pointed Π-labeled graphs (G, v) where a path exists from v to some u with p ∈ λ(u). An R-simple aggregate-combine GNN[R] over (Π, 1) (where C = A = 1, b = 0 and 1 is the only accepting feature vector) can express P: In round 0, a node w's state is 1 if p ∈ λ(w) and else 0. In later rounds, w's state is 1 if w's state was 1 or it gets 1 from its out-neighbours; else the state is 0. Remark 2.2. Notice that unrestricted GNN[R]s can express, even in a single iteration, node properties such as that the number of immediate out-neighbours of a node is a prime number. In fact, for any U ⊆ N, including any undecidable set U , a GNN[R] can express the property that the number l of immediate out-neighbours is in the set U . See [6] for related undecidability results.Informally, a floating-point system contains a finite set of rational numbers and arithmetic operations • and +. Formally, if p ∈ Z + , n ∈ N and β ∈ Z + \ {1}, then a floating-point system is a tuple S = ((p, n, β), +, •) that consists of the set D S of all rationals accurately representable in the form0.d 1 • • • d p × β e or -0.d 1 • • • d p × β ewhere 0 ≤ d i ≤ β -1 and e ∈ {-n, . . . , n}. It also consists of arithmetic operations + and • of type D S × D S → D S . We adopt the common convention where + and • are defined by taking a precise sum/product w.r.t. reals and then rounding to the closest float in D S , with ties rounding to the float with an even least significant digit, e.g., 0.312 + 0.743 evaluates to 1.06 if the real sum 1.055 is not in the float system. Thus, our float systems handle overflow by capping at the maximum value instead of wrapping around. We typically just write S for D S .Consider GNNs using floats in the place of reals. In GNNs, sum is a common aggregation function (also used in R-simple GNNs), and the sum of floats can depend on the ordering of floats, since it is not associative. In real-life implementations, the set V of nodes of the graph studied can typically be associated with an implicit linear order relation < V (which is not part of the actual graph). It is then natural to count features of out-neighbours in the order < V . However, this allows float GNNs to distinguish isomorphic nodes, which violates the desire that GNNs should be invariant under isomorphism. For example, summing 1, -1 and 0.01 in two orders in a system where the numbers must be representable in the form 0.d 1 d 2 × 10 e or -0.d 1 d 2 × 10 e : first (1 + (-1)) + 0.01 = 0 + 0.01 = 0.01 while (1 + 0.01) + (-1) = 1 + (-1) = 0, since 1.01 is not representable in the system. A float GNN could distinguish two isomorphic nodes with such ordering of out-neighbours.To ensure isomorphism invariance for GNNs with floats that use sum, it is natural to order the floats instead of the nodes. For example, adding floats in increasing order (of the floats) is a natural and simple choice. Summing in this increasing order is also used widely in applications, being a reasonable choice w.r.t. accuracy (see, e.g., [32] , [29] , [18] ). Generally, floating-point sums in applications have been studied widely, see for example [19] . Summing multisets of floats in increasing order leads to a bound in the multiplicities of the elements of the sum; see Proposition 2.3 for the formal statement. Before discussing its proof, we define the k-projection of a multiset M as M |k where M |k (x) = min{M (x), k}. Given a multiset N of floats in float system S, we let SUM S (N ) denote the output of the sum f 1 + • • • + f ℓ where (1) f i appears N (f i ) times (i.e., its multiplicity) in the sum, (2) the floats appear and are summed in increasing order and (3) + is according to S. Proposition 2.3. For all floating-point systems S, there exists a k ∈ N such that for all multisets M over floats in S, we have SUM S (M ) = SUM S (M |k ).A.2. Let u = 0.0 • • • 01 × β e and v = 0.10 • • • 0 × β e+1. Now notice that for a large enough ℓ, summing u to itself m > ℓ times will always give v.Due to Proposition 2.3, GNNs with floats using sum in increasing order are bounded in their ability to fully count out-neighbours. Thus, it is natural to assume that floating-point GNNs are bounded GNNs, i.e., the aggregation function can be written as M k (U d ) → U d for some bound k ∈ N, i.e., for every multiset M ∈ M(U d ), we have AGG(M ) = AGG(M |k ), where M |k is the k-projection of M (and U d is the set of states of the GNN). We finally give a formal definition for floatingpoint GNNs: a floating-point graph neural network (GNN[F]) is simply a bounded GNN where the set of states and the domains and co-domains of the functions are restricted to some floatingpoint system S instead of R (note that S can be any floating-point system). In R-simple GNN[F]s, SUM S replaces the sum of reals as the aggregation function, and their bound is thus determined by the choice of S. A GNN[F] obtained by removing the condition on boundedness is called an unrestricted GNN [F] . Note that by default and unless otherwise stated, a GNN[R] is unbounded, whereas a GNN[F] is bounded. Now, it is immediately clear that unrestricted GNN[F]s (with an unrestricted aggregation function) are more expressive than GNN[F]s: expressing the property that a node has an even number of out-neighbours is easy with unrestricted GNN[F]s, but no bounded GNN[F] with bound k can distinguish the centers of two star graphs with k and k+1 out-neighbours.We then define the logics relevant for this paper. For Π ⊆ LAB, the set of Π-formulae of graded modal logic (GML) is given by the grammar φ ::= ⊤ | p | ¬φ | φ ∧ φ | ♢ ≥k φ, where p ∈ Π and k ∈ N.The connectives ∨, →, ↔ are considered abbreviations in the usual way. Note that node label symbols serve as propositional symbols here. A Π-formula of GML is interpreted in pointed Π-labeled graphs. In the context of modal logic, these are often called (pointed) Kripke models. Let G = (V, E, λ) be a Π-labeled graph and w ∈ V . The truth of a formula φ in a pointed graph (G, w) (denoted G, w |= φ) is defined as usual for the Boolean operators and ⊤, while for p ∈ Π and ♢ ≥k φ, we define that G, w |= p iff p ∈ λ(w), and G, w |= ♢ ≥k φ iff G, v |= φ for at least k out-neighbours v of w. We use the abbreviations ♢φ := ♢ ≥1 φ, □φ := ¬♢¬φ and ♢ =n φ := ♢ ≥n φ ∧ ¬♢ ≥n+1 φ. The set of Π-formulae of ω-GML is given by the grammar φ ::= ψ | ψ∈Ψ ψ, where ψ is a Π-formula of GML and Ψ is an at most countable set of Π-formulae of GML. The truth of infinite disjunctions is defined in the obvious way: G, w |= ψ∈Ψ ψ ⇐⇒ G, w |= ψ for some ψ ∈ Ψ.We next introduce the graded modal substitution calculus (or GMSC), which extends the modal substitution calculus [24, 1, 3] with counting capabilities. Define the setVAR = { V i | i ∈ N } of schema variable symbols. Let T = {X 1 , . . . , X n } ⊆ VAR. The set of (Π, T )-schemata of GMSC is defined by the grammar φ ::= ⊤ | p | X i | ¬φ | φ ∧ φ | ♢ ≥k φ where p ∈ Π, X i ∈ T and k ∈ N. A (Π, T )-program Λ of GMSC consists of two lists of expressions X 1 (0) :-φ 1 • • • X n (0) :-φ n X 1 :-ψ 1 • • • X n :-ψ nwhere φ 1 , . . . , φ n are Π-formulae of GML and ψ 1 , . . . , ψ n are (Π, T )-schemata of GMSC. Moreover, each program is associated with a set A ⊆ T of appointed predicates. A program of modal substitution calculus MSC is a program of GMSC that may only use diamonds ♢ of the standard modal logic. The expressions X i (0) :φ i are called terminal clauses and X i :ψ i are called iteration clauses. The schema variable X i in front of the clause is called the head predicate and the formula φ i (or schema ψ i ) is called the body of the clause. The terminal and iteration clauses are the rules of the program. When we do not need to specify T , we may refer to a (Π, T )-program as a Π-program of GMSC. Now, the nth iteration formula X n i of a head predicate X i (or the iteration formula of X i in round n ∈ N) (w.r.t. Λ) is defined as follows. The 0th iteration formula X 0 i is φ i and the (n + 1)st iteration formula X n+1 i is ψ i where each head predicate Y in ψ i is replaced by the formula Y n . We write G, w |= Λ and say that Λ accepts (G, w) iff G, w |= X n for some appointed predicate X ∈ A and some n ∈ N. Moreover, for all (Π, T )-schemata φ that are not head predicates and for n ∈ N, we let φ n denote the formula (w.r.t. Λ) where each Y ∈ T in φ is replaced by Y n .Recall that monadic second-order logic MSO is obtained as an extension of first-order logic FO by allowing quantification of unary relation variables X, i.e., if φ is an MSO-formula, then so are ∀Xφ and ∃Xφ, see e.g. [9] for more details. Given a set Π ⊆ LAB of node label symbols, an FOor MSO-formula φ over Π is an FOor MSO-formula over a vocabulary which contains exactly a unary predicate for each p ∈ Π and the edge relation symbol E. Equality is admitted.Let φ be an ω-GML-formula, GMSC-schema, GMSC-program, or a rule of a program. The modal depth (resp. the width) of φ is the maximum number of nested diamonds in φ (resp. the maximum number k ∈ N that appears in a diamond ♢ ≥k in φ). If an ω-GML-formula has no maximum depth (resp., width), its modal depth (resp., width) is ∞. If an ω-GML-formula has finite modal depth (resp., width), it is depth-bounded (resp., width-bounded). The formula depth of a GML-formula or GMSC-schema is the maximum number of nested operators ¬, ∧ and ♢ ≥k . Given a Π-program of GMSC or a Π-formula of ω-GML φ (respectively, a formula ψ(x) of MSO or FO over Π, where the only free variable is the first-order variable x), we say that φ (resp., ψ(x)) expresses a node property P over Π, if for each pointed Π-labeled graph (G, w): (G, w) ∈ P iff G, w |= φ (or resp. G |= ψ(w)). A node property P over Π is expressible in GMSC (resp., in ω-GML, FO or MSO) if there is a Π-program of GMSC (resp., a Π-formula of ω-GML, FO or MSO) expressing P. Example 2.4. Recall the property reachability of node label symbol p over Π defined in Example 2.1. It is expressed by the Π-program of GMSC X(0) :p, X :-♢X, where X is an appointed predicate. The ith iteration formula of X is X i = ♢ • • • ♢p where there are exactly i diamonds. Example 2.5 ([24] ). A pointed Π-labeled graph (G, w) has the centre-point property P over Π if there exists an n ∈ N such that each directed path starting from w leads to a node with no outneighbours in exactly n steps. It is easy to see that the Π-program X(0) :-□⊥, X :-♢X ∧ □X, where X is an appointed predicate, expresses P. In [24] , it was established that the centre-point property is not expressible in MSO and that there are properties expressible in µ-calculus and MSO that are not expressible in MSC (e.g., non-reachability), with the same proofs applying to GMSC. Proposition 2.6. Properties expressible in GMSC are expressible in ω-GML, but not vice versa.Proof. A property over Π expressed by a Π-program Γ of GMSC is expressible in ω-GML by the Π-formula Xi∈A, n∈N X n i , where X n i is the nth iteration formula of appointed predicate X i of Γ. Like GNN[R]s, ω-GML can express undecidable properties (cf. Remark 2.2). Clearly GMSCprograms Λ cannot, as configurations defined by Λ in a finite graph eventually loop, i.e., the truth values of iteration formulae start repeating cyclically.While GMSC is related to the graded modal µ-calculus (µGML), which originates from [22] and is used in [26] to characterize a recurrent GNN model, µGML and GMSC are orthogonal in expressivity. Iteration in GMSC need not be over a monotone function and does not necessarily yield a fixed point, and there are no syntactic restrictions that would, e.g., force schema variables to be used only positively as in µGML. The centre-point property from Example 2.5 is a simple property not expressible in µGML (as it is not even expressible in MSO, into which µGML translates). Conversely, GMSC offers neither greatest fixed points nor fixed point alternation. In particular, natural properties expressible in the ν-fragment of µGML such as non-reachability are not expressible in GMSC; this is proved in [24] for the non-graded version, and the same proof applies to GMSC. However, the µ-fragment of the graded modal µ-calculus translates into GMSC (by essentially the same argument as the one justifying Proposition 7 in [24] ). We also note that GMSC translates into partial fixed-point logic with choice [28] , but it is not clear whether the same holds without choice. 
connecting gnns and logics via automata: 
 In this section we establish exact matches between classes of GNNs and our logics. The first main theorem is Theorem 3.2, showing that GNN[F]s, R-simple aggregate-combine GNN[F]s and GMSC are equally expressive. Theorem 3.4 is the second main result, showing that GNN[R]s and ω-GML are equally expressive. We begin by defining the concept of distributed automata which we will mainly use as a tool for our arguments but they also lead to nice additional characterizations. Informally, we consider a model of distributed automata called counting message passing automata and its variants which operate similarly to GNNs. These distributed automata update the state of each node according to the node's own state and the multiset of states of its out-neighbours.Formally, given Π ⊆ LAB, a counting message passing automaton (CMPA) over Π is a tuple (Q, π, δ, F ) where Q is an at most countable set of states and π, δ and F are defined in a similar way as for GNNs: π : P(Π) → Q is an initialization function, δ : Q × M(Q) → Q a transition function and F ⊆ Q a set of accepting states. Computation of a CMPA over Π is defined in a Π-labeled graph G analogously to GNNs: for each node w in G, the initialization function gives the initial state for w based on the node label symbols true in w, and the transition function is applied to the previous state of w and the multiset of states of out-neighbours of w. Acceptance is similar to GNNs: the CMPA accepts (G, w) if the CMPA visits (at least once) an accepting state at w in G. A bounded CMPA is a CMPA whose transition function can be written as δ : Q × M k (Q) → Q for some k ∈ N (i.e., δ(q, M ) = δ(q, M |k ) for each multiset M ∈ M(Q) and state q ∈ Q). A finite CMPA (FCMPA) is a CMPA with finite Q. We define bounded FCMPAs similarly to bounded CMPAs. A CMPA A over Π expresses a node property P over Π if A accepts (G, w) iff (G, w) ∈ P. We define whether a node property P is expressible by a CMPA in a way analogous to GNNs.For any Π, a Π-object refers to a GNN over Π, a CMPA over Π, a Π-formula of ω-GML or a Πprogram of GMSC. Let C be the class of all Π-objects for all Π. Two Π-objects in C are equivalent if they express the same node property over Π. Subsets A, B ⊆ C have the same expressive power, if each x ∈ A has an equivalent y ∈ B and vice versa. It is easy to obtain the following. Proposition 3.1. Bounded FCMPAs have the same expressive power as GMSC.Proof. (Sketch) Details in Appendix B.2. To obtain a bounded FCMPA equivalent to a GMSCprogram Λ, we first turn Λ into an equivalent program Γ where the modal depth of terminal clauses (resp., iteration clauses) is 0 (resp., at most 1). Then from Γ with head predicate set T ′ , we construct an equivalent FCMPA A as follows. The set of states of A is P(Π∪T ′ ) and A enters in round n ∈ N in node w into a state that contains precisely the node label symbols true in w and the predicates X whose iteration formula X n is true at w. For the converse, we create a head predicate for each state in A, and let predicates for accepting states be appointed. The terminal clauses simulate π using disjunctions of conjunctions of non-negated and negated node label symbols. The iteration clauses simulate δ using, for each pair (q, q ′ ), a subschema specifying the multisets that take q to q ′ . We are ready to show equiexpressivity of GMSC and GNN[F]s. This applies without relativising to any background logic. The direction from GNN[F]s to GMSC is trivial. The other direction is more challenging, in particular when going all the way to R-simple GNN[F]s. While size issues were not a concern in this work, we observe that the translation from GNN[F]s to GMSC involves only polynomial blow-up in size; the related definitions and proofs are in appendices A.1, B.2 and B.3. We also conjecture that a polynomial translation from GMSC to R-simple GNN[F]s is possible by the results and techniques in [3] , taking into account differences between GNN[F]s and R-simple GNN[F]s w.r.t. the definition of size. A more serious examination of blow-ups would require a case-by-case analysis taking other such details into account. Theorem 3.2. The following have the same expressive power: GNN[F]s, GMSC, and R-simple aggregate-combine GNN[F]s.Proof. (Sketch) Details in Appendix B.3. By definition, a GNN[F] is just a bounded FCMPA and translates to a GMSC-program by Proposition 3.1. To construct an R-simple aggregate-combine GNN[F] G for a GMSC-program Λ with formula depth D, we first turn Λ into an equivalent program Γ, where each terminal clause has the body ⊥, the formula depth of each body of an iteration clause is D ′ (linear in D) and for each subschema of Γ that is a conjunction, both conjuncts have the same formula depth if neither conjunct is ⊤. We choose a floating-point system that can express all integers up to the width of Γ. We define binary feature vectors that are split into two halves: the 1st half intuitively calculates the truth values of the head predicates and subschemata of Γ one formula depth at a time in the style of Barceló et al. [5] . The 2nd half records the current formula depth under evaluation. G simulates one round of Γ in D ′ + 1 rounds, using the 2nd half of the features to accept nodes only every D ′ +1 rounds: the truth values of head predicates are correct in those rounds. Note that the choice of floating-point system in G depends on Λ and thus no single floating-point system is used by all GNNs resulting from the translation. In fact, fixing a single floating-point system would trivialize the computing model as only finitely many functions could be defined.To show that GNN[R]s and ω-GML are equally expressive, we first prove a useful theorem. Theorem 3.3. CMPAs have the same expressive power as ω-GML.Proof. (Sketch) Details in Appendix B.4. To construct a CMPA for each ω-GML-formula χ, we define a GML-formula called the "full graded type of modal depth n" for each pointed graph (G, w), which expresses all the local information of the neighbourhood of w up to depth n (with the maximum out-degree of G plus 1 sufficing for width). We show that each ω-GML-formula χ is equivalent to an infinite disjunction ψ χ of types. We then define a CMPA that computes the type of modal depth n of each node in round n. Its accepting states are the types in the type-disjunction ψ χ . For the converse, to show that each CMPA has an equivalent ω-GML-formula, we first show that two pointed graphs satisfying the same full graded type of modal depth n have identical states in each round ℓ ≤ n in each CMPA. The ω-GML-formula is the disjunction containing every type T such that some (G, w) satisfying T is accepted by the automaton in round n, where n is the depth of T .Next we characterize GNN[R]s with ω-GML without relativising to a background logic. As the theorems above and below imply that GNN[R]s and CMPAs are equally expressive, it follows that GNN[R]s can be discretized to CMPAs having-by definition-an only countable set of states. Theorem 3.4. GNN[R]s have the same expressive power as ω-GML.Proof. (Sketch) Details in Appendix B.5. For any GNN[R], we build an equivalent ω-GML-formula using the same method as in the proof of Theorem 3.3, where we show that for each CMPA, we can find an equivalent ω-GML-formula. For the converse, we first translate an ω-GML-formula to a CMPA A by Theorem 3.3 and then translate A to an equivalent CMPA A ′ with maximal ability to distinguish nodes. Then we build an equivalent GNN[R] for A ′ by encoding states into integers. Remark 3.5. It is easy to show that unrestricted GNN[F]s have the same expressive power as FCMPAs. Moreover, the proof of Theorem 3.4 is easily modified to show that bounded GNN[R]s have the same expressive power as width-bounded ω-GML. See Appendix B.6 for the proofs.In Appendix B.7 we show that our model of constant-iteration GNN[R]s is equivalent to the one in Barceló et al. [5] . Thus Theorem 3.6 (proven in Appendix B.8) generalizes the result in [5] saying that any property P expressible by FO is expressible as a constant-iteration GNN[R] iff it is expressible in GML. Furthermore, any such P is expressible in GML iff it is expressible in ω-GML. Theorem 3.6. Constant-iteration GNN[R]s have the same expressive power as depth-bounded ω-GML. 
characterizing gnns over mso-expressible properties: 
 In this section we consider properties expressible in MSO. The first main result is Theorem 4.1, where we show that for properties expressible in MSO, the expressive power of GNN[R]s is captured by a finitary logic. In fact, this logic is GMSC and by Theorem 3.2, it follows that relative to MSO, GNN[R]s have the same expressive power as GNN[F]s (Theorem 4.3 below). Our arguments in this section work uniformly for any finite set Σ N of node label symbols. Theorem 4.1. Let P be a property expressible in MSO. Then P is expressible as a GNN[R] if and only if it is expressible in GMSC.Theorem 4.1 is proved later in this section. The recent work [26] relates to Theorem 4.1; see the introduction for a discussion. The proof of Theorem 4.1 can easily be adapted to show that a property P expressible in MSO is expressible as a constant-iteration GNN[R] iff it is expressible in GML. This relates to [5] which shows the same for FO in place of MSO. However, in this particular case the MSO version is not an actual generalization as based on [10] , we show the following in Appendix C.1. To put Theorem 4.3 into perspective, we note that by Example 2.5, the centre-point property is expressible in GMSC, but not in MSO. From Theorem 3.2, we thus obtain the following. Proposition 4.4. There is a property P that is expressible as a GNN[F] but not in MSO.Theorem 3.6 shows that constant-iteration GNN[R]s and depth-bounded ω-GML are equally expressive. The proof of Proposition 2.6 shows that already depth-bounded ω-GML can express properties that GMSC cannot, in particular undecidable ones. Thus, by Theorem 3.2 we obtain the following. Proposition 4.5. There is a property expressible as a constant-iterationGNN[R] but not as a GNN[F].We next discuss the proof of Theorem 4.1. We build upon results due to Janin and Walukiewicz [31, 20] , reusing an automaton model from [31] that captures the expressivity of MSO on treeshaped graphs. With a tree-shaped graph we mean a potentially infinite graph that is a directed tree. The out-degree of nodes is unrestricted (but nevertheless finite), different nodes may have different degree, and both leaves and infinite paths are admitted in the same tree.We next introduce the mentioned automaton model. Although we are only going to use it on treeshaped Σ N -labeled graphs, in its full generality it is actually defined on unrestricted such graphs. We nevertheless call them tree automata as they belong to the tradition of more classical forms of such automata. In particular, a run of an automaton is tree-shaped, even if the input graph is not. Formally, a parity tree automaton (PTA) is a tuple A = (Q, Σ N , q 0 , ∆, Ω), where Q is a finite set of states, Σ N ⊆ LAB is a finite set of node label symbols, q 0 ∈ Q is an initial state, ∆ : Q × P(Σ N ) → F is a transition relation with F being the set of all transition formulas for A defined below, and Ω : Q → N is a priority function. A transition formula for A is a disjunction of FO-formulas of the form∃x 1 • • • ∃x k diff(x 1 , . . . , x k ) ∧ q 1 (x 1 ) ∧ • • • ∧ q k (x k ) ∧ ∀z( diff(z, x 1 , . . . , x k ) → ψ)where k ≥ 0, diff(y 1 , . . . , y n ) shortens an FO-formula declaring y 1 , . . . , y n as pairwise distinct, q i ∈ Q are states used as unary predicates and ψ is a disjunction of conjunctions of atoms q(z), with q ∈ Q. A PTA A accepts a language L(A) consisting of (possibly infinite) graphs G. We have G ∈ L(A) if there is an accepting run of A on G, and runs are defined in the spirit of alternating automata. While details are in Appendix C.2, we mention that transition formulas govern transitions in the run: a transition of a PTA currently visiting node v in state q consists of sending copies of itself to out-neighbours of v, potentially in states other than q. It is not required that a copy is sent to every out-neighbour, and multiple copies (in different states) can be sent to the same out-neighbour. However, we must find some (q, λ(v), ϑ) ∈ ∆ such that the transition satisfies ϑ in the sense that ϑ is satisfied in the graph with one element for each out-neighbour of v and unary predicates (states of A) are interpreted according to the transition. This specific form of PTAs is interesting to us due to the following. Theorem 4.6. Let P be a property expressible in MSO and in ω-GML. Then there is a PTA A such that for any graph G: (G, w) ∈ P iff the unraveling of G at w is in L(A).Proof. Let φ(x) be the MSO-formula over Σ N that expresses P. Theorem 9 in [20] states that for every MSO-sentence ψ, there is a PTA A such that for every tree-shaped Σ N -labeled graph G we have that G ∈ L(A) iff G |= ψ. To obtain a PTA for φ(x), we start from the MSO-sentence ψ := ∃x (φ(x) ∧ ¬∃yE(y, x)) and build the corresponding PTA A. Then A is as desired. In fact, (G, w) ∈ P iff G |= φ(w) iff U |= φ(w) with U the unraveling of G at w since P is expressible by an ω-GML-formula which is invariant under unraveling (defined in Appendix C.1). Moreover,U |= φ(w) iff U |= ψ iff U ∈ L(A).Since GMSC-programs are invariant under unraveling, we may now prove Theorem 4.1 by considering PTAs obtained by Theorem 4.6 and constructing a Σ N -program Λ of GMSC for each such PTA A = (Q, Σ N , q 0 , ∆, Ω) so that the following holds: For every tree-shaped Σ N -labeled graph G with root w, we have G ∈ L(A) iff G, w |= Λ. We then say that A and Λ are tree equivalent.For a state q ∈ Q, let A q be the PTA defined like A but with q as its initial state. For a tree-shaped graph T , setQ T = {q ∈ Q | T ∈ L(A q )}. We say that Q ⊆ P(Q) is the universal set for P ⊆ Σ N if Q consists precisely of the sets Q T ,for all tree-shaped graphs T , whose root is labeled exactly with the node label symbols in P . Let T = (V, E, λ) be a tree-shaped graph with root w and k ∈ N, and let V k be the restriction of V to the nodes on level at most k (the root being on level 0). A k-prefix decoration of T is a mapping µ : V k → P(P(Q)) such that the following conditions hold: (1) for each S ∈ µ(w): q 0 ∈ S; (2) for all v ∈ V on the level k, µ(v) is the universal set for λ(v); (3) for each v ∈ V on some level smaller than k that has out-neighbours u 1 , . . . , u n and all S 1 ∈ µ(u 1 ), . . . , S n ∈ µ(u n ), µ(v) contains the set S that contains a state q ∈ Q iff we have ∆(q, λ(v)) = ϑ such that ϑ is satisfied in the following graph: the universe is {u 1 , . . . , u n } and each unary predicate q ′ ∈ Q is interpreted as {u i | q ′ ∈ S i }. Intuitively, a k-prefix decoration of T represents a set of accepting runs of A on the prefix T k of T . As these runs start in universal sets, for each extension of T k obtained by attaching trees to nodes on level k, we can find a run among the represented ones that can be extended to an accepting run of A on that extension. In fact T is such an extension. The following crucial lemma is proved in Appendix C.2. Lemma 4.7. For every tree-shaped Σ N -labeled graph T : T ∈ L(A) if and only if there is a k-prefix decoration of T , for some k ∈ N.Using the above, we sketch the proof of Theorem 4.1; the full proof is in Appendix C.2.Proof of Theorem 4.1. By Lemma 4.7, given a PTA A obtained from Lemma 4.6, we get a tree equivalent GMSC-program Λ by building Λ to accept the root of a tree-shaped graph G iff G has a k-prefix decoration for some k. This requires care, but is possible; the details are in Appendix C.2. A crucial part of the proof is transferring the set of transition formulas of A into the rules of Λ. 
conclusion: 
 We have characterized the expressivity of recurrent GNNs with floats and reals in terms of modal logics, both in general and relative to MSO. Particularly, in restriction to MSO, GNNs with floats and with reals have the same expressiveness. We mention two interesting directions for future research. The first one is to extend our GNN model, e.g., with global readouts. On the GML side, these correspond to the (counting) global modality [7] . Interestingly, it can be proved-via showing that fixed points can be defined-that this extension makes non-reachability expressible, cf. Example 2.5. The second direction is to consider other acceptance conditions for recurrent GNNs. Intuitively, it should be possible to establish Theorem 3.2 for virtually any GNN acceptance condition, as long as the acceptance condition of GMSC is changed accordingly. Both of these directions are explored in [4] . In particular, it is shown there (and in Appendix D.1) that Theorem 3.2 also holds for recurrent GNNs where termination is based on fixed points, studied under the name "RecGNN" in [26] . These fixed points require only that a round is reached where the examined node does not exit the set of accepting states which is closely related to but different from the fixed point condition in the inaugural works [30, 11] which requires all nodes in the network to reach a stable state.Limitations: For our acceptance condition (and for many others such as those based on fixed points), training and applying a recurrent GNN brings questions of termination. These are very important from a practical perspective, but not studied in this paper. A particularly interesting question is whether termination can be learned in a natural way during the training phase. 
experiments compute resources: 
 Question: For each experiment, does the paper provide sufficient information on the computer resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?Answer: [NA]Justification: The paper does not include experiments.Guidelines:• The answer NA means that the paper does not include experiments.• The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage. • The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute. • The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make it into the paper). 
code of ethics: 
 Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [NA] Justification: The article is a theory paper, and (sufficiently direct) paths to specific positive or negative applications are difficult to conceive.Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] Justification: The article does not involve any datasets.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [NA]Justification: The paper does not use existing assets.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper. • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 
 
 Appendix: We start this appendix by presenting definitions for the sizes of GMSC-programs, GNN[F]s and bounded FCMPAs.The size of a Π-program of GMSC is here defined as the size of Π plus the number of occurrences of node label symbols, head predicates and logical operators in the program, with each ♢ ≥k adding k to the sum instead of just 1.The size of a GNN[F] or bounded FCMPA over Π is defined here as follows. For We note that there is no single way to define the sizes of the objects above. For example, counting each node label symbol, head predicate or state into the size just once may be naïve, as there may not be enough distinct symbols in practice. To account for this, we could also define that the size of each node label symbol, head predicate and state is instead log(k), where k is the number of node label symbols, head predicates or states respectively. Likewise, the size of a diamond ♢ ≥ℓ could be considered log(k), where k is the maximum ℓ appearing in a diamond in the program. However, this happens to not affect the size of our translation from GNN[F]s to GMSC. As another example, defining the size of a single floating-point number as one may be naïve; one could define that the size of a single floating-point number is the length of the string that represents it in the floating-point system instead of one.We recall Proposition 2.3 and give a more detailed proof. Proposition 2.3. For all floating-point systems S, there exists a k ∈ N such that for all multisets M over floats in S, we have SUM S (M ) = SUM S (M |k ).Proof. Consider a floating-point system S = ((p, n, β), +, •) and a multiset M ∈ M(S). We assumef = 0.d 1 • • • d p × β e ∈ S (the case where f = -0.d 1 • • • d p × β e is symmetric). Assume that the sum of all numbers smaller than f in M in increasing order is s ∈ S. Let s + f 0 denote s and let s+f ℓ+1 denote (s+f ℓ )+f for all ℓ ∈ N. It is clear that s+f ℓ+1 ≥ s+f ℓ , and furthermore, ifs + f ℓ+1 = s + f ℓ , then s + f ℓ ′ = s + f ℓ for all ℓ ′ ≥ ℓ. If s + f ℓ+1 = s + f ℓ , then we say that the sum s + f ℓ has stabilized. Let β ′ := β -1. We may assume that s ≥ -0.β ′ • • • β ′ × β n . Since s + f ℓ+1 ≥ s + f ℓ for each ℓ ∈ N and S is finite, there must exist some k ∈ Z + such that either s + f k = s + f k-1 or s + f k = 0.β ′ • • • β ′ × β n but then s + f k+1 = s + f k . Clearly, k = |S|is sufficient for each s and f , and thus satisfies the condition of the proposition.A smaller bound can be found as follows. Assume without loss of generality that d 1 ̸ = 0 (almost all floating-point numbers in S can be represented in this form and the representation does not affect the outcome of a sum; we consider the case for floats not representable in this way separately). Now, consider the case where s= -0.β ′ • • • β ′ × β e ′for some e ′ ∈ [-n, n], as some choice of e ′ clearly maximizes the number of times f can be added. Now it is quite easy to see that thats + f β p -β p-1 ≥ -0.10 • • • 0 × β e ′, unless the sum stabilizes sooner. This is because there are exactlyβ p -β p-1 numbers in S from -0.β ′ • • • β ′ × β e ′ to -0.10 • • • 0 × β e ′. After this another 2β p-1 additions ensures that s + f β p +β p-1 ≥ 0. (Consider the case where p = 3 and β = 10 and we add the number f = 0.501 × 10 0 to -0.100 × 10 3 repeatedly. We first get -0.995 × 10 2 , then -0.990 × 10 2 , etc. Each two additions of f is more than adding f ′ = 0.001 × 10 3 once, and f ′ can be added exactly β p-1 times to -0.100 × 10 3 until the sum surpasses 0, meaning that f can be added at most 2β p-1 times. On the other hand, if f were 0.500 × 10 0 or smaller, then the sum would have never reached -0.100 × 10 3 in the first place.) Let ℓ := β p + β p-1 . Let s ′ := s + f ℓ and assume the sum s ′ has not yet stabilized. Next, it is clear that for any i ∈[p] we have s ′ + f β i ≥ 0.10 • • • 0 × β e+i because d 1 ≥ 1. For d 1 ≤ β 2 , we have that s ′ + f β p = 0.10 • • • 0 × β e+pwhich is where the sum stabilizes. If on the other hand d 1 > β 2 , we have that s ′ + f β p+1 = 0.10 • • • 0 × β e+p+1 , which is where the sum stabilizes (this is because d 1 > β 2 causes the sum to round upwards until the exponent reaches the value e + p + 1). Thus, we get a threshold ofβ p+1 + β p + β p-1 .The case where d 1 = 0 for all representations of f is analogous; we simply choose one representation and shift our focus to the first i such that d i ̸ = 0 and perform the same examination. The position of i does not affect the overall analysis.We conjecture that a smaller bound than β p+1 +β p +β p-1 is possible, but involves a closer analysis.We give a more detailed definition for distributed automata. Given Π ⊆ LAB, a counting message passing automaton (or CMPA) over Π is a tuple (Q, π, δ, F ), where • Q is an at most countable non-empty set of states,• π : P(Π) → Q is an initialization function, • δ : Q × M(Q) → Q is a transition function, and • F ⊆ Q is a set of accepting states.If the set of states is finite, then we say that the counting message passing automaton is finite and call it an FCMPA. Note that in the context of FCMPAs, finiteness refers specifically to the number of states. We also define a subclass of counting message passing automata: a k-counting message passing automaton (k-CMPA) is a tuple (Q, π, δ, F ), where Q, π and F are defined analogously to CMPAs and the transition function δ can be written in the form Q × M k (Q) → Q, i.e., for all multisets M ∈ M(Q) we have δ(q, M ) = δ(q, M |k ) for all q ∈ Q. A k-FCMPA naturally refers to a k-CMPA whose set of states is finite; this is truly a finite automaton. For any k ∈ N, each k-CMPA (respectively, each k-FCMPA) is called a bounded CMPA (resp., a bounded FCMPA).Let G = (V, E, λ) be a Π-labeled graph. We define the computation of a CMPA formally. A CMPA (or resp. k-CMPA) (Q, π, δ, F ) over Π and a Π-labeled graph G = (V, E, λ) define a distributed system, which executes in ω-rounds as follows. Each round n ∈ N defines a global configuration g n : V → Q which essentially tells in which state each node is in round n. If n = 0 and w ∈ V , then g 0 (w) = π(λ(w)). Now assume that we have defined g n . Informally, a new state for w in round n + 1 is computed by δ based on the previous state of w and the multiset of previous states of its immediate out-neighbours. More formally, let w be a node and v 1 , . . . , v m its immediate out-neighbours (i.e., the nodes v ∈ V s.t. (w, v) ∈ E). Let S denote the corresponding multiset of the states g n (v 1 ), . . . , g n (v m ). We define g n+1 (w) = δ(g n (w), S). We say that g n (w) is the state of w at round n.A CMPA (or resp. k-CMPA) accepts a pointed graph (G, w) if and only if g n (w) ∈ F for some n ∈ N. If g n (w) ∈ F , then we say that the CMPA accepts (G, w) in round n. The computation for FCMPAs is defined analogously (since each FCMPA is a CMPA).Note that extended definitions for automata are in Appendix B.1.First we recall Proposition 3.1. Proposition 3.1. Bounded FCMPAs have the same expressive power as GMSC.To prove Proposition 3.1 (in the end of this subsection), we first prove an auxiliary Lemma B.1 that informally shows that we can translate any GMSC-program into an equivalent program, where the modal depth of the terminal clauses is zero and the modal depth of the iteration clauses is at most one. Then in Lemma B.2 we show with the help of Lemma B.1 that for each GMSC-program we can construct an equivalent bounded FCMPA. Finally, we show in Lemma B.3 that for each bounded FCMPA we can construct an equivalent GMSC-program.We start with an auxiliary result. Lemma B.1. For every Π-program of GMSC, we can construct an equivalent Π-program Γ of GMSC such that the modal depth of each terminal clause of Γ is 0, and the modal depth of each iteration clause of Γ is at most 1.Proof. The proof is similar to the proof of Theorem 11 in [1] (or the proof of Theorem 5.4 in [2] ). We consider an example and conclude that the strategy mentioned in the cited papers can be generalized to our framework.For simplicity, in the example below we consider a program where the modal depth of each terminal clause is zero, since it is easy to translate any program of GMSC into an equivalent GMSC-program, where the modal depth of the terminal clauses is zero. Then from the program of GMSC, where the modal depth of each terminal clause is zero, it is easy to obtain an equivalent GMSC-program where the modal depth of each terminal clause is zero and the modal depth of each iteration clause is at most one.Consider a {q}-program Λ, with the rules X(0) :-⊥, X :-♢ ≥3 (¬♢ ≥2 ♢ ≥1 X ∧ ♢ ≥3 q). The modal depth of the iteration clause of Λ is 3. The program Λ can be translated into an equivalent program of GMSC where the modal depth of the iteration clauses is at most one as follows. First, we define the following subprogram called a "clock":T 1 (0) :-⊤ T 1 :-T 3 T 2 (0) :-⊥ T 2 :-T 1 T 3 (0) :-⊥ T 3 :-T 2 .We split the evaluation of each subformula between corresponding head predicates X 1,1 , X 1,2 , X 2 and X 3 and define their terminal clauses and iteration clauses as follows. The body for each terminal clause is ⊥ and the iteration clauses are defined by• X 1,1 :-(T 1 ∧ ♢ ≥1 X 3 ) ∨ (¬T 1 ∧ X 1,1 ), • X 1,2 :-(T 1 ∧ ♢ ≥3 q) ∨ (¬T 1 ∧ X 1,2 ), • X 2 :-(T 2 ∧ ♢ ≥2 X 1,1 ) ∨ (¬T 2 ∧ X 2 ), • X 3 :-(T 3 ∧ ♢ ≥3 (¬X 2 ∧ X 1,1 )) ∨ (¬T 3 ∧ X 3 ).The appointed predicate of the program is X 3 .Let us analyze how the obtained program works. The program works in a periodic fashion: a single iteration round of Λ is simulated in a 3 step period by the obtained program. The clock (i.e. the head predicates T 1 , T 2 and T 3 ) makes sure that each level of the modal depth is evaluated once during each period in the correct order. For example, if T 2 is true, then the truth of X 2 depends on the truth of ♢ ≥2 X 1,1 and when T 2 is false, then the truth of X 2 stays the same. The head predicate X 3 essentially simulates the truth of X in Λ in the last round of each period. It is easy to show by induction on n ∈ N that for all pointed {q}-labeled graphs (G, w) and for all k∈ [0; 2]: G, w |= X n iff G, w |= X n3+k 3 .With Lemma B.1, it is easy to construct an equivalent bounded FCMPA for any GMSC-program. Lemma B.2. For each Π-program of GMSC, we can construct an equivalent bounded FCMPA over Π.Proof. Let Λ be a (Π, T )-program of GMSC. By Lemma B.1 we obtain an equivalent (Π, T ′ )program Γ where the modal depth is 0 for each terminal clause and at most 1 for each iteration clause. Let k be the width of Γ. We create an equivalent k-FCMPA A Γ as follows.We create a state for each subset q ⊆ Π ∪ T ′ ; these form the state set Q = P(Π ∪ T ′ ).We formulate the initialization function π as follows: π(P ) = q if Π ∩ q = P and for each head predicate X ∈ T ′ (with the terminal clause X(0) :φ) we have that X ∈ q if and only if φ is true when exactly the node label symbols in P are true. (Here it is vital that the terminal clauses have modal depth 0.)Before we define the transition function, we define an auxiliary relation ⊩ for schemata with modal depth at most 1. Let N ∈ M(Q) be a multiset of states and let q be a state. Given a (Π, T )-schema ψ with modal depth at most 1, we define the relation (q, N ) ⊩ ψ recursively as follows: (q, N ) ⊩ ⊤ always, (q, N ) ⊩ p iff p ∈ q, (q, N ) ⊩ X iff X ∈ q, (q, N ) ⊩ ¬φ iff (q, N ) ̸ ⊩ φ, (q, N ) ⊩ φ ∧ θ iff (q, N ) ⊩ φ and (q, N ) ⊩ θ, and (q, N ) ⊩ ♢ ≥ℓ φ iff there is a set Q ′ ⊆ Q of states such that q ′ ∈Q ′ N (q ′ ) ≥ ℓ and (q ′ , ∅) ⊩ φ for all q ′ ∈ Q ′ (note that φ has modal depth 0). Now we shall formulate the transition function δ as follows. Let N ∈ M(Q) be a multiset of states and let q be a state. For each node label symbol p ∈ Π, p ∈ δ(q, N ) iff (q, N ) ⊩ p (i.e. p ∈ q). For each head predicate X ∈ T ′ with the iteration clause X :ψ we have that X ∈ δ(q, N ) if and only if (q, N ) ⊩ ψ. (Here it is crucial that the iteration clauses have modal depth at most 1.)The set of accepting states is defined as follows. If X ∈ q for some appointed predicate X of Γ then q ∈ F ; otherwise q / ∈ F .If G is Π-labeled graph and v is a node in G, then we let v n denote the state of A Γ at v in round n. Moreover, if N is the set of out-neighbours of v, we let N n v denote the multiset {{u n | u ∈ N }}. Then we prove by induction on n ∈ N that for any (Π, T ′ )-schema φ of modal depth 1 and for each pointed Π-labeled graph (G, w), we have(w n , N n w ) ⊩ φ iff G, w |= φ n . If n = 0 we prove by induction on the structure of φ that (w 0 , N 0 w ) ⊩ φ iff G, w |= φ 0 . • Case φ = p ∈ Π: Trivial, since (w 0 , N 0 w ) ⊩ p iff p ∈ w 0 iff G, w |= p iff G, w |= p 0 . • Case φ = X ∈ T ′ : Let ψ X be the body of the terminal clause of X. Now, (w 0 , N 0 w ) ⊩ X iff X ∈ w 0 iff G, w |= ψ X iff G, w |= X 0 .Now, assume that the induction hypothesis holds for (Π, T ′ )-schemata ψ and θ with modal depth at most 1.• Case φ := ¬ψ: Now, (w 0 , N 0 w ) ⊩ ¬ψ iff (w 0 , N 0 w ) ̸ ⊩ ψ. By the induction hypothesis, this is equivalent to G, w ̸ |= ψ 0 which is equivalent to G, w |= ¬ψ 0 .• Case φ := ψ ∧ θ: Now, (w 0 , N 0 w ) ⊩ ψ ∧ θ iff (w 0 , N 0 w ) ⊩ ψ and (w 0 , N 0 w ) ⊩ θ. By the induction hypothesis, this is equivalent to G, w |= ψ 0 and G, w |= θ 0 , which is equivalent to G, w |= ψ 0 ∧ θ 0 .• Case φ := ♢ ≥ℓ ψ: First it is easy to show that for every (Π, T ′ )-schema ψ of modal depth 0 and for every state q of A Γ that (q, ∅) ⊩ ψ iff (q, N ) ⊩ ψ for every multiset N of states of A Γ . Now, (w 0 , N 0 w ) ⊩ ♢ ≥ℓ ψ iff there is a set Q ′ ⊆ Q of states such that q ′ ∈Q ′ N 0 w (q ′ ) ≥ ℓ and (q ′ , ∅) ⊩ ψ for every q ′ ∈ Q ′ iff there is a set N of out-neighbours of w such that |N | ≥ ℓ and (u 0 , N 0 u ) ⊩ ψ for every u ∈ N . By the induction hypothesis this is true iff there is a set N of out-neighbours of w such that |N | ≥ ℓ and G, u |= ψ 0 for every u ∈ N , which is equivalent to G, w |= ♢ ≥ℓ ψ 0 . Now, assume that the induction hypothesis holds for n and let us prove the case for n+1. Similarly to the case n = 0, we prove by induction on structure of φ that (w n+1 , N n+1 w) ⊩ φ iff G, w |= φ n+1 .The proof by induction is almost identical, except in the case where φ = X ∈ T ′ . Let χ X be the body of the iteration clause of X. Then (w n+1 , N n+1 w ) ⊩ X iff X ∈ w n+1 iff (w n , N n w ) ⊩ χ X . By the induction hypothesis, this is equivalent to G, w |= χ n X , which is equivalent to G, w |= X n+1 . Thus, the result above implies that for all pointed Π-labeled graphs (G, w), the automaton A Γ is in the state q at w in round n iff G, w |= X n and G, w |= p for every X, p ∈ q, and G, w ̸ |= X n and G, w ̸ |= p for every p, X / ∈ q. Therefore, by the definition of the set of accepting states we see that A Γ is equivalent to Γ.The converse direction is easier. Note that the definitions for sizes of GMSC-programs and bounded FCMPAs can be found in Appendix A.1. Lemma B.3. For each bounded FCMPA over Π, we can construct an equivalent Π-program of GMSC. The size of the constructed GMSC-program is polynomial in the size of the FCMPA.Proof. The proof below is analogous to the proof of Theorem 1 in [24] . Let Π be a set of node label symbols, and let A = (Q, π, δ, F ) be a k-FCMPA over Π. For each state q ∈ Q, we define a head predicate X q and the corresponding rules as follows. The terminal clause for X q is defined by X q (0) :-P ⊆Π, π(P )=q p∈P p ∧ p∈Π\P ¬p .To define the iteration clause for each X q we first define some auxiliary formulae. Given q, q ′ ∈ Q,we let M k (q, q ′ ) = { S ∈ M k (Q) | δ(q, S) = q ′ }.Notice that the number of multisets S specified by the set M k (q, q ′ ) is finite. Now, for each S ∈ M k (q, q ′ ) we defineφ S := q∈Q, S(q)=n, n<k ♢ =n X q ∧ q∈Q, S(q)=k ♢ ≥k X q .Then the iteration clause for X q is defined by X q :q ′ ∈Q X q ′ → S∈M k (q ′ ,q) φ S . It is easy to show by induction on n ∈ N that for every pointed Π-labeled graph (G, w) it holds that G, w |= X n q if and only if w is in the state q in round n (see [24] for the details; the only difference is swapping sets for multisets). Proof of Proposition 3.1. Note that the proof uses auxiliary results that are introduced in this subsection. Lemma B.2 shows that for every Π-program of GMSC we can construct an equivalent bounded FCMPA over Π. Lemma B.3 shows that for every bounded FCMPA over Π we can construct an equivalent Π-program of GMSC. Thus, we conclude that GMSC has the same expressive power as bounded FCMPAs.First we recall Theorem 3.2.Theorem 3.2. The following have the same expressive power: GNN[F]s, GMSC, and R-simple aggregate-combine GNN[F]s.In the end of this appendix section, we formally prove Theorem 3.2. Informally, this is done in the following steps. First, we note that it is easy to obtain an equivalent bounded FCMPA for a given GNN[F] and by Proposition 3.1 we can translate the bounded FCMPA into an equivalent GMSCprogram. The converse direction is much more interesting. In Lemma B.5 we show that for each GMSC-program we can construct an equivalent R-simple aggregate-combine GNN[F].Before we show how to obtain an equivalent R-simple GNN[F] for each GMSC-program, we first want to modify the programs so that they are easier to handle via R-simple GNN[F]s. In particular, the terminal clauses of a program may involve diamonds, the rules of a program may have differing amounts of nested logical operators, and so may the two conjuncts of each conjunction. Thus we prove a lemma which intuitively shows how to "balance" GMSC-programs such that this is not the case. We let fdepth(φ) denote the formula depth of a schema φ (see the definition of formula depth in Section 2.2). The formula depth of a terminal clause (resp., of an iteration clause) refers to the formula depth of the body of the clause. The formula depth of a GMSC-program is the maximum formula depth of its clauses.Lemma B.4. For each Π-program Λ of GMSC with formula depth D, we can construct an equivalent Π-program Γ of GMSC which has the following properties.1. Each terminal clause is of the form X(0) :-⊥.2. Each iteration clause has the same formula depth max(3, D + 2).3. If φ ∧ θ is a subschema of Λ such that neither φ nor θ is ⊤, then φ and θ have the same formula depth.Proof. First we define a fresh auxiliary predicate I with the rules I(0) :-⊥ and I :-⊤. Informally, we will modify the rules of Λ such that the terminal clauses are simulated by the iteration clauses with the help of I. Then for each head predicate of Λ with terminal clause X(0) :φ and iteration clause X :ψ we define new rules in Γ as follows: X(0) :-⊥ and X :-(¬I ∧ φ) ∨ (I ∧ ψ). Now, the formula depth of Γ is max(3, D + 2).First, we "balance" the formula depth of each iteration clause in Γ according to the second point in the statement of the lemma. Let d be the formula depth of an iteration clause X :ψ, letD ′ = max(3, D + 2) and let n = D ′ -d. If n is even, then the new iteration clause for X is X :-(¬) n ψ, where (¬) n = ¬ • • • ¬ denotes n nested negations. If n is odd, then the new iteration clause for X is X :-(¬) n-1 (ψ ∧ ⊤).In either case, the new iteration clause for X has formula depth D ′ .Then we show how to "balance" each subschema of Γ according to the third point in the statement of the lemma as follows. Let φ ∧ ψ be a subschema of Γ such that neither φ nor ψ is ⊤, and w.l.o.g. assume that fdepth(φ) < fdepth(ψ) and let n = fdepth(ψ) -fdepth(φ). If n is even, then we replace φ ∧ ψ in Γ with (¬) n φ ∧ ψ. If n is odd, then we replace φ ∧ ψ in Γ with (¬) n-1 (φ ∧ ⊤) ∧ ψ.We have now obtained the desired Γ. It is easy to see that Γ is equivalent to Λ as follows. If X is a head predicate that appears in both Λ and Γ, then for each n ∈ N and for each pointed Π-labeled graph, we have G, w |= X n w.r.t. Λ iff G, w |= X n+1 w.r.t. Γ. In Γ, the auxiliary predicate I makes sure that each head predicate X in Γ that appears in Λ simulates in round 1 the corresponding terminal clause of X in Λ and in subsequent rounds simulates the corresponding iteration clause of X in Λ. Furthermore, for each head predicate X in Γ and for each pointed Π-labeled graph (G, w), we have G, w ̸ |= X 0 w.r.t. Γ. Thus, Γ and Λ are equivalent. • u has one bit per each (distinct) subschema of a body of an iteration clause in Γ as well as for each head predicate, and v 1 keeps track of their truth values, and• w has D + 1 bits and it keeps track of the formula depth that is currently being evaluated.Therefore, G Γ is a GNN[F] over (Π, N + D + 1), where N is the number of (distinct) subschemata of the bodies of the iteration clauses of Γ as well as head predicates, and D is the maximum formula depth of the bodies of the iteration clauses. In order to be able to compute values, the floating-point system for G Γ is chosen to be high enough. More precisely, we choose a floating-point system S which express all integers from 0 at least up to K max , where K max is the width of Γ. Note that 0s and 1s are also represented in the floating-point system S. Note that although feature vectors exist that have elements other than 1s and 0s, they are not used.Next we define the functions π and COM, and the set F of accepting states for G Γ . (Note that AGG is just the sum in increasing order.) We assume an enumeration SUB(Γ) := (φ 1 , . . . , φ N ) of subschemata and head predicates in Γ such that if φ k is a subschema of φ ℓ , then k ≤ ℓ. The initialization function π of G Γ with input P ⊆ Π outputs a feature vector v ∈ {0, 1} N +D+1 , where the value of each component corresponding to a node label symbol is defined as follows: the component for p is 1 iff p ∈ P . The other components are 0s (excluding the possible subschema ⊤ which is assigned 1, as well as the very last (N + D + 1)th bit which is also assigned 1).Recall that S is the floating-point system for G Γ For all ℓ ≤ N we define as follows.• Ifφ ℓ ∈ Π ∪ {⊤}, then C ℓ,ℓ = 1.• If φ ℓ is a head predicate X with the iteration clause X :φ k , then C k,ℓ = 1.• If φ ℓ = φ j ∧ φ k , then C j,ℓ = C k,ℓ = 1 and b ℓ = -1. • If φ ℓ = ¬φ k , then C k,ℓ = -1 and b ℓ = 1. • If φ ℓ = ♢ ≥K φ k , then A k,ℓ = 1 and b ℓ = -K + 1.Next, we define that the bottom-right (D + 1) × (D + 1) submatrix of C is the (D + 1) × (D + 1) identity matrix, except that the rightmost column is moved to be the leftmost column. More formally, for all N + 1 ≤ ℓ < N + D + 1 we have C ℓ,ℓ+1 = 1 and also C N +D+1,N +1 = 1. Lastly, we define that all other elements in C, A and b are 0s. Finally, we define that v ∈ F if and only if v ℓ = 1 (i.e., the ℓth value of v is 1) for some appointed predicate φ ℓ and also v N +D+1 = 1.Recall that the formula depth of Γ is D. Let v(w) t i denote the value of the ith component of the feature vector in round t at node w. It is easy to show by induction that for all n ∈ N, for all pointed Π-labeled graphs (G, w), and for every schema φ ℓ in SUB(Γ) of formula depth d, we have [5] for the details), but we go over the proof as there are some additional considerations related to recurrence.v(w) n(D+1)+d ℓ = 1 if G, w |= φ n ℓ and v(w) n(D+1)+d ℓ = 0 if G, w ̸ |= φ n ℓ .For the base case, let n = 0. We prove the case by induction over the formula depth d of φ ℓ . First, let d = 0. • Case 2: φ ℓ = X, where X is a head predicate of Γ. Now v(w) 0 ℓ = 0 due to the definition of the initialization function π, and G, w ̸ |= X 0 because each head predicate of Γ has the terminal clause ⊥. Now, assume the claim holds for n = 0 for any formulae φ j , φ k with formula depth d -1. We show that the claim holds for n = 0 for formulae φ ℓ of formula depth d.• Case 1: φ ℓ ∈ Π ∪ {⊤}. Now v 0 ℓ = 1 and G, w |= ⊤ 0 if φ ℓ = ⊤. If φ ℓ = p ∈ Π,• Case 3: φ ℓ = φ j ∧ φ k for some φ j , φ k (recall that Γ only contains conjunctions where both conjuncts have the same formula depth if neither of them are ⊤). This means we have C j,ℓ = C k,ℓ = 1 and b ℓ = -1. Moreover, C m,ℓ = 0 for all m ̸ = j, k and A m,ℓ = 0 for all m. Now v(w) d ℓ = ReLU * v(w) d-1 j + v(w) d-1 k -1 . Thus v(w) d ℓ = 1 iff v(w) d-1 j = v(w) d-1 k = 1.v(w) d ℓ = ReLU * -v(w) d-1 k + 1 . Thus v(w) d ℓ = 1 iff v(w) d-1 k = 0. By the induction hypothesis this is equivalent to G, w ̸ |= φ 0 k which is further equivalent to G, w |= (¬φ k ) 0 . Likewise, v(w) d ℓ = 0 iff v(w) d-1 k = 1. By the induction hypothesis this is equivalent to G, w |= φ 0 k which is equivalent to G, w ̸ |= (¬φ k ) 0 .• Case 5: φ ℓ = ♢ ≥K φ k for some φ k . This means we have A k,ℓ = 1 and b ℓ = -K + 1.Moreover, C m,ℓ = 0 for all m and A m,ℓ = 0 for all m ̸ = k. Nowv(w) d ℓ = ReLU * SUM S {{ v(v) d-1 k | (w, v) ∈ E }} -K + 1 ,where SUM S : M(S) → S is the sum of floating-point numbers in S in increasing order (see Section 2.1 for more details) and E is the set of edges of G. Thus v(w) d ℓ = 1 iff there are at least K out-neighbours v of w such that v(v) d-1 k = 1. By the induction hypothesis, this is equivalent to there being at least K out-neighbours v of w such that G, v |= φ 0 k which is further equivalent to G, w |= (♢ ≥K φ k ) 0 . Likewise, v(w) d ℓ = 0 iff there are fewer than K out-neighbours v of w such that v(v) d-1 k = 1. By the induction hypothesis, this is equivalent to there being fewer than K out-neighbours v of w such that G, v |= φ 0 k which is equivalent to G, w ̸ |= (♢ ≥K φ k ) 0 .Next, assume the claim holds for n for all formulae of any formula depth. We show that it also holds for n + 1. We once again prove the claim by structure of φ ℓ . Cases 3, 4 and 5 are handled analogously to how they were handled in the case n = 0, so we only consider cases 1 and 2.• Case 1: φ ℓ ∈ Π ∪ {⊤}. This means we have C ℓ,ℓ = 1 and b ℓ = 0. Moreover, C m,ℓ = 0 for all m ̸ = ℓ and A m,ℓ = 0 for all m. Now v(w)(n+1)(D+1) ℓ = ReLU * v(w) n(D+1)+D ℓ .Thus we see that v(w)(n+1)(D+1) ℓ = v(w) n(D+1)+D ℓand a trivial induction shows that also v(w) .EQUATIONThus v(w)(n+1)(D+1) ℓ = 1 iff v(w) n(D+1)+D k = 1. By the induction hypothesis this is equivalent to G, w |= φ n k which is equivalent to G, w |= X n+1 . Likewise, v(w) (n+1)(D+1) ℓ = 0 iff v(w) n(D+1)+D k = 0. By the induction hypothesis this is equiva- lent to G, w ̸ |= φ n k which is equivalent to G, w ̸ |= X n+1 .This concludes the induction.We also know for all n ≥ 1 and all By the initialization this means for all 1 ≤ ℓ, ℓ ′ ≤ D + 1 and all n ∈ N that v(w)N + 1 ≤ ℓ < N + D + 1 that v(w) n ℓ+1 = v(w) n-1 ℓ and v(w) n N +1 = v(w) n-1 N +D+1 . This is because C ℓ,ℓ+1 = 1, C ℓ ′ ,n(D+1)+ℓ ′ N +ℓ = 1iff ℓ ′ = ℓ and 0 otherwise. Specifically, this means that v(w)n(D+1)+ℓ ′ N +D+1 = 1 iff ℓ ′ = D + 1 and v(w) n(D+1)+ℓ ′ N +D+1 = 0 otherwise.Thus if φ ℓ is an appointed predicate X of Γ, then we know for all n ∈ N that G, w |= X n iff v(w)n(D+1) ℓ= 1 and we also know that v(w)n(D+1) N +D+1 = 1 and thereby v(w) n(D+1) ∈ F . Thus G Γ is equivalent to Γ.Since G Γ is equivalent to Γ which is equivalent to Λ, we are done.We note that the proof of Lemma B.5 generalizes for other types of GNN[F]s, such as the type described below. Let S = ((p, n, β), +, •) be the floating-point system, where p = 1, n = 1 and β = K max + 1, where K max is again the maximum width of the rules of Γ in the proof above. We believe that the proof generalizes for other floating-point systems which can represent all nonnegative integers up to K max . Recall that K max is the width of Γ in the proof of Lemma B.5. Consider a class of GNN[F]s over S with dimension 2(N + D + 1) (twice that in the proof above) where the aggregation function is SUM S : M(S) → S (the sum of floating-point numbers in S in increasing order applied separately to each element of feature vectors) and whose combination function COM : S 2(N +D+1) × S 2(N +D+1) → S 2(N +D+1) is defined byCOM (x, y) = ReLU(x • C + y • A + b),where C, A ∈ S 2(N +D+1)×2(N +D+1) are matrices, b ∈ S 2(N +D+1) is a bias vector and ReLU is the rectified linear unit defined by ReLU(x) := max(0, x) as opposed to ReLU * . The last 2(D + 1) elements of feature vectors function as they do above, counting the 2(D + 1) steps required each time an iteration of Γ is simulated (here the computation takes twice as long compared to above). The first 2N elements calculate the truth values of subformulae as before, but now each calculation takes two steps instead of one as each subschema is assigned two elements instead of one. The first of these elements calculates the truth value of the subschema as before. However, due to the use of ReLU instead of ReLU * the value of the element might be more than 1 if the subschema is of the form ♢ ≥K φ k . Thus, the second element normalizes the values by assigning a weight of K max ensuring that each positive value becomes K max and then assigning the bias -K max + 1 to bring them all down to 1. More formally, for each subschema φ ℓ , let ℓ be the first and N + ℓ the second element associated with φ ℓ . In the initialization step we define that if φ ℓ ∈ P ⊆ Π or φ ℓ = ⊤, then π(P ) N +ℓ = 1 and other elements of π(P ) are 0s. Now we define as follows for all 1 ≤ ℓ ≤ N .• If φ ℓ ∈ Π ∪ {⊤}, then C N +ℓ,ℓ = 1. • If φ ℓ is a head predicate X with the iteration clause X :-φ k , then C N +k,ℓ = 1. • If φ ℓ = φ j ∧ φ k , then C N +j,ℓ = C N +k,ℓ = 1 and b ℓ = -1. • If φ ℓ = ¬φ k , then C N +k,ℓ = -1 and b ℓ = 1. • If φ ℓ = ♢ ≥K φ k , then A N +k,ℓ = 1 and b ℓ = -K + 1.In each of the above cases we also define that C ℓ,N +ℓ = K max and b N +ℓ = -K max + 1. Lastly for all 2N +1 ≤ ℓ < 2(N +D+1) we define (as before) that C ℓ,ℓ+1 = 1 and also C 2(N +D+1),2D+1 = 1. All other elements of C, A and b are 0s. The set F of accepting feature vectors is defined such that v ∈ F iff v N +ℓ = 1 for some appointed predicate φ ℓ and also v 2(N +D+1) = 1. It is then straightforward to prove for all n ∈ N, for all pointed Π-labeled graphs (G, w) and for every schemaφ ℓ ∈ SUB(Γ) of formula depth d that v(w) 2n(D+1)+2d-1 ℓ ≥ 1 and v(w) 2n(D+1)+2d N +ℓ = 1 if G, w |= φ n ℓ and v(w) 2n(D+1)+2d-1 ℓ = v(w) 2n(D+1)+2d N +ℓ = 0 if G, w ̸ |= φ n ℓ .The proof is similar to the above, but we also need to show that normalization works as intended, i.e., v(w)2n(D+1)+2d-1 ℓ ≥ 1 implies v(w) 2n(D+1)+2d N +ℓ = 1 and v(w) 2n(D+1)+2d-1 ℓ = 0 implies v(w) 2n(D+1)+2d N +ℓ= 0. To see this, observe that C ℓ,N +ℓ = K max and b N +ℓ = -K max + 1 and also C ℓ ′ ,N +ℓ = 0 for all ℓ ′ ̸ = ℓ and A ℓ ′ ,N +ℓ = 0 for all ℓ ′ . Thusv(w) 2n(D+1)+2d N +ℓ = ReLU K max • v(w) 2n(D+1)+2d-1 ℓ -K max + 1 , which is 0 if v(w) 2n(D+1)+2d-1 ℓ = 0 and 1 if v(w) 2n(D+1)+2d-1 ℓ ≥ 1 (because by the choice of S we have K max • x = K max for all x ∈ S, x ≥ 1).Having proved Lemma B.5, we are now ready to conclude the main theorem of this appendix section expressed below. The proof of Theorem 3.3 is in the end of this subsection but we need some auxiliary results first. We show in Lemma B.7 that we can construct an equivalent counting type automaton over Π for each Π-formula of ω-GML. Informally, to do this, we first define a Π-formula of GML called the "full graded type of modal depth n" for each pointed graph, which expresses all the local information of its neighbourhood up to depth n. We show in Proposition B.6 that for each ω-GML-formula there is a logically equivalent disjunction of types. We also define counting type automata that compute the type of modal depth n of each node in every round n. The accepting states of the resulting automaton are exactly those types that appear in the disjunction of types.Then we show in Lemma B.9 that for each CMPA over Π we can construct an equivalent Π-formula of ω-GML. Informally, to do this we first prove in Lemma B.8 that two pointed graphs that satisfy the same full graded type of modal depth n also have identical states in each round ℓ ≤ n in each CMPA. For each n ∈ N, we consider exactly those full graded types of modal depth n which are satisfied by some pointed graph that is accepted by the automaton in round n. We obtain the desired ω-GML-formula by taking the disjunction of all these types across all n ∈ N.By similar arguments, we also obtain Theorem B.10 which is analogous to Theorem 3.3 but restricted to bounded CMPAs and width-bounded ω-GML, which involves defining analogous widthbounded concepts. Now, we start formalizing the proof of Theorem 3.3. To show that for each ω-GML-formula we can construct an equivalent CMPA, we need to define the concepts of graded Π-types, full graded Π-types and counting type automata. The graded Π-type of modal depth n and width k of a pointed Π-labeled graph (G, w) is a Π-formula of GML that contains all the information from the n-neighbourhood of w (according to outgoing edges), with the exception that at each distance from w we can only distinguish between at most k identical branches. The full graded Π-type of modal depth n lifts this limitation and contains all the information from the neighbourhood of depth n of w. A counting type automaton of width k is a k-CMPA that calculates the graded Π-type of modal depth n and width k of a node in each round n. Likewise, we define counting type automata which calculate the full graded Π-type of modal depth n of a node in each round n.Let Π be a set of node label symbols, let (G, w) be a pointed Π-labeled graph and let k, n ∈ N. The graded Π-type of width k and modal depth n of (G, w) (denoted τ(G,w) k,n) is defined recursively as follows. For n = 0 we define thatτ (G,w) k,0 := pi∈λ(w) p i ∧ pi / ∈λ(w) ¬p i .Assume we have defined the graded Π-type of width k and modal depth n of all pointed Π-labeled graphs, and let T k,n denote the set of such types. The graded Π-type of (G, w) of width k and modal depth n + 1 is defined as follows:τ (G,w) k,n+1 := τ (G,w) k,0 ∧ k-1 ℓ=0 { ♢ =ℓ τ | τ ∈ T k,n and G, w |= ♢ =ℓ τ } ∧ { ♢ ≥k τ | τ ∈ T k,n and G, w |= ♢ ≥k τ }.Canonical bracketing and ordering is used to ensure that no two types are logically equivalent, and thus each pointed Π-labeled graph has exactly one graded Π-type of each modal depth and width.A counting type automaton of width k over Π is a k-CMPA defined as follows. The set Q of states is the set n∈N T k,n of all graded Π-types of width k (of any modal depth). The initialization function π :P(Π) → Q is defined such that π(P ) = τ (G,w) k,0where (G, w) is any pointed Π-labeled graph satisfying exactly the node label symbols in P ⊆ Π. Let N : T k,n → N be a multiset of graded Π-types of width k and modal depth n, and let τ be one such type (note that T k,n is finite for any k, n ∈ N). Let τ 0 be the unique type of modal depth 0 in T k,n that does not contradict τ . We define the transition function δ :Q × M(Q) → Q such that δ(τ, N ) = τ 0 ∧ k-1 ℓ=0 { ♢ =ℓ σ | N (σ) = ℓ } ∧ { ♢ ≥k σ | N (σ) ≥ k },For other N and τ that do not all share the same modal depth, we may define the transition as we please such that δ(q, N ) = δ(q, N |k ) for all q and N .We similarly define the full graded Π-type of modal depth n of a pointed Π-labeled graph (G, w) (denoted by τ (G,w) n) which contains all the local information of the n-depth neighbourhood of (G, w) with no bound on width. For n = 0, we define that τ(G,w) 0 = τ (G,w) k,0for any k ∈ N. Assume that we have defined the full graded Π-type of modal depth n of all pointed Π-labeled graphs, and let T n be the set of such full types. The full graded Π-type of modal depth n + 1 of (G, w) is defined as follows:τ (G,w) n+1 := τ (G,w) 0 ∧ ℓ≥1 { ♢ =ℓ τ | τ ∈ T n , (G, w) |= ♢ =ℓ τ } ∧ ♢ =|N (w)| ⊤,where N (w) is the set of out-neighbours of w. The formula tells exactly how many out-neighbours of a node satisfy each full graded type of the previous modal depth; to keep the formulae finite (over finite graphs), instead of containing conjuncts ♢ =0 τ it tells exactly how many out-neighbours a node has.A counting type automaton over Π is a CMPA defined as follows. The set of states is the set of all full graded Π-types. The initialization function π :P(Π) → Q is defined such that π(P ) = τ (G,w) 0where (G, w) is any pointed Π-labeled graph satisfying exactly the node label symbols in P . Let N : T n → N be a multiset of full graded Π-types of some modal depth n, and let τ be one such type. Let τ 0 be the unique full type of modal depth 0 in T n that does not contradict τ . We define the transition function δ :Q × M(Q) → Q such that δ(τ, N ) = τ 0 ∧ ℓ≥1 { ♢ =ℓ σ | N (σ) = ℓ } ∧ ♢ =|N | ⊤,For other N and τ that do not all share the same modal depth, we may define the transition as we please.We prove the following useful property. Proposition B.6. Each Π-formula φ of modal depth n and width k of GML has 1. a logically equivalent countably infinite disjunction of full graded Π-types of modal depth n and 2. a logically equivalent finite disjunction of graded Π-types of width k and modal depth n.Proof. First we prove the case for graded types of width k, then we prove the case for full graded types. Let T k,n , as above, denote the set of all graded Π-types of width k and modal depth n.Let Φ = { τ ∈ T k,n | τ |= φ } and ¬Φ = { τ ∈ T k,n | τ |= ¬φ }, and let Φ denote the disjunction of the types in Φ. Note that this disjunction is finite since the set T k,n is finite. Obviously we have that Φ ∩ ¬Φ = ∅ and Φ |= φ. To show that φ |= Φ, it suffices to show that Φ ∪ ¬Φ = T k,n . Assume instead that τ ∈ T k,n \ (Φ ∪ ¬Φ). Then there exist pointed Π-labeled graphs (G, w) and (H, v) that satisfy τ such that G, w |= φ and H, v |= ¬φ. Since (G, w) and (H, v) satisfy the same graded Π-type of modal depth n and width k, there can be no Π-formula of GML of modal depth at most and width at most k that distinguishes (G, w) and (H, v), but φ is such a formula, which is a contradiction. Ergo, Φ and φ are logically equivalent.In the case of full graded types we first observe that the set T n of full graded Π-types of modal depth n is countable. Thus the setsΦ = { τ ∈ T n | τ |= φ } and ¬Φ = { τ ∈ T n | τ |= ¬φ }are also countable. Now, with the same proof as for graded types of width k, we can show that Φ and φ are logically equivalent. Therefore, φ is also logically equivalent to a countably infinite disjunction of full graded Π-types of modal depth n.Now, we are ready to show the translation from ω-GML to CMPAs. Lemma B.7. For each Π-formula of ω-GML, we can construct an equivalent counting type automaton over Π. If the formula has finite width k, we can also construct an equivalent counting type automaton of width k.Proof. Assume the class K of pointed Π-labeled graphs is expressed by the countable disjunction ψ := φ∈S φ of Π-formulae φ of GML.First, we prove the case without the width bound. By Proposition B.6, each φ ∈ S is logically equivalent with a countably infinite disjunction φ * of full graded Π-types of GML such that the modal depth of φ * is the same as the modal depth of φ. We define a counting type automaton A whose set F of accepting states is the set of types that appear as disjuncts of φ * for any φ ∈ S. Now (G, w) ∈ K if and only if G, w |= ψ if and only if G, w |= τ for some τ ∈ F if and only if the state of (G, w) is τ in round n in A, where n is the modal depth of τ . Ergo, A accepts exactly the pointed Π-labeled graphs in K.The case for the width bound is analogous. First with Proposition B.6 we transform each disjunct φ ∈ S to a finite disjunction φ + of graded Π-types with the same width and modal depth as φ.Then, for ψ we construct an equivalent type automaton of width k, where the set of accepting states is the set of graded types of width k that appear as disjuncts of φ + for any φ ∈ S.Before we prove Lemma B.9 we prove another helpful (and quite obvious) lemma. Lemma B.8. Two pointed Π-labeled graphs (G, w) and (H, v) satisfy exactly the same full graded Π-type of modal depth n (respectively, graded Π-type of width k and modal depth n) if and only if they share the same state in each round up to n for each CMPA (resp., each k-CMPA) over Π.Proof. We prove the claim by induction over n without the width bound, since again the case for the width bound is analogous. Let n = 0. Two pointed Π-labeled graphs (G, w) and (H, v) share the same full graded Π-type of modal depth 0 if and only if they satisfy the exact same node label symbols if and only if each initialization function π assigns them the same initial state. Now assume the claim holds for n. Two pointed Π-labeled graphs (G, w) and (H, v) satisfy the same full graded Π-type of modal depth n + 1 if and only if 1) they satisfy the same full graded Π-type of modal depth 0 and 2) for each full graded Π-type τ of modal depth n, they have the same number of neighbors that satisfy τ . Now 1) holds if and only if (G, w) and (H, v) satisfy the same node label symbols, and by the induction hypothesis 2) is equivalent to the neighbors of (G, w) and (H, v) sharing (pair-wise) the same state in each round (up to n) for each CMPA. This is equivalent to (G, w) and (H, v) satisfying the same full graded Π-type of modal depth 0, and receiving the same multiset of states as messages in round n in each CMPA. By the definition of the transition function, this is equivalent to (G, w) and (H, v) sharing the same state in round n + 1 for each CMPA.Now, we are able to show the translation from CMPAs to ω-GML.Lemma B.9. For each CMPA (respectively, each k-CMPA) over Π, we can construct an equivalent Π-formula of ω-GML (resp., of width k).Proof. We prove the claim without the width bound, since the case with the width bound is analogous. Assume that the class K of pointed Π-labeled graphs is expressed by the counting message passing automaton A over Π. Let T be the set of all graded Π-types and letΦ = { τ (G,w) n ∈ T | A accepts the pointed Π-labeled graph (G, w) ∈ K in round n }.We define the countable disjunction τ ∈Φ τ and show that G, w |= τ ∈Φ τ if and only if A accepts (G, w). Note that Φ is countable since T is countable.If G, w |= τ ∈Φ τ , then G, w |= τ (H,v) nfor some pointed Π-labeled graph (H, v) accepted by A in round n. This means that (G, w) and (H, v) satisfy the same full graded Π-type of modal depth n. By Lemma B.8, this means that (G, w) and (H, v) share the same state in A in each round ℓ ≤ n.Since A accepts (H, v) in round n, A also accepts (G, w) in round n. Conversely, if A accepts (G, w) in round n, then τ (G,w) n ∈ Φ and thus G, w |= τ ∈Φ τ .Finally, we prove Theorem 3.3.Proof of Theorem 3.3. Note that the proof uses auxiliary results that are introduced in this subsection. Lemma B.7 shows that for each Π-formula of ω-GML we can construct an equivalent CMPA over Π and Lemma B.9 shows that for each CMPA over Π we can construct an equivalent Π-formula of ω-GML.By Lemma B.7 and Lemma B.9, it is also straightforward to conclude a similar result for bounded CMPAs and width-bounded ω-GML-formulae. Informally, Theorem 3.4 is proved as follows (in the end of this section we give a formal proof). We first prove Lemma B.12 which shows that we can translate any GNN[R] into an equivalent ω-GMLformula. To prove Lemma B.12, we need to first prove an auxiliary result Lemma B.11, which shows that if two pointed graphs satisfy the same full graded type of modal depth n, then those two pointed graphs share the same feature vector in each round (up to n) with any GNN[R]. For these results, we need graded types which were introduced in Section B.4.Informally, the converse direction (Lemma B.13) is proved as follows. We first translate the Πformula of ω-GML into an equivalent CMPA over Π by Theorem 3.3. Then we translate the equivalent CMPA into an equivalent counting type automaton (again, see Section B.4 for the definition of counting type automata). Then we prove that we can construct an equivalent GNN[R] for each counting type automaton. Informally, we encode each state of the counting type automaton into an integer and the GNN[R] can use them to mimic the type automaton in every step.In both directions, we also consider the case where GNN[R]s are bounded and the ω-GML-formulae are width-bounded.Before proving Lemma B.12, we first establish the following useful lemma. Lemma B.11. Two pointed Π-labeled graphs (G, w) and (H, v) satisfy exactly the same full graded Π-type of modal depth n (respectively the same graded Π-type of width k and modal depth n) if and only if they share the same state in each round (up to n) for each unbounded GNN[R] (resp., GNN[R] with bound k) over Π.Proof. The proof is analogous to that of Lemma B.8.With the above lemma, we are ready to prove Lemma B.12. Lemma B.12. For each GNN[R] G over Π, we can construct an equivalent Π-formula of ω-GML. Moreover, if G is bounded with the bound k, we can construct an equivalent Π-formula of ω-GML of width k.Proof. Assume that G is a GNN[R] over (Π, d). Let K be the class of pointed Π-labeled graphs expressed by G. Now letΦ = { τ (G,w) n | G accepts the pointed Π-labeled graph (G, w) ∈ K in round n }, where τ (G,w) nis the full graded Π-type of modal depth n of (G, w) (see Section B.4). Note that there are only countably many formulae in Φ since there are only countably many full graded Π-types. Consider the counting type automaton A over Π, where Φ is the set of accepting states. We will show that A accepts (G, w) if and only if G accepts (G, w).If (G, w) is accepted by A, then G, w |= τ (H,v) nfor some pointed Π-labeled graph (H, v) accepted by G in round n. This means that (G, w) and (H, v) satisfy the same full graded Π-type of modal depth n. By Lemma B.11, this means that (G, w) and (H, v) share the same state in G in each roundℓ ≤ n. Since G accepts (H, v) in round n, G also accepts (G, w) in round n. Conversely, if G accepts (G, w) in round n, then τ (G,w) n∈ Φ and thus (G, w) is accepted by A by the definition of counting type automata. Thus A and G are equivalent. By Theorem 3.3 we can translate the type automaton A into an equivalent Π-formula of ω-GML. Therefore, for G we can obtain an equivalent ω-GML-formula.Next consider the case where G is bounded. We follow the same steps as above with the following modification: instead of constructing a set of full graded types, we construct a set of graded types of width k:Φ = { τ (G,w) k,n| G accepts the pointed Π-labeled graph (G, w) ∈ K in round n }. The reasoning of the second paragraph is then modified to refer to graded types of width k and GNNs with the bound k respectively using Lemma B.11. By Theorem B.10 we obtain an equivalent widthbounded ω-GML-formula for the counting type automaton of width k.We then show the other direction of Theorem 3.4 in the next lemma. We first define a graph neural network model that is used as a tool in the proof that follows. A recurrent graph neural network over natural numbers GNN[N] over (Π, d), is a GNN[R] over (Π, d) where the feature vectors and the domains and co-domains of the functions are restricted to N d instead of R d . Lemma B.13. For each Π-formula of ω-GML, we can construct an equivalent GNN[R] over (Π, 1). Moreover, for each Π-formula of ω-GML of width k, we can construct an equivalent bounded GNN[R] over (Π, 1) with the bound k.Proof. We first give an informal description, and then we give a formal proof. We show that each counting type automaton over Π can be translated into an equivalent GNN[N] over (Π, 1), which suffices since counting type automata have the same expressive power as ω-GML and CMPAs by Lemma B.9 and by Lemma B.7. Informally, each counting type automaton can be simulated by a graph neural network as follows. Each full type has a minimal tree graph that satisfies the full type. Each such tree can be encoded into a binary string (or more precisely into an integer) in a standard way. These binary strings are essentially used to simulate the computation of the counting type automaton. At each node and in each round, the GNN[N] simulates the counting type automaton by combining the multiset of binary strings obtained from its out-neighbours and the local binary string into a new binary string that corresponds to the minimal tree that satisfies the type that would be obtained by the counting type automaton in the same round at the same node. Now, we formally prove the statement. Let A be a counting type automaton. Now we create an equivalent GNN[N] G over (Π, 1) as follows. Each full graded type is converted into the unique finite rooted tree graph (T , r) of the same depth as the modal depth of the full type. This graph is encoded into a binary string (in a standard way) as follows.• The first n bits of the string are 1s, telling the number of nodes in the tree; we choose some ordering v 1 , . . . , v n for the nodes. (A natural ordering would be to start with the root, then list its children, then its grandchildren, etc.. The children of each node can be ordered in increasing order of magnitude according to the encodings of their generated subtrees.Another option is to assume that the domain of the tree is always [n] for some n ∈ N and use the standard ordering of integers.) This is followed by a 0.• The next nk bits are a bit string b that tells which node label symbol is true in which node; for each ℓ ∈ [n] and i ∈ [k], the ((ℓ -1)k + i):th bit of b is 1 if and only if T , v ℓ |= p i .• Finally, the last n 2 bits form a bit string b ′ , where for each i, j ∈ [n], the ((i -1)n + j):th bit of b ′ is 1 if and only if (v i , v j ) ∈ E, i.e., there is an edge from v i to v j .The GNN G operates on these binary strings (we can either use the integers encoded in binary by the binary strings, or interpret the binary strings as decimal strings). In round 0, the initialization function maps each set of node label symbols to the encoding of the unique one-node tree graph where the node satisfies exactly the node label symbols in question. In each subsequent round n, each node receives a multiset N of binary encodings of full graded types of modal depth n -1. The aggregation function calculates a binary string that encodes the following graph:• The graph contains a node r where every node label symbol is false.• For each copy of each element in the multiset N , the graph contains a unique copy of the rooted tree encoded by that element.• There is an edge from r to the root of each of these rooted trees; the result is itself a rooted tree where r is the root.The combination function receives a binary string corresponding to the node's full graded type τ of modal depth n -1, as well as the string constructed above. It takes the above string and modifies the bits corresponding to the node label symbols at the root; it changes them to be identical to how they were in the root in τ . The obtained binary encoding is the feature of the node in round n.It is clear that the constructed GNN[N] G calculates a node's full graded type of modal depth n in round n. This is because our construction is an embedding from full graded types to natural numbers. Any other such embedding would also suffice, as the images of the aggregation and combination function are always full graded types and GNN[R]s do not limit the aggregation and combination functions. We can choose the accepting states to be the numbers that encode the accepting states in the corresponding counting type automaton A, in which case the GNN accepts exactly the same pointed graphs as A.Now consider the case where A is a counting type automaton of width k. We follow similar steps as above with the following modifications.• We convert each graded type of width k and modal depth n to a corresponding rooted tree. We choose the tree with depth n and the least amount of branches; in other words, each node has at most k identical out-neighbours.• The aggregation function of G constructs a graph in the same way as above, except that it creates at most k copies of a graph encoded by an element in the multiset.It is clear that the resulting GNN is bounded, as the aggregation function is bounded by k.We have now shown that for each counting type automaton we can construct an equivalent GNN[R] (or more precisely an equivalent GNN[N]) and respectively for each counting type automaton of width k we can construct an equivalent bounded GNN[R] (or more precisely an equivalent bounded). Therefore, by Lemma B.9 and by Lemma B.7 for each formula of ω-GML (and respectively for each CMPA) we can construct an equivalent GNN[R]. Analogously, for each widthbounded formula of ω-GML (and resp., for each bounded CMPA) we can construct an equivalent bounded GNN[R].We are now ready to formally prove Theorem 3.4.Proof of Theorem 3.4. Note that the proof uses auxiliary results that are introduced in this subsection. By Lemma B.12 we can construct an equivalent Π-formula of ω-GML for each GNN[R] over Π. By Lemma B.13 we can construct an equivalent GNN[R] over Π for each Π-formula of ω-GML.B.6 Proof of Remark 3.5In this section we formally prove the claims in Remark 3. Proof. We encode the FCMPA fully into the GNN[F]. First we give an informal description. The feature vectors encode which state a node is in using one-hot encoding, i.e., only the bit corresponding to the occupied state is 1 and others are 0. For a received multiset M of feature vectors, the aggregation function encodes the function δ M : Q → Q, δ M (q) = δ(q, M ) into a vector, i.e., it tells for each state q i which state q j satisfies δ(q i , M ) = q j . To encode such a function we need |Q| 2 components in the feature vector. Finally, the combination function receives (the encodings of) q and δ M and computes (the encoding of) δ M (q). Now we define the construction formally. Let Π be a set of node label symbols. Let A = (Q, π, δ, F ) be an FCMPA over Π. Assume some arbitrary ordering < Q between the states Q. Let q 1 , . . . , q |Q| enumerate the states of Q w.r.t. < Q . Given a multiset M ∈ M(Q) the function δ M : Q → Q, δ M (q) = δ(q, M ) specified by M is possible to encode to the binary string d M ∈ {0, 1} |Q| 2 as follows. If δ M (q i ) = q j , then the ((i -1)|Q| + j):th bit of d M is 1; the other bits are 0. That is, d M encodes the function δ M in binary.We construct a GNN over (Π, |Q| 2 ) over a floating-point system S that includes at least 0 and 1 (that is to say, small floating-point systems suffice). For all i ≤ |Q|, we let d i ∈ S |Q| 2 denote the one-hot string where exactly the ith bit is 1 and the other bits are 0s.• Let P ⊆ Π. The initialization function π ′ is defined as π ′ (P ) = d i where π(P ) = q i .• The aggregation function AGG is defined as follows. Assume that the multiset M contains only one-hot strings d i , where i ≤ |Q|. Now M corresponds to a multiset M * , where each d i is replaced by q i . Then AGG(M ) is d M * . Otherwise, the aggregation function is defined in an arbitrary way.• The combination function COM is defined as follows. Let d, d ′ ∈ S |Q| 2 such that d = d i is a one-hot string for some i ≤ |Q| and d ′ = d M for some multiset M ∈ M(Q). Then we define that COM(d, d ′ ) = COM(d i , d M ) = d j if and only if δ M (q i ) = q j . Otherwise COM is defined in an arbitrary way.• The set F ′ of accepting states is defined as follows. If d = d j is a one-hot string, then d j ∈ F ′ if and only if q j ∈ F . Otherwise F ′ is defined in an arbitrary way.It is easy to show by induction over n ∈ N that for any pointed Π-labeled graph (G, w), the state of A at w in round n is q i ∈ Q if and only if the state of G at w in round n is d i .We note that this proof is based only on providing two embeddings to S d where S is the floatingpoint system and d is the dimension of the GNN[F]. The first is an embedding from the set Q Now, assuming that x ∈ R d+N M ∈ M(R d+N ) such that exactly the ith element of x ′′ and each y ′′ in M is 1 and others are 0s, we define that δ ′ (x, M ) = (δ i (x ′ , M ′ ), f (x ′′ )) (i.e., we concatenate δ i (x ′ , M ′ ) and f (x ′′ )). For other inputs, we define δ ′ arbitrarily. The set F ′ of accepting feature vectors is the set of feature vectors (x 1 , . . . , x d , 0, . . . , 0, 1), where (x 1 , . . . , x d ) is an accepting feature vector of G N . It is easy to show that (G, N ) accepts a pointed Π-labeled graph (G, w) if and only if G N accepts (G, w) (note that for both N -layer GNN[R]s and constant-iteration GNN[R]s, only the feature vector of a node in round N counts for acceptance).B.8 Proof of Theorem 3.6First we recall Theorem 3.6.Theorem 3.6. Constant-iteration GNN[R]s have the same expressive power as depth-bounded ω-GML.Proof. Note that we heavily use the proofs of Lemma B.12 and Lemma B.13.Assume that (G, N ) is a constant-iteration GNN[R] over (Π, d). Let K be the class of pointed Π-labeled graphs expressed by (G, N ). Now letΦ = { τ (G,w) N | G accepts (G, w) ∈ K in round N } where τ (G,w) Nis the full graded Π-type of modal depth N of (G, w) (see Section B.4). Consider the counting type automaton A over Π, where Φ is the set of accepting states. It is easy to show with an analogous argument as in the proof of Lemma B.12 that A accepts (G, w) if and only if (G, N ) accepts (G, w).For the converse, assume that ψ is a depth-bounded ω-GML-formula over Π of modal depth D. First by Lemma B.6 we translate ψ into an equivalent formula ψ * which is a disjunction of full graded Π-types such that the modal depth of ψ * is the same as ψ. By Lemma B.7, ψ * is equivalent to a counting type automaton A over Π whose accepting states are the types that appear as disjuncts of ψ * . Since the depth of each type is bounded by D, each pointed graph accepted by A is accepted in some round r ≤ D. By the proof of Lemma B.13 we can construct an equivalent GNN[R] G over Π such that for all pointed Π-labeled graphs (G, w) and for all n ∈ N: A accepts (G, w) in round n iff G accepts (G, w) in round n. Now, it is easy to modify G such that if G accepts a pointed graph in round m then it also accepts that pointed graph in every round m ′ > m. Therefore, for all pointed graphs (G, w) we have that (G, D) accepts (G, w) iff G, w |= ψ * iff G, w |= ψ.C Appendix: Characterizing GNNs over MSO-expressible properties C.1 Proof of Lemma 4.2In the end of this subsection we give the formal proof of Lemma 4.2. First we give some preliminary definitions.Let G = (V, E, λ) be a graph and let w 0 ∈ V be a node in G. A walk in G starting at w 0 is a sequence p = w 0 , . . . , w n of elements of V such that (w i , w i+1 ) ∈ E for all i ≤ n -1. We use tail(p) to denote w n . Now, the unraveling of G at w 0 is the graph U = (V ′ , E ′ , λ ′ ) defined as follows:V ′ = the set of all walks in G starting at w 0E ′ = { (p, p ′ ) ∈ V ′ × V ′ | p ′ = pw for some w ∈ V } λ ′ (p) = λ(tail(p)) for all p ∈ V ′ .We say that a formula φ(x) is invariant under unraveling if for every graph G = (V, E, λ) and every w ∈ V , we have G |= φ(w) iff U |= φ(w), with U the unraveling of G at w. Invariance under unraveling is defined in the same way also for GNNs. The following is easy to prove, see for example [7] .Lemma C.1. The following are invariant under unraveling: ω-GML, GMSC, GNN[F]s, GNN[R]s, and their constant iteration depth versions.which shows that for all tree-shaped graphs T : the automaton for φ accepts T iff there is a k-prefix decoration of T for some k ∈ N. Intuitively, a k-prefix decoration of T represents a set of accepting runs of the automaton for φ on the prefix T k of T (the formal definitions are in Section 4). Then we build a GMSC-program that accepts a tree-shaped graph T with root w iff there is a k-prefix decoration of T for some k ∈ N.We next define in a formal way the semantics of parity tree automata (the definition of a parity tree automaton (PTA) is in Section 4). For what follows, a tree T is a subset of N * , the set of all finite words over N, that is closed under prefixes. We say that y ∈ T is a successor of x in T if y = xn for some n ∈ N. Henceforth we will call successors out-neighbours. Note that the empty word ε is then the root of any tree T . A Σ-labeled tree is a pair (T, ℓ) with T a tree and ℓ : T → Σ a node labeling function. A maximal path π in a tree T is a subset of T such that ε ∈ π and for each x ∈ π that is not a leaf in T , π contains one out-neighbour of x.Definition C.2 (Run). Let G be a Σ N -labeled graph with G = (V, E, λ) and A = (Q, Σ N , q 0 , ∆, Ω) a PTA. A run3 of A on G is a Q × V -labeled tree (T, ℓ) such that the following conditions are satisfied:1. ℓ(ε) = (q 0 , v) for some v ∈ V ;2. for every x ∈ T with ℓ(x) = (q, v), the following graph satisfies the formula ∆(q, λ(v)):4 • the universe consists of all u with (v, u) ∈ E;• each unary predicate q ′ ∈ Q is interpreted as the set { u | there is an out-neighbour y of x in T such that ℓ(y) = (q ′ , u) }.A run (T, ℓ) is accepting if for every infinite maximal path π of T , the maximal i ∈ N, for which the set {x ∈ π | ℓ(x) = (q, d) with Ω(q) = i} is infinite, is even. We use L(A) to denote the language accepted by A, i.e., the set of Σ N -labeled graphs G such that there is an accepting run of A on G.We remark that, in contrast to the standard semantics of FO, the graph defined in Point 2 of the above definition may be empty and thus transition formulas may also be interpreted in the empty graph. A transition formula is true in this graph if and only if it does not contain any existential quantifiers, that is, k = 0. Note that a transition formula ϑ without existential quantifiers is a formula of the form ∀z( diff(z) → ψ), where ψ is a disjunction of conjunctions of atoms q(z) which are unary predicates for the states of the automaton. Such a formula may or may not be true in a non-empty graph. For example, if ψ in ϑ is a logical falsity (the empty disjunction), then ϑ is satisfied only in the empty graph.Let P be a node property over Σ N which is expressible in MSO and also in ω-GML. Let A = (Q, Σ N , q 0 , ∆, Ω) be a PTA that is obtained by Theorem 4.6 from P. If ψ is the ω-GMLformula expressing P, then we may simply say that A and ψ are equivalent. We identify a sequence S 1 , . . . , S n of subsets of Q with a graph struct(S 1 , . . . , S n ) defined as follows:• the universe is {1, . . . , n};• each unary predicate q ′ ∈ Q is interpreted as the set {i | q ′ ∈ S i }.For a tree-shaped graph T , we let T k denote the restriction of T to the nodes whose distance from the root is at most k. An extension of T k is then any tree-shaped graph T ′ such that T ′ k = T k , that is, T ′ is obtained from T k by extending the tree from the nodes at distance k from the root by attaching subtrees, but not from any node at distance ℓ < k from the root. Note that k-prefix decorations of T and universal sets of states are defined in Section 4. Lemma 4.7. For every tree-shaped Σ N -labeled graph T : T ∈ L(A) if and only if there is a k-prefix decoration of T , for some k ∈ N.Proof. "⇒". Assume that T ∈ L(A). Let i ψ i be the Σ N -formula of ω-GML that A is equivalent to. Then T |= ψ i for some i. Let k be the modal depth of ψ i . Then T ′ |= ψ i for every extension T ′ of T k .Next we construct a mapping µ : V k → P(P(Q)) and show that µ is a k-prefix decoration of (T, w). We construct µ as follows. For all v ∈ V on the level k, we define µ(v) as the universal set for λ(v). Then analogously to the third condition in the definition of k-prefix decorations, we define µ(v) for each node v on a level smaller than k. Now, all we have to do is show that the first condition in the definition of k-prefix decorations is satisfied, i.e., for each S ∈ µ(w), q 0 ∈ S. Then we may conclude that µ is a k-prefix decoration.Assume by contradiction that there exists a set S ∈ µ(w) such that q 0 / ∈ S. (Note that µ(v) ̸ = ∅ for all v ∈ V k by the definition of k-prefix decorations.) By Condition 3 of k-prefix decorations, there must exist sets S 1 1 ∈ µ(u 1 1 ), . . . , S 1 n1 ∈ µ(u 1 n1 ) (where u 1 1 , . . . , u 1 n1 are the nodes on level 1) such that q ∈ S iff the transition formula ∆(q, (λ(w))) is satisfied in the graph where each u 1 i is labeled S 1 i for each 1 ≤ i ≤ n 1 . By the same logic, we find such sets S m 1 ∈ µ(u m 1 ), . . . , S m nm ∈ µ(u m nm ) (where u m 1 , . . . , u m nm are the nodes on level m) for each m ≤ k (note that these nodes do not necessarily share the same predecessor). Let T ′ be an extension of T k that is obtained by attaching to each node u k i of T k on level k some rooted tree T ′′ that is accepted by A precisely when starting from one of the states in the set we chose for that node, i.e., Q T ′′ = S k i . Now, we can demonstrate that there is no accepting run r T ′ = (T T ′ , ℓ) of A on T ′ . Any such run has to begin with ℓ(ε) = (q 0 , w). Note that the out-neighbours of ε cannot be labeled with exactly the labels (q, u 1 i ) such that q ∈ S 1 i because ∆(q 0 , λ(w)) is not satisfied in the graph consisting of the out-neighbours u 1 i of w labeled with S 1 i for each 1 ≤ i ≤ n 1 . In fact, the out-neighbours of ε cannot be labeled with any subset of such labels either, because by definition all transition formulae ϑ are monotonic in the sense that (V, E, λ) ̸ |= ϑ =⇒ (V, E, λ ′ ) ̸ |= ϑ for all λ ′ ⊆ λ. Thus, there is an out-neighbour x 1 of ε in T T ′ such that ℓ(x 1 ) = (q, u 1 i ) where q / ∈ S 1 i , and we may continue this examination starting from x 1 in the same way. Inductively, we see that for any level m we find a son x m of x m-1 such that ℓ(x m ) = (q, u m i ) where q / ∈ S m i , including the level m = k where we let ℓ(x k ) = (q, u k i ). Thus q / ∈ S k i . However, we have S k i = Q T ′′ and it is witnessed by the run r T ′ that A accepts the tree T ′′ rooted at u k i when started in state q. Thus, q ∈ S k i , a contradiction. "⇐". Let µ : V k → P(P(Q)) be a k-prefix decoration of T , for some k. We may construct from µ an accepting run r = (T ′ , ℓ) of A on T . For every node v in T k on level k, let T v denote the subtree of T rooted at v. Let a semi-run be defined like a run except that it needs not satisfy the first condition from the definition of runs (that is, it need not start in the initial state of the PTA). A semi-run being accepting is defined exactly as for runs.Take any node v in T k on level k. Since µ(v) is universal for λ(v), we find an S v ∈ µ(v) such that q ∈ S v if and only if T v ∈ L(A q ). (Note that µ(v) ̸ = ∅ for all v ∈ V k by the definition of k-prefix decorations.) Consequently, for each q ∈ S v we find an accepting semi-run r v,q = (T ′ v,q , ℓ v,q ) of A on T v with ℓ v,q (ε) = (q, v). We now proceed upwards across T k , assembling all these semi-runs into a run. In particular, we choose a set S u ∈ µ(u) for every node u in T k and, for all q ∈ S u , a semi-run r u,q = (T ′ u,q , ℓ u,q ) with ℓ u,q (ε) = (q, u). Let v be a node in T k that has not yet been treated and such that its out-neighbours u 1 , . . . , u n have already been treated, that is, we have already selected a set S ui ∈ µ(u i ) for 1 ≤ i ≤ n along with the associated semi-runs. Due to Condition 3 of k-prefix decorations, we find a set S v ∈ µ(v) such that for each q ∈ S v : ∆(q, λ(v)) is satisfied by the graph struct(S u1 , . . . , S un ). Choose this set S v . 5 As for the semi-runs, let q ∈ S v . Then ∆(q, λ(v)) is satisfied by the above graph. We may thus choose as r v,q the semi-run that is obtained as follows:1. start with a fresh root ε and set ℓ v,q (ε) = (q, v); 2. for each i ∈ {1, . . . , n} and each q ′ ∈ S ui , add the semi-run r ui,q ′ as a subtree, making the root of r ui,q ′ an out-neighbour of the fresh root that we had chosen.For each set P of node label symbols and set S of states, we can specify the set of counting configurations in M K+1 (P(Q)) that satisfy a formula ∆(q, P ) if and only if q ∈ S with the following disjunction: Ψ S,P := c∈M K+1 (P(Q)) c|=∆(q,P ) iff q∈S ψ c .Recall also that the formula φ P specifies the set of node label symbols in P . The iteration clause for X S must state that there is a set P of node label symbols that are true and for which Ψ S,P is true. This can be expressed as below:X S :-P ⊆Σ N φ P ∧ Ψ S,P .We prove that the GMSC-program Λ characterizes k-prefix decorations associated with A. A pseudo k-prefix decoration µ is defined like a k-prefix decoration except that it needs not satisfy the first condition of the definition of k-prefix decorations (that is, every set in the root given by µ does not need to contain the initial state). Now, given ℓ ∈ N and a tree-shaped Σ N -labeled graph T , let µ ℓ T denote the pseudo ℓ-prefix decoration of T . For each ℓ ∈ N and each set S of states of Λ, we show by induction on n ∈ [0; ℓ] that for every tree-shaped Σ N -labeled graph T and for each node v in T on level ℓ -n, we haveT, v |= X n S ⇐⇒ S ∈ µ ℓ T (v).In the case n = 0, the claim holds trivially for the nodes v on level ℓ by definition of Λ, since then T, v |= X 0 S if and only if S is in the universal set for P , where P is the set of node label symbols that appear in v.Assume that the claim holds for n < ℓ; we will show that it also holds for n + 1. Let v be a node of T on the level ℓ -(n + 1).First assume that T, v |= X n+1 S , that is, for some P ⊆ Σ N , we have T, v |= φ n P and T, v |= Ψ n S,P . Therefore, there is a multiset c ∈ M K+1 (P(Q)) such that c |= ∆(q, P ) iff q ∈ S and T, v |= ψ n c . Thus, for every set S ′ of states of A we have that if c(S ′ ) = m ≤ K, there are exactly m outneighbours v 1 , . . . , v m of v such that T, v i |= X n S ′ for every i ∈ [m], and if c(S ′ ) = K + 1, there are at least K + 1 out-neighbours v 1 , . . . , v K+1 of v such that T, v i |= X n S ′ for every i ∈ [K + 1]. By the induction hypothesis, for every set S ′ of states of A we have that if c(S ′ ) = m ≤ K, there are exactly m out-neighbours v 1 , . . . , v m of v such that S ′ ∈ µ ℓ T (v i ) for every i ∈ [m], and if c(S ′ ) = K + 1, there are at least K + 1 out-neighbours v 1 , . . . , v K+1 of v such that S ′ ∈ µ ℓ T (v i ) for every i ∈ [K +1]. Since c |= ∆(q, P ) iff q ∈ S and by the definition of pseudo k-prefix decorations, we have S ∈ µ ℓ T (v). Then assume that S ∈ µ ℓ T (v). Let {v 1 , . . . , v m } be the set of out-neighbours of v. By the induction hypothesis for each i ∈ [m] and each set S ′ of states of A, it holds that S ′ ∈ µ ℓ T (v i ) iff T, v i |= X n S ′ . By the definition of pseudo k-prefix decorations there are sets S 1 ∈ µ ℓ T (v 1 ), . . . , S m ∈ µ ℓ T (v m ) such that q ∈ S iff struct(S 1 , . . . , S m ) |= ∆(q, P ), where P is the set of node label symbols that are true in v. Now, let c ∈ M K+1 (P(Q)) be a counting configuration realized by S 1 , . . . , S m . Now since K is the maximum over all k such that ∆ mentions a transition formulaϑ := ∃x 1 • • • ∃x k diff(x 1 , . . . , x k ) ∧ q 1 (x 1 ) ∧ • • • ∧ q k (x k ) ∧ ∀z( diff(z, x 1 , . . . , x k ) → ψ) ,we have c |= ∆(q, P ). Therefore, T, v |= ψ n c and trivially T, v |= φ n P , and thus T, v |= X n+1 S . Now, if Λ accepts a Σ N -labeled tree-shaped graph (T, w), then by the result above it means that there is a pseudo k-prefix decoration µ such that T, w |= A k+1 . Thus in round k we have T, w ̸ |= X k S for all S where q 0 / ∈ S. Therefore S / ∈ µ(w) for all S where q 0 / ∈ S, i.e., µ is actually a k-prefix decoration. Similarly if a tree-shaped graph (T, w) has a k-prefix decoration, then T, w |= A k+1 by the result above. Thus we have proved the lemma below. Lemma C.4. For every tree-shaped Σ N -labeled graph T with root w: T, w |= Λ iff there is a k-prefix decoration of T , for some k. into an equivalent bounded FCMPA A over Π such that the following holds. Let x t w denote the feature vector of G in round t at node w and respectively let y t w denote the state of A in round t at node w. Let F G and F A denote the accepting states of G and A respectively. Then for all pointed Π-labeled graphs (G, w) and for all t ∈ N it holds that x t w ∈ F G ⇐⇒ y t w ∈ F A . Moreover, the construction in the proof of Lemma B.3 shows that we can construct a GMSCprogram Λ over Π for A with the set A of appointed predicates such that for all pointed Π-labeled graphs (G, w) and for all t ∈ N we have G, w |= X t for some X ∈ A ⇐⇒ y t w ∈ F A . Clearly, for all pointed Π-labeled graphs (G, w): G fixed point accepts (G, w) iff Λ fixed point accepts (G, w).Then we show that each GMSC-program Λ can be translated into an equivalent R-simple aggregatecombine GNN[F] G relative to fixed point acceptance. We simply modify the proof of Lemma B.5 as follows: we add to the set of accepting feature vectors all feature vectors v where v N +D+1 ̸ = 1. Now it is clear for all pointed graphs (G, w) that Λ fixed point accepts (G, w) if and only if G fixed points accepts (G, w).• The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions). • The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.) • The assumptions made should be given (e.g., Normally distributed errors). • It should be clear whether the error bar is the standard deviation or the standard error of the mean. • It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have a 96% CI, if the hypothesis of Normality of errors is not verified. • For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative error rates). • If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.Justification: The code of ethics is not violated, as the paper does not involve datasets and is theoretical so that it is practically impossible to predict any harmful consequences. We have discussed all related work to the best of our knowledge and pointed out the limitations of our results, with even a short limitations-section included.Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction).38th Conference on Neural Information Processing Systems (NeurIPS 2024).In[5,26] an initialization function is not explicitly included in GNNs; instead each node is labeled with an initial feature vector in place of node label symbols. However, these two approaches are essentially the same.2 In GNNs here, messages flow in the direction opposite to the edges of graphs, i.e., an edge (v, u) ∈ E means that v receives messages sent by u. This is only a convention that could be reversed via using a modal logic that scans the inverse relation of E instead of E.Often semantics for parity tree automata are given with parity games, for the details see for example[14]. Informally, parity games are played by two players called Eloise and Abelard, where Eloise tries to show that the PTA accepts a given graph. Informally, the semantics introduced here represents a winning strategy of Eloise in parity games and similar semantics are used for example in[23].Note that the graph is empty if and only if v is a dead end in G.Note that if v has no out-neighbours, then Sv is the set of states q such that ∆(q, λ(v)) is satisfied in the empty graph. 


Decision: All reviewers agree that the submission made a significant contribution on characterizing the expressiveness of GNNs from various perspectives, specifically through logical frameworks. Although the work is purely theoretical, the presentation is good enough to make the submission comprehensible by audients having some logical basis. Thus a spotlight acceptance is recommended.

Reviews: review: paper_summary: paper_summary: The authors analyze the expressive power of recurrent graph neural networks (GNNs) through the lens of logic, focusing on uniform expressibility, which refers to functions expressible over all input graphs. Their findings are as follows:
- Expressive Equivalence: GNNs with floating-point numbers and the graded modal substitution calculus (GMSC) exhibit equal expressive power. The GMSC, a concept recently introduced in the context of circuits and distributed computation, is shown to be equivalent in expressiveness to simple GNNs—those that employ truncated rely and summation as aggregation functions.
- Reals vs. Floats: When floats are replaced with real numbers, an infinitary logic is required.
- MSO Definable Properties: For properties definable by monadic second-order logic (MSO), the distinction between reals and floats becomes irrelevant. Consequently, when considering MSO properties, recurrent GNNs over reals are equivalent to the finitary GMSC logic.
strength_weakness: strength_weakness: **W1 Related Work:** While the authors cite Grohe [12], Benedikt et al. [6], and Pfluger et al. [23], the relationship to Grohe’s work is not well-elaborated. A more detailed description of related work would enhance the context.

**W2 Type of Recurrent GNN:** The initialization function π\piπ can be arbitrarily chosen, such as an indicator vector for the initial vertex in reachability. This approach appears non-standard, as recurrent GNNs are not typically used once per vertex. Clarification is needed on how the analysis would change if the initialization were fixed (e.g., an all-ones vector). The use of accepting feature vectors also seems tailored to achieve desired results. Furthermore, the relationship to recurrent GNNs, interpreted as a fixed point equation, should be elucidated.

**W3 Distributed Automata:** The paper’s introduction mentions characterizing GNNs in terms of distributed automata, but this aspect is unclear in the main text. Making this contribution more explicit would benefit readers from the machine learning community.
questions: questions: - Please comment on **W1**, **W2** and **W3**.
 
- Please comment on **Proof Sketch of Theorem 3.2**: In the proof sketch  you seem to assume/define a specific floating-point system? However,  the results are applicable to arbitrary floating-point systems, right? Could you clarify this point?
limitations: limitations: This has been addressed in a satisfactory way by the authors.
paper_summary: paper_summary: This paper introduces a new logical characterization for recursive Graph Neural Networks (GNNs) following the aggregation-combine or message-passing paradigm. Among other topics, it primarily focuses on understanding the differences between GNNs in the typically considered theoretical setting—where an arithmetic with unlimited representation sizes (i.e., all reals are representable) is assumed—and practical settings, where GNNs operate using floating-point arithmetic.

In particular, the paper demonstrates that:
- GNNs working with floats, even those with a “simple” aggregation-combine structure, are equally expressive as the graded modal substitution calculus (GMSC).
- GNNs working with reals are equally expressive as graded modal logic with infinite disjunctions.
- Relative to queries expressible by monadic second-order logic (MSO), GNNs working with reals and those working with floats are equally expressive.

As a byproduct, the arguments employ automata-theoretical tools, providing a concise characterization of GNNs through the concept of counting message-passing automata (CMPA).
strength_weakness: strength_weakness: I have a single, but rather general, weakness to point out:

- The accessibility of the topic could be improved. The paper expects readers to be very familiar with certain theoretical topics, particularly logics, which I assume are non-standard for most readers. Fortunately, I have a sufficient understanding of these subjects, but I believe that readers less familiar with them will find it challenging to grasp the key ideas of this work. This is not to suggest that the paper is misplaced; I firmly believe there is room for such specialized work in this venue. However, the main part of the paper could benefit from more examples, illustrations, or intuitive explanations, rather than a heavy focus on preliminaries. These extensive preliminaries could also be shortened and major parts be placed in the appendix, to make room for other stuff.
questions: questions: - If I am not mistaken, in your definition of floating-point arithmetic, you only describe how to handle rounding situations, but what about overflows? As far as I understand, you assume a saturating scenario, correct? If so, could you provide a brief comment on whether handling overflow with wrap-around would make a difference?
limitations: limitations: The clearly stated results of this paper also imply their clear limitations. Additionally, the authors added open questions, which I count as a valueable statement for limitations as well.
paper_summary: paper_summary: The paper presents logical characterizations of recurrent GNNs in terms of logical formalisms, following the line of previous work by Barceló et al. It is shown that recurrent GNNs have the same expressive power as the infinitary extension of graded modal logic, when arbitrary precision is allowed for feature vectors, and as the graded modal substitution calculus (GMSC), when only fixed precision is admitted. In addition, arbitrary precision boils down to finite precision if the property that is being considered can be expressed in monadic second order logic (MSO).
strength_weakness: strength_weakness: I see no weakness on the paper. This is a comprehensive and solid piece of work that should clearly be accepted at the conference.
questions: questions: This is something that intrigues me: Is it possible to establish a connection between the GMSC and some version of (partial) fixed-point logics? 

Btw, in his survey on GNNs, Grohe mentions the following question: 

Question 2. Let Q be a unary query expressible in a suitable modal (2-variable) fixed-point logic with counting. Is there a
recurrent GNN (with global readout) expressing Q? 

Do you have an answer to this question?
limitations: limitations: The authors have correctly addressed the limitations of their work.
paper_summary: paper_summary: This paper examines the relationship between GNN models based on real numbers, which are predominantly studied in theory, and GNN models based on floating point numbers, which are commonly used in practice. Additionally, the paper advances the state of the art in the study of recurrent GNNs, where the computation is not restricted to a fixed number of layers. Termination in the studied recurrent GNNs is indicated by designated "accepting" feature vectors.

The GNNs studied in this paper feature a termination condition indicated by designated accepting feature vectors. The authors establish connections between the expressive power of these GNNs and logical formalisms such as the graded modal substitution calculus (GMSC) and Monadic Second Order Logic (MSO). Specifically, the authors prove that recurrent GNNs over floats and GMSC are equally expressive and, also, that for properties of Kripke structures definable in MSO, recurrent GNNs over floats and reals have the same expressive power.
strength_weakness: strength_weakness: - The paper is accessible only to seasoned logicians, a very small proportion of the NeurIPS community. I would have expected the authors to make an effort to present their results in a manner more accessible to the broader representation learning community. Instead, this feels more like a submission to LICS, and the authors appear not to have considered the suitability of their chosen venue for their work.

- There is no empirical evidence demonstrating that the proposed recurrent GNNs can be successfully trained to accomplish a useful task in practice. Specifically, it remains unclear whether the proposed recurrent model can address (some of) the limitations of standard GNNs in practical applications. The only mention of applications is in the first three lines of the introduction, which are generic statements about standard GNNs. I would have expected the authors to at least attempt to identify some practical needs unmet by standard GNN models, which their proposed recurrent models could potentially fulfil.

- Relevant related work has been cited. However, I would have expected a more in-depth discussion on the contributions of this paper with respect to [23] and also some discussion on the connection between GMSC and recent logics proposed to capture standard GNNs with a fixed number of layers beyond the framework of First-Order logic, such as the use of counting terms or Presburger quantifiers.

- The fixpoint termination condition proposed by the authors, based on a set of designated final feature vectors feels indeed natural from an automata-theoretic perspective; it is, however, unclear to me how these vectors could be learnt, as suggested by the authors. Concerning termination, it would appear to me that the recurrent application of these GNNs may not terminate at all (e.g., if the acceptance vectors are never reached during recurrent computation). I would have expected the authors to comment on the implications of this possibility.

- It is unclear whether the expressivity results also provide an effective procedure for computing, given a trained recurrent GNN, the corresponding GMSC theory. What would be the size of such a theory based on the size of the GNN representation?
questions: questions: - Please comment on potential applications of this work
- Please provide a more detailed account on the differences of this work wrt [23] as well as on the connection between GMSC and logics with counting terms and/or presburger quantifiers.
- Please comment on the possibility of learning the acceptance vectors and the possibility of non-termination.
limitations: limitations: The authors have indicated some limitations of their work in the paper.

Comments: title: Thanks for the clarifications
Thanks for the clarifications!
comment: Thanks for the clarifications. 

I would appreciate it if you could make the suggested changes to the paper as they would certainly improve readability and accessibility. I feel that termination issues are important, and so are practical considerations related to training.
I have the read the rebuttal. The authors address all my comments/questions in a very satisfactory. This is really a **very nice** paper and I will boost my score since it will be an **excellent addition to the conference program**.  And yes, I would really appreciate it if the authors expand the paper (or possible online version) with the promised additional explanations mentioned in the rebuttal.
Thank you very much for the clarification and your agreement on the addition of illustrative examples and so on.

I stand with my initial review and strongly recommend this paper to be accepted.