Logical characterizations of recurrent graph neural networks with reals and floats
Authors: Veeti Ahvonen
Damian Heiman
Antti Kuusisto
Carsten Lutz
Venue: NeurIPS 2024 poster (2024)
Keywords: graph neural networks
logic
distributed computing
descriptive complexity
Primary area: graph_neural_networks
TL;DR: The paper provides logical characterizations of recurrent graph neural network models.

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.

Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats
Veeti Ahvonen', Damian Heiman', Antti Kuusisto', Carsten Lutz
Taampere University, "Lippig University, SSaDDS. AT, Dresden/L.eipzig first trrstname... las cestname@tuni.... 2.3 cllu@informat uni-leipzig.de
Abstract
In pioneering work from 2019, Barceló and coauthors identified logics that pre- cisely match the expressive power of constant iteration- depth graph neural net- works (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-poin numbers and (2) with reals. For floats, the formal- ism matching recurrent GNNs is 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 logies and GNNs in the recurrent setting without rel- ativising to a background logic in either case, but using some natural assumptions about floating point arithmetie. Applying our characterizations, that, relative to graph properties definable in monadic recond-order logic (MSO), infinitary and rule-based logics are equally expressive. This implies that current 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. 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.
also prove
Introduction
have proven to be highly useful for processing graph data in numerous applications that span remarkable range of disciplines including bioinformat- ies [35 recommender systems [3 traffic forecasting (21), and multitude of others. The success of GNNs in applications has stimulated lively research into their theoretical properties such as ex- pressive power. A landmark result is due Barceló al. [5] which was among the first charac- terize 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 basic GNN model with 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.
Graph Neural Networks (GNNs) [1 30 34
In this article, we advance the analysis of the expressive power of GNNs in two directions. First, study the relation between GNN models based real numbers, mostly studied in theory, and GNN models based on floating-poins numbers, as mostly used practice. And second, we focus on family of basic recurrent GNNs while previous research has mainly considered GNNs with constant number of iterations, with the notable exception of [26). The GNNs studied in the current paper have 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 constant iteration GNNs and to recurrent GNNs with a termination condition based on fixed points, as used in the inaugural work on GNNs [II]: see the conclusion section for further details.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

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 12 3. This is a rule- based 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 and Boolean circuits M. GMSC is related to the graded modal ju-calculus, but orthogonal in expressive power, The correspondence between GNN[F|s and GMSC is as follows.
24
Theorem 3.2 The following have the same expressive power: GNNF]s,, GMSC, and R-simple segregate-combing Gs.
Here R-simple aggregate-comban GNN[F]s mean GNN that use basic eegregate-combing func- tions as specified by Barceló et al. [5] and the truncated ReLU the non- son-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 R-simple ones. We emphasize that the characterization provided by Theorem B.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-pon arithmetics. We believe that this assumption is entirely natural it reflects practical implementations of floats.
Our second result shows that recurrent GNNs with reals, or GNN[R]s, have the same expressive power the infinitary modal logic w-GML that consists of infinite disjunctions of GMI-formulas.
Theorem 3.4
GNN[R]s have the same expressive power as w-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 w-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 G and GNN(F]s relative to very expressive background logic, probably the most natural choice in the recurrent GNN context: monadic recond-order logic MSO.
Theorem 4.3 Let P be property expressible in MSO. Then P is expressible as GNN and only if it is expressible as a GNN
This result says that, remarkably, for the very significant and large class of MS0-expressible proper- ties, using actual reals with unrestricted arithmetic gives no more expressive power than using floats, by Theorem 3.2 even in the R-simple aggregate-combing 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 -eso-sxpeessible properties, GNN[R]s are equivalent 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 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 multisel 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 E N. A summary of our main results, both absolute and relative to MSO, is given in Table
Table I: A summary of our main results. The first row contains the results obtained without relativis- ing to background logic and the second row contains results relative to MSO. Here x = y means that x and 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"
Absolute: GNN[F] R-ipple AC- AC-GNN[F] = GMSC = bad. FCMPA < GNN [R] - w-GM = CMPA
MSO: GNN F R-sipple AC-GNN GMSC = bnd. FCMPA GNN RR] w- G-GL = CMPA
Related Work. Barceló et al. S study aggregate-combine GNNs with a constant number of itera- tions. They characterize these GNNs in restriction to properties expressible in first-order logic-in

---

terms of graded modal logic GML and show that global readout mechanism leads to model equiv- alent to the two-variable fragment of first-order logic with counting quantifiers FOC*. Our work extends the former result to include recurrence in natural way while we leave studying global read- outs 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
bounded-depth circuits, linking (non-recurrent) GNNs to the circuit complexity class TC Grohe's 's characterization utilises dyadic rationals rather than floating-poii numbers. Benedikt et al. [6] use logics with a generalized form of counting via Presburger quantifiers to obtain characterizations for (non-recurrent) GNNs with bounded activation function. The article also investigates questions of decidability concerning GNNs-a topic we will not study here. As general remark on related work, it worth mentioning that the expressive power of (basic) recurrent GNN-models is invariant under the Weisfeiler-Lemar test. This link has been recently studied in numerous articles 25 36
Pfluger et al. [26] investigate recurrent GNNs with two kinds of termination conditions: one based on reaching 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 least fixed-point operator over unary monotone formulas. The characterization itself is given in terms of the graded two-way p-calculus. We remark that MSO significantly generalizes LocMMFP and that the graded two-way μ-ccaccuus 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ó 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-passie -aaggggggggnngggggg 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( of local distributed algorithms with modal logic. Later Ahvonen al. [ 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.
2 Preliminaries
We let N, Z+ and denote the sets of non-negative integers, positive integers, and real numbers respectively. For all n E Σ+, we let [n] := [l,..., n and for all n E N, we let [0: == {0. n). With |X] we denote the cardinality of the set X, with P 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 (X) we denote the set of k-multisets over X, i..., the set of functions X + I0; k). Given k-multiset M E (X) and
x E X, intuitively (x) n < k means that there are exactly n copies of x and M(r) k means that there are i or more copies of a.
We work with node-labeled directed graphs (possibly with self-loops), and simply refer to them as graphs. Let LAB denote countably infinite set of node label symbols, representing features. We denote finite sets of node label symbols by IT C LAB. Given any IT C L.AB, a IT-abeled graph is a triple G = (V, E, A) where V is a set of nodes, E C V V is set of edges and A: V + PII) is a node labeling function. Note that a node can carry multiple label symbols. A pointed graph pair (G, with U E V. Given a graph (V, E, A), the set of out-neighbours of E V is { w (v. w) E E }. Unless stated otherwise, we only consider finite graphs, i.e., graphs where the set of nodes finite, A node property over II class of pointed II-labeled graphs. A graph property over II is class of II-labeled graphs. A graph property G over II corresponds to node property A over if the following holds for all IIllbeled graphs G: E g iff (G,v) E W 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.
3

---

2.1 Graph neural networks
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 cal- culate with real numbers and communicate synchronously in discrete rounds. More formally, a recurrent graph neural network GNN[R] over (II, d), with II C LAB and d Z is a tu- ple 9 (R", x, 5, F). A recurrent graph neural network computes in a (node-labeled) directed graph as follows. In any Il-labeled graph (V, E, A), the initialization function æ: P(I)) + Rd assigns to each node an initial feature vector or state x = x <>\(t)) M In each subsequent round t = 1,2.... every node computes a new feature vector x; using transition function 5: Rd x (Rd) + 0(., y) = COM(x, (y)( which a composition of an aggregation function AGG: M(Rd) - R (typically sum, min, max or average) and a combination function COM: Rd x I&d - Rd such that x = COM (x AGG (ff a (v, u) E E B)) where dou- The recurrent GNN G accepts a pointed I1-labeled graph (G. v) if visits (at least once) a state the set F S Rd of accepting feature vectors, i.e., ry E F for some 1 E N. When we do not need to specify d. we may refer to a GNN[R] over (II, d) as a GNN[R] over II. A constant-iteration GNN(RR is a pair (G, N) where 9 is GNN [R] and N E N. It accepts pointed graph (G.v) if x. É F. Informally, we simply run G for N iterations and accept (or do not accept) based on the last iteration. We say that G (resp., NG) expresses a node property P over 11, if for each pointed I1-labeled graph (G, w): (G, w) E P iff G (resp.. (9, N)) accepts (G, w). A node property P over 11 is expressible as a GNN[R] (resp. as a constant-iteration GIN( if there is a GNN[R]] (resp. constant-iteration GN expressing P.
ble curly brackets {{...} denote multisets F
One common, useful and simple possibility for the aggregation and combination functions, which is also used by Barceló et al. (see [.) and also the papers (25] [5]) is defined by COM (,t-1, AGG (E{ (((=))1) (v, u) E EE))) = =s(t--1 C + E(en)EE "h A + b), where f: IRd + Rd is non-linearity function (such as the truncated ReLU also used by Barceló et al. in [5) defined by (x) = min(max x). and applied separately to each vector element), C, A E Baxd are matrices and b E Bdd is a bias vector. We refer to GNNs that use aggrega- tion and combination functions of this form and ReLU as the non-linearity function as R-simple aggregate-combine GNNs (here 'R' stands for ReI.U*).
Example 2.1. Given IT and p E IT, reachability of node label symbol p is the property P over IT that contains those pointed IT-labeled graphs (G, v)) where a path exists from to some u with p E A(u). An R-simple aggregate-combine GNN[R] over (II, 1) (where C' = A = 1, b = 0 and is the only accepting feature vector) can express P: In round O, a node w's state is if X(w) and else 0. In later rounds, w's s state is if w's state was 1 or it gets from its out-neighbours: else the state is O.
Remark 2.2. Notice that unrestricted GNN[R]s can express, even in a single iteration, node prop- erties such as that the number of immediate out-neighbours of node is prime number. In fact, for any U C N. including any undecidable set U, a GNN [R] can express the property that the number / of immediate out- net-neigss is in the set U. See [6] for related undecidability results.
Informally, a floating-point system contains finite set of rational numbers and arithmetic operations and +. Formally, if p E Z,, n E N and 3 E Z,4 (1), then a moating-point system a tuple S= ((p, n, B), +) that consists of the set Dg of all rationals accurately representable in the form 0.d ..d...d. dp x 3 or -0.d ... dp x 8 where < d, < B 3-1 and e E {-n,.... n1. It also consists of arithmetic operations- + and of type Ds x Ds + Ds. 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 Ds. with ties rounding to the float with even least significant digit, e.g.. 0.312 0.743 evaluates to 1.06 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 Ds-
Consider GNNs using floats in the place of reals. In GNNs, sum a common aggregation function (also used in R-simple GNNs), and the sum of floats can depend on the ordering of floats, since it
'In 5 Zd 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 essentially the same. IIn GNNs here, messages flow in the direction opposite to the edges of graphs, i... an edge (v, u) e E means that receives messages sent by This is only a convention that could be reversed via using a modal logic that scans the inverse relation of E' instead of E.

---

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 < (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 system where the numbers must be representable in the form 0.d1d2 x 10a or -0.d,d2 d2 x 10 first (1 + (-1)) + 0.01 = 0 + 0.01 = 0.01 while (1 + 0.01) + (-1) = 1 + (-1) = O, since 1.01 is not representable in the system. A float GNN could distinguish two isomorphic nodes with such ordering of out-neigbbuurs.
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) a natural and simple choice. Summing in this increasing order is also used widely in applications, being reason- able choice w.r.t. accuracy (see, egg., 32, 29 . 18). ). Generally, fooatingppoin sums in applications have been studied widely, see for example 119] 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 Mis where Ma (z) the output of the sum S1 + ................................ + Se where (1) fa appears (J() times (i.e., its multiplicity) in the sum, (2) the floats appear and are summed in increasing order and (3) + is according to S.
(x)), k}. Given a multiset N of floats in float system S, we let SUM (N) denote
Proposition 2.3. For all floating doating-point point systems S, there exists a ls E N such for all multisets M over floats in S, we have SUMs(M) = SUMs(Mp))
Proof. (Sketch) See also in Appendix A.2
Let u = 0.0..... 01 x 8 and v = 0.100...0 0 ge-1, Now notice that for a large enough L, summing to itself m > E 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 Ma (U4) - Udd for some bound & E N, i.e. for every multiset M M(U"), we have (GG of M (and (dd is the set of states of the GNN). We finally give a formal definition for floating- point GNNs: a floating-poin 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 floating- point system S instead of R (note that S can be any floating-poin system). In R-simple GNN[F]s, SUMs 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[RR] is unbounded, whereas a GN is bounded. Now, is immediately clear that unrestricted GNN (with an unrestricted aggregation function) are more expressive than GNN 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 i can distinguish the centers of two star graphs with ls and k++1 out-neighbours.
(MR), where Mj. is the k-projection
2.2 Logics
We then define the logics relevant for this paper. For II C LAB, the set of II-formulae of graded modal logic (GML) is given by the grammar Pp ::= T and k N. The connectives V, -,, ++ are considered abbreviations in the usual way. Note that node label symbols serve as propositional symbols here. A IT-formula of GML is interpreted in pointed Illabeled graphs. In the context of modal logic, these are often called (pointed) Kripke models. Let G = (V, E, X) be II-labeled graph and to E V. The truth of a formula yp in pointed graph (G, w) (denoted G, -= sp) is defined usual for the Boolean operators and T, while for p ΠI and O244P, we define that G, w p p E A(w), and G, w F= 0 iff G, v F op for at least k: out-neighbours of w. We use the abbreviations Op- 121 Cp == - and =n == 02n A -02411.. The set of II-formulae of w-GML is given by the grammar == &b V NEW 15, where &b is a II-formula of GML and V is an at most countable set of I1-formulae of GML. The truth of infinite disjunctions is defined in the obvious way: G, + VNEw vi < G, w += &é for some s E v.
-4 yp A yp Q2x4, where p e II
We next introduce the graded modal substitution calculus (or GMSC), which extends the modal substitution calculus (24
3 with counting capabilities. Define the set VAR = (V. i E N) of schema variable symbols. Let T = (X1. [X1...., Xn) S VAR. The set of (TI, -)schmaaaa of
5

---

X; mp A 024p where E II, X, E ET and & E N. A (II, -prrorrm A of GMSC consists of two lists of expressions
GMSC is defined by the grammar vp : T
Xi :- p1
x.. :- P
X1 : 4/1
Xn :- the
where .I.....: 9P are N-formulae of GML. and 1/1 Un are (IT, T) -schemata of GMSC. More- over, each program is associated with a set A C T of appointed predicates. A program of modal substitution calculus MSC is program of GMSC that may only use diamonds & of the standard modal logic. The expressions (0) :- s are called terminal clauses and X; :- 3/; are called iteration clauses. The schema variable X; in front of the clause is called the head predicate and the formula p (or schema 1h)) 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 (II, 7) 1-program as Il-program of GMSC. Now, the nith iteration formula X," of a head predicate X, (or the iteration formula of X; in round n E N) (w.r.t A) is defined as follows. The Oth iteration formula X² is yo; and the (n 1 Jst iteration formula X is th where each head predicate Y in a/s is replaced by the formula Y We write G, w }= A and say that A accepts (G, w) iff G, w }= X" for some appointed predicate X E A and some n E N. Moreover, for all (II, -cchhemata yp that are not head predicates and for v E N, we let sr denote the formula (w.r.t A) where each Y E T in yp is replaced by Y".
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.c., if o0 is an MSO-formula, then so are io and Ex see c.g. [9] for more details. Given set I1 C LAB of node label symbols, an FO- or MSOOformula over 11 is an FO- or MSO-formula over a vocabulary which contains exactly a unary predicate for each p E II and the edge relation symbol E. Equality is admitted.
Let op be an a-GMLl-fomula, GMSC-schema, depth (resp. the width) of &p is the maximum number of nested diamonds in yp (resp. the maximum number k E N that appears a diamond O> vp) If an w-GMulformula has no maximum depth (resp., width), its modal depth (resp., width) is co. If an w-GMI has finite modal depth (resp., width), it depth-bounded (resp., width-bounded) The formula depth of a GMIL-formula or GMSC-schema is the maximum number of nested operators A and >- Given 11-program of GMSC or a II-formula of w-GM yp (respectively, a formula (xx) of MSO or FO over 11, where the only free variable is the first-order variable x), we say that yp (resp., (xxx) expresses node property P over II, if for each pointed II-labeled graph (G, w): (G. w) E P iff G. w = yp (or resp. G = vl())). A node property P over II is expressible in GMSC (resp., in w- W-GML, FO or MSO) if there is a II-program of GMSC (resp., a II-formula of w- G-G, FO or MSO) expressing P.
-roogram or rule of a program. The modal
Example 2.4. Recall the property reachability of node label symbol p over I1 defined in Exam- :-
2.1 It is expressed by the Il-program of GMSC X(0)= :- p, X :- QX, where X is an appointed predicate. The ith iteration formula of X is X* = Op where there are exactly i diamonds.
Example 2.5 (24] ). A pointed IIllbbled graph (G, w) has the centre-poite ponnte-point/oee property P over IT if there exists an n E N such that each directed path starting from w leads to a node with no out- neighbours in exactly n steps. It is easy to see that the II-program X(0) :- O.. X :- QX A OX, where X 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 ju-calculus and MSO that are not expressible in MSC (e.g., non non- reachabilityy,, with the same proofs applying to GMSC. Proposition 2.6. Properties expressible in GMSC are expressible in w-GML, but not vice versa.
Proof. A property over II expressed by a I--roorrmm I of GMSC is expressible in w-GM by the II-ormula V Vx,eA, nER X?, where X is the 7ith iteration formula of appointed predicate X, of T. Like GNN[R]s, w-GML can express undecidable properties (cf. Remark 2.2 Clearly GMSC- programs A cannot, as configurations defined by A 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 p-calculus (HGML), which originates from 22 and is used in 26 to characterize a recurrent GNN model, pGML and GMSC are orthogonal in expres- sivity. Iteration in GMSC need nor be over 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 JG.L The centre-point property from Example 2.3 is simple property not expressible in pGML, (as not even expressible in MSO, into which JGML, translates). Con- versely, GMSC offers neither greatest fixed points nor fixed point alternation. In particular, natural

---

properties expressible in the v-fragment of pGML 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 G.SSC. However, the ju-fragment of the graded modal ju-caluulus translates into CMSC (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.
3 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 GNs[F]s, R-simple aggregate-combing GNN[F]s and GMSC are equally expressive. Theorem 3.4 is the second main result, showing that GNN and w-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 nice additional characterizations. Informally, we consider a model of distributed automata called counting message passing automata and its variants which operate similarly 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 11 C LAB, a counting message passing automaton (CMPA) over II is tuple (Q, T, 6. F) where Q is an at most countable set of states and æ. 5 and F are defined in a similar way as for GNNs: and F S Q a set of accepting states. Computation of a CMPA over II is defined in a II-labeled graph G anallogouslyy to GNNs: for each node 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 GNNs: the
PIII- + Q is initialization function, 5: Q X MQ) - Q a transition function
state of and the multiset of states of out-neighbours of w. Acceptance is similar
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₂(Q) + Q for some & E N (i.e., ((g M) = 8(g,M1k) M1+) for each multiset M E M(Q) and state E Q). A finite CMPA (FCMPA) is a CMPA with finite Q. We define bounded FCMPAs similarly to bounded CMPAs. A CMPA A over II expresses a node property P over II if A accepts (G, w) iff (G, w) E P. We define whether a node property P is expressible by CMPA in way analogous to GNNs.
For any II, a IToojecc refers to a GNN over II, a CMPA over II, a II-formula of w-GML. or a II- program of GMSC. Let C be the class of all IToojeccss for all IT. Two IT-objecs in C are equivalent they express the same node property over IT. Subsets A, B C C have the same expressive power, if each x E A has an equivalent y E B and vice versa. It is easy 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 GMSC-
program A, we first turn A into an equivalent program I where the modal depth of terminal clauses
(resp., iteration clauses) is 0 (resp., at most 1). Then from I' with head predicate set T', we construct
an equivalent FCMPA A as follows. The set of states of is P(IUU") and A enters in round n E 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" is true 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 8 using, for each pair (q, q'), subschema specifying the multisets that take q to q' N
We are ready to show cquiexpressivity 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 GN 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 We also conjecture that a polynomial translation from GMSC to R-simple GNN F ss is possible by the results and techniques R taking into account differences between GNN [N] and R-simple GNN[F]s w.r.t. the definition of size. A more serious examination of blow-ups would require case-by-case base analysis taking other such details into account.
and B33
Theorem 3.2. The following have the same expressive power: GNN[F]s, GMSC, and R-simple combene GNN[F]s.
7

---

Proof. (Sketch) Details in Appendix B.3 By definition, a GNN(F) is just bounded FCMPA and translates to a GMSC-program by Proposition 3.1] To construct an R-simple aggregate-combine GNN[F] G for a GMSCC-roggram A with formula depth D, we first turn A into equivalent program T, where each terminal clause has the body 1, the formula depth of each body of iteration clause is D' (linear in D) and for each subschema of I that is conjunction, both conjuncts have the same formula depth if neither conjunct is T. We choose a poatiing-pontt system that can express all integers up to the width of I' 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 I one formula depth a time in the style of Barceló al. [5]. The 2nd half records the current formula depth under evaluation. G simulates one round of I in D' + rounds, using the 2nd half of the features to accept nodes only every D' + rounds: the truth values of head predicates are correct in those rounds. Note that the choice of mating--pint system in & depends on A and thus no single floating-poin system is used by all GNNs resulting from the translation. In fact, fixing single floating-pon system would trivialize the computing model as only finitely many functions could be defined.
To show that GNN and w-GML are equally expressive, we first prove useful theorem. Theorem 3.3. CMPAs have the same expressive power as w-GML.
Proof. (Sketch) Details in Appendix B.4 To construct a CMPA for each w- u-GMI-formula X. we define a GML-formula called the "full graded rype of modal depth n" for each pointed graph (G, w), which expresses all the local information of the neighbourhood of w up depth (with the maxi- mum out-degree of G plus sufficing for width). We show that each w-GML-formula X is equivalent to an infinite disjunction dix of types. We then define a CMPA that computes the type of modal depth of each node in round n. Its accepting states are the types in the type-disjunction d.x- For the con- verse, to show that each CMPA has an equivalent w- GM--formula, we first show that two pointed graphs satisfying the same full graded type of modal depth n have identical states in each round S n in each CMPA. The u-GML-formula is the disjunction containing every type such that some (G, w) satisfying T is accepted by the automaton in round n, where n is the depth of T. D
Next we characterize GNN with w- w-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- definition-and only countable set of states. Theorem 3.4. GNN have the same expressive power as w-GML.
Proof. (Sketch) Details in Appendix B.5 For any GNN we build an equivalent G.GGGMLLfoouuu using the same method as in the proof of Theorem 3.3 where we show that for each CMPA, can find an equivalent w-GMLL
For the converse, we first translate an w-GML-formulll to a CMPA A by Theorem 3.3 and then translate A equivalent CMPA A' with maximal ability to distinguish nodes. Then we build an equivalent GNN[R] for A'' by encoding states into integers. L
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 G-G See Appendix B.6 for the proofs.
In Appendix B.7 we show that our model of constant-iteration GNN RRs is equivalent to the one in Barceló al. [5] Thus Theorem 3.6 (proven in Appendix B.S 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 expressible in GML iff it is expressible in w-GL
Theorem 3.6. Constunt-iteration GNN[R|s have the same expressive power depth-bounded w-GML.
4 Characterizing GNNs over MSO-expressible properties
In this section we consider properties expressible in MSO. The first main result is Theorem where we show that for properties expressible in MSO, the expressive power of GNN 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 (Theorem 4.3 below). Our arguments in this section work uniformly for any finite set Ex of node label symbols.
8

---

Theorem 4.1. Let P be a property expressible in MSO. Then P is expressible as a GNN[R] if and only if is expressible in GMSC.
the introduction for a discussion. The proof of Theorem[4.IJam easily be adapted to show that a property P expressible in MSQ is expressible as constant-fteratio GNN [R] iff it is expressible in GML. This relates to [ which shows the same for FO in place of MSO. However, in this particular case the MSO version is not actual generalization based on 10 we show the following in Appendix C.I
Theorem is proved later in this section. The recent work [26] relates to Theorem
Lemma 4.2. Any property expressible in MSO and as a constant-iteration GNN is also FO- expressible.
Uniting Theorems and 3.2 we see that (recurrent) GNN[R|s and GNN[F]s coincide relative to MSO. is easy to get a similar result for constant- -tteratti GNNs (the details are in Appendix C.3)
Theorem 4.3. Let P be a property expressible in MSO. Then is expressible as a GNN[R] ifan only if it is expressible as GNN(F). The same is true for constant-iteration GNNs.
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 property P that is expressible GNN[F] but not in MSO.
Theorem 3.6 shows that constant- GNN and depth-bounded w- w-GLL are equally expres- sive. The proof of Proposition 2h6 shows that already depth-bounded w-G WMG 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-iteration GNN[R] but not as a GNN(F).
We next discuss the proof of Theorem We build upon results due to Janin and Walukiewicz 31 20), reusing an automaton model from 31 that captures the expressivity of MSO on tree- shaped graphs. With 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 on tree- shaped Ex-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, run of an automaton is tree-shaped, even if the input graph is not. Formally, parity tree automaton (PTA) finite set of states, EN S LAB is a finite set of node label symbols, A: Q x P(EN) - F a transition relation with F being the set of all transition formulas for A defined below, and Ω Q + N is priority function. A transition formula for A is a disjunction of FO-formulas of the form
tuple A = (Q, ΣN, . qo. S2). where Q is a E Q is an initial state,
Ro ... Rork (diff(x1,, FK) A gi (21) A (xrx)))) A Vz (dfff T1, I1) + vb))
Un) shortens an FO-formula declaring yı..... In as pairwise distinet, q: Q are states used as unary predicates and & is a disjunction of conjunctions of atoms (=)), with q Q. A PTA A accepts a language L(AA consisting of (possibly infinite) graphs G. We have G E 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 PTA currently visiting node in state q consists of sending copies of itself to net-neigsbours of e, potentially in states other than q. It is not required that copy is sent to every nug-neigh and multiple copies (in different states) can be sent to the same out-neighbour. However, we must find some (q. A(v), 8) E A such that the transition satisfies & in the sense that & satisfied in the graph with one element for each neg-neigh of u 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.
where k 2 0, diff
Theorem 4.6. Let P be a property expressible in MSO and in w- GML, Then there is a PTA such that for any graph G: (G.w) E P iff the unraveling of G at w is in L(AA).

---

Proof. Let x0x)) be the MSO-formula over ΣN that expresses P. Theorem 9 in 20 states that for every MSO-sentence v. there is PTA A such that for every tree-shaped Ex labeled graph G we have that G E (AA iff G - tb. To obtain a PTA for so(x), we start from the MSO-sentence ;b := A ((((x) A - Fly, x)) and build the corresponding PTA A. Then A is as desired.
fact, (G, w) E P iff G F se(w)) iff U F (((w) with U the unraveling of G at w since P is expressible by an G-GL--formulla which is invariant under unraveling (defined in Appendix C.I. Moreover,
U F (w)) U } &e iff U E L(A).
Since GMSC-programs are invariant under unraveling, we may now prove Theorem 4.1 by consid- ering PTAS obtained by Theorem 4.6 and constructing Ev- Ey-program A of GMSC for each such PTA A = (Q, ΣN. qu: A, .t) so that the following holds: For every tree-shaped Ex-labeled graph G with root w, we have G E L(A) iff G, w F= A. We then say that A and A are tree equivalent.
For state E Q let Ag be the PTA defined like A but with as its initial state. For a tree-shaped graph T. set QT = tu E Q T E L(A,)). We say that Q C P(Q) is the universal set for P if Q consists precisely of the sets Qr. for all rre-shhped graphs T, whose root is labeled exactly with the node label symbols in P. Let T = (V, E, A) be a tree-shaped graph with root w and k E N, and let 1/2 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 μ : V22 + P()(Q)) such that the following conditions hold: (1) for each S E ((()): 9o S: (2) for all E V on the level k, ju(v) is the universal set for X(1); (3) for each u E V on some level smaller than that has out-neighbours U1, "1,..... Un and all S1 E (l(1)..... Sn E p((n)) ju(e) contains the set S that contains state q E Q iff we have Agg, ((v) = 1 such that / is satisfied in the following graph: the universe is (u),..., Un and each unary predicate o' E Q is interpreted as {u: d' E S. Intuitively, a k-prefix decoration of T represents a set of accepting runs of A on the prefix TІ of T. As these runs start in universal sets, for each extension of T3 obtained by attaching trees nodes on level k. we can find 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 Ex-labeled graph T: T E I(A) if fand only if there is a k-prefix decoration of for some ks E N.
Using the above, we sketch the proof of Theorem 4.1 the full proof is in Appendix
Proof of Theorem 4./ By Lemma 4.7 given PTA A obtained from Lemma 4.6
we get tree
equivalent GMSC-prrggram A by building A to accept the root of a tree-shaped graph 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 AA into the rules of A.
5 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 re- search. 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 77. Interestingly, it can be proved via showing that fixed points can be defined this extension makes non-reachability expressible, cf. Example The second direction is to consider other acceptance conditions for recurrent GNNs. Intuitively, should be possible to establish Theorem 3.2 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.Ip that Theorem 3.2 also holds for recur- rent GNNs where termination is based on fixed points, studied under the name "ReeGNN" in [26]. These fixed points require only that 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 II] which requires all nodes in the network to reach stable state.
Limitations: For our acceptance condition (and for many others such as those based on fixed points), training and applying recurrent GNN brings questions of termination. These are very important from practical perspective, but not studied in this paper. particularly interesting ques- tion is whether termination can be learned in natural way during the training phase.
10

---

Acknowledgements
The list of authors the first page is given based the alphahetical order. Veeti Ahvonen was supported by the Vilho, Yrjö and Kalle Väisälä Foundation of the Finnish Academy of Science and Letters. Damian Heiman was supported by the Magnus Ehrnrooth Foundation. Antti Kuu- sisto was supported by the Research Council of Finland consortium project Explaining AI via Logic (XAILOG), grant number 345612, and the Research Council of Finland project Theory of compu- tational logics, grant numbers 352419, 352420. 353027, 324435, 328987: Damian Heiman was also supported by the same project, grant number 353027. Carsten Lutz was supported by the Federal Ministry of Education and Research of Germany (BMBF) and by Sächsisches Stuatsministerium für Wissenschaft, Kultur und Tourismus in the program Center of Excellence for Al-research "Center for Scalable Data Analytics and Artificial Intelligence Dresden/leippa ber: ScaDS. Lutz is also supported by BMBF in DAAD project 57616814 14 (SECAL, School of Embedded Composite AI) as part of the program Konrad Zuse Schools of Excellence in Artificial Intelligence.
project identification num-
References
[1] Veeti Ahvonen, Damian Heiman, Lauri Hella, and Antti Kuusisto. Descriptive complexity for distributed computing with circuits. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPlcs, pages 9:1-9:15. Schloss Dagstuhl- Leibniz-Zentruu für Informatik, 2023. doi : 10. 4230/LIPICS. MFCS 2023.9
[2] Veeti Ahvonen, Damian Heiman, Lauri Hella, and Antti Kuusisto. Descriptive complexity for distributed computing with circuits, 2023. arXiv:2203 04735
[3] Veeti Ahvonen, Damian Heiman, and Antti Kuusisto. Descriptive Complexity for Neural Net- works via Boolean Networks. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic (CSL. 2024), volume 288 of Leibniz Interna- tional Proceedings Informatics (LJPlcs). pages 9:1-9:22, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-7entrum für Informatik. 10. 4230/LIPIcs wWw.LIIII............... 2024.9
[4] Veeti Ahvonen, Damian Heiman, Antti Kuusisto, and Carsten Lutz. Logical characterizations of recurrent graph neural networks with reals and floats, 2024. arXiv: 2 14606
2405
[5] Pablo Barceló, Egor V. Kostylev, Mikaël Monet, Jorge Pérez, Juan I.. Reutter, and Juan Pablo Silva. The logical expressiveness of graph neural networks. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenRe- view.net, 2020.
[6] Michael Benedikt, Chia-Hsuan Lu, Boris Motik, and Tony Tan. Decidability of graph neural networks via logical characterizations. CoRR, 18152 2024. arxiv: 18151
[7] Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors. Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning. Horth-Holland, 2007.
[8] David Tena Cucala, Bernardo Cuenca Grau, Boris Motik, and Egor V. Kostylev. On the cor- respondence between monotonic max-sum GNNs and datalog. In Pierre Marquis, Tran Cao Son, and Gabriele Kern-Isherner, editors, Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023, pages 558-667 2023. doi: :0. 1..1...42//2.. 2023/64
[9] H.D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Undergraduate Texts in Mathematics. Springer New York, 1996.
[10] Michael Elberfeld, Martin Grohe, and Till Tantau. Where first-order and monadic second-order logic coincide. ACM Trans. Comput. Log., 17(4):25, 2016. doi :10:10.:0 1145/2946699
[11] Marco Gori, Gabriele Monfardini, and Franco Scarselli. A new model for learning in graph domains. Proceedings. 2005 IEFE International Joint Conference on Neural Networks, 2005., 2:729-734 vol. 2, 2005.
11

---

[12] Martin Grohe. The logic of graph neural networks. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy June 29 July 2021, pages 1-17. IEEE, 2021. doi 10. 1109/LICCS2224 0021.9970677
[13] Martin Grohe. The descriptive complexity of graph neural networks. In LICS, pages 1-14, 2023. doi : 10. 111111100111//
10175735
[14] Erich Grädel, Wolfgang
Thomas, and Thomas Wilke. Automata, Logics, and Infinite Games: A Guide Current Research, volume 2500 of Lecture Notes in Computer Science. Springer Nature, Berlin, Heidelberg, I edition, 2003.
[15] William L.. Hamilton, Zhitao Ying. and Jure Leskovec. Inductive representation learning on large graphs. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 1024-1034, 2017.
[16] Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempiäinen, Kerkko Luosto, Jukka Suomela, and Jonni Virtema. Weak models of distributed computing, with connections to modal logie. In Proceedingy of the 2012 ACM Symposium on Principles of distributed computing, pages 185-194, 2012.
[17] Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempiäinen, Kerkko Luosto, Jukka Suomela, and Jonni Virtema. Weak models of distributed computing, with connections to modal logic. Distributed Comput, 28(1):11-33, 2015. 2015.
[18] Nicholas J. Higham. The accuracy of floating point summation. 14(4):783-799, 1993. doi: 101:100.137/0910055
SIAM J. Sci. Comput.,
[19] Nicholas J. Higham. Accuracy and stability of numerical algorithms, Second Edition. SIAM, 2002. doi: 10. 1137/1 97880987888888111
[20] David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu- calculus with respect to monadic second order logic. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR '96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings, volume 1119 of Lecture Notes in Computer Science, pages 263- 277. Springer, 1996. doi: :000 0000//33540--6666 77_60
[21] Weiwei Jiang and Jiayun Luo. Graph neural network for traffic forecasting: A survey, Expert Syst. Appl., 1007:111911.11 2022. doi :00:10.:00
10. 1016/J ESWA 2022. 117921
[22] Orna Kupferman, Ulrike Sattler, and Moshe Y. Vardi. The complexity of the graded p- calculus. In Andrei Voronkov. editor, Automated Deduction CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceed- ings, volume 2392 of Lecture Notes in Computer Science, pages 423-437. Springer, 2002. 10:1 540 45620000-460011333333
[23] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time time model checking. J. ACM, 12(2):312-360, mar 2000, doi 10. 2114//339970
333987
[24] Antti Kuusisto. Modal Logic and Distributed Message Passing Automata. In Computer Sci- ence Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in Informatics (LIPles), pages 452-468, 2013.
[25] Christopher Morris, Martin Ritzert, Matthias Fey, William L. Hamilton, Jan Eric Lenssen, Gaurav Rattan, and Martin Grohe Weisfeiler and leman go neural: Higher-order graph neural networks. The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 February 1, 2019, pages 4602-4609, AAAI Press, 2019.
12

---

[26] Maximilian Pfluger, David Tena Cucala, and Egor V. Kostylev. Recurrent graph neural net- works and their connections bisimulation and logic. Proceedings of the AAAI Conference on Artificial Intelligence,
2024. doi: 1e..1669aaaaaa v38i13........ 29377
[27] Fabian Reiter. Asynchronous distributed automata: A characterization of the modal mu- fragment. Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming. ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 LIPIcs, pages 100:1 100:1-100:14. Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2017. doi : 10. 4230/LIPIIOO ICALP 2017 100
[28] David Richerby. Logical characterizations of PSPACE. In Jerzy Marcinkowski and An- drzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceed- ings, volume 3210 of Lecture Notes in Computer Science, pages 370-384. Springer, 2004. do1 20079978-3-540-001100 --000-30124-
[29]
Thomas G. Robertazzi and Stuart C. Schwartz. Best "ordering" for floating- addition. ACM Trans. Math. Softw., 14(1):00--110 1988. 11....1444422888 32/1///228844443333
[30] Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfar- dini. The graph neural network model. IEEE Trans. Neural Networks, 20(1):61-88) -80 2009.
doi: 10.1:00.0 1109 / TNN. 2008 2005605
[31] Igor Walukiewicz. Monadic second order logic tree-like structures. In Claude Puech and Rüdiger Reischuk, editors, STACS 96, 13th Annual Symposium on Theoretical Aspects of Computer Science, Grenoble, France, February 22-24, 1996, Proceedings, volume 1046 of Lecture Notes in Computer Science, pages 401-413. Springer, 1996. doi: 1007/
1-540-60922--00 93
[32] James Hardy Wilkinson. Rounding errors in algebraic processes. In Information Processing, Proceedings of the 1st International Conference on Information Processing, UNESCO, Paris 15-20 June 1959, pages 44-53, UNESCO (Paris), 1959.
[33] Shiwen Wu, Fei Sun, Wentao Zhang, Xu Xie, and Bin Cui. Graph neural networks in recommender systems: A survey, ACM Comput. Surv, 55(5):97:1-97:37, 2023, doi: 10. 1145/3335511
[34] Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S. Yu. A comprehensive survey graph neural networks. IEEE Trans. Neural Networks Learn. Syst., 32(1):4-24, 2021. doi: : :0. 1109/TNNLS. 2020 2978386
[35] Zhang XM, Liang L, Liu L, and Tang MJ. Graph neural networks and their current applications bioinformatics. Frontiers in Genetics, 21, 2021. doi: 10. www.3/3399/eeeee. 2021 00002.66000999
[36] Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019.
13

---

A Appendix: Preliminaries
A.1 Notions of size
We start this appendix by presenting definitions for the sizes of GMSCCprograms,, GN and bounded FCMPAs.
The size of 11-program of GMSC is here defined as the size of II plus the number of occurrences of node label symbols, head predicates and logical operators in the program, with each 22 adding k to the sum instead of just 1.
The size of a [F or bounded FCMPA over IT is defined here as follows. For FCMPAs define U := Q. and for GNN[F]s define U == St where S is the floating pring system and d the dimension of the GNN[F]. In both eases, let
|0] and let & be the bound. Note that the cardinality of
multiset M2 is the number (k + 1)" " of different functions of type U - [0; k]] Then the size of
the GNN(F) bounded FCMPA is [PT( plus n (k + 1)", i.e., the sum of the cardinality [PT(I))
of its initialization function P(TT) - U and the cardinality n. (k + 1)" of its transition function
U x MU) + U as look-up tables.
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 naive, 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 diamond 22 could be considered log(k), where k is the maximum appearing in 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 single floating-point number 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.
A.2 Proof of Proposition 2.3
We recall Proposition 2.3 and give a more detailed proof.
Proposition 2.3 For all floating-point systems S, there exists a k E N such that for all multisets M over floats in S, we have SUMs (M) = (MR))
Proof. Consider a floating point system S = ((p, n. +), and a multiset M E M(S). We dp
assume f = 0.d₁ .......... dp x 8 S (the case where f -0.d ...dp x 8 is symmetric). Assume that the sum of all numbers smaller than f in M in increasing order is E S. Let + fd denote and let s + pf+1 denote (s+ (s+f*) f f for all E N. it clear that 8+ ff+1 f 2 s fe, and furthermore, if 8 + pe+1 = + _², then 8 + = + f for all l' 2 l. If 8 + pl+1 = + f then we say that the sum 8 + f has stabilized.
Let 18' == 3 1. We may assume that 2 -0.3' ... B' 8r. Since + pe+1 2 8 + le for each l E N and S is finite, there must exist some & E E+ such that either + f* = s + pk-1 or s + pk = 0.3' ... 3' x 8d but then s + fu+1 = s + ft. 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 di * 0 (almost all floating-poin numbers in S can be represented in this form and the representation does not affect the outcome of sum; we consider the case for floats not representable in this way separately). Now, consider the case where s = -0. ... 3' 3e' for some e' E [-n, mi], as some choice of e' clearly maximizes the number of times f can be added. Now it is quite easy to see that that + 13"38-1 2 -0.10...0 0 3e', unless the sum stabilizes sooner. This is because there exactly 8 8 300- numbers in S from -0.33' ... B 3 to -0.10 0 x ,e'". After this another
2-3-11 additions ensures that + +0" 2 0. (Consider the case where p = 3 and / 10 and we add the number f= 0.501 x 10 to -0. 00.100 x 10 repeatedly. We first get -0.995 x 102, then -0.990 102, etc. Each two additions of f is more than adding I' 0.001 x 10 once, and f' can be added exactly 30-1 times to -0.100 x 10 until the sum surpasses 0, meaning that / can
14

---

be added at most 2 times. On the other hand, if f were 0.500 x 10 or smaller, then the sum would have never reached -0.100 10 in the first place.)
Let 8 == 3p + 3P-1 Let s'= == 8 l and assume the sum s' has not yet stabilized. Next, is clear that for any i E [p] we have s' + f 2 0.10 x ge+i because dj 2 1. For d₁ S S. we have that s' + f 0.10
g which where the sum stabilizes. If on the other hand d1 > 2' we have that s' + I = 0.10 ... 0 ge+p+1, which is where the sum stabilizes (this is because 2 causes the sum to round upwards until the exponent reaches the value e + p + 1). Thus, we get a threshold of g + BP + 30---
d > &
The case where d1 for all representations of is analogous; we simply choose one represen- tation and shift our focus to the first i such that d, * 0 and perform the same examination. The position of does not affect the overall analysis.
We conjecture that a smaller bound than 30+1 + 38 + +pp is possible, but involves a closer analysis.
B Appendix: Connecting GNNs and logics via automata
B.1 An extended definition for distributed automata
We give more detailed definition for distributed automata. Given II C LAB, a counting message passing automaton (or CMPA) over II is tuple (Q, n. 6, F), where
Q is an at most countable non-empty set of states,
* P(II) - Q is initialization function,
. 6: Q M(Q) - Q is transition function, and
. F C Q is 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, π. 6, F), where Q, π and are defined analogously to CMPAs and the transition function can be written in the form Q x (Q) - Q. i.e.. for all multisets M M(Q) we have 8(q, M) = 8(g. Maa) for all q E 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 E N. each k-CMPA (respectively, each k- 4-FMPAA) called bounded CMPA (resp., bounded FCMPA).
Let G = E, be a II-lablldd graph. We define the computation of a CMPA formally. A n, O, F) over II and II-lablled graph G (V, define distributed system, which executes in w-rounds as follows. Each round n. E N defines a global configuration In. V Q which essentially tells in which state each node is in round n. If n and w E V, then (w) = xA(w)), Now assume that we have defined 9n- Informally, a new state for w in round n + is computed by d based on the previous state of and the multiset of previous states of its immediate out-neighbours. More formally, let w be node and v..... Um its immediate nut-neigh (i.e., the nodes V s.t. (w, v) E E). Let S denote the corresponding multiset of the states 9n (v1)...., In In (.)). We define (n+ = 8(g,, (w), We say that (w) is the state of w round n.
CMPA (or resp. k-CMPA) (Q,
A CMPA (or resp. k-CMPA) accepts a pointed graph (G, w) if and only if (w) E F for some N. If gn (w) F, then say that the CMPA accepts (G,w) in round The computation for FCMPAs is defined analogously (since each FCMPA is a CMPA).
B.2 Proof of Proposition 3.1
Note that extended definitions for automata are in Appendix B.I
First we recall Proposition 3.1
Proposition
3.1 Bounded FCMPAs have the same expressive power GMSC.
15

---

To prove Proposition 3.1 (in the end of this subsection), we first prove 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 [.2 we show with the help of Lemma B. 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 1l-program of GMSC, we can construct an equivalent 11-program of GMSC such that the modal depth of each terminal clause of I' is O, and the modal depth of each iteration clause of most 1.
Proof. The proof is similar to the proof of Theorem 11 in D (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 program where the modal depth of each terminal clause is zero, since it is easy to translate any program of GMSC into an equivalent GMMSC-rrogram, 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 (g)-program A, with the rules ( :- 1, 22aa00022221-1--- A 0239). The modal depth of the iteration clause of A 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 follows. First, we define the following subprogram called a "clock":
(0) :- T
Ti :- T3
T2(0): :- L
T: :- Ti
(0( :- T3 :- T2.
We split the evaluation of each subformula between corresponding head predicates XI,1, X1,2, X2 and X3 and define their terminal clauses and iteration clauses as follows. The body for each terminal clause and the iteration clauses are defined by
X1,1 :- (Ti A 021 (-T, (-T A111).
X1,2 :- (Ti A (23g) V (-T1AX1.)
X2 :- ( 122 (-T2A X2).
X3 : (T3 125(022(-X2 X1,)) (-Ts A Xz).
The appointed predicate of the program X3-
Let us analyze how the obtained program works. The program works in a periodic fashion: a single iteration round of A simulated in 3 step period by the obtained program. The clock (i.e. the head predicates Tı, T2 and T3)) makes sure that each level of the modal depth is evaluated once during each period in the correct order. For example, if T. true, then the truth of X, depends on the truth of 022 and when T2 is false, then the truth of X2 stays the same. The head predicate Xa essentially simulates the truth of X A in the last round of each period. induction on n E N that for all pointed (laelle graphs (G, w) and for all & [0; 2]: G, w } X iff G, + +k
easy to show by
With Lemma B.I it is easy to construct an equivalent bounded FCMPA for any GMSC-program. Lemma B.2. For each II-program of GMSC, we can construct equivalent bounded FCMPA over
Proof. Let A be (II, prrogram of GMSC. By Lemma B.1 we obtain equivalent (II, T')- program where the modal depth for each terminal clause and at most for each iteration clause. Let & be the width of I', We create an equivalent A-FCMPA Ar as follows.
16

---

We create a state for each subset q - II IUTT: these form the state set Q = PTI
We formulate the initialization function æ as follows: T (P)) g if IT n P and for each head predicate X E 'T' (with the terminal clause X(0) :- () we have that X E q if and only if o 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 IF for schemata with modal depth at most 1. Let N E MM()) be a multiset of states and let q be a state. Given a (II, -)sshheaa
d with modal depth at most 1, we define the relation (g. N)) Il & recursively as follows: (g. N) IF T always, (q. .V IF p iff p E q. (g. .N |+ X iff X E q. (q. N) ) IF mp iff N) If y. (q. IF yp A iff (q It to and (q. N) It 8, and (g. N) It 2 iff there is set Q' S Q of states such that Eyeqq ((1)) 2 l and (d',0) IF o for all of E Q' (note that has modal depth 0).
Now we shall formulate the transition function 8 as follows. Let N E M()) be a multiset of states and let q be a state. For each node label symbol p II, p E 8(q, iff (q. N) IH p (i.e. p q). For each head predicate X E T with the iteration clause X :- ab we have that X E (gg.N) if and only if (q, N) IF v. (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 E q for some appointed predicate of T then q E F; otherwise q & F.
If G is 11-labeled graph and v node in G, then we let vn denote the state of Ap in round n. Moreover, if N is the set of out-neighbours of v, we let No denote the multiset {(u" u E N}.. Then we prove by induction on n E N that for any (II, T')-emmmma yp of modal depth 1 and for each pointed II-ladeled graph (G, w). we have (w", ,N) IH iff G, w -p"
If n 0 we prove by induction on the structure of y that (w N2) IF 4p iff G, G.w. F po.
Case y = p E II: Trivial, since (w",N% IF piffy p E w iff G. w F p pff G. - p..
Case y = X E T": Let x be the body of the terminal clause of X. Now, (w (2) IF X iff E w iff G, w + xx iff G, w X
Now, assume that the induction hypothesis holds for (11, "")7"'))sceemaa &b and 0 with modal depth at most 1.
Case y := -p:: Now, (w" (N) It - iff (w", No) 1V vb By the induction hypothesis, this is equivalent to G, w I 66 which is equivalent to G, w -= -
Case == vb A 0: Now, (w0, No) IF &e A iff (wo, No) It sb and (w ( It O. By the induction hypothesis, this is equivalent to G, F vo and G, w F 80, which is equivalent to G, w -= ~0.
Case 4 == Ozev: First it is easy to show that for every (II, T') J')-semema vi of modal depth 0 and for every state q of Ar that (g. 0) IF &b iff N) It vb for every multiset N of states of Ar. Now, (wo N20 It Ozer iff there is a set Q' c Q of states such that Egeo No (q') 2 and (q', 0) IF for for every g' E Q' iff there is set N of neighbigs of w such that |N] 2 l and (u², No) IF vb for every u E N. By the induction hypothesis this true iff there is a set N of out-neighbours of w such that [N] 2 l and G, } 80 for every u E N, which is equivalent to G, w } O2066
Now, assume that the induction hypothesis holds for n and let us prove the case for n++1. Similarly to the case n = O, we prove by induction on structure of to that (w=+1, ,N*+1) Il yp iff G, w }= r
The proof by induction is almost identical, except in the case where & = X E T'. Let Xx be the body of the iteration clause of X. Then (w1++1 Nx++1) the induction hypothesis, this is equivalent to G, - x² which is equivalent to G, F X=+1
1) It X iff X E =1+1 iff (w", No) I- Xx. By
Thus, the result above implies that for all pointed IIlabeled graphs (G, w). the automaton Ar is in the state g at w in round iff G. F x and G, w } p for every X.p E g, and G, w ifz X and G, w f p for every p. X & q. Therefore, by the definition of the set of accepting states we see that Ar is equivalent to r.
17

---

The converse direction is easier. Note that the definitions for sizes of GMSC- programs FCMPAs can be found in Appendix [A.]
GMoSCprrogamss and bounded
Lemma B.3. For each bounded FCMPA over II, construct an equivalent 11 I1-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 [2 Let IT be set of node label symbols, and let A = (Q, π, 6, F) be a k-FCMPA over II. For each state E Q, we define a head predicate X, and the corresponding rules as follows. The terminal clause for X, is defined by
V (Apa A A)) PEILIP
(0)
PEIL =(P)=g PEP
To define the iteration clause for each X, we first define some auxiliary formulae. Given g. E Q, we Mz(g, (') = {S E Ma(Q) 8(g. S) = =q') J. Notice that the number multisets S specified by the set Ma(g, d') is finite. Now, for each S 4') we define
Ps =
A
D=n A
A
Oz
gEQ.S(g) neck
qEQ.S(g)=K
Then the iteration clause for X, is defined by X,= AreE Xx - V VSEM. (o' ps) It easy to show by induction on N that for every pointed 11-labeled graph (G, w) it holds that G, w X 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).
The size of A is [P(LI) + [Q]( + 1) by definition. The size of all terminal clauses of the constructed program is altogether [Q] + O(III [P(II)),, as there |Q] terminal clauses that altogether encode each element of P(II) and each encoding is of size O(II). The size of all iteration clauses of the constructed program is altogether e + 2 [ +1)1Q) = ( ()) 9)), as there are |Q2 iteration clauses with [Q] conjuncts each, and they altogether encode every element of (M) exactly [Q] times and each encoding is of size (kk(Q)). Note that the cardinality of Ma(Q) is (k + 1)191, i.e., the number of functions of type Q + program is
[0; kj. Thus, the size of the
I IQ1 + O(II] ( OKKQ 1)19)) II P(I) + 4|Q/ 1)1Q1)
which clearly less than ((P((TT)) + IQ (k= + 1)12)2 and therefore polynomial in the size of A. If head predicates and states were encoded in binary, the result would still be polynomial, as it would simply add a factor of log( and log((Q) respectively to the sizes of terminal and iteration clauses.
Note that the proof uses auxiliary results that are introduced in this sub- section. Lemma B.2 shows that for every II-program of GMSC bounded FCMPA over II. Lemma B. shows that for every bounded FCMPA over II we can con- struct an equivalent II-prgrrm of GMSC. Thus, conclude that GMSC has the same expressive power as bounded FCMPAs.
Proof of Proposition 3.1
construct equivalent
B.3 Proof of Theorem 3.2
First we recall Theorem
3.2
Theorem 3.2 The following have the same expressive power: GNN GMSC, and R-simple eagregate-combing GNN[F]s.
In the end of this appendix section, we formally prove Theorem 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 translate the bounded FCMPA into equivalent GMSC- program. The converse direction much more interesting. In Lemma B.5 we show that for each GMSC-program we construct equivalent R-simple aggregate-combing 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 casier to handle via R-simple GNN[F]s. In particular,
18

---

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 lemma which intuitively shows how to "balance" MMMS--prggrams such that this is not the case. We fdepth((p) denote the formula depth of schema yp (see the definition of formula depth in Section 2.2). The formula depth of terminal clause (resp., of an iteration clause) refers to the formula depth of the body of the clause. The formula depth of proorra is the maximum formula depth of its clauses.
Lemma B.4. For each I1-program A of GMSC with formula depth D, can construct equiv- alent II- prograam I of GMSC which has the following properties.
1. Each terminal clause is of the form (())= :- :-
2. Each iteration clause has the same formula depth max(3, D 22)
3. If p A 0 is subschema of A such that neither vp nor 0 is T, then and 0 have the same formula depth.
Proof. First we define a fresh auxiliary predicate I with the rules [0)) :- I and I :- T. Informally, will modify the rules of A such that the terminal clauses are simulated by the iteration clauses with the help of J. Then for each head predicate of A with terminal clause X(0) :- and iteration clause X :- z define new rules in T as follows: X(0) 1 and X (-J p) (T vb).
Now, the formula depth of I is max(3, D 2).
First, we "balance" the formula depth of each iteration clause in I according to the second point in the statement of the lemma. Let d be the formula depth of an iteration clause :- v. let D' max(3, D + 2) and let D' d. If n is even, then the new iteration clause for X is - : (-)² v. where (-) - denotes n nested negations. If n is odd, then the new iteration clause for X is X :- (-)"-1(c (+b T). In either case, the new iteration clause for X has formula depth D'
Then we show how to "balance" each subschema of T according to the third point in the statement of the lemma as follows. Let yp A d be a subschema of I such that neither yo nor v is T, and w.l.o.g. assume that fdepth((p) < f1) and let n fdepth (b) fdepth((p)). If n is even, then replace up A in with (-)" sb. n is odd, then we replace yp A t in I' with (-)"
(yp ( T)A A.d.
We have now obtained the desired r. It is easy to see that I is equivalent to A as follows. If X is a head predicate that appears in both A and I, then for each n E N and for each pointed II-labeled graph, we have G, w } X" w.r.t. A iff G, w + X w.r.t. r. In r, the auxiliary predicate I makes sure that each head predicate X in that appears in A simulates in round 1 the corresponding terminal clause of X in A and in subsequent rounds simulates the corresponding iteration clause of X in A. Furthermore, for each head predicate in T and for each pointed IT-labeled graph (G, w)), we have G, w # X w.r.t. Т. Thus, I and A are equivalent.
Now are ready to show the translation from GMSC R-simple aggregate-combine GNN[F]s. Lemma B.5. For each II II-program of GMSC we can construct an equivalent R-simple aggregate- combine GNN[F] over II.
Proof. Let A be Il-program of GMSC, Informally, an equivalent R-simple aggregate-combin GNN(F] for A is constructed as follows. First from A we construct an equivalent II-program of GMSC with Lemma B.4 Let D be the formula depth of T.
Intuitively, we build an R-simple aggregate-combine GNN[F] Gr for I which periodically computes single iteration round of T in D + rounds. The feature vectors used by Gr are binary vectors
v uw where:
u has one bit per each (distinct) subschema of a body of an iteration clause in I' as well as for each head predicate, and v, keeps track of their truth values, and
* has D + 1 bits and it keeps track of the formula depth that is currently being evaluated.
19

---

Therefore, Gr is a GNN[F] over (II, N + 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 peating-point system for Gr is chosen to be high enough. More precisely, we choose a floating-pone poini system S which express all integers from O at least up to K max. where K max is the width of T. Note that Os and Is are also represented in the seating-point system Note that although feature vectors exist that have elements other than Is and Os, they are not used.
Next we define the functions т and COM, and the set F of accepting states for gr. (Note that AGG is just the sum in increasing order.) We assume an enumeration (T)( == [41..... NN of subschemata and head predicates in I such that if (p is a subschema of ye,, then < l. The initialization function π of Gr with input P C II outputs a feature vector v E (0 where the value of each component corresponding to a node label symbol is defined as follows: the component for p is iff E P. The other components are Os (excluding the possible subschema T which is assigned 1, as well as the very last (N + + 1 )thh bit which is also assigned 1).
Recall that S is the floating-point system for Gr. The combination function (as per the definition of R-simple GNNs) COM(x, o(x C + y A + b) where a is the truncated ReLU (ReLU*) (0), 1), b
defined by ReLU* (1x) where b, C' and AA are defined as follows. For k. f < N D 1, we let CA.E (resp. Ax,e) denote the element of C (resp. A) the kth row and /th column. Similarly for S N + D++1 1 and for any vector v E SN+++1 including b, we let Vy denote the êth value of v. Now, we define the top-left N N submatrices of C and and the first N elements of b in the same way as Barceló et al. (5) For all e s N we define as follows.
SN+D+1 and C, A E SIN+D+DD(N++++)
If pp IO [T}. then Ct,E =
If yo is a head predicate X with the iteration clause X :- Pkk, then Cz.e 1.
If yox upj A Sp.. then Cz,e Cz = 1 and b -1
If pp PP then OR,e = 1 and b& = 1.
If ypx = 02K then Ax.E = 1 and b; = - K +
Next, we define that the bottom-right (D + 1) (D 1) submatrix of C is the (D + 1) x (D 1) identity matrix, except that the rightmost column is moved to be the leftmost column. More formally, for all N +1 < f < N + D ++1 1 we have Cr,e+1 and also CN- DVN-+1,, 1,N, = 1. Lastly, we define that all other elements in C, A and are Os. Finally, we define that v E F and only if va = (i.e., the éth value of is 1) for some appointed predicate fo and also VN+D+1 =
Recall that the formula depth of I is D. Let v(w); 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 E N, for all pointed TI-laeledd graphs (G, w), and for every schema yor in (TB of formula depth d, we have
v(w), (n(++(+)) = 1 if G, w + 4pt and v(w), (((+)(+))+) = 0 if G, w + 4p
Most of the work already done by Barceló et al. (see [5] for the details), but we go over the proof as there are some additional considerations related to recurrence.
For the base case, let 0. We prove the case by induction over the formula depth d of ype. First, let d = O.
. Case 1: yee E ITU (T). Now vÍ = and G,w w F To if sp T. If yo p E TT then by the definition of the initialization function π we have vww)) = 1 iff E X(w) iff G, w - p", and v(w) = 0 iff p & A(w) iff G, w / p".
.
Case 2: of the initialization function ग, and G, w j X because each head predicate of I has the terminal clause 1.
X, where X is head predicate of T. Now v(w) = 0 due to the definition
Now, assume the claim holds for n = 0 for any formulae yjj ykk with formula depth d 1. We show that the claim holds for n. = 0 for formulae &e of formula depth d.
20

---

Case 3: 3e 9j A pp for some 9j, Pb (recall that I only contains conjunctions where both conjunets have the same formula depth if neither of them are T). This means we have Cj.e Ca,e and by = -1. Moreover, Cm.t = 0 for all m + j. and Am. = 0 for all m. Now
v(w) ReLU* (v(w)) + v(w)
d -)
Thus v(w) 1 iff v(w);-1 v(w) 1. By the induction hypothesis this is equivalent to G, w += sj and G,w w F 4p which is equivalent to G, w } (vy A spx) Likewise, vww); = 0 iff ( -
O. By the induction hypothesis this is equivalent G, Hf pf or G, H ph which equivalent G, w bfr (ey A ppx)
Case 4: Op = for some Px. This means have Cs,E -1 and b, 1. Moreover, Cm, = 0 for all m * k and Am.t = 0 for all m. Now
v(w) ReLU* (-v(w)) +1)
Thus v(w)g = 1 iff v(w) = O. By the induction hypothesis this is equivalent to G,w I 2k which is further equivalent to G, w }= (-xx)) Likewise, v(w); = iff
v(w) d- 1. By the induction hypothesis this is equivalent to G. F &% which is equivalent to G, w 1 (-9x))
Case 5: 9pt = 02KRs for some sk. This means we have AR,E = and by = + 1. Moreover, Cm.t 0 for all and Am,t 0 for all & k. Now
v(w); = ReLU* (SUMs ((I(()) (w, E E }}) K +1)
where SUMs: MM() + S is the sum of floating-poin numbers in S in increasing order the set of edges G. Thus v(w){ = iff there
(see Section 2.1 for more details) and are at least K out-neighbours v of to such that v(u) ((u)d-1 = 1. By the induction hypothesis, this is equivalent to there being at least K oui-neigsbours v of w such that G. = pf which is further equivalent to G, w + (0zkPx)) Likewise, v(w), = 0 iff there are fewer than K out-neighbours v of w such that v(v) 1. By the induction hypothesis, this is equivalent to there being fewer than K out-neighbours of w such that G. v = p2 which is equivalent to G, / (02k(k))
Next, assume the claim holds for n for all formulae of any formula depth. We show that it also holds for n + We once again prove the claim by structure of pe. Cases 3, 4 and are handled analogously to how they were handled in the case n = 0, so we only consider cases and 2.
Case 1: T (T). This means we have Ct. and b, 0. Moreover, Cm,e 0 for all m # and Am, = 0 for all m. Now
v(w) (n))++((+)) = ReLU (v(w) (()))(D++++
Thus we see that v(w) (n+ = v(w)) (Dt))(DD1)+ and a trivial induction shows that also v(w); (n+))(++++) v(w), ((w) m(D+1) Now v(w) (x+1)(++))
iff v(w), n(D+1) v(w)r((+1) 1. By the induction hypothesis this is equivalent to G, w -= oo which is equivalent to G, w } iff v(w))((+1) 0. By the induction hypothesis this is equivalent to G, w # of which is equivalent to G, w H 4p 7+1
xp p1+1 because opt +1 sp Likewise, v(w) ((w)(++1 (1+1)(D+1)
Case 0p X, where X a head predicate of with the iteration clause (a of formula depth D (recall that in I, each iteration clause has formula depth D). This means we have C = and by 0. Moreover, Cm,t = for all m + k and Am, = for m. Now
v(w) (1+1)(D) = RCLU (v(w) m(D+)(+))++))))))
Thus v(w) v( (n+1)D+11 = iff v(w) nDD+((+ = 1. By the induction hypothesis this is equivalent to G, w }= of which equivalent to G,w w }= xx+1, Likewise, v(w)( (n)))+)((++)) = 0 iff (())(D++)+D 0. By the induction hypothesis this is equiva- lent to G, w # oof which is equivalent G, w I x
21

---

This concludes the induction.
We also know for all 2 and all N + < l < N + D + 1 that v( v(w)) and
v v(w) N+1 = v(w)x+++ This is because C2, = 1, Cr.e+1 = 0 for all e" + l and b = and thus
v(w) = ReLU" (v(w)²
and also CN+D+IN+I 1, Cr.N+I for all l' + N D + and bx+1 and thus v(w) = ReL. ((=+))++++))
By the initialization this means for all 1 S e, S D + 1 and all N that (w) iff l' E and otherwise. Specifically, this means that v(w) v(W) b = D + and
1D++1)44 otherwise. N++N+++1
Thus if po is appointed predicate X of r. then we know for all n NN that G, w F X iff ((D+1) v(w), m(D+1) = 1 and we also know that v(w) N+D+1 = 1 and thereby v(w) E F. Thus Gr
is equivalent to r'
Since 9r is equivalent to I which is equivalent to A, 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, 3). +.)) be the floating-point system, where p = 1, n 1 and 3 = Kmax + 1, where K max is again the maximum width of the rules of I in the proof above. We believe that the proof generalizes for other floating-point systems which can represent all non- negative integers up to K maxx- Recall that Kmax is the width of T in the proof of Lemma B..5 Consider class of GNN[F)s over S with dimension ( + + 1) (twice that in the proof above) where the aggregation function is SUMs: 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: 52(N+D+1) 52(N+D+1) + +2(+++11) is defined by
COM (z, v) = ReLU(x
A-y-AA+b
where C, A E S2(N=D+1)x2( are matrices, b E 5*(N+++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 I' 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 of the form P2K Thus, the second element normalizes the values by assigning a weight of Kmax ensuring that each positive value becomes K Kmax and then assigning the bias -mmax + to bring them all down to 1. More formally, for each subschema yee, let l be the first and N + l the second element associated with pp. In the initialization step we define that if pp E P S I1 or fe = T, then (P) = 1 and other elements of T (PP) are Os. Now we define as follows for all 1 < l < N.
If ype E II {T}. then CN-e,e = 1.
*
:- pk,, then CN = 1. If yoy is a head predicate X with the iteration clause X-
If yo= 4j A (kk, then CN+5.e = -N- = 1 and b = -1.
If yp: -ip then CN+K,E -1 and by 1.
. If Pp O then AN+K.t = -1 and b = -K + 1.
In each of the above cases also define that Cr,N+e Kmax and b = -mma + Lastly for all 2N+1 < E < 2(N++(( +D+1) we define (as before) that C2,e+1 = and also C2 11122+11 = 1. All other elements of C, A and b are Os. The set F of accepting feature vectors is defined such that v E F iff VN+* = for some appointed predicate for and also v2(N+D+1) = 1. It is then straightforward to prove for all n E N, for all pointed I1-labeled graphs (G, w) and for every schema ie E SUB(T) of formula depth d that
v(w) 2n(D+1)-24
> 1 and v(w) 2n(D+1)+2d 1 iff G, w T= 46
22

---

and
v(w)e (W))n(DD+11 (n((D+))-2d v(w) 2n 2n(D+1)+22 0 if G, w 4
The proof is similar the above, but we also need show that normalization works as intended, ie., (w))m(D+))+2dd1
2 implies v(w)N+( 2n(D=1)+2d = 1 and v(w){ ( = 0 smpliee
2n(D+1)+2d = 0. To see this, observe that Ct,N+E = Mmax and bN+E = - K mmax + and also v(w) N+E
CR,N+e= = 0 for all L' + and AB,N+E = 0 for all E. Thus
v(W)N+e 2m( = ReLU (Kmax v(w), ( Kmax + 1),
which is if (1r) ( = 0 and 1 if v(w); (2(D+1)+22-1 > (because by the choice of S we have Kmax I Kmax for all x E S, x 1).
Having proved Lemma B.5 we are now ready to conclude the main theorem of this appendix section expressed below.
Proof of Theorem 3.2 Note that the proof uses auxiliary results introduced in this subsection. Each GNN[F] is trivial to translate into equivalent bounded FCMPA with linear blow-up in size by the fact that the definitions of GNN[F]s and bounded FCMPAs are almost identical. Lemma B.5 shows that each GMSC-program can be translated into an equivalent R-simple aggregate-combine GNN[F]. The translation from GNN[F]s to GMSC--rogrrms causes only polynomial blow-up in size by Lemma B.3
B.4 Proof of Theorem
Note that k: d-CMPAs are defined in Appendix B.1 First we recall Theorem 3.3
Theorem CMPAs have the same expressive power w- G..
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 11 for each Il-formula of w-GML Informally, to do this, we first define a II-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 u-GMM-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 (.ainaaBBBute that for each CMPA over TT we can construct equivalent fI-forula of w-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 é S n in each CMPA. For each n E N. we consider exactly those full graded types of modal depth n which are satisfied by some pointed graph that accepted by the automaton round n. We obtain the desired w- f-GMul- by taking the disjunction of all these types across all n E N.
By similar arguments, we also obtain Theorem B.10 which is analogous Theorem 3.3 but stricted to bounded CMPAs and width-bounded w- GMG., which involves defining analogous width- bounded concepts.
To show that for each w-GML-formula can construct equivalent CMPA, need to define the concepts of graded 11-types, full graded Il-types and counting type automata. The graded 11-type modal depth n and width & of a pointed II-labeled graph (G, w) is II-ormula 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 can only distinguish between most identical branches. The full graded II-type of modal depth n lifts this limitation and contains all the information from the neighbourhood w. A counting type automaton of width l is k-CMPA that calculates the graded IT-type of modal depth n and width l of a node in each round n. Likewise, we define counting type automata which calculate the full graded IT-type of modal depth of node in each round
Now, we start formalizing the proof of Theorem 3.3
depth n of
Let II be a set node label symbols, let (G, w) be a pointed II-labeled graph and let k. n E N. The graded IT-type of width & and modal depth of (G, w) (denoted (G.w), is defined recursively as kkn
23

---

follows. For nt = 0 we define that
(G,w) k000
A PAA A pi- pleA(w)
P.AA(1)
Assume we have defined the graded 11-type of width and modal depth of all pointed 11-labeled graphs, and let T denote the set of such types. The graded II-type of (G, w) of width and modal depth n + 1 is defined as follows:
(G.w) = T1 7k,t1
(G.w)
A { (0=eT 1 Tk and G, w F 0=eT}
2=
A A
Tk,n and G, w F 024T).
Canonical bracketing and ordering is used to ensure that no two types logically equivalent, and thus each pointed II-labeled graph has exactly one graded II-type of each modal depth and width.
A counting type automaton of width k over II is k-CMPA defined as follows. The set Q of states the set UnEN Tk.n of graded IT-types of width & (of any modal depth). The initialization function т: PIII) + Q is defined such that π (PP) Tk.0
(G.w) where (G, w) is any pointed II-labeled
graph satisfying exactly the node label symbols in S II. Let :: Tk.n + N be multiset of graded I1-types of width k and modal depth and let J be one such type (note that Tk.n is finite for any k, n N). Let To be the unique type of modal depth 0 in Tk,n that does not contradict We define the transition function d: Q x M(Q) + Q such that
k-1 N(T, = To 1 N(6) = ()A N(O) 2 k},
For other N and 7 that do not all share the same modal depth, we may define the transition as we please such that 8(g, N) = 8(g, NiR) for all y and N.
We similarly define the full graded TT-yye of modal depth n of a pointed IT-labeled graph (G, w) (denoted by ((,")) 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 TO (G.ww = (G.w) for any E N. Assume that we have defined the full graded II-type modal depth n of all pointed II-labeled graphs, and let Tū be the set of such full types. The full graded II-type of modal depth + 1 of (G, w) is defined as follows:
(G,w)) A A (G, - Q=ET } A - (G.w) n1 = To
E21
where N(w) is the set of out-neighbours of w. The formula tells exactly how many neighboiss of node satisfy each full graded type of the previous modal depth; to keep the formulae finite (over finite graphs), instead of containing conjuncts O tells exactly how many out-neighbours a node has.
counting type automaton over II is CMPA defined as follows. The set of states is the set of all full graded II-types. The initialization function :: PIII) > Q defined such that x(P) = T (G,w) where (G, w) is any pointed II-lablled graph satisfying exactly the node label symbols in P. Let N: T, + be multiset of full graded II-types some modal depth n, and let t be one such type. Let To be the unique full type of modal depth 0 in Tú that does not contradict We define the transition function 5: Q x M(Q) - Q such that
8(T, N) = To A A10- [N()= = E
E2
For other N and that do not all share the same modal depth, we may define the transition please.
We prove the following useful property.
Proposition B.6. Each Il-formula yp of modal depth and width & of GML has
24

---

1. a logically equivalent countably infinite disjunction full graded I1-types of modal depth n and
2. a logically equivalent finite disjunction graded II-rypes of width 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..m. as above, denote the set of all graded I1-types of width and modal depth n. Let T = (T of the types in t. Note that this disjunction is finite since the set Ta. is finite. Obviously we have that + n- = 0 and V ② F= y. To show that yp - V ②b, it suffices to show that tb U - n Assume instead that r E Tg. { D Then there exist pointed II-labeled graphs (G, w) and (H, that satisfy such that G, w F sp and H, v F -. Since (G, and (H, v) satisfy the same graded Il-ypee of modal depth n and width k; there can be no II-formula of GML of modal depth at most and width most k that distinguishes (G, w)) and (H, v), but y is such a formula, which is a contradiction. Ergo, V & and & are logically equivalent.
Tk,n
F ()) } and -h = {T Tk.n
F - ), and let V t denote the disjunction
In the case of full graded types we first observe that the set Tú of full graded 11-types of modal depth n is countable. Thus the sets +- = {r E T, F= (p } and - = {T E Ta 7 F -i) } are also countable. Now, with the same proof as for graded types of width k we can show that V t and yp are logically equivalent. Therefore, yp is also logically equivalent to a countably infinite disjunction of full graded II-types of modal depth
Now, we are ready to show the translation from w-GML. to CMPAs.
Lemma B.7. For each N-formula of w-GMT, we can construct an equivalent counting type au- tomaton over 11. If the formula has finite width k, we can also construct an equivalent counting type automaton of width k.
Proof. Assume the class IC of pointed IT-labeled graphs is expressed by the countable disjunction pES oo of II-formulae yp of GMT.
First, we prove the case without the width bound. By Proposition B.6 each to E S is logically equivalent with countably infinite disjunction sp of full graded I1-types of GML such that the modal depth of 9e is the same as the modal depth of so. We define a counting type automaton A whose set F of accepting states is the set of types that appear as disjuncts of yp for any ip S. Now (G, w) E KC if and only if G, w T v if and only if G, w = for some T E F if and only if the state of (G, w) is J in round n in A, where n is the modal depth of Ergo. A accepts exactly the pointed I1-labeled graphs in K.
The case for the width bound is analogous. First with Proposition B.6 we transform each disjunct E S to a finite disjunction g of graded II-type with the same width and modal depth as so. Then, for 2 we construct an equivalent type automaton of width ks where the set of accepting states is the set of graded types of width k that appear as disjuncts of x for any & E S.
Before we prove Lemma B.9 we prove another helpful (and quite obvious) lemma.
Lemma B.8. Two pointed TTlabeled graphs (G, w) and (H, v) satisfy exactly the same full graded 11-type of modal depth (respectively, graded l1-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 II.
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 = O. Two pointed II-labeled graphs (G, w) and (H, v) share the same full graded 11-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 II-labledd graphs (G.w) and (H,v) satisfy the same full graded HItype of modal depth n + if and only if 1) they satisfy the same full graded II-type of modal depth 0 and 2) for each full graded II-type of modal depth n, they have the same number of neighbors that satisfy= r. Now 1) holds and only (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 equivalent to (G, w) and (H, v) satisfying the same full graded 11-type of modal depth 0, and receiving the
25

---

same multiset of states messages in round in each CMPA. By the definition of the transition function, this is equivalent to (G, w) and (H, v) sharing the same state round for each CMPA.
Now, we are able to show the translation from CMPAs w-GML.
Lemma B.9. For each CMPA (respectively, each k- k-CMPA) over IT, we can construct an equivalent TI-orrula of W-GML, (resp., of width k).
Proof. We prove the claim without the width bound, since the case with the width bound is analo- gous. Assume that the class KC of pointed 11-labeled graphs is expressed by the counting message passing automaton over II. Let be the set of all full graded I1-types and let
-
(G,w) E T A accepts the pointed II-labeled graph (G, w) K. in round }. [
We define the countable disjunction VrE and show that G, F Vre+ if and only if A accepts (G, w). Note that 4 is countable since T is countable.
If G, F Vre T, then G, }= Tn (ff,e) for some pointed II-labeled graph (H, v) accepted by A in round This means that (G, w) and (H, v) satisfy the same full graded II-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 s 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 Tn
(G.w)
E Φ and thus G, w + Vrea
Finally, we prove Theorem 3.3
Proof of Theorem 3.3 Note that the proof uses auxiliary results that are introduced in this subsec- tion. Lemma B.7 shows that for each II-formula of w-GML we can construct an equivalent CMPA over II and Lemma B. shows that for each CMPA over II we can construct an equivalent Il-formula of w-GML
By Lemma B.7 and Lemma B.9 is also straightforward to conclude a similar result for bounded CMPAs and width-bounded w- f-rmullf
Theorem B.10. Bounded CMPAs have the same expressive power as bidth-bounded w-GMT, formulae.
B.5 Proof of Theorem
3.4
First we recall Theorem 3.4
Theorem 3.4 GNN have the same expressive power w-GML.
Informally, Theorem 3.4 is proved follows (in the end of this section we give formal proof). We first prove Lemma 1.12 which shows that we can translate any GNN into an equivalent w-GML- formula. To prove Lemma [B.12, we need to first prove an auxiliary result Lemma [B.1 which shows that if two pointed graphs satisfy the same full graded type of modal depth then those two pointed graphs share the same feature vector each round (up to n) with any GNN[B). For these results, we need graded types which were introduced in Section B.4
Informally, the converse direction (Lemma B.13 proved as follows. We first translate the II- formula of w-GML into an equivalent CMPA A over 11 by Theorem 3.3 Then we translate the equiv- alent 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, also consider the where GNN(R]s s are bounded and the w-Gmul-formulae are width-bounddd.
Before proving Lemma B. 12 we first establish the following useful lemma.
26

---

Lemma B.11. Two pointed II-labeled graphs (G, w) and (H, v) satisfy exactly the same full graded II-type of modal depth n (respectively the same graded II-rype of width lo 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 IT.
Proof. The proof is analogous to that of Lemma B.8
With the above lemma, we ready prove Lemma B.12
Lemma B.12. For each GNN[R] 9 over IL, we can construct equivalent II-formula of w- w-GML. Moreover, if is bounded with the bound k, we can construct an equivalent Il-formula of w-GML of width k.
Proof. Assume that 9 GN over (II,). Let K. be the class of pointed II-labeled graphs expressed by G. Now let
4 T (G,ar) | 9 accepts the pointed II-labeled graph (G, w) E KC in round n }.
where To (G.w), is the full graded II-type of modal depth n of (G, w) (see Section B.4). Note that there are only countably many formulae in & since there only countably many full graded Il-types. Consider the counting type automaton A over II, where
the set of accepting states. We will
show that A accepts (G, w) if and only if G accepts (G,
If (G, w) is accepted by A, then G, w F= Ty (H,v) for some pointed II-labeled graph (H, v) accepted by G in round n. This means that (G,w) and (H, u) satisfy the same full graded II-type of modal depth n. By Lemma B.II] this means that (G, w) and (H, v) share the same state in G in each round f & n. Since G accepts (H, 2) in round n, G also accepts (G, w) in round n. Conversely, if g
(G,w) + and thus (G, w) is accepted by A by the definition of accepts (G, w) in round n, then Tn
counting type automata. Thus A and 9 are equivalent. By Theorem 3.3 we can translate the type automaton A into an equivalent II-formula of GGGL Therefore, for G we can obtain an equivalent w-GMI-formula.
Next consider the case where 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 A: o- _ G accepts the pointed II-labeled graph (G, w) K. in round }. The reasoning of the second paragraph is then modified refer to graded types of width i and GNNs with the bound i respectively using Lemma B.11 By Theorem B. we obtain an equivalent width- bounded w- Gormull 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 tool in the proof that follows. A recurrent graph neural network over natural numbers GNN[N] over (II, d). is a GNN[R] over (II, d) where the feature vectors and the domains and co-domains of the functions are restricted to Nd instead of Rdd
Lemma B.13. For each II-formula of wf GMGL, we can construct an equivalent GNN over (II, 1). Moreover, for each Il-foruua of w-GML of width k, we can construct an equivalent bounded GNN(R] over (TI,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 II can be translated into an equivalent GNN[N] over (II, 1). which suffices since counting type automata have the same expressive power as w-GML and CMPAs by Lemma B.y and by Lemma B.7 Informally, each counting type automaton can be simulated by graph neural network as follows. Each full type has minimal tree graph that satisfies the full type. Each such tree can be encoded into 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.
27

---

Now, we formally prove the statement. Let A be counting type automaton. Now we create an equivalent GN over (II, 1) 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 binary string (in 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 ....... Un 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 to assume that the domain of the tree always [ni] for some n N and use the standard ordering of integers.) This is followed by a O.
The next nk bits are bit string b that tells which node label symbol is true in which node; for each & E [n] and i E [k], the ((e - 1) + i): bit of b is and only if T, TT,0 De - Pt.
Finally, the last n² bits form a bit string b', where for each i. E [n]. the ((i - 1)m + j)thh bit of b' is 1 if and only if (o,, vy) E, i..., there is an edge from 2s to v/y.
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 O, the initialization function maps each set of node label symbols to the encoding of the unique one-node tree graph each subsequent round n,
where the node satisfies exactly the node label symbols question. each node receives a multiset N of binary encodings of full graded types of modal depth 1. The aggregation function calculates a binary string that encodes the following graph:
The graph contains a node where every node label symbol is false.
For each copy of each element in the multiset N, the graph contains unique copy of the rooted tree encoded by that element.
There is an edge from to the root of each of these rooted trees; the result is itself rooted tree where r is the root.
The combination function receives a binary string corresponding to the node's full graded type r of modal depth 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
is clear that the constructed GNN [N] & 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[[Rss do not limit the aggregation and combination functions. We can choose the accepting states 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 counting type automaton of width k. We follow similar steps as above with the following modifications.
We convert each graded type of width i and modal depth corresponding rooted tree. We choose the tree with depth n and the least amount of branches; in other words, each node has most l: identical netgneigb
The aggregation function of G constructs a graph in the same way as above, except that it creates at most & copies of a graph encoded by an element in the multiset.
is clear that the resulting GNN is bounded, as the aggregation function is bounded by A.
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 & we can construct an equivalent bounded GNN[[R (or more precisely an equivalent bounded
28

---

GNN[N). Therefore, by Lemma B.9 and by Lemma B.7 for each formula of w- w-GML (and re- spectively for each CMPA) we can construct an equivalent GN Analogously, for each width- bounded formula of w-GML (and resp., for each bounded CMPA) we can construct an equivalent bounded [..
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 subsec-
tion. By Lemma B.12
2 we can construct an equivalent II-formll of w-GML for each GNN[R]
over IT. By Lemma B.13 w-GML.
we can construct an equivalent GNN[R] over II for each II-formula of
B.6 Proof of Remark 3.5
In this section we formally prove the claims Remark 3.5 expressed in Theorems B.15 and B.16 Note that we do not require boundedness for FCMPAs in the statement of the lemma below.
First we prove an auxiliary result.
Lemma B.14. For each FCMPA over II with state sel Q, we can construct an equivalent unre- stricted GNN[F) over (Q
Proof. We encode the FCMPA fully into the GNN[F]. First we give an informal description. The feature vectors encode which state a node in using one-hot encoding, i.e., only the bit correspond- ing to the occupied state is 1 and others are O. For a received multiset M of feature vectors, the 6(g, M) into vector, i.e., it tells
aggregation function encodes the function d Q - Q, 2, for each state which state g satisfies 8(q,, M) = 9, To encode such a function we need |Q]² components in the feature vector. Finally, the combination function receives (the encodings of) g and âM and computes (the encoding of) d
Now we define the construction formally. Let II be set of node label symbols. Let A = (Q, n. 0, F) be an FCMPA over II. Assume some arbitrary ordering <q between the states Q. Let 91.... 900 enumerate the states of Q w.r.t. <q- Given a multiset M E M(() the function dA Q Q.
(g)(g) = ((g. M) specified by M is possible to encode to the binary string d E f0, 1 as follows. d (4:) = gj. then the ((i- - 1)[Q1 + j):th bit of d 1; the other bits are 0. That is, dM encodes the function dar in binary.
We construct GNN over (II, [Ql²) over a floating prinngg-ponnttto system S that includes at least and 1 (that is to say, small floating-poit systems suffice). For all I IQ), we let d; E sIQI denote the one-hot string where exactly the ith bit is and the other bits are Os.
Let P PCI II. The initialization function x' is defined as T'() = d, where π T(P) = 4i-
The aggregation function AGG is defined as follows. Assume that the multiset M contains only one-hot strings d,, where IQ]. Now M corresponds to multiset M where each d is replaced by d:- Then AGG(M) is dyr. Otherwise, the aggregation function is defined an arbitrary way.
The combination function COM is defined as follows. Let d, d' E SIQI such that d = d; is a one-hot string for some [Q] and d' d for some multiset M M(Q). Then we define that COM(d, d') COM(d, d dj if and only if ( gı. Otherwise COM is defined in an arbitrary way.
The set F" of accepting states defined as follows. If d = d, is a one-hot string, then dj F' if and only if 93 E F. Otherwise F² is defined in arbitrary way.
is easy to show by induction over n E N that for any pointed II-lablldd graph (G, w). the state of A at w in round q E Q if and only if the state of G at w in round is d,-
We note that this proof based only on providing two embeddings to Sd where the floating- point system and d is the dimension of the GNN[F]. The first is embedding from the set Q
29

---

aa) and and the second is an embedding from the set of functions Q - Q, and the two embeddings need be related in any way. Thus, any choice of floating-poin system and dimension such that there are at least [Q expressible feature vectors, would suffice and we would be able to define such embeddings and the subsequent aggregation and combination functions. In particular, dimension |Q1 suffices for any floating-poin system S.
L
The first claim in Remark 3.5 is stated as follows.
Theorem B.15. FCMPAs have the same expressive power unrestricted GNN[F]s.
Proof. It is straightforward translate an unrestricted GNN[F] into an equivalent FCMPA. By Lemma B.14 we can also construct an equivalent unrestricted GNN[F) for each FCMPA.
The second claim in Remark 3.5 is stated as follows.
Theorem B.16. Bounded [k)s have the same expressive power width-bounded w- GM..
[B3] By Lemma B.12 12 can Proof. Note that this proof uses auxiliary results that are in Appendix B.5 construct an equivalent width-bounded IT-formula of w-GMT. for each bounded GNN over IT. By Lemma 1.13 we construct an equivalent bounded GNN[R] over II for each width-bounded II-fomula of w-G
B.7 Proof that multiple GNN layers can be simulated using a single layer
In the literature, GNNs are often defined as running for constant number of iterations unlike our recurrent GNN model, see for example [5] 13 12] Fach iteration of the GNN is considered its own layer, and each layer has own aggregation and combination function. More formally for any N N, an N-layer GNN[R] GN over (II, d) is tuple (IR n, (8) (E(N)) F), where m: P(IT) - Rd the initialization function, 85: Rd M(Rd) + Rd is the transition function of layer i of the form (g) .) COM' (M)) (where AGG' M(R")) Rd is the aggregation function of layer and COM': Rdd Rdd Rd is the combination function of layer i) and F C I is the set of accepting feature vectors. We define the computation of GN in a II-labeled graph G = (V, E, A) follows. In round O, the feature vector of node is z क (A())). In round E [N] the feature vector of node is
/ - [| (t. u) E E = COM' AGG (11 (
(v, E E E)))
We say that IN accepts a pointed graph (G, w) if and only if x E F. Concepts concerning node properties, equivalence and same expressive power are defined as for other models of GNNs. Proposition B.17. For each N-layer GNN[R], GN
construct equivalent constant-iteratio
Proof. Intuitively, we add clock to the feature vectors of the N-layer GNN that tells the transi- tion function of the constant-iteration GNN(RR which layer to simulate.
Let GN (Rd, (5') )iE(). F) be an N-layer GNN[R] over (II, d). We construct constant- iteration GNN[R] NG ((R+N n',8 8' F"), over (II, d + N) as follows. all feature vectors used, exactly one of the last N elements is and the others are Os. For the initialization function n' define for all / that (PP) (T(P) (ill...,,(((),,, 1,0, O) E M where (P), denotes the ith element of (P)) Rdd. Before specifying the transition function, define the following:
For each feature vector x = (xI, (a+N) E Rd+N we let x' x" = (Ia+1...., T.N.N..
Likewise, for each M E M(RR+N), let M' be M where each r M is replaced with x'.
Let f: N + R be a function such that we have f(1, (1,0,, .,................ ,0) (0, 1,0, .......... 0), ...0.....))........... = (0, 0, 1, 0, .....)........... 1,..,,
..... 0),
and so forth until f(O.... 0, 1) (O.... ........00 0)
30

---

Now, assuming that z E RA+N and M E M(R2+N) such that exactly the ith element of x" and each y" in M is 1 and others are Os, we define that (z, M (6 MM). ; f (a")) (i.e.. we concatenate (a',, M*) and (x))). For other inputs, we define 8' arbitrarily. The set F* of accepting feature vectors is the set of feature vectors (#1..... Td. 0, ........... 0, 1), where (I1,...,,4a) F.)
an accepting feature vector of GN. It is easy to show that (G. N) accepts a pointed II-labeled graph (G, w) if and only if GN accepts (G, w) (note that for both N-layer GNN[R]s and constnntittrration GNN[R]s.
only the feature vector of node in round N counts for acceptance).
B.8 Proof of Theorem 3.6
First we recall Theorem
3.6
Theorem 3.6 w-GML.
Constant-iteration GNN[R]s have the same expressive power as depth-bounded
Proof. Note that we heavily use the proofs of Lemma B.12 and Lemma B.13
Assume that (G, N) is constant-iteratioo CNN[RR over (T, Let K. be the class of pointed II-labeled graphs expressed by (G,N), N). Now let
(G.w) = TN
g accepts (G, w) E KC in round N
(G,w) is the full graded II-type of modal depth N of (G, w) (see Section B.4 Consider the where IN counting type automaton A over II, where & is the set of accepting states. It is easy to show with an analogous argument as in the proof of I Lemma B.12 that A accepts (G, w) if and only if (9, N) accepts (G, w).
For the converse, assume that ta is a depth-bounded u-GML-formula over 11 of modal depth D. First by Lemma B.6 translate into an equivalent formula v² which is a disjunction of full graded I1-types such that the modal depth of v/* is the same as v. By Lemma B.7 v6* is equivalent counting type automaton A over whose accepting states are the types that appear as disjuncts of qi" Since the depth of each type is bounded by D. each pointed graph accepted by A is accepted in some round r S D. By the proof of Lemma B.13 we can construct an equivalent GNN[R] G over II such that for all pointed II-labeled graphs (G, w) and for all N: AA accepts (G, w) in round iff G accepts (G, w) in round n. Now, it is easy to modify 9 such that 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 += 4/" iff G, w -= vb.
C Appendix: Characterizing GNNs over MSO-expressible properties
C.1 Proof of Lemma
In 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 wo E V be node in G. walk in G starting at wo is sequence p w...... wn of elements of V such that (w,, w;41) E E for all S n - 1. We use tail(p) to denote wa. Now, the unraveling of G at wo the graph U (V', E', X') defined as follows:
V' the set of all walks in starting at wp
E" { (p.p') V' V' p' pw for some E VV
(p) X(tail(p)) for all p V
We say that formula (0x) is invariant under unraveling if for every graph G (V, E, A) and every w V. we have -= (pw) iff }= p(w), with U the unraveling of at w. Invariance under unraveling is defined in the same way also for GNNs. The following is easy to prove, see for example 77.
Lemma C.I. The following are invariant under unraveling: w-GML, GMSC, GNN[F)s, GNN[R]s, and their constant iteration depth versions.
31

---

We recall Lemma
4.2 and prove it.
Lemma
4.2 expressible.
Any property expressible in MSO and constant-iteratoon GNN is also FO-
Proof. We present two different proofs. The first one is independent from Theorem and the second one is not.
Assume that the MSO-formula ((x)) over En expresses the same node property as the constant iteration depth GNN[R] (G, k) over EN, where & E N is the iteration depth of G. It is shown in [TO] that on every class of graphs of bounded treedepth, MSO and FO have the same expressive power. The class C' of all tree-shaped Ely-labeled graphs of depth at most & has bounded treedepth. We thus find an FO-formula (xx) over NN that is logically equivalent to p(x) on C, i.e. for all T E C with root w we have 7' - ((w) iff p(w).
We may manipulate (1r) into an FO-formula (xx) such that for any pointed graph (G, w²), we have G + (w) if and only if UR + (w) with UR the restriction of the unraveling of G w to elements on level at most k. More precisely, to construct (z) we do the following:
First we define auxiliary formula
(xx = V
Byo. ... Bye (v0 = x
A 0Sm<e
E(ym, Bm+1))
OSESk
which intuitively states that y lies at distance most from x.
Then 0(x) is obtained from ((x) by recursively replacing subformulae of type Byd with ( 3) A +b) as follows. First, we simultancously replace each subformula of quan- tifier depth 1. Having replaced subformulae of quantifier depth E, we then simultaneously replace subformulae of quantifier depth +
We then have, for every graph G, the following where U is the unraveling of G at w and Ug denotes the restriction of U to elements on level most (the root being on level 0):
G = ((w) iff UR F ((w) iff UR + ((w) iff G + Aw)
The first equivalence holds because is expresses the same property as G, the second one by choice of 0, and the third one by construction of 0.
We also present an alternative proof which takes advantage Theorem 4.1 By Theorem 3.6 (G. k) is equivalent to some depth-bounded En-formula & of w-GML. On the other hand, by Theorem some GMSC-program A, since the property expressed by is expressible
4.1 is equivalent in MSO. By the proof of Proposition 2.6] A is equivalent to some width-bounded Ex-formula si of w-GM. Now, it is easy show that & is equivalent some -frfouulla v0- of GML, since v is depth-bounder and v/ is disjunctions of (non-full) graded types by applying Proposition [ (see also Appendix [B.4 for the definition of graded types). Since (G. k) is equivalent to the Ey-foorull ri* of GML, it expresses node property also expressible in FO, since GML fragment of FO.
This can be seen by transforming ab and a// into
C.2 Proof of Theorem
First we recall Theorem
Theorem 4.1 Let P be property expressible in MSO. Then P is expressible as a GNN[ER if and
only if it is expressible in GMSC.
We recall some details of the proof sketch of Theorem We use an automaton model proposed 31 that captures the expressive power of MSO on tree-shaped graphs. (Note that the automaton model is defined in Section 4 We then show that the automaton for an MSO-formula şo that expresses the same property as GNN(R] (and thus a formula of w-GMT.) can be translated into GMSC-program expressing the same property. To do this, prove the important Lemma
32

---

which shows that for all tree-shaped graphs T: the automaton for accepts T iff there is k- p-reffx decoration of ' for some E N. Intuitively, a k-prefi decoration of I represents a set of accepting runs of the automaton for yp on the prefix T& of 7 (the formal definitions are in Section 4. Then we build GMSC-program that accepts a tree-shaped graph 7 with root w iff there k-prefix decoration of T for some &s E N.
We next define in formal way the semantics of parity tree automata (the definition of parity tree automaton (PTA) is in Section 4 For what follows, a tree 7' is a subset of N", the set of all finite words over N. that closed under prefixes. We say that y E T is a successor of x in T y zn for some 72 E N. Henceforth we will call successors out-neighbours. Note that the empty word then the root of any tree T. E-labeled tree is pair (T, E) with T tree and f: T + Σ node labeling function. A maximal path π in tree T is a subset of 'T' such that E E т and for each E π that is not a leaf in T, æ contains one out-neighhour of x.
Definition C.2 (Run). Let G be a Ey-labeled graph with G = (V, E, X) and = (Q. Ex. 10. A, PTA. A run of A on G is a Q x V-labeled tree (T) such that the following conditions are satisfied:
((e) = (qo: 2) for some e E V;
2. for every x E T with {(x) = (g. v). the following graph satisfies the formula Agg. A(v)
the universe consists of all a with (v, u) E E; each unary predicate q' Q is interpreted as the set
{ [u] there is an out-neighbout y of a in such that E(y) = (4', u)
run (T, E) is accepting if for every infinite maximal path æ of T, the maximal i E N, for which the set for ((x) (g, d) with 224)) i} is infinite, is even. We use L(A) to denote the language accepted by A, i.e., the set of Ia-llbee graphs such that there is an accepting run A on G.
We remark that, in contrast to the standard semantics of FO, the graph defined in Point 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 = O. Note that a transition formula & without existential quantifiers is a formula of the form A=( diff(=) -> v). where 1a a disjunction of conjunctions of atoms g(z) which are unary predicates for the states of the automaton. Such formula may or may not be true in non-empty graph. For example, if vo in d is a logical falsity (the empty disjunction), then e is satisfied only in the empty graph.
Let P be node property over En which is expressible in MSO and also in w-GML. Let A = (Q, Σn, qu. A. be PTA that is obtained by Theorem 4.6 from P. If v is the w-GML- formula expressing P, then we may simply say that A and 3 are equivalent. We identify a sequence Si...., Sn of subsets of Q with a graph struct(S)...., defined as follows:
the universe is [1,...,n]:
* each unary predicate q' E Q is interpreted as the set {i g' S.).
For tree-shaped graph T. we let Tj denote the restriction of T to the nodes whose distance from the root is at most k. An extension of Ti is then any tree-shaped graph T" such that T% = Th. that is, T' is obtained from Ti by extending the tree from the nodes at distance l from the root by attaching subtrees, but not from any node at distance & < k from the root. Note that k-prefix decorations of and universal sets of states are defined in Section 4
Lemma 4.7 For every tree-shaped Σ -laeele graph T: T L(A) and only if there is a k-prefix decoration of T", for some k e N.
'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 given graph. Informally, the semantics introduced here represents a winning strategy of Eloise parity games and similar semantics are used for example in (3].
Note that the graph is empty if and only if is dead end in G.
33

---

Proof. "=". Assume that T E L(A). Let V, ii be the En-formula of w- that A is equivalent to. Then T - Vi for some Let be the modal depth of v/ Then T - vb; for every extension T" of Th.
Next we construct a mapping f:: V2 P(P(Q)) and show that js is a k--prefix decoration of (T, w))- We construct μ as follows. For all v E V on the level k. we define juv) as the universal set for \(v). Then analogously the third condition in the definition of k-prefix decorations, we define uut) for each node on 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 E p(w), Qo E S. Then we may conclude that is a k-prefix decoration.
Assume by contradiction that there exists set S E pu()) such that qu & S. (Note that uu(o) * 0 for all v E V2 by the definition of k-prefix decorations.) ) By Condition 3 of k-prefix decorations, there must exist sets S p(ut),...., S,,, E pl(),, (where ut,-.. ui,...,,M u% are the nodes on level 1) such that q E S iff the transition formula Agg (A(w)) is satisfied in the graph where each ut is labeled S for each S S ni. By the same logic, we find such sets ST E ju(u"",, ,,.,, Sme (where "I"
E uu u(v"... ) 1n are the nodes on level m) for each m S k (note that these nodes do not necessarily share the same predecessor). Let T be extension of Ti that is obtained by attaching to each node u of Te on level h 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.c., Q1" = S.
Now, we can demonstrate that there is no accepting run rT (Trx, E) of A on T'. Any such run has to begin with f(E) (go. w). Note that the out-neighbours of cannot be labeled with exactly the labels u() such that q E S) because (1o, X(wi) is not satisfied in the graph consisting of the out-neighbours ot of w labeled with S for each S i S 01. In fact, the out-neighhours 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) 1 - (V,E,X) / a for all X CA
Thus, there is an out-neighbour I1 of E in Tr such that {(z)) (q. u!) where q $ S. and we may continue this examination starting from xı in the same way. Inductively, we see that for any level m we find a son Im of dmm-1 such that f(rm) = (g, u,") where q & S.T including the level m = where we let {(xx)) by the run 'Ty that A accepts the tree T rooted at uf when started in state q. Thus, q E St. contradiction.
(q, n²). Thus q & S/S However, we have S QI and is witnessed
"<", Let u: V2 + P(P(Q)) be a k-prefix decoration of T. for some k. We may construct from an accepting run r = (T', E) of A on T. For every node v in T. on level k let T. denote the subtree of T rooted at Let semi-run be defined like 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 Tg on level Since p(v) is universal for A(e). we find an S. E ((v)) such that q E S. if and only if T, E L(Ag)- (Note that (u(o) * 0 for all v E Vi by the definition of k-prefix decorations.) Consequently, for each q E S, we find an accepting semi-run Te.g = (Th.. ev.g) of A on T, with (e) = (4, r). We now proceed upwards across Te, assembling all these semi-runs into a run. In particular, we choose set S. E u(u) for every node in Tg and, for all q E Su, a semi-run r Tu.q = (Ta.g> lu.g) with (e) = (q. u).
Let be node in T's that has not yet been treated and such that its out-neighbours .j...., Un have already been treated, that is, we have already selected a set S.,, E p(u.) for S S n along with the associated semi-runs. Due to Condition 3 of k-prefix decorations, we find a set S, E μ(v) such that for each 9 E S,: Agg. X(v)) is satisfied by the graph struct(Sa,.... S..). Choose this set S. I As for the semi-runs, let S.. Then A(q, A(v)) is satisfied by the above graph. We may thus choose as Fn.g the semi-run run that is obtained as follows:
1. start with a fresh root e and set (x.g(e) (4, v);
2. for each E fl...., n and each o' Su,, add the semi-run "ar.g' as a subtree, making the root of Tu an out-neighbour of the fresh root that we had chosen.
'Note that if u has no oui-neigh then S. is the set of states 9 such that A(g. A(v)) is satisfied in the empty graph.
34

---

Note in step 2 that for each 1 S i n, if Su, 00 then semi-run Fu..'' is added as subtree. Let w the root of T. view of Condition 1 of k-prefix decorations, it is easy to verify that the semi-run Tw-go is in fact a run of A on T. Moreover, this run is accepting since we had started with accepting semi-runs at the nodes v in TE on level k and the finite initial piece that Tw fw.go adds on top of those semi-runs has no impact on which states occur infinitely often in infinite paths.
L
may finish the proof of Theorem 4.1 by constructing that for every tree-shaped Na-labeled graph 7 with root w, we have T, w == A iff there is k-prefix decoration of T, for some k. The definition of A follows the definition of k-prefix decorations. This construction serves as the proof of Lemma C.4
By Lemma 4.7
such
below it.
We define fresh schema variable Xs for all S S Q. First, set P Σn of node label symbols can be specified with the formula
A PEP
A P. PEEN\PP
:p:=
which states that the node label symbols P are true and all others are false. Let Qp denote the universal set for P. For every Xs, the program A contains the following terminal clause, reflecting Condition 2 of k-prefix decorations:
Xs(0)=
V sp. SEQ,
Note that if the disjunction is empty, we have Xs(0) :-
We also define a special appointed predicate A that true when all the head predicates Xs that do not contain go are false, reflecting Condition I of k-prefix decorations. More formally A is the only appointed predicate of the program, and it is defined as follows: A(0) and
A
Xs.
90
For the iteration clauses of head predicates Xs. we need some preliminaries. Let K be the maximum over all A such that A mentions transition formula
1z Bark (diff ,., A (z1)
(xx) A A= diff (1. rx) v))
MK+1(P(()) is multiset of sets of states that contains each set of states at most K + 1 times. A sequence Si...., S,, of subsets of Q realizes the counting configura- tion e for each S S Q, one of the following holds:
counting configuration
c(S) < K and the number of sets St among S Sn with S; S is c(S);
* c(S) K and the number of sets S, among S,,...,,,
Sn with S, S exceeds K.
It is easy to prove the following lemma.
Lemma C.3. Let be a transition formula mentioned in and assume that Si,..., Sn and counting configuration. Then struct(S,....,.5., satisfies 0 iff "S. satisfies 0.
S!...., Sy,, realize the
By the above lemma, we may write e - 0, meaning that struct(S),.... S.)) satisfies 1 for any (equivalently: all) Si..... S, that realize
is easy to see that can specify counting configuration E MM+ (P(()) in GMSC because we can count out-neighbours; for example, we can write the following formula, which states that for each set S of states there exactly c(S) out-ncighbours where the label includes S, unless c(S) K + 1, in which case it permits more such ouighbigb..uss
w= ==
A
A
A
O2K+1Xs.
c(S)
c(5)=K+1
35

---

For each set P of node label symbols and set S of states, we can specify the set of counting con- figurations in (P(I( that satisfy formula Agq, P) and only q E S with the following disjunction:
V
S.P
(F
Recall also that the formula yr specifies the set of node label symbols in P. The iteration clause for Xs must state that there is a set P of node label symbols that are true and for which s,r is true. This can be expressed as below:
Xs V (ppAWs.r)
PCEN
We prove that the GMMC--rrggrm A characterizes k-prefix decorations associated with A. A pseudo k-prefix decoration l defined like a k-prefix decoration except that it needs not sat- isfy the first condition of the definition of k-prefix decorations (that is, every set in the root given by Iu does not need to contain the initial state). Now, given
N and a tree-shaped -y-labeled graph T, let pły denote the pscudo Ê-prefix decoration of T. For each e E N and each set S of states of A, we show by induction on n E [0; {] that for every tree-shaped -a-llllled graph T and for each
node in T on level e n,, we have
T, T = SE
In the case n = 0, the claim holds trivially for the nodes v on level & by definition of A, since then T, Xg 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 + 1. Let v be node of on the level 8 - (n 1 1)..
First assume that T. Xg*t that is, for some P ΣN, we have T, F o6 and T, F V, Therefore, there is a multiset e E MK+1 (P(Q)) such that e + Agg, P) iff q E S and T, += v2 Thus, for every set S' of states of A we have that if c(S") neighbours vI..... Um of such that T, 1; }= Xÿ. for every E [m], and if (SS)) K 1, there are at least K + 1 out neighbours Ui...., UK+1 of v such that T, U, + Xg. for every i E [K + 1]. By the induction hypothesis, for every set S' of states of A we have that c(S') m S K, there exactly
m S K, there are exactly m out-
out-neighbours U1:--., Um of such that S' 11 for every i [m], and if c(S') K 1, there at least K + 1 out-neighbours 11,- .1..... UK+1 U1+1 of v such that S' E (1:) for every i E [K +1]. Since e F A(q, P) iff & E S and by the definition of pseudo k-prefix decorations, we have S E (t).
Then assume that S E (v). Let (ui...., Um be the set of out-neighbours of v. By the induction hypothesis for each E [m]] and each set Set S' of states of A. it holds that S" E (1. iff T, vs } X By the definition of pseudo k-prefix decorations there sets S₁ (v1)). S, (vm) such that 9 E 5 iff struct(S),.-.. Sm) F Aqg, P), where P is the set of node label symbols that true in Now, let c MK+1 (P(()) be counting configuration realized by Si...., Sm. Now since K is the maximum over all A such that A mentions a transition formula
1 3z Boyk (diff (aff IK) A (x1) A (xxx) A A2( diff (2 21. ................................ 2K) +)).
have + A(q, P). Therefore, T, v + vi and trivially T, + 4p. and thus T, -x5+1
Now, if accepts a Labelee tree-shaped graph (T, w), then by the result above it means that there a pseudo k-prrefi decoration μ such that T, w }= A Thus in round & we have T, w IA X for all S where qo & S. Therefore S & p(w) for all S where go $ S, i.e., is actually k-prefix decoration. Similarly if a tree-shaped graph (T' w) has a k-prefix decoration, then T, w f=r A by the result above. Thus we have proved the lemma below.
Lemma C.4. For every tree-dhaped Llabelled graph T with root we T. |= A iff there is k-prefix decoration T,, for some
Now we are ready to prove Theorem
36

---

Proof of Theorem 4.7 Note that some of the results needed for this proof are given in this appendix section and some are given outside the appendix. Let be a node property expressible in MSO by an MSO-formula (f(x) over EN-
Assume that P is expressible by Ey-program of GMSC. By Proposition 2.6 P is also expressible CN-ffrmula of w-GML and thus by Theorem 3.4 as GNN[R] over Vvv For the converse, assume that P is expressible as GNN[[R] over N'.. Thus P expressible by 2 of w-GML by Theorem 3.4 Therefore, there is a PTA A and a Ex-program A of GMSC such that for any Exyllbeled graph G with root ws
G = (ww)
Theyrem
the unraveling U of G at w is in L(A)
Lemma
47
there a k-prefix decoration of U, for some & E
Lemana
U, w F
Lemma M
G, w = A.
Thus, we have proven Theorem
C.3 Proof of Theorem
We recall and prove Theorem
Theorem 4.3, Let P be a node property expressible in MSO. Then P expressible as a GNN[RR if and only if t is expressible as a GN The same is true for constant constant-ttrration GNNs.
P expressible as GNN[R] iff it is expressible in GMSC. Thus by Theorem 3.2 P is expressible as a GNN[R] iff it is expressible as a GNN[F).
Proof. Let P an MS0-expressible property over Σx. By Theorem 4.1
For constant-iteration GNNs we work as follows. First assume that P is expressible as a constant- iteration GNN[R] over Σv. Then by Lemma 4.2 is also expressible in FO. Thus, by Theorem 4.2 in [5] P is expressible by Nn-formula of GML (trivially, each constant-iteration GNN (G. L) trivial translate to an L-layer GNN; see Appendix [B.7 for the definition of L--layer GNNs). For GML-formula it is easy to construct an equivalent constant-iteration GNN[F]; the technique essentially the same as in the proof of Lemma (omit the clock in the construction) and in the proof of Theorem 4.2 in (5] The converse direction is trivial.
D Appendix: Conclusion
D.1 note on other termination conditions
A variant of our proofs gives a counterpart of Theorem 3.2 for recurrent GNNs with a termination condition based on fixed points, studied under the name of "ReeGNN" in 26 and closely related to the termination condition in 30 II.
We start by defining fixed point acceptance condition for GNNs and for GMSC. Let & be GNN over II, let (G, w) be a pointed II-labeled graph, and let ott denote the feature vector of w in round We say that G fixed point accepts (G, w) if there is round N such that
F for all T > L.
We define the same accepting condition for GMSC analogously. Let A be a I1-program of GMSC, let A be the set of appointed predicates of A and let (G, w) be pointed 11-labeled graph. We say that A fixed point accepts (G, w) if there is a round E N such that for all T Z t we have G. w === X for some X E A.
Next we discuss how the proof of Theorem 3.2 modified such that the same result holds with fixed point acceptance.
Theorem D.I. The following three have the same expressive power relative to fixed point accep-
tance: GNN[Fss, GMSC, and R-simple aggregate-combine GNN[F]s.
Proof. We start by showing that each GNN can be translated into an equivalent GMSC- proogra relative to fixed point acceptance. First we note that it is easy translate a GNN[F] & over (II, d)
37

---

into an equivalent bounded FCMPA A over II such that the following holds. Let x denote the feature vector of & in round at node w and respectively let y denote the state of A in round at node w. Let Fg and FA denote the accepting states of G and A respectively. Then for all pointed IT-labeled graphs (G, w) and for all E it holds that
a'y Fg > viw E
Moreover, the construction in the proof of Lemma B.3 shows that we can construct GMSC- program over II for A with the set of appointed predicates such that for all pointed I[-labeled graphs (G, w) and for all t N we have
G X' for some X E A + ynn E FA-
Clearly, for all pointed Il-labeled graphs (G, w): g fixed point accepts (G, w) iff A fixed point accepts (G, w).
Then we show that each GMSC- proogram A can be translated into an equivalent R-simple aggregate- combine GNN[F] 9 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 VN+++1 7 Now it is clear for all pointed graphs (G, w) that A fixed point accepts (G, w) if and only if G fixed points accepts (G, w)
38

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: This theoretical paper and all results listed the abstract and intro are ultimately justified via proofs, occasionally with proof sketches with full proofs in the appendix. We also discuss limitations of our results.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results
be expected to generalize other settings.
fine to include aspirational goals motivation as long it is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors? Answer: [Yes]
Justification: The limitations are introduced in the "Limitations" section the conclusion and also outside that in the paper.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "L.mmtations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The au- thors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the ap- proach. For example, a facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to ad- dress problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't it acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
39

---

Answer: [Yes]
Justification: All claims are formally and fully proven, but some of the proofs are in the appendix. For proofs in the appendix, sketches provided in the main text, with the exception of three results relating to constant-iteration GNNs, two of which have highly corresponding, more general results in the paper, and one of which follows mainly from an external article.
Guidelines:
The answer NA means that the paper does not include theoretical results. All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theo- rems.
The proofs can either appear in the main paper the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be comple- mented by formal proof's provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclu- sions of the paper (regardless of whether the code and data are provided or not)?
Answer: [NA]
Justification: The paper does not include experiments.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, No answer this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how replicate the results, access a hosted model (e.g.. in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate the research performed.
While NeurlPS does not require releasing code, the conference does require all sub- missions to provide some reasonable avenue for reproducibility, which may depend on the nature the contribution. For example
(a) If the contribution is primarily new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (c.g., a large language model), then there should either be way to access this model for reproducing the results or way to produce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case au- thors are welcome to describe the particular way they provide for reproducibiliity In the case of closed-source models, it may be that access to the model is limited in
40

---

some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [NA]
Justification:
The paper does not include experiments requiring code.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips. cc/
public/guide saaec//ggiss//eee /ttp///dee//eeeuuuiiisssseeeeeee wwweeaummsssiooooooooooooooooooo Policc for more details.
While we encourage the release of code and data, understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed reproduce the results. See the NeurlPS code and data submission guidelines (https: //nips.c//// htwpbiipguuule/////pppppeeeeeeet http://gieeeeeeeeeubmbeieeeeeee woweddeSbmsssiiioooooo
for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [NA]
Justification:
The paper does not include experiments.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropri- ate information about the statistical significance of the experiments?
Answer: [NA]
Justification:
The paper does not include experiments.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
41

---

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 the standard error of the mean.
It is OK to report I-sigma error bars, but one should state it. The authors should prefer- ably 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 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 the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
Question:
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed 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, 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 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 t make it into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics https: http://wwwppp.ppppooo..cccccaaaa
Answer: [Yes]
Justification: The code of ethics is not violated, as the paper does 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 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 deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (c.g., if there is special consid- cration due to laws or regulations their jurisdiction).
10. 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 theory paper, and (sufficiently direct) paths to specific positive negative applications are difficult to conceive.
42

---

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 spe- cific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied partieular applications, let alone deployments. However, if there is direct path any negative applications, the authors should point it out. For example, it is legitimate to point that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, is not needed to point out that a generic algorithm for optimizing neural networks could enable people 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 mitiga- tion strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of MI..
11. Safeguards
Does the paper deseribe safeguards that have been put in place for responsible release of data or models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
The article does not involve any datasets.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by re- quiring 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 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 used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
43

---

For scraped data from a particular source (e.g., website), the copyright and terms of service of that souree should be provided.
assets are released, the license, copyright information, and terms of use the pack- age should be provided. For popular datasets, patasets.paeerswittte paperswithcode cww dataseta has curated licenses for some datasets. Their licensing guide can help determine the li- cense of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is available online, the authors are encouraged to reach out to the asset's s creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documenta- tion provided alongside the assets?
Answer: [NA]
Justification:
The paper does not release new assets.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/moodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
For crowdsourcing experiments and research with human subjects, does the pa- per include the full text of instructions given participants and screenshots, if applicable, as well as details about compensation (if any)?
Question:
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contri- bution of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, cura- tion, or other labor should paid at least the minimum wage the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
44

---

Depending on the country in which research is conducted, IRB approval (or equiva- lent) 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.
45


Reviews:
[{"review_id": "N3oaRIjWwo", "reviewer": "Reviewer_3ziF", "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:\n- 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.\n- Reals vs. Floats: When floats are replaced with real numbers, an infinitary logic is required.\n- 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.", "questions": "- Please comment on **W1**, **W2** and **W3**.\n \n- 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": "This has been addressed in a satisfactory way by the authors.", "rating": 8, "confidence": 5, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "**S1 Relevant Research Question:** The investigation into the expressive power of recurrent GNNs is pertinent and interesting, despite their less widespread use compared to non-recurrent GNNs.\n\n**S2 Precise Characterization:** The results offer a robust and precise characterization of the power of recurrent GNNs, using either floats or reals, from a logical perspective. These findings surpass the seminal work by Barceló et al., achieving results without assuming a background logic. When MSO is considered, the results extend those of Pfluger et al., and they also allow for the recovery of the first-order logic case as discussed by Barceló et al.\n\n**S3 Well-Written and Interesting Techniques:** The paper is well-written, and the proofs involve intriguing techniques, yielding non-trivial results.", "weaknesses": "**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.\n\n**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.\n\n**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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Concerning **W1**: Grohe's setup is different from ours in both [11] and [12]; most notably, Grohe uses non-recurrent GNNs rather than recurrent ones. Also, the articles use reals and dyadic rationals. We will add further discussion on Grohe's work as well as on [6] and [23].\n\nConcerning the first part of **W2**, our approach is equivalent to that used in related work on the topic, in particular that of Barceló et al. [5], where the labeling of the nodes with proposition symbols is itself viewed as the initial feature vector in the GNN computation. It is easy to simulate the initialization of [5] in our setting and vice versa. The main difference is that we have explicitly included a separate initialization function (based on the propositions true at a node) to the definition of GNN.\n\nWe suppose that the initialization being fixed (e.g., an all-ones vector) means that we run GNNs in graphs without node labels. In that setting, our results remain true as this scenario is the special case of our approach where the propositional vocabulary is empty.\n\nConcerning the second part of **W2**: There are different kinds of semantics for recurrent GNNs in the literature, including ones with different kinds of fixed points. For example, the pioneering GNN paper [26] uses global fixed points; a global fixed point means that a computation step of the GNN would not change the feature vector of any node in the graph. On the other hand, the RecGNN semantics of [23] uses local fixed points, that is, only the node in question must ultimately keep repeating within an appointed set of feature vectors. This is less restrictive than the case with global fixed points. The exact relation between different recurrent GNN formalisms depends on many parameters including whether reals or floats are used, which aggregate-combine functions are admitted, and whether global readouts are available. We will add some first observations to the paper, but leave a thorough investigation for future work. Please note that the issue of investigating only one acceptance condition is also discussed in the limitations section of our paper, so it was in that sense not in the primary scope of the current submission.\n\nAlso, as pointed out in the conclusion, we obtain a counterpart of Theorem 3.2 for floating-point GNNs with the same accepting condition as in [23] by modifying the acceptance condition of GMSC accordingly. Furthermore, it is interesting to note that the mu-fragment of graded mu-calculus translates into GMSC (cf. the response to all reviewers), bringing its least-fixed point acceptance to the picture.\n\nConcerning **W3**, we agree that the connection between distributed automata and GNNs should be made more clear, which we will do. Our main result on this is Proposition 3.1, which links finite-state distributed automata to GMSC, and GMSC is further linked to floating-point GNNs via Theorem 3.2. Also, Theorem 3.3 links unrestricted distributed automata to omega-GML, and omega-GML is also further linked to GNNs with reals via Theorem 3.4. Please note also that with these equivalences, Theorem 4.3 gives various links between distributed automata and GNNs. Concerning Proposition 3.1, it states expressive equivalence between GMSC and the distributed algorithm class MB (cf. [15]) when based on finite-state distributed automata on directed, node-labeled graphs. Intuitively, an algorithm in MB reads multisets of a node's neighbours' messages and thereby determines its next state, also taking into account its own previous state.\n\nRegarding the question about the **Proof Sketch of Theorem 3.2**, please note that the choice of the floating-point system used in the GNN depends on the constants k that occur in the counting modalities of the GMSC program. So the resulting GNNs are actually equipped with different floating-point systems, depending on the GMSC program that they encode. Please note that fixing a single floating-point system would in some sense trivialize the computing model, because only a finite number of functions could be defined. It is indeed good to mention this more explicitly in the paper, and we shall do so.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "tgGLoqF9uq", "reviewer": "Reviewer_vmsJ", "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.\n\nIn particular, the paper demonstrates that:\n- GNNs working with floats, even those with a “simple” aggregation-combine structure, are equally expressive as the graded modal substitution calculus (GMSC).\n- GNNs working with reals are equally expressive as graded modal logic with infinite disjunctions.\n- Relative to queries expressible by monadic second-order logic (MSO), GNNs working with reals and those working with floats are equally expressive.\n\nAs a byproduct, the arguments employ automata-theoretical tools, providing a concise characterization of GNNs through the concept of counting message-passing automata (CMPA).", "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": "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.", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 4, "strengths": "This work aligns with a current trend in characterizing the expressiveness of GNNs from various perspectives, specifically through logical frameworks. This direction of research is by now well-established, making this work highly relevant.\n\nThe quality of the paper is exceptionally high, particularly in the formal sections dealing with logics, automata, and their theoretical intricacies. Every statement, including lemmas, propositions, and theorems, is precisely articulated, leaving no room for doubt or misinterpretation.\n\nThe presented characterizations are novel and intriguing within the context of related work on logical characterizations, making this a valuable and noteworthy contribution to the field.", "weaknesses": "I have a single, but rather general, weakness to point out:\n\n- 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Concerning the weakness mentioned, we will make the preliminaries somewhat lighter---possibly moving some non-essential parts to the appendix---and instead add more examples. For example, we will include a GMSC program for reachability in order to complement the corresponding GNN example. We will also add more illustrative remarks. However, there is probably a limit to what we can achieve, as we still would not like to compromise rigor in relation to the definitions. But some illustrations and examples can surely be added, and excess details removed.\n\nConcerning the question about floats, we indeed use saturating floating-point systems. We will point this out. The wrap-around case is different: using that approach, Proposition 2.3 would not hold and thus a GNN with floating-point numbers would not be bounded.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "IEb7zmq9mv", "reviewer": "Reviewer_TUPQ", "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).", "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? \n\nBtw, in his survey on GNNs, Grohe mentions the following question: \n\nQuestion 2. Let Q be a unary query expressible in a suitable modal (2-variable) fixed-point logic with counting. Is there a\nrecurrent GNN (with global readout) expressing Q? \n\nDo you have an answer to this question?", "limitations": "The authors have correctly addressed the limitations of their work.", "rating": 8, "confidence": 5, "soundness": 4, "presentation": 3, "contribution": 4, "strengths": "This is one of the most important papers to have appeared in the area of the expressiveness of GNNs over the last years. While several of these results can be considered kind of folklore in hindsight, I really appreciate the fact that the authors have spelled out all these connections in full detail and clarified several missing points. In particular, the study of finite precision GNNs is very interesting and the connection to GMSC of great importance. \n\nI have no doubts about the pertinence and technical quality of the article, and I think it should be accepted to NeurIPS.", "weaknesses": "I see no weakness on the paper. This is a comprehensive and solid piece of work that should clearly be accepted at the conference.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Concerning question 1, GMSC translates into partial fixed-point logic with choice (see, e.g., David Richerby, Logical Characterizations of PSpace (CSL 2004)): it is easy to see that GMSC has PSpace data complexity upper bound (one simply keeps in memory a subset of the graph domain for each schema variable), and partial fixed-point logic with choice captures PSpace on all (including unordered) models. It is also interesting to note that GMSC of course does not translate to any monadic fixed-point logic contained in MSO (simply because GMSC and MSO are orthogonal in expressive power).\n        \nConcerning question 2, we probably do not have a definite answer, but several relevant observations:\n    \n* The mu-fragment of graded modal mu-calculus translates into GMSC (cf. the response to all reviewers). Thus our results imply that every property expressible by the mu-fragment of graded mu-calculus is expressible by a recurrent floating-point GNN (without global readout).\n    \n* On the other hand, non-reachability is expressible in the mu-calculus, but it is not even in omega-GML, which is easy to show as follows. If non-reachability of p was expressible by omega-GML, then a node w in a small cycle, from where we cannot reach any node satisfying p, would satisfy one of the disjuncts φ of some modal depth n. Consequently, a node w' in a larger cycle with an isomorphic local environment up to modal depth n would satisfy φ also, even if p was reachable from w' at a distance greater than n. This is a contradiction.\n\n* The situation with the expressive power of GMSC changes with global readouts added. In GMSC with global readouts, non-reachability becomes expressible, because we can \"detect\" fixed points. Let Chi be a program such that the head predicate X will reach a fixed point containing precisely those nodes from where a node satisfying p is reachable; this program is definable already in the mu-fragment. Now, additionally, we can use auxiliary head predicates to keep track of interpretations of X at any two successive stages of computation. To detect when the fixed point of X is reached, we essentially simply use a global readout and the auxiliary head predicates to state that X has remained unchanged globally for two successive rounds. Once we know that the fixed-point has been reached, we accept all nodes in the complement of the fixed point of X.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Jdw9c35n4p", "reviewer": "Reviewer_2zSg", "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.\n\nThe 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.", "questions": "- Please comment on potential applications of this work\n- 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.\n- Please comment on the possibility of learning the acceptance vectors and the possibility of non-termination.", "limitations": "The authors have indicated some limitations of their work in the paper.", "rating": 6, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "- The paper advances the state of the art in the theoretical study of the expressive power of graph representation learning formalisms. The authors rightly point out that most theoretical work has been focused on standard GNNs with a fixed number of layers and that only recently in [23] this has been extended to GNNs with some form of fixpoint computation. The separate consideration of floating point numbers in a theory paper is also novel and interesting, as most theoretical studies assume real-valued feature vectors throughout the computation of the GNNs.\n\n- The paper is rigorously written to a high standard of quality and precision. \n\n- The obtained results are non-trivial and can motivate further theoretical study on the connection between graph representation learning models and logic.", "weaknesses": "- 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.\n\n- 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.\n\n- 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.\n\n- 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.\n\n- 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?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We first address the weaknesses.\n\nWe will improve the accessibility of the paper by lightening the preliminaries by moving non-essential parts to the appendix and adding examples (including a GMSC-program for reachability, to complement the corresponding GNN example) and illustrating remarks.\n\nAbout the remark on empirical evidence, we view our GNN model as a basic yet expressive version of recurrent GNNs. Please note that the upper bound of expressivity of our model with reals is ω-GML (Theorem 3.4), and thus one can conceive this upper bound as a sequence of GML-formulas of increasing modal depth. Barceló et al. [5] showed that GML-formulas correspond to constant-time GNNs, so our model relates to sequences of constant-time GNNs with the constant gradually increased. Also, our GNN[F]s can express all properties in the mu-fragment of the graded mu-calculus (cf. the response to all reviewers). We expect that typical properties relevant in practice fall into that class. However, we indeed did not perform practical experiments, concentrating instead on theory. We will add a remark on this to the limitations section.\n\nThe weaknesses regarding relevant work, learning acceptance vectors and non-termination are addressed later below.\n\nConcerning the size of a GMSC theory corresponding to a recurrent GNN and its computability: the translation GNN[F]s -> GMSC is effective with only polynomial blowup. It is indeed good to point this out.\n\nWe then address the questions.\n\nRegarding potential applications, studying the expressivity of GNN models, and characterizing GNNs via logic, is an active research theme, and our main aim is to contribute to that. While results of this kind have no immediate applications to practical learning, they are useful for understanding (also the practical) limitations of GNNs.\n\nConcerning whether our recurrent GNN model, with its specific termination condition, has practical applications: note that there is no standard termination condition for recurrent GNNs, and in publications on practical applications of recurrent GNNs, the termination condition is often not made explicit. We believe our condition is natural. Please note also that our GNNs contain the mu-fragment of graded mu-calculus; we expect that typical properties relevant in practice fall into that class. Also, as noted in the conclusion and appendix, our characterization in Theorem 3.2 also applies to the fixpoint acceptance condition of [23] if GMSC is modified accordingly. We will make this more explicit.\n\nWe will improve the discussion on [23] and [6]. Some central points:\n\n[23] differs from our setup in three crucial ways: (i) [23] studies GNNs with reals (not floats), and (ii) with unrestricted (possibly even non-computable) aggregation and combination functions, and (iii) with different termination conditions.\n\nThe setup of [23] can express all (even undecidable) bisimulation-invariant properties and yields potentially extremely powerful GNNs. Our main results concern the case of floats and R-simple GNNs not studied in [23]. The ensuing logical characterizations are quite different:\n\n- the background logic of [23] is LocMMFP (a version of monadic least fixpoint logic) while we use the more expressive MSO.\n\n- our characterization is via GMSC while theirs is via the (two-way) graded mu-calculus; as pointed out in our paper, these logics are orthogonal in expressivity. This is due to the differences (i) to (iii).\n\n[6] studies constant iteration-depth GNNs, not recurrent ones. In the case of eventually constant activation functions, equivalence to a certain Presburger modal logic is shown; this does not extend to activation functions that are not eventually constant. Our results enable any activation function, except for R-simple GNNs which use truncated ReLU. The logic ω-GML contains Presburger modal logic as a proper fragment.\n\nWe then comment on the possibility of learning acceptance vectors. With \"termination can be learned in the training phase\" in the intro, we only meant the following: specify a fixed set F of accepting feature vectors before training and try to train the model so that termination is achieved on all training examples. If this doesn't work, declare failure or modify F by making it smaller or larger, and try again.\n\nRegarding the possibility of non-termination, for many acceptance conditions, such as ours or conditions based on fixed point constructs, training and applying a recurrent GNN brings questions of termination. For GNNs over reals with our accepting condition, any node that accepts is classified \"accepting\" in a finite number of rounds. Non-accepting nodes might not be classified \"non-accepting\" in any finite number of rounds (in the general setting with no additional assumptions). The same issue is true of, e.g., the node-local fixed-points of the GNNs in [23], where the issue concerns both accepting and non-accepting nodes. Now, with float GNNs---at least in a certain theoretical sense---everything conceivably \"terminates\" due to GNNs always reaching a global attractor (meaning global configurations ultimately start repeating). But this is indeed a theoretical remark. Also, the mu-fragment contained in GMSC (please see above) is based on local fixpoints with better convergence properties, so many scenarios are more favourable with suitable assumptions.\n\nFrom a less theory-oriented perspective, if gradient descent is used for training, one needs to repeatedly evaluate the model with its current parameterization on training examples, possibly facing non-termination. In practice, this could be dealt with by declaring non-termination after a certain number of steps, e.g., via a function of the size of the training example. We will note in the limitations section that the we do not address training of GNNs, which is a fair point. When applying a trained GNN, one may also face non-termination. Again, in practice this could be dealt with by stopping after a certain number of steps.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:
We thank the reviewers for the reviews, all of which help clarify the paper and summarize it.

We point out the following fact concerning our responses to three of the reviews: It follows from the results in [21] (by essentially the same argument as the one justifying Proposition 7 of that article) that the mu-fragment of the graded modal mu-calculus translates into GMSC. The mu-fragment is the one with only least fixed-point operators and no greatest fixed-point ones (when presented in negation normal form).

Meta-review: 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.
Decision: Accept (poster)