Halting Recurrent GNNs and the Graded $\mu$-Calculus

TL;DR

This paper introduces a halting mechanism for recurrent GNNs that can express all node classifiers in graded mu-calculus, ensuring termination and expanding their expressive power on graph-structured data.

Contribution

It proposes a novel halting mechanism for recurrent GNNs and develops a new approximate semantics for graded mu-calculus, enabling expressiveness and termination guarantees.

Findings

The halting recurrent GNN can express all classifiers in graded mu-calculus.

A new counting algorithm for model-checking is introduced.

The counting algorithm is implementable on halting recurrent GNNs.

Abstract

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.