Recurrent GraphNeural NetworkswithSet-BasedAggregation
Paper proves two-directional equivalence between recurrent GNNs with set-based aggregation and Boolean closure of reachability/safety properties in modal mu-calculus, checkable from weights.
The authors study recurrent graph neural networks with set-based aggregation and identify sufficient conditions, checkable directly from network weights, for compiling networks into logical formulas and formulas into networks. They establish an effective two-directional equivalence with the Boolean closure of reachability and safety properties, the fragment BΣ°1 of the modal μ-calculus, shown to be the exact expressive level of stabilization over finite vocabulary. The correspondence needs no counting logic, external halting signal, or non-effective acceptance condition, yielding a verifiable path from weights to symbolic explanations.
- Weight-checkable conditions enable compiling between recurrent GNNs and logic formulas
- Exact equivalence with Boolean closure of reachability and safety in modal μ-calculus
- No counting logic, halting signal, or non-effective acceptance condition required
- Provides verifiable symbolic explanations for qualifying networks
Full article155 words · extracted from arxiv.org · click to collapse
Recurrent GNNs iterate message passing to convergence, and their logical characterizations to date rely on multi-set aggregation, graded (counting) logics, and halting or acceptance conditions that cannot be verified from the network's parameters. We study recurrent GNNs with set-based aggregation and identify sufficient conditions checkable from the weights for networks to compile into formulas and formulas into networks. The main result is an effective, two-directional equivalence between a class of networks and the Boolean closure of reachability and safety properties, the fragment B$Σ^{\circ}_1$ of the modal $μ$-calculus. The fragment is not an artifact: it is the exact expressive level of stabilization over finite vocabulary, which supports fixed points of a single polarity and Boolean combinations thereof, but not the composition of fixed points of opposite polarities. The correspondence needs no counting logic, no external halting signal, and no non-effective acceptance condition, yielding a verifiable path from weights to symbolic explanations for networks meeting the conditions.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.15932