본 논문은 그래프 구조 데이터를 처리하는 기계 학습 모델인 그래프 신경망(GNNs)에 대한 연구입니다. 특히, 순환 GNNs의 종료 보장 문제를 해결하기 위해 새로운 종료 메커니즘을 제안합니다. 이 종료 메커니즘을 통해 그래프 크기에 무관하게 graded modal mu-calculus로 정의 가능한 모든 노드 분류기를 표현할 수 있음을 증명합니다. 이를 위해 graded mu-calculus에 대한 새로운 근사 의미론을 개발하고, 그래프 크기에 무관한 새로운 모델 검증 알고리즘(counting algorithm)을 제시합니다. 마지막으로, 이 counting algorithm을 종료 순환 GNN에 구현할 수 있음을 보입니다. 유한 그래프에서 graded modal mu-calculus의 표현력에 대한 최근 연구 결과를 바탕으로, 제한된 조건 하에 순환 GNNs가 graded modal mu-calculus로 정의 가능한 노드 분류기만을 표현할 수 있음을 시사합니다.