# Decidability of Graph Neural Networks via Logical Characterizations

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Apr 2024.

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

- [Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats](https://mlsanity.com/paper/2405.14606/) (2024)
- [Exact Verification of Graph Neural Networks with Incremental Constraint Solving](https://mlsanity.com/paper/2508.09320/) (2025)
- [Logical Expressiveness of Graph Neural Networks with Hierarchical Node Individualization](https://mlsanity.com/paper/2506.13911/) (2025)
- [A Logical View of GNN-Style Computation and the Role of Activation Functions](https://mlsanity.com/paper/2512.19332/) (2025)
- [Verifying Quantized Graph Neural Networks is PSPACE-complete](https://mlsanity.com/paper/2502.16244/) (2025)
- [The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics](https://mlsanity.com/paper/2505.11930/) (2025)
- [Expressive Power of Graph Transformers via Logic](https://mlsanity.com/paper/2508.01067/) (2025)
- [Sound Logical Explanations for Mean Aggregation Graph Neural Networks](https://mlsanity.com/paper/2511.11593/) (2025)
- [From Neural Networks to Logical Theories: The Correspondence between Fibring Modal Logics and Fibring Neural Networks](https://mlsanity.com/paper/2509.23912/) (2025)
- [How Expressive Are Graph Neural Networks in the Presence of Node Identifiers?](https://mlsanity.com/paper/2601.21882/) (2026)
- [Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing](https://mlsanity.com/paper/2510.18591/) (2025)
- [Structural Preservation and the Logical Expressiveness of Graph Neural Networks](https://mlsanity.com/paper/2606.17882/) (2026)
- [The Boolean Power of ReLU](https://mlsanity.com/paper/2608.12617/) (2026)
- [Beyond Trained Models: Compiling GNNs for a Sound Explainer Benchmark](https://mlsanity.com/paper/2610.03526/) (2026)

## Abstract (arXiv)

We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving "Presburger quantifiers". We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.