This paper studies graph neural networks (GNNs), a machine learning model that processes graph-structured data. Specifically, we propose a novel termination mechanism to address the guaranteed termination problem of recurrent GNNs. Existing recurrent GNNs suffer from the problem of providing the graph size to the model or lacking a termination guarantee. In this paper, we propose and prove a termination model that can represent all node classifiers defined by graded modal mu-calculus, even in a standard GNN variant that ignores graph size. To achieve this, we develop a novel approximation semantics for graded mu-calculus and, based on this, propose a new model verification algorithm (counting algorithm) that does not consider graph size. Finally, we demonstrate that the counting algorithm can be implemented in a terminating recurrent GNN.
