The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics

TL;DR

This work establishes a formal link between temporal graph neural networks and two-dimensional product logics to characterize spatio-temporal expressiveness. It shows that recursive TGNNs can express all properties definable in the product logic $\mathsf{PTL}_{\mathsf{P}{},\mathsf{Y}_{}}{\times}\mathsf{K}$, with analogous results for variants using $K^{\#}$ and $\mathcal{L}\text{-}\mathsf{MP}^2$ and corresponding MPNNs. In contrast, time-and-graph TGNNs and global TGNNs cannot express all such properties, but each can capture specific fragments ($\mathcal{L}_1$ and $\mathcal{L}_2$) through restricted interaction patterns between temporal and spatial operators. This work opens routes for principled analysis of TGNNs, enabling the extraction of temporal-spatial rules and guiding the design of architectures with desired logical capabilities.

Abstract

In recent years, the expressive power of various neural architectures -- including graph neural networks (GNNs), transformers, and recurrent neural networks -- has been characterised using tools from logic and formal language theory. As the capabilities of basic architectures are becoming well understood, increasing attention is turning to models that combine multiple architectural paradigms. Among them particularly important, and challenging to analyse, are temporal extensions of GNNs, which integrate both spatial (graph-structure) and temporal (evolution over time) dimensions. In this paper, we initiate the study of logical characterisation of temporal GNNs by connecting them to two-dimensional product logics. We show that the expressive power of temporal GNNs depends on how graph and temporal components are combined. In particular, temporal GNNs that apply static GNNs recursively over time can capture all properties definable in the product logic of (past) propositional temporal logic PTL and the modal logic K. In contrast, architectures such as graph-and-time TGNNs and global TGNNs can only express restricted fragments of this logic, where the interaction between temporal and spatial operators is syntactically constrained. These provide us with the first results on the logical expressiveness of temporal GNNs.

Figures (4)

• Figure 1: A temporal graph of length $4$; colour $c_1$ is denoted by a red filling (node $u$ in $G_3$ and node $v$ in $G_4$) and colour $c_2$ is denoted by a blue filling (node $v$ in $G_1$ and node $u$ in $G_4$)
• Figure 2: Counterexample, used in Theorem \ref{['th:TandGweak']}; colour $c_1$ is denoted by a red filling (node $u_1$ in $G_2$ and node $u_1'$ in $G_2'$) and colour $c_2$ is denoted by a blue filling (node $u_2$ in $G_1$ and node $w_2'$ in $G_1'$)
• Figure 3: An overview of our expressive power results
• Figure 4: Pointed temporal graphs $(TG,v)$ and $(TG',v')$, both including two snapshots, used as an counterexample in the proof of Theorem \ref{['thm:globTGNNweak']}. Here, colour $c_1$ is denoted by a red filling (applies for node $v$ in $G_1$, $G_2$ and node $v'$ in $G_2'$).

Theorems & Definitions (40)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Theorem 6
• proof : Proof sketch.
• Theorem 7
• proof : Proof sketch
• Theorem 8