A Modal Logic for Explaining some Graph Neural Networks

TL;DR

This paper introduces a modal logic framework with counting modalities that can be transformed into graph neural networks and vice versa, establishing decidability of satisfiability and exploring computational complexity.

Contribution

It presents a novel modal logic for explaining GNNs, with transformations between formulas and networks, and analyzes the decidability and complexity of the logic.

Findings

Formulas can be transformed into GNNs and vice versa.

Satisfiability in the logic is decidable.

Variants of the logic are in PSPACE.

Abstract

In this paper, we propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that each GNN can be transformed into a formula. We show that the satisfiability problem is decidable. We also discuss some variants that are in PSPACE.