Recurrent Graph Neural Networks with Set-Based Aggregation

Introduction

• Earlier recurrent-GNN characterizations use multiset aggregation and counting logics, with halting or acceptance conditions that may not be verifiable from network weights.For the graded µ-calculus with genuine alternation, the converse direction is known only conditionally.Source: Introduction · p. 1
• Set-based aggregation yields a complete, effective correspondence under sufficient conditions checkable from the network weights.The framework uses regularity, a finite vocabulary, and admissibility; contraction and monotonicity provide checkable sufficient conditions.Source: Introduction · p. 1
• Ratchet nets compute exactly the vertex queries in BΣ⋄ 1, with effective translations in both directions and no counting apparatus or external halting classifier.BΣ⋄ 1 is the Boolean closure of reachability and safety properties.Source: Introduction · p. 1
• Stabilization over finite vocabulary supports fixed points of one polarity and their Boolean combinations, but not composition of fixed points of opposite polarities.The paper relates this boundary to the absence of a certificate that an inner computation has stabilized.Source: Introduction · pp. 1–2
• The authors implement net-to-logic and logic-to-net compilers and report extensive experimental validation; they also connect the result to max/min aggregation’s use in neural algorithmic reasoning.They present the logical meaning of set-based aggregation as relevant to this architectural choice.Source: Introduction · p. 2

GNNs with Set-Based Aggregation

• For each atomic type and layer, the architecture specifies initial embeddings, weight tensors, a set-to-embedding aggregator, and component-wise activations.The described activations include ReLU and clipped ReLU; the update aggregates the finite set of neighbor embeddings, with the empty set mapped to zero.Source: GNNs with Set-Based Aggregation · p. 2
• In the recurrent case, the network reuses the same one-step update and is called converging when every vertex’s embedding has a limit.Whether convergence occurs depends on the weights, activation, and graph structure; results also extend to recurrent blocks with multiple layers.Source: GNNs with Set-Based Aggregation · p. 2
• Graphs may be directed, with each vertex’s neighborhood comprising its outgoing successors; undirected graphs are the symmetric special case.The positive results therefore also apply to undirected graphs.Source: GNNs with Set-Based Aggregation · p. 2

Finite Types and Their Embeddings

• At each layer, a vertex type records its prior type and the set of types among its neighbors, yielding the equivalence classes for set-based bisimulation.Vertices of the same type receive the same embeddings regardless of the architecture.Source: Finite Types and Their Embeddings · p. 2

Compiling Depth-Bounded Nets

• The compiler uses formulas deciding vertex types to characterize whether each register of a depth-bounded net’s final embedding is greater than zero.The characterization is established by induction on layer depth.Source: Compiling Depth-Bounded Nets · p. 3
• The number of layer-ℓ types grows as a tower of exponentials, supporting previously reported empirical compilation blow-ups for similar compilations.The passage relates the type count to the Hintikka-style normal forms of modal formulas of depth at most ℓ.Source: Compiling Depth-Bounded Nets · p. 3

Recurrent Nets

• Recurrent characterization is harder because convergence time, encountered types, and reachable fixed-point embeddings are not bounded in advance.Regularity makes a vertex’s fixed-point embedding depend on its atomic type and its neighbors’ fixed-point embeddings, allowing a quotient table over the vocabulary.Source: Recurrent Nets · p. 3
• The net’s embedding is the limit of its finite-type embeddings, and equal set-based bisimulation types yield equal embeddings.The quotient table maps an atomic type and a finite set of vocabulary embeddings to an embedding.Source: Recurrent Nets · p. 3
• An admissible game over finite vocabulary matches the net’s final embeddings and converges within |V|n steps, or n(|V|−1) steps when ordered.The game can converge faster than the original network, whose contractive run converges only in the limit.Source: Recurrent Nets · p. 4

Contractive Nets

• Contraction and a 1-Lipschitz aggregator guarantee convergence; contraction in the vertex embedding additionally gives regularity and a well-defined vocabulary.Full contraction with a 1-Lipschitz aggregator also guarantees an admissible game.Source: Contractive Nets · p. 4

Monotone Nets

• Monotonicity, given nonnegative initial embeddings that are pre-fixed points, yields regularity and an admissible, ordered game when both network and aggregator are monotone.With max aggregation, the induced game is monotone.Source: Monotone Nets · p. 4
• An order over the finite vocabulary turns the system into a terminating process by ruling out cycles and oscillation.The resulting finite-vocabulary system is a cellular automaton on the graph, with the quotient table as its local rule.Source: Monotone Nets · p. 4
• Compiling the game rather than the run replaces possibly infinite transients with a finite quotient that fixed-point formulas can track.Admissibility ensures the game selects the solution produced by iteration, while trajectory-dependent alternatives are described as infinitary or non-effective.Source: Monotone Nets · p. 4

Translating Recurrent Nets into IFP

• The IFP compiler constructs simultaneous one-step unary relations that characterize a regular net with finite vocabulary and an admissible, ordered game.The IFP definitions use a vector of relations; the net-to-logic output can be linear in the quotient table as a shared system, although flattening to closed formulas can be exponential.Source: Translating Recurrent Nets into IFP · p. 5, Contractive net · p. 5

Contractive net.

• One illustrated net has a finite ordered vocabulary despite infinite oscillating transient sequences.The passage says this net meets the required properties but neither of the two stated sufficient conditions, illustrating that the class extends beyond them.Source: Contractive net · p. 5
• Ratchet nets implement exactly the BΣ⋄ 1 queries, the Boolean closure of reachability- and safety-style fixed-point properties.The net-to-logic compiler produces formulas for vocabulary elements, and the converse translation compiles formulas into Ratchet nets.Source: Contractive net · pp. 5–6
• Finite-vocabulary stabilization cannot compute νY.♢Y or µX.□X, so the target excludes first-level properties requiring opposite-polarity fixed points.The barrier assumes regularity and admissibility, but not an ordered or monotone game; on directed graphs it also excludes EF EG p.Source: Contractive net · pp. 5–6

Examples

• The examples include a net computing a fixpoint-free query of modal depth 2 despite infinitely many transient embeddings.A separate example translates a reach-red-while-avoiding-green formula into a width-2 net that tracks reachability and safety.Source: Examples · p. 6

Experimental Validation

• Across 9,960 pointed-graph checks for 13 branching-time properties, the differential test found no discrepancies.Each property was tested on at least 30 random pointed graphs by comparing compiled denotations with an independent Lµ evaluator.Source: Experimental Validation · p. 6

Depth-bounded GNNs and logic.

• Depth-bounded GNNs are characterized by first-order logic with counting, while PTK characterize recurrent regimes using monadic monotone fixpoint logics but provide non-effective lim-inf acceptance.The paper contrasts its weight-checkable admissibility conditions and constructive compilers with PTK’s lack of finite stabilization certificates, decidable membership, and size bounds.Source: Depth-bounded GNNs and logic · p. 6

Uniform expressivity and other aggregations.

• Other aggregation choices yield different characterizations: recurrent sum-GNNs use counting, mean-aggregation work gives other logics, and set-based aggregation yields BΣ⋄ 1.The cited sum-GNN result addresses computational completeness with graph size as input, unlike this paper’s effective logical characterization under convergence.Source: Uniform expressivity and other… · p. 6

Halting and converging recurrent GNNs.

• Prior recurrent-GNN results use halting classifiers or graph-growing counters to provide stabilization certificates, whereas finite-vocabulary regular admissible nets have no such certificate.The paper presents its result as a counting-free counterpart and a constructive converse for BΣ⋄ 1; BV’s equivalence is over undirected graphs, and its simulation breaks on directed graphs.Source: Halting and converging recurrent GNNs · p. 7

Max-aggregation GNNs and Datalog.

• The max-aggregation GNN-to-Datalog translation is depth-bounded and based on finiteness intrinsic to max aggregation, unlike this paper’s finiteness-of-types basis.The cited work reports that full equivalent programs are typically too large to compute and instead extracts fact-specific explanations.Source: Max-aggregation GNNs and Datalog · p. 7

Conclusions

• Ratchet nets have an effective two-directional correspondence with the alternation-free modal µ-calculus, with compiler bounds measured against the quotient table or source formula.The shared net-to-logic system is linear in the quotient table, while flattening to one closed Lµ term can be exponential.Source: Conclusions · p. 7
• The correspondence applies only to nets satisfying Ratchet conditions, and all results concern finite graphs; applying the compiler to trained recurrent GNNs remains future work.Characterizing exactly which weight configurations qualify is open, and the examples are illustrative rather than empirical.Source: Conclusions · p. 7
• Regular admissible nets cannot compute νY.♢Y, µX.□X, or EF EG p, so extending the correspondence requires stabilization certificates or a richer convergence regime.The cited certificate mechanisms are halting classifiers or counters that grow with the graph.Source: Conclusions · p. 7

Appendix for section: Finite Types and Their Embeddings

• For layer ℓ, vertex u’s embedding equals E_t(θ) for t = τ^ℓ(x,u).The proof is by direct induction on ℓ.Source: Appendix for section: Finite Types and… · p. 9
• The embedding correspondence is stated for a parameter θ, a pointed graph, and a layer index within the architecture.The theorem identifies the type t from the pointed graph and layer before assigning its parameter-dependent embedding.Source: Appendix for section: Finite Types and… · p. 9
• The appendix also states a compiler theorem parameterized by θ for the architecture (W, L, ATP).The supplied theorem statement begins a relation involving the layer embedding, but does not include the complete conclusion.Source: Appendix for section: Finite Types and… · p. 9

• Bisimilar pointed graphs have equal infinite types and therefore equal limit embeddings.Source: Appendix for section: Recurrent Nets · p. 9
• Contractivity plus a 1-Lipschitz aggregator gives convergence; contractivity in z then gives regularity and a well-defined vocabulary, while full contractivity also yields admissibility.Source: Appendix for section: Recurrent Nets · p. 9
• With max aggregation and a 1-Lipschitz activation, ||Aα||mars < 1 ensures z-contraction, while ||Aα||mars + ||Bα||mars < 1 ensures full contraction.Source: Appendix for section: Recurrent Nets · pp. 10–11
• For a converging net with non-negative pre-fixed-point initial embeddings, monotonicity gives a well-defined vocabulary; monotone net and aggregator also yield regularity, admissibility, and an ordered game.Source: Appendix for section: Recurrent Nets · p. 11
• Under the monotone-net assumptions, the canonical sequence converges to the least fixed point above eα for each finite set S of non-negative embeddings.Source: Appendix for section: Recurrent Nets · p. 11
• With a 1-Lipschitz aggregator, non-negative Aα and Bα ensure monotonicity; integer non-negative weights, clipped activation, and integer initial embeddings ensure a finite vocabulary.Source: Appendix for section: Recurrent Nets · p. 12

IFP Compiler

• For regular nets over finite vocabularies with admissible ordered games, a vector IFP characterization matches each embedding’s converged value on every pointed graph.The construction uses unary relations for vocabulary values to encode the game’s evolution.Source: Appendix for section: Translating… · pp. 13–14

Second example

• Every reachable limit lies in {1/3, 2/3, 7/9, 1}; closing V0 = {1/3, 2/3} under the rows yields exactly V.Source: Appendix for section: Translating… · p. 14

Net-to-logic

• Every Ratchet net with finite vocabulary has BΣ⋄1 formulas characterizing each register value; the construction uses monotone games and a least fixed point of witness-based, diamond-only formulas.The formulas assert witnessed neighbor values, relying on the target sets being up-sets and the game being monotone.Source: Appendix for section: Translating… · p. 15

Network construction

• Synchronous rules use pointwise max aggregation, with max ∅ = 0 making ♢ false at successor-less vertices, and keep all reachable registers Boolean.The rules are compositions of clipping with affine maps, and map Boolean inputs to Boolean outputs.Source: Appendix for section: Translating… · p. 17

Convergence proof

• Each closed block’s synchronous run is non-decreasing and reaches its semantic least fixed point within |Rβ| × n steps; derived registers follow with one-step delay.Boolean coordinates can flip at most once, and the block’s least fixed point equals its semantic state.Source: Appendix for section: Translating… · p. 17

Translation correctness

• The net converges on every n-vertex graph within W × n steps and is regular, so it is a Ratchet net that computes γ.The regularity proof uses equality between each vertex’s frozen local solution and its value in the global limit.Source: Appendix for section: Translating… · p. 18

Expressive barrier

• No converging regular net with finite vocabulary and an admissible game computes νY.♢Y, µX.□X, EG p, or EF EG p; BΣ⋄1 is strictly contained in the alternation-free fragment.The path and self-loop argument forces the same vocabulary element to receive conflicting readout values.Source: Appendix for section: Translating… · pp. 18–19

Example

• For γ = µX.(r ∨ ♢X) ∧ ¬µY.(g ∨ ♢Y), logic-to-net translation yields a width-2 network, and net-to-logic recovers γ.The two registers propagate red-reachability and green-reachability, respectively.Source: Appendix for section: Translating… · p. 19

Appendix: Experimental Validation

• The curated suite contained 13 branching-time properties drawn from model-checking literature.The section also reports the test graphs, methodology, results, and several findings.Source: Appendix: Experimental Validation · pp. 19–20
• 9,960 checks across 13 properties found no discrepancy between formula truth values and values read from the recompiled equation systems.The comparison used many random graphs.Source: Appendix: Experimental Validation · p. 20
• The differential test compiled each formula to a net, recovered an abstract game table, and compiled the table back to logic.The recompiled, un-flattened equation system supplied the recovered value at each vertex.Source: Appendix: Experimental Validation · p. 20

Methodology

• The pipeline compiles each formula into a net, extracts its finite vocabulary and quotient table, then compiles that table into a guarded equation system.Extraction simulates frozen single-vertex systems to fixed points for reachable aggregate values; the order uses core registers and excludes generic-negation registers.Source: Methodology · p. 20
• The recompiled query is evaluated by simultaneous Kleene iteration rather than Bekič-flattening the equation system into closed formulas.The passage notes that flattened formulas can be exponentially larger than their originating system.Source: Methodology · p. 20
• A mechanical checker verified suite membership in BΣ⋄ 1 and rejected µX.□X and νY.♢Y, the queries excluded by Proposition 17.The recovered readout is compared with an independent direct denotational evaluator.Source: Methodology · p. 20

Property Suite

• The 13-property suite exercises pure Σ⋄ 1 and Π□ 1 blocks, flat Boolean combinations, and same-polarity nesting at depths two and three.Depth-three cases include sequencing_chain and invariant_chain.Source: Property Suite · p. 20
• Vertices receive independent p, q, and r labels, so their atomic types are joint subsets rather than mutually exclusive single labels.The suite uses joint valuations as atomic types.Source: Property Suite · p. 20
• The suite includes reachability, safety, existential-until, reach-avoid, reachability-and-invariant, and sequencing properties.Other listed cases include mutual exclusion, implication-invariant, reach-both, and combined_three_way.Source: Property Suite · p. 20
• Controls confirmed AF p and EG p are outside BΣ⋄ 1; opposite-polarity nested examples EF(p ∧AG q) and AG(p →EF q) were also checked as excluded.The two controls match Proposition 17; the nested examples test closed blocks of opposite polarity inside a µ/ν body.Source: Property Suite · p. 20

Graph Generation

• Random directed graphs excluded self-loops; edges and each vertex’s propositions were sampled independently.The main sweep used n ∈ {6, 10, 14, 20, 25}, three edge probabilities per property, and four graphs per size-probability pair, yielding 60 graphs and 900 pointed checks per property.Source: Graph Generation · p. 21

Reproducibility

• Frozen manifests retain graph-generation parameters and random seeds, making every checked graph independently regenerable; code and results were slated for public release in the final version.Source: Reproducibility · p. 21

Analysis

• Round-trip agreement is empirical, not machine-checked proof, and supports implementation only on the tested sub-fragment: flat Boolean blocks and same-polarity nesting through depth 3.Source: Analysis · p. 21

Results

• Across all 13 properties, 9,960 checks showed no discrepancy between formula truth and recompiled-system semantics.The table reports round-trip agreement over random pointed graphs.Source: Results · p. 21, Table 1 · p. 22