# Halting Recurrent GNNs and the Graded μ-Calculus

arXiv: https://arxiv.org/abs/2505.11050 · HTML: https://mlsanity.com/paper/2505.11050/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 23 references that are in the map.
- First posted on arXiv 16 May 2025.

## Builds on (most cited first, 8 of 8)

- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [A Survey on The Expressive Power of Graph Neural Networks](https://mlsanity.com/paper/2003.04078/) (2020)
- [The Logic of Graph Neural Networks](https://mlsanity.com/paper/2104.14624/) (2021)
- [Graded modal logic and counting bisimulation](https://mlsanity.com/paper/1910.00039/) (2019)
- [Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats](https://mlsanity.com/paper/2405.14606/) (2024)
- [On the expressive power of message-passing neural networks as global feature map transformers](https://mlsanity.com/paper/2203.09555/) (2022)
- [Tree algebras and bisimulation-invariant MSO on finite graphs](https://mlsanity.com/paper/2407.12677/) (2024)

## Built on by (most cited first, 2 of 2)

- [Recurrent Graph Neural Networks and Arithmetic Circuits](https://mlsanity.com/paper/2603.05140/) (2026)
- [On Halting vs Converging in Recurrent Graph Neural Networks](https://mlsanity.com/paper/2604.25551/) (2026)

## Abstract (arXiv)

Graph Neural Networks (GNNs) are a class of machine-learning models that operate on graph-structured data. Their expressive power is intimately related to logics that are invariant under graded bisimilarity. Current proposals for recurrent GNNs either assume that the graph size is given to the model, or suffer from a lack of termination guarantees. In this paper, we propose a halting mechanism for recurrent GNNs. We prove that our halting model can express all node classifiers definable in graded modal mu-calculus, even for the standard GNN variant that is oblivious to the graph size. To prove our main result, we develop a new approximate semantics for graded mu-calculus, which we believe to be of independent interest. We leverage this new semantics into a new model-checking algorithm, called the counting algorithm, which is oblivious to the graph size. In a final step we show that the counting algorithm can be implemented on a halting recurrent GNN.