The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics
Authors: Marco Sälzer
Przemysław Andrzej Wałęga
Martin Lange
Venue: NeurIPS 2025 poster ()
Keywords: temporal graph neural networks
temporal logic
expressiveness
Primary area: theory
TL;DR: We analyse the expressive power of different classes of TGNNs via standard combinations of temporal and modal logics.

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.

The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics
Marco Sälzer RPTU Kaiserslautem-Landd Kaiserslautem, Germany
Przemyslaw Andrzej Walega
Queen Mary University of London, UK University of Lódž, Poland p. w.laga@mmul ac.uk
marco. saelzer@rptu.cc
Martin Lange
Theoretical Computer Science Formal Methods
University of Kassel, Germany
martin. martin.langedn
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 atten- tion is turning to models that combine multiple architectural paradigms. Among them particularly important, and challenging 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 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 capture all properties definable in the product logic (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 syntactically constrained. These provide with the first results on the logical expressiveness of temporal GNNs.
Introduction
Recent years have seen significant progress in understanding the expressive power of neural architec- tures using tools from logic, formal language theory, and graph theory. Some of the most prominent results concern Graph Neural Networks (GNNs), whose distinguishing power has been famously and whose logical expressiveness These insights have revealed both the limitations and strengths of GNNs, inspiring the development of more expressive variants such higher-order GNNs [3T]. They have also opened the way for extracting logical rules from GNNs, advancing explainability in graph-based learning [42 43]. Consequently, the logical expressiveness of GNNs has become rapidly evolving research area.
characterised with the Weisfeiler-Lematt isomorphism test [1 46
has been captured with modal and first-order logics 3
17
32
5
As the capabilities of standard GNN architectures become relatively well understood, research interest shifting to more complex architectures, which combine multiple dimensions of structure. One particularly prominent and challenging case is that of Temporal Graph Neural Networks (TGNNs) 26 [4]. which can seen as an extension of GNNs enabling to process temporal graphs,
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

that is. graphs whose topology evolves over time. As result, TGNN computations combine the spatial (graph structure) with temporal (changes in time) dimensions. Considerable advancements have been made in the design of various TGNN architectures (26 and their deployment across diverse applications such as traffic forecasting, financial applications, and epidemiological contexts 44 33 21] However understanding expressive capabilities of TGNNs remains limited, with the first steps only comparing some TGNN architectures
[I4 g or establishing relations with temporal versions of the Weisfeiler-Leman test [41 44). To the best of our knowledge no connection of TGNNs with logics has been established prior to this work.
Our contribution. In this work, we initiate the analysis of the logical expressiveness of TGNNs. Our goal is to characterise the temporal graph properties that TGNNs can express using logical languages. To achieve this, propose a novel aaproach-analyseee TGNNs using two-dimensional product logics. This is based on the key insight that the computations of TGNNs, which process both the structural properties of static graphs and their evolution over time, naturally correspond to combinations of modal and temporal properties.
the logical expressiveness of
Both modal and temporal logics have been extensively studied in the logic community for decades, and more recent work has connected them to the expressiveness of neural architectures 3 47 Likewise, nany-dimensional logics, especially products of modal and temporal logics, have a rich theoretical foundation and csllbestablishe tools for amalysing definability and complexity [24 6 28). We are the first to apply product logics framework for analysing the expressive power of TGNNs,
At a technical level, we show that certain TGNN architectures are (in-)capable of expressing certain combinations of
properties. Our results are as follows:
The class Trea [M] of TGNNs recursively applying standard static GNNs (from class M) over time, can express all properties definable in the product logic PTLp,y x K, which combines the seminal (past) propositional temporal logic PTLp,y y and the modal logic K (Theorem O)
Analogous results hold if we replace M and K with matching expressiveness GNNs and logics. In particular, we show that such results hold for two specific pairs of static GNNs and logics, recently
studied in literature 32 5 (Theorem 7
In contrast to recursive TGNNs, the class of time-and- ganddggrphhhoo TGNNs 14 does not allow us to express all properties expressible in PTLp, xK (Theorem 8). We show, however, that time-and- graph TGNNs can express all properties definable in a fragment of PTLp.y in which the allowed interplay between temporal and modal operators is syntactically restricted (Theorem 99).
The class of global TGNNs [44) also does not allow us to express all properties expressible in X (Theorem TOp. As in the previous case, we determine a fragment of PTLp.y xK, such that global TGNNs can express all properties definable in this fragment (Theorem This fragment, however, allows for different interactions between temporal and modal operators, than the fragment from Theorem 8
We show how our results allow to determine relative expressive power of TGNN classes considered in the paper (Corollary [2 and Theorem
Beyond their theoretical significance, these results open the door to novel avenues in explainable and trustworthy AL. Just as logical characterisations of static GNNs have enabled the extraction of symbolic rules from neural models (42 (3), our analysis lays the foundation for extracting temporal rules and dynamic specifications from TGNNs.
2 Related work
Temporal GNNs. There exists plethora of TGNN models (26). differing on representation and processing temporal graphs. There exist various classifications of TGNNs (26.. but one of the main distinction is between taapshot-basedd models, where temporal graph is given as a sequence of its [I] and event-based based models, where a temporal graph is given In this paper we focus on the snapshot-based TGNNs, but it is worth to observe that in many settings these two types of temporal graph representation can translated into each other. Initial work on the expressive power of TGNNs has been conducted exploiting their relation to variants of the Weisfeiler-Lemt isomorphism test
timestamped snapshots [18 38 30 48
as a sequence of events modifying the graph structure 45
35 27

---

41 44] and by directly comparing expressiveness of particular TGNN architectures [14 8 However, to the best of our knowledge, no work has yet studied the expressive power of TGNNs from the perspective of logics.
Logical expressiveness of static GNNs. The seminal logical characterisation of sanessage-passing GNNs established that the properties expressible both by GNNs and first-order logic coincide with those definable in graded modal logic [3] Subsequent work moved beyond the assumption of first- order expressibility, aiming to identify logics that capture the full expressive power of GNNs. This line of research led to the introduction of logics such as the modal logic K# (32) and logics extended with Presburger quantifiers [5]. More recent results have provided logical characterisations of further
GNN architectures using logics with quantised parameters [I 37 or standard modal logics [2]
There are also results on the logical expressiveness of GNNs extended with global readouts R 20
Product logics multi-diimnnsioal product logics 24 offer general framework for combining multiple modal logics, each capturing distinct aspect of reasoning such as space, time, or knowledge. In these systems, states are represented as tuples drawn from the component logics, and accessibility relations are defined componentwise, enabling interaction between different modal dimensions. There long-standing tradition of studying the complexity and axiomatisation of multi-dimensional logics-a line of research that often proves to be highly challenging [24, 29) Two-dimensional product logics, in particular, have been extensively investigated due to their applicability in spatio- temporal [6], cemporal-epistemic [19], temporal-standpoint [13 [3]. and temporal description logic 2 settings. Of particular relevance to our work is the two-dimensional product logic PTL x K, which combines propositional temporal logic (PTL) [4] with the modal logic K (23). This logic, along with its various extensions and variants, has been the subject of extensive study in the literature (24).
3
Notation
We will briefly describe basic notions, notation, and conventions used in the paper.
We use bold symbols, such as æ and y. to represent vectors, we assume that they are given as column vectors. In particular, we use for vectors containing only Os; their dimension will usually be clear from context. We let 2; be the ith element of æ. and x y the concatenation of x and y. that is, vector obtained by stacking æ onto y. We use I[ ...... B to denote multisets, that is, sets with possibly multiple occurrences of elements.
(static, undirected, node-labelled graph, G E, is a triple consisting of a finite set V of nodes, set E of undirected edges over V, and labelling e V -- R of nodes with vectors in RR If : V - {0, }}²; we call vector entries colours and say that the graph is coloured (with & colours). pointed graph a pair (G,u) consisting of graph and one of its nodes.
A temporal graph, TG = (G1, (GI,t1)..... (Gn, tn), is a finite sequence of pairs (G,, t.). where = =V=(V., E,, c.) is static graph such that Vi = timestamp, such that 1 < .... < tn We call n the length of TG. We usually refer to the set of nodes of TG V. We call temporal graph discrete, if t, i for each timestamp f, A timestamped node is a pair (v, f.) of a node and a timestamp; a pointed temporal graph is a pair (TG, (v, tt)) of a temporal graph and a timestamped node. Often, we will write (TG, v) instead of (TG, (u, t)))
Vn, and t, IR is number, also called
4 Massagg-passing GNNs and TGNNS
In this section, we briefly present the standard message-passing GNNs [6]. referred to as message passing neural networks (MPNNs) here, but also called gggregation-combine GNNs (AC-GNNs) 3. Afterwards, we present three ways of extending them to the temporal setting, which gives rise the three classes of temporal GNNs we will study in this paper.
Definition 1. A maassage-pasiingg GNN (MPNNs), M = 1*), is finite sequence of message- passing layers of the form l' (comb', agg'), ), where comb' are combination functions mapping pairs of vectors to single vectors, and agg are aggregation fugeegttionuunction functions mapping multisets of vectors to
single vectors. An application of M to graph G (V, E, c) yields embeddings (3) computed for
3

---

all E V and i i+ 1 S k as follows:
h (0) = c(u), = comb ++1
(h.)). (mmb++((hh)))
agg ( [u,u) E EB)).
= For a pointed graph (G, v), we let M(G, h!d
(2) be the final embedding computed for v.
Depending on the type of combination and aggregation functions we obtain various classes of MPNNs, usually written as M. In particular, we use M for the class of MPNNs whose combination functions are realised by feedforward neural networks with truncated- U max (0, mi)(1,=)) as
activation function and with aggregation given by the entrywise sum agg (S) = Exes We denote the class of these FNN by [NN[LL]LLU] (see Appendix A. for a formal definition). Another class of MPNNs we consider is Mmag which is similar to M, but aggregations are now given by agg( S) = Emes msg(a)) where msg is a feedforward neural network from FNN[trReLU]
Next, we discuss three classes of TGNNs obtained by extending MPNNs in order to process temporal (G,, l.). The first type, recursive TGNNs, starts processing TG by applying an MPNN to the first static graph G1. It then extends G2 by concatenating node labels with the embeddings computed by the MPNN. Next, it applies the same MPNN to the obtained static graph. This process is applied recursively in rounds, until all graphs Gi,..., Gn are processed. The formal definition of such models is given below.
graphs TG = (G),4)).
Definition 2. Recursive TGNNs M. class M of MPNNs, are pairs T (M, out), where M E M and out is an output function mapping vectors to binary values in {0. 1]. An application of T (M, out) to a temporal graph TG = (G,,t)).... (Gn,ta) with G3 (V, Ej, Cj). yields the following embeddings for all v E V and j + +15 n:
h1t0) (4)) = cx)
h (()+1) = (+)(())])))))))))))())))))) (ty). E5, [u+ (1,)), (()) - (t))=((VV))))))) ((V,, E,,
(0) (t,)) is labelling function mapping each where l is the number of layers in M and [u + h
u E V, to the vector h (tz).
We remark that we introduce the Trec architecture to represent approaches that directly leverage existing MPNN architectures for temporal graphs (48) without employing a specialised architecture.
The second type, time-and-graph TGNNs, are studied in several papers D4 g and akin to several models 125
7 39.. Such TGNNs perform computations by exploiting not only MPNNs, but also cell functions (e.g. a gated recurrent unit (10) mapping vectors to vectors. In particular, time- and-graph TGNNs use two MPNNs (M1 and M2) and one cell function (Cell). A temporal graph TG =G=(0 (C1,tt)...... (Gn, tx) is, again, processed from left to right in steps. In each step j 1, the TGNN applics M, to Gj+1 and M2 to Gj+1 with node labels replaced by embeddings computed in step j. This results in computing two vectors for each node, which are combined into single vector using Cell. After n steps of such processing, the TGNN terminates its computations.
Definition Time-and- graph TGNNs Trando C), for a class M of MPNNs and class C of cell functions, are tuples T = (M1, M2, Cell, out), where M1, M2 E M have the same number of layers, Cell E C, and out an output function (as in Definition 2 An application of T = (M1, M2, Cell, out) to a temporal graph TG = (G1, (11,t))..... ........ (Gr, (n) with Gj = (Vj, yields the following embeddings for all V E V and j 1 n
(t1) = Cell(M1((1,, 0), E1, [u + O)), be (1g-1))) = (G M2((V Esgr, [u + h (())))))) where [u + hn,(t)) is described in Definition 2
The third class, global TGNNs 44 is also realised by several TGNN models B5 27 Instead of processing a temporal graph in each time point, global TGNNs exploit a temporal message-passing mechanism. It allows messages to be passed among nodes from different time points. To capture the time difference between nodes between which messages passed, global TGNNs use time functions & R + R...
Definition 4. Global TGNNs Toiol M,, Q, o). for a class M of MPNNs, a class Q of time functions, and an operation combining two vectors of the same dimensionality, tuples T = (M, o, out)

---

where M E Mó E Q and out is an output function (as in Definition 2 An application of T (M, 9, out) to a temporal graph TG (G,,tt),.... (G,, ta) with G3 (V,, C,) yields embeddings he +1:t1) (l)))) for all E V, 7,i+11 15 S k (for k the number of layers in M), and j S n.
(1z)
h. = c,()), h (1)) comb' #+1 (h, agg ++1 ag (h. (la) (1a)
oll, - 1n) (v,u) E En,h S iB)).
In all TGNN models considered above, an output function out is used to determine the final classifi- cation. Formally, for TGNN I' and pointed temporal graph (TG, v), we let the output of T be T(TG, v) ou 9 (t,)). We will assume that out functions are realised by a single-layer FNN from the class FNN(tr
5 Logical Expressiveness via Product Logics
We will exploit two-dimensional-preee -produuct logics as a tool for analysing the expressive power of TGNNs. Specifically, we consider two-dimensional logics which are products of modal and temporal logics, allowing combinations of structural and temporal properties to be expressed. Importantly, this approach provides an opportunity to control the interaction between logical operators corresponding to the two dimensions. By modifying allowed interactions in product logics we will obtain logics that are suitable to analyse the expressive power of various classes of TGNNs.
Before introducing product logics, we specify the notion of the expressive power that we will consider in this paper. corresponds the "logical expressiveness" also called "uniform expressiveness". which is broadly studied in the literature [3] 20 5 12) and is defined as follows.
Definition 5. Let & be a logical language, whose formulas y are evaluated at timestamped nodes (v, (n) of temporal graphs TG (G1,41) (1).......... ..... (Gn, tn)- We write TG, (u, F up if up holds at (v. tn) in TG. A TGNN class T is at least as expressive as L. written L S T, ffr every formula yp of L, there exists a model T such that, for all (coloured) pointed temporal graphs (TG, (v, bn)):
TG, (v,tn)) tn) - up if and only T(TG,)
Informally, L S means that TGNNs from the class T are powerful enough to express all properties that can be written (arbitrarily long and complex) formulas of the logics L.
In order to study the expressive power of TGNNs, we will establish their relation to two-dimensional product logics [4 6 28 The first dimension will correspond to time and will allow us to capture cvolution of graph in time. The second dimension will correspond to the spatial structure of graphs and will allow to express properties of the static graphs at fixed time points. The product logics we consider here are combinations of the most prominent temporal and modal logics, namely propositional temporal logic PTL (4] and the basic modal logic K 23
Temporal logic PTLp,y. We consider the past-time version PTLp.Y of PTL which contains only ("sometime in the past") and Y ("yesterday") as native temporal operators. PTLp, y formulas built using propositions (I,- c1....: Cs which stand for colours that nodes of temporal graphs can take, together with unrestricted use of Boolean connectives for "not", A for "and", for "if ... then ...", "na <> for if and only if". Formulas of the logic PTLp,y can state, for example, that a node has currently colour ej and sometime in the past had colour C2 in two consecutive timepoints. This is written as C₁ A P(c2 A Yc2).
Modal logic K. For the static part we use the basic modal logic K. Its formulas are similar those of PTLp,y. y. but instead of the temporal operators P and Y it features a single modal operator Q The intuitive reading of Qxp is "P holds at one of neighbours (via graph edges) of the current node". Logic K can express, for example, that node has an outgoing path of three hops leading to node of colour ej or a two-hop path to a node whose colour e2 and not C3 000c1 V (0(c2 A -Cs)
Product logic PTL,,yxK. The product of logics PTLp,y and K allows us to write formulas with any combination of operators from PTLp,y and K. For example, & = C₁ (Poz) A (((-e) A o2) A Y ((ı A -02)) is satisfied at vertex v in time point t, if is coloured o₁ at tn and at some past
5

---

timestamp t < i.. was coloured with c2. Moreover, there is neighbour of u that is currently coloured with 22 but not ej t, whereas in the preceding timestamp fn- was coloured with ei but not with <2. An example of a pointed temporal graph (TG, v) satisfying y in in la is given in Figure T From the technical perspective, the semanties of PTLp, x K is defined over Cartesian products of models of PTLp,y and K, which justifies the name "product logic". A formal definition of syntax and semantics this product logic is given in Appendix A.2
G2
Ge
2
fg
44
Figure 1: A temporal graph of length 4; colour ej is denoted by a red filling (node u in G3 and node in G4) and colour 02 is denoted by blue filling (node in G1 and node in G4)
We also consider variants of PTLp,y K obtained by replacing the modal logic with other modal logics known from the literature, by syntactically restricting how temporal and modal operators can co-occur in formulas. Such variants differentiate the expressive power of various TGNN models.
Logical expressiveness of recursive TGNNs
We provide expressive power results for recursive TGNNs by relating them with product logics. We show that TGNNs from the class [M] can express all properties definable in PTLp,y xK.
Theorem 6. XK < Mr..
Proof sketch. For each formula yo E PTL,,yXK, we enumerate its subformulas PP,,..., Pm, Pm+1y..., Pn = in such a way that the m atomic ones come first, and (p is a subformula of 4oj, written as s E sub(sp)) then S j. We construct TGNN T (M, out) E [Me where M consists of m + 1 layers: one layer for each non-atomic subformula and final shift layer. At each time & and for each node of the current temporal graph, T.p computes the hidden state he ((nm)(t), (t), which encodes (I) the current truth values of all subformulas şi in the first n dimensions, (I)) the truth values of all subformulas oi at f - 1 in dimensions n + to 2n, and (II)) the disjunction of truth values of subformulas yp; over all earlier time points dimensions 2n + to 3n. The final shift layer (layer n m + 1) updates (III) using (II) without altering (1). Correctness follows by nested induction over time and subformula structure, showing that for each S n, dimension correctly tracks satisfaction of spi, dimension
i tracks Yup;, and dimension 2n. + tracks Pip: The output oul simply reads the value for &p at the final time point. A full proof given Appendix B.
We provide two further analogous results obtained by replacing and M with pairs of logics and MPNNs of matching expressiveness known from the literature. This suggests general connection between product logies and recursive TGNNs. First, K can be replaced with the logic K# incor- porating linear arithmetics, and M with the class of MPNNs Mバ* of matching expressive power 332. Second, an analogous result is obtained when using the logic C-MP", incorporating Presburger Arithmetic, and the class OCtrReLU-GNT of MPNNs, for which matching expressiveness results have been shown [5]. For the formal details of these logics, see Appendix[A.. A.33 and we remark that is evident that both strictly subsume PTLp,y
Theorem 7. PTLp,y K## < [Rr and PTLp, < (Ot.LOOLLLLU
Proof sketch. We apply similar inductive argument as used in Theorem 6 For each formula p, we enu- merate its subformulas . Pm Pmm +1..... Pm,,
Pn = sp, so that all subformulas of the form Yι or Pub occupy positions m: for 1...., k. Each group of purely non-temporal subformulas (situated between m. and m;41, assuming that formulas ye with i S m; are already addressed) is captured inductively by stacks of MPNN layers whose existence is guaranteed by results

---

(TG.v)
(TG', x/)
Figure 2: Counterexample, used in Theorem 8 colour ej is denoted by red filling (node un in G2 and node w/ in G%2) and colour 02 is denoted by a blue filling (node u2 in G1 and node w/ in G3)
from literature 32 This necessitates that OCtRReLU-GNN and MM* are closed under arbitrary but well-defined combinations of MPNN layers. Temporal subformulas You and Pub are handled by simple dimension shifts, reading values stored at previous timepoints across past histories, similar to Theorem [6] Here, we use the same form of hidden states, divided into three blocks tracking the current, previous, and past satisfaction of subformulas. Correctness follows by nested induction over time and subformula structure: for non-temporal subformulas, correctness can be shown exploiting results from literature [S] [2], while for temporal subformulas, follows from the way which the
temporal operators Y and P are addressed. The full proof is in Appendix B.2
7 Logical expressiveness of time-and-graph and global TGNNs
Next, we focus on two variants of TGNNs that have been considered in the literature thus far, aiming to unveil certain differences in their logical expressiveness.
First, we examine time-and-ee -ime-and-graph TGNNs [4], denoted by TrandG [M, CJ and parametrised by a class of MPNNs M and class of cell functions C. These TGNNs differ from the previously discussed classes [M]], not in the specific form MPNNs used, but in how temporal information pro- cessed. In particular, TaandG appears less powerful at processing the combined information of current snapshot (G,, t4) and the embedded information of the past snapshots (G1,t1),.... (G.
Theorem 8. PTLp,y E TM, C), for all M and C.
Proof sketch. Consider the PTLp, XK formula y Oc Y0c2). satisfied by all pointed temporal graphs (TG, (v, (n)) where n 2 2 and node v has a neighbour that is of colour at timestamp t, and which has a neighbour of colour c2 at timestamp - For example, see Figure where (TG, v) satisfies and (TG', v') does not. We can show that there exists no TGNN T = (MM,Ms, Cell) E [MM, C] for any class of MPNNs M and cell functions C that captures sp Intuitively, Mi handles the present label information and M2 the past information, but neither handles both. While Cell can use outputs of M, and M2, has no access to the topology of the static graph. However, to check whether is satisfied, this is necessary. This results in the fact that T either accepts both (TG, v) and (TG', o') of Figure or none. A formal proof of this is provided in Appendix B.3
The natural next question is identify a fragment of PTLp.y xK whose formulas can be expressed by time-and- graph TGNNs. Let F c. FNN[trReLU be the class of single layer FNNs with truncated- ReLU activations. We let C be the fragment of PTLP. K containing only formulas op such that for all Qrb E sub(Gp) there is either no Qx E (ub())) with Q E (Y, P) or for all E sub(s) there is Qx E sub(w) with Q E (Y, P} such that e sub(x). Hence, L1 restricts the allowed interaction of operators in PTLp,Y xK. For example (Pc; is formula of L1, but (Pcc A 62) is not.
Theorem 9. L1 TTandG (M,
Proof sketch. We apply the inductive approach of Theorems G and 7 to formulas op E L1. We construct time-and-graph TGNNs Tp (M1, M2, Cell, out) E TrandG
[M, Tranda where the three components partition the evaluations according to the syntactic form of the subfornulas yo; of yo. The MPNN Mi captures all subformulas yp, that do not include the temporal operators Y or P, meaning processes static properties of the current snapshot. Similarly, the MPNN M2 handles all subformulas
7

---

where every atomic subformula is nested under temporal operator, indicating that the formula evaluation relies solely on the prior hidden states, The cell function Cell manages the remaining subformulas, which must be Boolean subformulas (~1/1 or 4/1 A x/2)) due to the definition of L1- Correctness is established through a nested induction over time and subformula structure, as done previously. The structure of L ensures that all subformulas are appropriately covered by the division among M1, M2, and Cell. A full proof is provided in Appendix (B.4
We remark that some line-and-grape TGNNs considered in the literature [14] utilise a gated recurrent unit (GRU) [0] as their cell function. The class of TGNNs considered in Theorem i subset of this broader class. There are also similar, time-then-graph TGNNs, considered in the literature [14]. They first process the temporal information of a temporal graph using a recurrent neural network (RNN), followed by the application of an MPNN to capture the topology. It is shown that for each -ngaad TGNN, there exists an equivalent time-then then-thhn--gaph TGNN [4] 3.6]. Thus, our results from Theorem 9
Theorems 3.5 and
transfer to time-then-graph TGNNs.
They parametrised by a class of MPNNs M, time functions from 2, and an operation o combining label and temporal information in the aggregation. Similarly to fime-and-graph TGNNs, Tglob cannot capture all properties definable in PTL.,y
Next we consider global TGNNs, Tglob M,, 2, recently studied in the literature 44
Theorem 10. PTLp,y xK 1 [M, 2, for all M, Q, and o.
Proof sketch. Consider the PTLp,y xK formula ş = Ye1, which is satisfied by all pointed temporal graphs (TG, (v, bn)) where n 2 2 and the node a was of colour ej at timestamp 1--1. Interestingly, there is no Tgiob[ (M, Q, o] for any M. Q, and o that can express this property. The reason is as follows: the notion of temporal neighbourhood utilised by global TGNNs does not give a node v access to its own past information. It can only access past informations of neighbours. Since this is the only form of temporal information used by such TGNNs, it excludes the ability to recognise whether itself was coloured e₁ in the past. For the full proof, see Appendix BB.
Next, we turn to identifying a fragment of PTLp, xK captured by Tglob- The architecture of global TGNNs appears to necessitate a class of MPNN components that effectively utilise temporal information. Specifically, we use MPNNs incorporating a learnable message function msg in their aggregation. This enables global TGNNs to process messages based on temporal information prior to aggregation. Thus, we use Mmsg (see Section 4 to recall the definition of such GNNs). Concerning ø and o, meaning the operations by which temporal information is processed and then combined with static neighbourhood information during aggregation, we employ time2vec [22] and concatenation II of vectors, akin to models such as TGAT or Temporal Graph Sum (35). Let Qtime2vec be the class of all time2vee functions (see Appendix A.3 for formal definition). We let Le be the fragment of PTLp,y xK, whose formulas &p are such that for all Q E sub(yp) with Q E (Y, P} we have &b = Ox for some formula x- For example PỘc₁ is formula of L2, but Pe₃ is not.
Theorem 11. L2 I [M Qtimezvec:
Proof sketch. We use the inductive approach from Theorem 6 but now use global TGNN T.p = (M, db out). For each subformula yei layer 7(0) in M computes its semantics. Boolean subformulas are handled as in previous results and temporal subformulas Yı and Ptb are deferred, since their semantics are captured indirectly through O subformulas, as ensured by the definition of Lg. The key mechanism to do this is the interaction between @ and msg: for each QOO with Q E {P, Y}. msg selectively passes information based on é(t), enforcing that only the correct previous or past timepoints contribute. If & is of the form YOX or POX, msg filters messages from exactly the previous timepoint or from all earlier timepoints, respectively. Otherwise, msg restricts aggregation to the current timepoint. Correctness follows by induction over time and subformula structure. A full proof is provided in Appendix B.6
While employing time2vec functions motivated by common practice, is not essential for achieving the previous result. In fact, it suffices to have function ø capable of mapping the values 0, -1, and 1, where 1 S 22, to distinct values. Similarly, I| not strictly necessary. The same result can be achieved, with slightly adapted construction, using entrywise multiplication or addition as
8

---

Tic M
[M Mx##
Tee(OCtRReLU GNN]
Th. VI
Th. 2 VI
PTLp. x
PTLay x (C MP)?
Th. 1 VI
Th.
PTLp, k
Tronaa F]
Th. 3
Th.
Tass MMnss Quimatves III
Th. 4
+
Th.
Figure 3: An overview of our expressive power results
Now, combining the previous results, namely Theorems II and the insight that (cc A Y0c2)= L2 and Yeι E L1 we immediately get the following inexpressiveness results. Let Ti and To be two classes of TGNNs. We let Ti S T2 if for all T Ti there is T" To such that for all discrete, pointed temporal graphs (TG, v) we have that T(TG, v) = if and only T ( (TG, v) = 1. Accordingly, we
define Ti T2 if Ti S T2 does not hold, and we define Ti * T2 if Ti 1 T2
1 Ti.
Corollary 12. [M
X Tandd Treo[Mi]
Mplog Qumeezee: ||]. and
TTandG MIFI # Tolob[Mmag: mag: Qtime2ves;
||].
To complement the picture expressiveness relationships obtained so far, we establish the following relationship between time-and- gouddggrphhhho and recursive TGNNs; recall that F S [FN[(tRRLLU] is the class of single layer FNNs with Muncated-ReLLA activations.
Theorem 13. Taand M, F] < Trea [M].
Proof. Let E Tranaa (anaa[M,,7 [ with = (M1, M2, Cell, out), where each M, is of input dimen- sionality m, and output dimensionality n4, and Cell is of input dimensionality nı + ny and output dimensionality nıs. The construction of the witness T" Trea [M] is straightforward: T' is given by (Ma, out), where M3 is given by Cello Mj M2 which represents the MPNN of input dimensionality my m2 and output dimensionality ny simulating M1 the first m, input dimensions, M2 on the last m2 input dimensions, and then applies a message message-passing layer, where the combination function ignores input from agg and uses Cell otherwise.
Figure summarises the expressive results we have established in the paper.
8 Conclusion
We have initiated the study of the expressive capabilities of TGNNs using logical languages, which is motivated by successful logical characterisation of static GNNs. As we have showed, product logics combining temporal and modal logics, are particularly well-suited to achieve this goal. In particular, we have studied three classes of TGNNs: recursive, time-and-grape showed that recursive TGNNs can express all properties definable in the product logic PTLP, K, combining the standard temporal and modal logics. Moreover we have obtained analogous results by relating variants of PTLp, Y xK to recursive TGNNs that exploit specific classes of MPNNs. In contrast, neither time-and-gran and-graph or global TGNNs can express all properties definable in PTLP, xK. The reason is that PTLp, Y xK allows for arbitrary interaction between logical operators expressing temporal and spatial properties. By restricting the form of these interaction, we have obtained fragments of PTLp,y XK which can be captured by tome-and-gras or global TGNNs, respectively.
and global TGNNs. We have
Our results provide new insights into the expressive power of TGNNs and show that TGNN architec- tures significantly differ on the spatio-temporal properties they can capture. Better understanding of TGNN capabilities crucial for choosing appropriate models for a downstream task and help in developing more powerful architectures. Since this is the first work on the logical expressiveness

---

of TGNNs, it has number of interesting next steps that can be performed in future. Among others, we plan to investigate tight expressive bounds, and for larger amount of TGNN architectures. Furthermore, we plan to transfer results known from research on product logics to TGNNs, including computational complexity analysis and finite model theory.
Limitations. The results established here are of strictly formal nature. Our expressive results focus on showing which classes of TGNNs can express (i.e. detect) temporal graph properties expressible in particular logics. Hence results do not aim show which properties can be learnt in practice, but to show fundamental relations between expressiveness of TGNNS and product logics.
Acknowledgments and Disclosure of Funding
This research partially funded by the European Union (ERC, ExtenDD, project number: 101054714). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
References
[1] V. Ahvonen, Heiman, A. Kuusisto, and C. Lutz. Logical characterizations of recurrent graph neural networks with reals and floats. In 38th Conference on Neural Information Processing Systems, 2024.
[2] A. Artale and E. Franconi. A survey of temporal extensions of description logics. Ann. Math. Artif. Intell., 1011-1) 2000.
[3] P. Barceló, E. V. Kostylev, M. Monet, J. Pérez, J. L. Reutter, and J. P. Silva. The logical expressiveness of graph neural networks. In 8th Conference on Learning Representations, ICLR, 2020.
[4] Barceló, A. Kozachinskiy, W. Lin, and V. Podolskii. Logical languages accepted by transformer encoders with hard attention. In 12th Conference Learning Representations, ICLR, 2024.
[5] M. Benedikt, C. Lu, B. Motik, and T. Tan. Decidability of graph neural networks via logical characterizations. 5/st Colloquium on Automata, Languages, and Programming, ICALP, LIPIcs. Schloss Dagstuhl- Leibniz-Zentrun für Informatik, 2024.
[6] B. Bennett, A. G. Cohn, F. Wolter, and M. Zakharyaschev. Multi-dinmensionll modal logic as a framework for spatio-temporal reasoning. Appl. Iniell., 17(3):239 2002.
[7] Chen, X. Wang, and X. Xu. GC-LSTM: graph convolution embedded L.TTM for dynamic network link prediction. Appl. Intell., 52(7):7513-7522 2022.
[8] Y. Chen and D. Wang. Calibrate and boost logical expressiveness of GNN over multi-relational and temporal graphs. In 37th Conference on Neural Information Processing Systems, 2023.
[9] K. Cho, B. van Merrienboer, Ç. Gülçehre, D. Bahdanau, F. Bougares, Schwenk, and Y. Bengio. Learning phrase representations using RNN encoder-decoder for statistical machine translation. In 2014 Conference on Empirical Methods Natural Language Processing, EMNLP, pages 17341734. ACL, 2014.
[10] Chung, Ç. Gülçehre, K. Cho, and Bengio. Empirical evaluation of gated recurrent neural networks sequence modeling. CoRR, abs/1411.3555, 2014.
[11] A. Cini, I. Marisca, M. Bianchi, and Alippi. Scalable spatiotemporal graph neural networks. 37th AAAI Conference Artificial Intelligence, 37(6):2118-7222 2023.
[12] B. Cuenca Grau, Feng, and A. Walega, The correspondence between bounded graph neural networks and fragments of first-order logic. arXiv preprint arXiv:2505.08021, 2025.
10

---

[13] S. Demri and P. A. Walega. Computational complexity of standpoint LTL. arXiv preprint arXiv:2408.086 08557, 2024.
[14] J. Gao and B. Ribeiro. On the equivalence between temporal and static equivariant graph representations. 39th Conference on Machine Learning, volume 162 of Proceedings of Machine Learning Research, pages 7052-7076. PMLR, 2022.
[15] N. Gigante, L. Gómez Alvarez, and T. S. Lyon. Standpoint linear temporal logic. In Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning. KR, pages 311 1-321, 2023.
[16] Gilmer, S. S. Schoenholz, F. Riley, O. Vinyals, and Dahl. Neural message passing for quantum chemistry. In 34th Conference on Machine Learning, ICML., Proceedings of Machine Learning Research. PMLR, 2017.
[17] M. Grohe. The logic of graph neural networks. In 36th ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 1-17. IEEE, 2021.
[18] E. Hajiramezanali, A. Hasanzadeh, K. R. Narayanan, N. Duffield, M. Zhou, and X. Qian. Variational graph recurrent neural networks. In 32nd Conference on Neural Information Processing Systems, NeurIPS, pages 10700-10710, 2019.
[19] Y. Halper and M. Y. Vardi. The complexity of reasoning about knowledge and time. lower bounds. J. Comput. Syst. Sci., 38(1):195-237, 1989.
[20] S. P. Hauke and P. A. Walega. Aggregate-combine--ann logic C2. arXiv preprint 2xXi:2558.0600), 2025.
GNNs are more expressive than
[21] A. Kapoor, X. Ben, L. Liu, B. Perozzi, M. Barnes, M. Blais, and S. O Banion.. Examining COVID-19 forecasting using spatio-temporal graph neural networks. CoRR, abs/2007.03113, 2020.
[22] S. M. Kazemi, R. Goel, S. Eghbali, J. Ramanan, J. Sahota, S. Thakur, S. Wu, C. Smyth, Poupart, and M. A. Brubaker. Time2vec: Learning a vector representation of time. CoRR, 2019.
[23] S. A. Kripke. Naming and Necessity. Harvard Univ. Press, 1972.
[24] A. Kurucz, Wolter, M. Zakharyaschev, and D. M. Gabbay, Many-dimensional modal logics: Theory and applications, volume 148. Elsevier, 2003.
[25] Li, Z. Han, H. Cheng, J. Su, Wang, Zhang, and L. Pan. Predicting path failure in time-evolving graphs. In 25th ACM SIGKDD Conference on Knowledge Discovery & Data Mining, KDD. ACM, 2019.
[26] A. Longa, V. Lachi, G. Santin, M. Bianchini, B. Lepri, P. Lio, F. Scarselli, and A. Passerini. Graph neural networks for temporal graphs: State of the art, open challenges, and opportunities. Trans. Mach. Learn. Res., 2023, 2023.
[27] Y. Luo and Li. Neighborhood-aware scalable temporal network representation learning. In 1st Learning on Graphs Conference, volume 198 of Proceedings of Machine Learning Research. PMLR, 2022.
[28] C. Lutz, F. Wolter, and M. Zakharyaschev. Temporal description logics: A survey. In S. Demri and C. S. Jensen, editors, 15th Symposium on Temporal Representation and Reasoning, TIME, pages 3-14. IEEE Computer Society, 2008
[29] M. Marx and Y. Venema. Mulii-dimensional modal logic, volume of Applied logic series. Kluwer, 1997.
[30] A. Micheli and D. Tortorella. Discrete-time dynamic graph echo state networks. Neurocomput- ing, 496:85-95, 2022.

---

[31] C. Morris, M. Ritzert, M. Fey, W. L. Hamilton, J. E. Lenssen, G. Rattan, and M. Grohe. Weisfeiler and leman go neural: Higher-order graph neural networks. In 33rd Conference on Artificial Intelligence, AAAI, volume 33, pages 4602-4608 2019.
[32] Nunn, M. Sälzer, Schwarzentruber, and N. Troquard. logic for reasoning about aggregate- combine graph neural networks. In 33rd Joint Conference Artificial Intelligence, IJCAI, pages 3532-3540. ijcai.org, 2024.
[33] A. Pareja, G. Domeniconi, J. Chen, T. Ma, T. Suzumura, H. Kanezashi, T. Kaler, T. B. Schardl, and C. E. Leiserson. Evolvegen: Evolving graph convolutional networks for dynamic graphs. In 34th Conference Artificial Intelligence, AAAI, pages 5363-5370. AAAI Press, 2020.
[34] A. Pnueli. The temporal logic of programs. In 18th Symp. on Foundations of Computer Science, FOCS, pages 46-57. IEEE, 1977.
[35] E. Rossi, B. Chamberlain, F. Frasca, D. Eynard, F. Monti, and M. Bronstein, Temporal graph networks for deep learning on dynamic graphs. arXiv preprint 1oXiv:2006116631 2020.
[36] M. Sälzer and M. Lange. Reachability in simple neural networks. Fundam. Informaticae, 189(3-4):241-259, 2022.
[37] M. Sälzer, F. Schwarzentruber, and N. Troquard. Verifying quantized graph neural networks is PSPACI--coplete. CoRR, abs/2502.16244, 2025.
[38] A. Sankar, Y. Wu, L. Gou, W. Zhang, and H. Yang. Dysat: Deep neural representation learning on dynamic graphs via self-attention networks. In 13th ACM Conference on Web Search and Data Mining, WSDM, pages 519-527. ACM, 2020.
[39] Y. Seo, M. Defferrard, P. Vandergheynst, and X. Bresson. Structured sequence modeling with graph convolutional recurrent networks. In 25th Neural Information Processing Conference, ICONIP, volume 1301 of Lecture Notes in Computer Science, pages 362-373. Springer, 2018.
[40] J. Skarding, B. Gabrys, and K. Musial. Foundations and modeling of dynamic networks using dynamic graph neural networks: A survey. IEEE Access, 9.79143-79168. 2021.
[41] A. H. Souza, D. Mesquita, S. Kaski, and V. K. Garg, Provably expressive temporal graph networks. 35th Conference on Neural Information Processing Systems, NeurlPS, 2022.
[42] D. Tena Cucala, B. Cuenca Grau, B. Motik, and E. V. Kostylev. On the correspondence between monotonic max-sum GNNs and datalog. In P. Marquis. T. C. Son, and G. Kern-Isberner, editors, 20th Conference on Principles of Knowledge Representation and Reasoning, KR, pages 658-667, 2023.
[43] J. Tena Cucala and B. Cuenca Grau. Bridging max graph neural networks and datalog with negation. In P. Marquis, M. Ortiz, and M. Pagnucco, editors, 21 Conference on Principles of Knowledge Representation and Reasoning, KR, 2024.
[44] P. A. Walega and M. Rawson. Expressive power of temporal message passing. 39th Conference on Artificial Intelligence, AAAI, 39120)21000021008, 2025.
[45] D. Xu, C. Ruan, E. Körpeoglu, S. Kumar, and K. Achan. Inductive representation learning on temporal graphs. In 8th Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
[46] K. Xu, W. Hu, J. Leskovee, and S. Jegelka. How powerful are graph neural networks? In 7th Conference on Learning Representations, ICLR, 2019.
[47] A. Yang and D. Chiang. Counting like transformers: Compiling temporal counting logic into softmax transformers. CoRR, abs/2404.04393. 2024.
[48] You, T. Du, and Leskovee. ROLAND: graph learning framework for dynamic graphs. In KDD '22: The 28th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, pages 2358-2366. ACM, 2022.
[49] B. Yu, H. Yin, and Z. Zhu. Spatio-temporal graph convolutional networks: A deep learning framework for traffic forecasting. In 27th Joint Conference on Artificial Intelligence, IJCAI, pages 3634-3640 ijcai.org. 2018.
12

---

A Omitted definitions
In this section, we provide full formal definitions of concepts that were introduced informally in the main part of the paper.
A.1 Feedforward neural networks
We present a formal definition the classical feedforward neural network (FNN) model.
Definition 14. An FNN node e is a function from R to R, where m E NN is the input dimension, computing
o(z o(b + + Σ w,x:),
i=1
where Wy E Q are the weights, b E Q is the bias. and a R + R. is the activation function. An FNN layer i is tuple consisting of some number n E FNN nodes (U1,..., vn), all having the same input dimensionality m. Then, & computes the function from R to RR", where is the output dimension, given by
[T = (111......... 2mm.......m................... ..... (21
Imm)..
Finally, a feedforward neural network (FNN) N is a tuple of some k N FNN layers (62,.... Cg). where the input dimension of E+t1 is equal to the output dimension of l, for all < k. Then, N computes the function from Rm to R"*, where my is the input dimensionality of nodes layer 1 and ng is the number of nodes in layer la given by
N (æ Im.) ca(-.. ( (21..... Tm..) ...).
Given this definition, we denote by FNN [e the class of all FNN where all nodes exclusively use (r)) max(0, min(x, 1)) the activation function.
A.2 The product logic PTLp,y
In the following, we define one of the key logics we consider, namely PKL,, Definition 15. We define the logic PTLp, xK given by all formulae defined by the grammar:
4p : : 1- & A Oyp Yip Py
where 0 J < k for some set of k colours. Let (TG, v) be a coloured, pointed temporal graph. Since the temporal operators in this logic oblivious of the exact timestamps in TG we assume that TG is discrete. We say that (TG, v) satisfies formula ip, written (TG, (v, t.)) } s. if given:
(v, Foj
iff
(v)) 1,
(G,(v,4) - up
iff
(1,4)) FP) A
iff
TG, (t,tt) F and TG, (v,t,) } 92,
(1,(4,4) 00
ilf
there is E V s.t. {u, ue E E, and TG, (u, F s,
(G, =Yp Yıp
iff
t + and TG, (v,4, =
(G,(4,4) Pup
i0'
there is lj < t such that TG, (v,4z) }
A.3
The product logics PTLP,yX(CMMPP and PTL
We give formal definitions of the logics PTLp, y x (C-MP² and PTLp,y #* based on the modal
logics presented in (5) and (32 These follow the same line as the definition of PTLp,y xK given in Definition 15
Definition 16. Formulae of X are defined by the grammur:
6 := T 6
a; #4p 5 bl - p Py
13

---

where e; ranges over propositional variables in a finite set C of colours, and a, a, e Q. Let (TG, v) be a coloured, pointed temporal graph. Since the temporal operators in this logic are oblivious of the exact timestamps in TG we assume that TG is discrete. We say that (TG,t) v) satisfies formula y, written (1, = s. if given:
(c,
iff true,
(1,44 Fc
iff
(v)) =1,
k (G, F Σ ai #oi b
iff Σ
q
Kuu E V {u, E E, and TG, ()) F sil s b,
i=1 (0, F 7p
1=1
iff (G,(u,t) + 4:
(0,44, F 91 92
iff
(U, F 41 and TG, (v,t,) F 92
(c,(), F Y
iff + O and TG, (u,t, - 1) F i,, and
(c,4) + Pt
iff there is t' < t, such that TG, (v, t') } sp. 1
Although it does not affect any of our results, we note that [5] consider MPNNs operating on directed graphs, whereas our focus is on static graphs with undirected edges. Consequently, there is technical difference in the definition of the semantics the E a, #i; S quantifier compared to [5].
Definition 17. Formulae of PTLL,y XK# are defined by the grammar:
6 ::=66 Σ a 1 Σ b, . #o up
where ranges propositional variables in a finite set C of colours, and az bi, d Z.
Let (TG, v) be coloured, pointed temporal graph. Since the temporal operators in this logic are oblivious of the exact timestamps in TG we assume that TG is discrete. We say that (TG, v) satisfies formula up, written (TG, (v, tn)) F s. if given:
(v,44, } ej
if (c,( 11
(v, - -p
iff
TG, (v, H
(G,(u,4) F #1 A A
iff TG, = 91 and TG, (v,t) F P2,
(G,(1,4) Yp
is 4 4nd aG, (v, F 4,
(G,(), Pp
iff there is such that TG, (v, t') } s, and
(G, F Σ
1p: +
Σ
by # S
iff
1=1
& Σ a. . 1=1
Pi iTT,, (v,
k
+
Σ b Hu E V I (u,u) E E, and TG, (v. tx) F p. s d,
otherwise,
We note here that we utilised a normal form of K# (refer to Theorem I in 32 to simplify the definition of P K## As the authors point out, it is straightforward to observe that each formula of the original K# syntax can be efficiently transformed into this normal form.
The time function time2vec
In the following, we define time2vee functions 22 Definition 18. We define o(4: tz) t2v(1; (t) as wht + bj t2v(t), (wwwt + by)
ifj=0 - 0, otherwise,
where Wy.b, E Q and a some periodic activation funnctnionfuunction. Correspondingly, denote the class of all such functions by Qtime2vec-
14

---

B
Omitted proofs
In this section, we provide all the formal proofs for the results presented in this work. This includes comprehensive proofs for the results of the paper that were merely outlined in the main section.
B.1 Proof of Theorem 6
Theorem 6. PTLp,y < MM..
Proof. Let yp be formula of P as defined in Definition 5 with m atomic subformulas. Let
PI..... Pm: fm+1:..... Pn
be an enumeration of the subformulas of o such that all atomic formulas are the (P1. .... Pm. and SP E sub(pp)) implies i & j. particular, we have Sn = 4.
We begin by describing how the TGNN Tр is constructed. We have Tp = out), where the MPNN M (L' ..... , 1m- and the layer (0) with S m given by (comb Σ) with comb (9) (z, y) = trReLU(Ca - Ay + b), and where Σ denotes entrywise sum as aggregation. The exact form of the 3n 3n matrices C, A, and the n-dimensional vector b depends on Pm=+ as follows:
if Pm+i mP,, we have Cm+i. = 1, and bm+4 = 1,
if fm++i PPj A Piz we have Cm+t.j = Cm = 1. and bm+i = -1,
if Pm+i =
O49j, we have Am-i.j =
if Pm++ =
Yıg,, we have Cm+ints =
if pm++ Pypj we have Cm+i,244 1, and
for all j S m we have Cjj- 1. All other entries of C, A, and b are zero. This implies that all layers 4 with i < m use the same parameters. The layer ("-m+1 = (comb" (comba-++1, -) is given by comb"-m+1 (x, y) = trReLU(C'xx A'y + 0), where A' is the 2n x 3n all-zero matrix, 0 is the 2n-dimensional all-zero vector, and C" is the 2n x 3n matrix with Cj. and C2 = for all j S n. All other entries are zero. The output function is given by out(z1,..... P2n) trR,)
C% Ch+jant
straightforward to see that T. [Me
Let (TG, v) be a pointed temporal graph where TG is of length k and V is its set of nodes. Regarding correctness, we prove the following statement: for all nodes V. all timepoints 4 with < k of TG and subformulas 3 with j S n of we have that
a) TG, (u, t4) - 2 if and only if h, (minn(U.jmm) (te)s
b) TG, (u, 1) + رP if and only if h.
(minn(..j-mm (t+)xtj and
c) TG, (u, (2) y2 for some i' i if and only if h (min(0.j-mm) (0))))))))))))a (ti)2ntj 1.
We prove this statement via strong induction on i and j.
Case: timestamp t1. First, let i = 1 and j E fl..... ..), and fix some u E V. The assumption j E {L,...,m² m) implies that by an atomic formula. Then, statement (a) is directly implied by the form of h (t,), including the colours of node u. Similarly, we have that statements (b) and (c) are given as T. initialises the dimensions
3n of h (tz) with which correct we are considering the first timestamp of TG. Next, assume that the statement holds for i = 1, j. and all V. Consider the case of j + 1, some u V, and focus on statement (a). The Boolean cases f0-11 1 = ,Pi and 40++1 4Pt, A Ptg are straightforward implication of the form of matrix C, vector b, as well as the activation function trReLU, and the fact that statement (a) holds for all 4,44 la < j. Similarly, the case 0ypl, implied by the form of matrix A, the activation function
15

---

trReLU, and that statement (a) holds for all I S and all w E V, including the neighbours of u. In the case of 9j+1 Yi, or -- P't,, we rely on the fact that = 1, which means that these are necessarily false. By the hypothesis, this is implied by (b) and (c) for all 1 S as matrix C' utilises the corresponding dimensions n + 1 and 2n + I1 respectively, which are all 0. The fact that we consider = 1 and that all dimenstions / >> are O also immediately implies statements (b) and (c).
Case: timestamp & with i > 1. Next, assume that statements (a) to (c) hold for i. all j S n, and all E V. and consider the case i + 1. Once again, the argument for statement (a) with j E {1,.... ,..... m) directly implied by the fact that T.p stores the colours of each node u in the respective dimension. Before addressing (b) and (c) for these j. consider the following two observations:
1. TGNN To ensures for all timestamps 4, j S and V that (0) (t++1)n+s h ( (tz),. and it ensures that ( (f+41)2nt5 = if and only if h (n-m) (tp) for some
1' Si
2. TGNN T. ensures for all timestamps 4, E V that hu
1 (4)5 = (4), holds for all
i {n + 1, ................................ ,n and / S n m, and it ensures that h. (t:); (ti, holds for all (t:);
j S n and j 5 m.
Informally, the first observation implies that dimensions + 1 to 2n store the previous state of node, and 2n + 1 to 3n store the disjunction over all previous states of a node, where 1 is interpreted as true and 0 as false. This is achieved by the way we built layer (m-m+11 The second observation simply states that, within a single timepoint 4, the TGNN T does not alter dimensions n + 1 to 3n within layers/ (2 to mn-m and that if the semantics of Sjj are computed in the j-th layer, they are preserved in subsequent layers. Now, consider statements (b) and (c) for + 1. E {1...., m) and some fixed u E V. Here, the first observation and induction hypothesis directly imply these statements. Therefore, keep u V fixed and consider + 1, while assuming that (a) to (c) hold for all j' S j. The Boolean and modal cases are argued exactly as before. Thus, consider ff+1 = Yup for some I S j. Using the first and second observations, we know that the semantics of yp: at timepoint t, are stored in hi++)) (l++1 )att, which utilised by T' to compute the semantics of Yupı. Given the induction hypothesis, this is correct. Similarly, the case Pj++ Pyp: is implied by the two observations and ((++)((t+))))))))))))))))) (f++1) 22++1 stores a 1 if fo: was true at any timepoint
the induction hypothesis, which state that h (i+1)
before 1,+1 and 0 otherwise. Given this, the correctness is immediate.
Finally, the correctness of the theorem is given by statement (a) for l and y.n = y in combination with observation that out uses the n-th dimension of h hg-m+I(la) to compute the overall output. D
B.2 Proof of Theorem 7
For formal definition of the logics PTLP,x((CMMP)) and X we refer to the corre- sponding subsection of Appendix A.3
The key results we rely are Theorem 26 of (5] and Theorem of [32 However, we need stronger form of these results that includes the capturing of the semantics of each subformula with a MPNN.
Definition 19. Let yp be an inductively built formula interpreted over pointed static graphs, and let M be an MPNN. We say that M inductively captures there exists an enumeration of all subformulas PP,,... : Pm of s, where yps E sub(s;;) implies i S j. such that for all pointed graphs (G, v) and formulas Pi there is layer of M such that
(f v) sps then h' ho)) = 1 for all 1 2 jo and
. (i, / pi then h' (v); = 0 for all I 2 ja
where h'(e) represents the state of u computed by the je-th layer of M. Furthermore, we require that j--1 S je for all i E (1.....m), We extend the notion of inductive capture to logic L over pointed static graphs and a class of MPNNs M in the obvious way and denote it by L < M.
Given this understanding, close examination of the arguments employed in 5 and 32 directly implies the inductive capture of the logics L-MP² and K # by the respective classes of MPNNs.
16

---

Lemma 1. Let L-MP? and K# be the logics introduced in [S] and [32] and OCtNReLU-MPNN and Mgs the respective classes of MPNNs. We have that L-MP² OEtReLUUMMNN and K# 4 MMg.
Proof. Both results, namely Theorem 26 from [5] and Theorem from [32]. are constructive in nature: for each formula y the authors construct an MPNN Mep that captures its semantics. Moreover, these constructions are inductive, meaning that all subformulas of yp are enumerated and the MPNN Mp is built such that it captures the semanties of the i-th subformula with its i-th layer and preserves it in subsequent layers. This establishes that these results in fact imply inductive capturing.
Now, we are set to prove that both PTLp, (C-MP²) and PTLp, x K are captured by the respec- tive classes of TGNNs.
Theorem 7. PTLp,yX I Trec|M*+ and PTLP,y S OCtreeeNrLL
Proof. First, we address the statement that PTLe,yX(-MPP) S Trea TTttReLNLLL Let y x with different subformulas of the form Yι or Ptp. Let
P1..... Pm, Pm, +1...., Pm2g Pma.1........................... pm.: Pmm+ Pn
be an enumeration of the subformulas of &p such that pi E sub({p) implies S J. 9s + Yıp and 9i * Pb if & (mi,.... m&}. and have ff, s. Furthermore, -mm41-17 with me = that the enumeration is such that Lemma applies to each formula of S,, where interpret potential occurrence of jo with j < m, as some fresh atomic formula.
assume for each set
S, = (9mc+1:-.
Let TV out). where out(21,... ..... .2..) trReLU(xx,)) and M is constructed follows. The initial layers are constructed to capture the semantics of the formulas f1 to (mm--1 in dimensions 1 to m2 1. 1. The existence of such peessage-passing layers is guaranteed by the existence of MPNNs capturing the formulas of S. = {fI..... 11) J. as indicated by Lemma [ Furthermore, these message-passing layers to 3n are mapped by the identity function within the range [0, 1]. The argument that these can be in- terconnected in M to form well-formed MPNNs is given by the fact that the class OLtRReUU-GN encompasses allows for arbitrary single-layer FNN with truncated-ReLLU activations as combinations. Next, consider (pm; which is either Ysp: or Pyp: for some i < m.. In the layer that maps dimension n + to dimension mi, and in the case of Pyp; we add a layer that maps dimension 2n i to dimension mi. Again, this is feasible due to the fact that DCCtReeL-MMPN includes arbitrary single-layer FNN with truncated-RR MenLateed-RLU activations as combinations. Subformulas Pmi+1 1m are handled like 90 (m,-1 using the stack of MPNNs implied by Lemma for 1.), }. combined accordingly. Then, Pma is addressed like pm, and so forth. Finally, we add layer that computes the exact same function as 1 p=-m+1 in the proof of Theorem 6 which ensures that previous and past semantics are preserved. Given this construction, we have that T.p E CereooottUeUUMMM
built with input and output dimensionality of 3n, where dimensions mi
of Y we add
S (fmm+1l-.. fmm--1
The correctness argument follows the exact same line of reasoning as that in Theorem 6 namely, arguing inductively over the timepoints of temporal graph and subformulae yoj. However, because we have not explicitly constructed T., we utilize the following arguments. For non-temporal subformulac (pj. we rely on the fact that Lemma [ applies to OCtrReLU-MPNN, which means that Py is captured after the respective layer. Note that this includes the observation that the assumptions we made for S, in order to apply Lemma [ makes no difference in the overall computation of M. Otherwise, we use precisely the same arguments.
Finally, for the case of P < Trec xT we note that Lemma 1 is applicable to both ## and Mg=. Moreover, the properties regarding the combination of MPNN layers needed above are also given for Mg.. Therefore, the argumentation presented above is equivalently applicable.
B.3 Proof of Theorem g
Theorem 8. XKL & MM. for all M and C.
17

---

Proof. Let E X be the formula y (c1 A Y0o2). We prove that there is no TGNN T E TrandG M, for any class of MPNNS M and functions such that for all pointed temporal graphs (TG, we have that (TG, v) F y if and only if TTTG, =
We consider the two pointed temporal graphs (TG,e) and (TG', e') fully specified in form of Fig- ure 2 It can be easily verified that (TG, u) F sp and (TG', x') + y. Let T E TrandG CJ be some TGNN. It is straightforward to see that for M1 of T, we have that (a) (I v) Mi (G', v'), Mi wz), (G,,,u w1) = M df), and (G1 w2)) M1 (G v2). This follows from the fact that M1 is a function and the input of the aggregation mutliset without any ordering. Similarly, this implies (b) M1 (G2, x) Mj (G2,, x')
M1 (I U1)
Mi (G1, wf), Mj (G1, u2)
for E {7, u1, U2 w1, W2 Also, we have that M2 outputs the same vector for each pair of nodes and x' at timestamp 11, due to the fact that all labels are assumed to be 0 and Ei = E Thus, the equalities of (a) are preserved by the application of Cell in the first timestamp f
Now, using (a), the same kind of argument gives that M2 outputs the same vector for v and v' at timestamp t2. Then, combining this with (b), we find that the function Cell receives identical inputs in the cases of (TG, v) and (TG', ,²) at timestamp 12, leading the conclusion that either both are accepted or both are rejected by T. Thus, T does not accept the exact same set of pointed temporal graphs as yp.
B.4 Proof of Theorem 9
Theorem 9. L1 S TrandG [an
The proof follows a similar line of reasoning as our previous results, notably the arguments presented in the proof of Theorem 66 Let yp be formula of the fragment Li and let .i..... . where yp E sub(s;;) implies S j. Specifically, we have y = 4p
Proof.
Let T = (M1, M2, Cell, out), where out(z1,.... .2n) = trReLU(Z,)) The components M1, M2. and Cell are constructed as outlined below. Mj and My consist of layers 1(0) and 110) respectively. In
the case of M1 we include layer (10) that maps vector æ E {0, 10 to x || 0 E {0, 10 t x x(0}"-m and in the case of M2 we include a layer 120) that maps vector æ E f0, 1) 2n 0 x E f0)" x 1).
Each layer 1/5) with E {1,2) is represented by (comb,) (1) E), where Σ means entrywise sum as aggregation and comb, (6) (xx, y) trReLU(C,a: A,y + by), where C1, A1 E (0. 1)xx" by E {0, 10" and C22 A2 E {0. 10,1133x00 33xx3n b2 {0,1)3m The function Cell is represented by an FNN Neal of input dimensionality 3n and output dimensionality 2n. The entries of Cj. Aj. bj with jE E (1,2), and the exact form of Neelt are determined by the enumeration of the subformulas Pt- We distinguish three cases, depending on the nature of pp:
Firstly, let ii be such that there is no subformula Qe sub((p;) with Q E PY, In this case, set the parameters of C1. A1, and b, based on μi as shown in the proof of Theorem 6 Informally, this means the semantics of (o; checked by M1.
Secondly, consider io; where for every subformula e E sub((p)). there exists Q E sub(ip:) with Q E (Y, PJ such that E sub) We configure the parameters C2, A2, and b2 based on yo following the procedure described in the proof of Theorem However, for yp; = Yup,, we use input dimension n + j. and for yo; Pypj. we use 2n + j. We also add final layer to M2, which maps vectors 31 22 Ø3. where Vy E {0, 13",, to x1 Ø33-
Thirdly. formulas sp; that do not belong to the first or second category are handled by .oeu of input dimensionality 3n and output dimensionality 2n. The definition of the fragment L1 ensures that s = my Pp; = th A 122. We refer to works such as (36). which demonstrate how to construct single-layer FNNs to check Boolean conditions. Besides processing these pi, the FNN Ncel maps input x; corresponding to p; of the first category by using the identity (simply realised by trReL (z)) to output yı and input zitti corresponding to yp, from the second category are mapped identically to output y as well. Additionally, for each j < n,, we add a component that computes trReLU(ar + Intj + x2+ts) as the n + jth output, ensuring that all Pvb subformulas are correctly processed.
18

---

Regarding correctness, the argument follows the same inductive approach as in Theorem 6 To avoid repetition, we provide a high-level outline here. Concerning the MPNN M,, it immediately implied by the construction of Theorem 6 that it functions as expected, meaning that it correctly captures the semantics of fr: of the first category. This is due to the fact that only utilised to check formulas devoid of temporal operators. For M2, consider that at the initial timestamp 4, its inputs are pointed graphs ((V,, E1, Iu + 0]), v), where all labels G₁ are replaced by O. Since M2 only used to verify formulas concerning past timepoints, the base case is correct. Otherwise, the inputs for M2 are ((V,, E,, [u + (4;-))] }]), v), where ha (ti-1) denotes the output of Cell for node at the previous timestamp. Here, our construction ensures that (t,-1) (t.-1) || (t, 1). where hy (t,-1) E {0, 13" contains the semantics of each subformula (P; at timestamp 4-11 and (t;-1)) E 1)" contains semantics of each subformula (a,, disjunctively combined over all t, with j 1-1 Due to the way L1 is defined, these are the necessary informations to compute the semanties of P; of the second category timepoint t,. Finally, New uses the outputs of M, and M2 compute the semantics of the remaining subformulas. Due to the way the fragment Li is defined, these can not be of the form Qrb, which N Cell could not handle, Q with Q E {Y,P), P). which are already handled by M2. This leaves only Boolean formulas. Otherwise, N Nelll ensures consistency and, thus, produces the output h, h,,(t) (t+) I| [1.((tt)) where (t4 E {0, 1}" contains the semantics of all subformulas of yp timepoint t; and (t,) (0, 1)" contains semantics of all subformulas, disjunctively combined over all t, with j & i. Finally, the output function out (I1...., .2n)) = trReLU(z,, ensures that T
outputs the semantics of Pn 4.
B.5 Proof of Theorem 10
G2
t1
(TG,
(TG', (')
Figure 4: Pointed temporal graphs (TG, v) and (T'", both including two snapshots, used as an counterexample in the proof of Theorem TO Here, colour o₁ is denoted by red filling (applies for node in G1, G2 and node e' in G)2).
Theorem 10. PTLp.y 1 Tglab|M Q, for all M, Q, and o.
Proof. Let p= Ycı. is evident that y is satisfied by all pointed temporal graphs (TG, v) of length such that was of colour at timestamp tj.
Consider the two pointed temporal graphs (TG, v) and (TG', e²), as specified by Figure 4 It is clear that (TG,)) v) + yp and (TG', v') + s.. Now, let T E TTgool/ Q, of for some M, Q, and o.
The argument is simple: We have A (t2 = 1 (t2) in the respective computation of T v) and T(TG', v'), and the input to agg the empty set in both cases, meaning that its output is in both cases. Thus, as T either accepts both or none of the temporal graphs (TG, v) and (TG', o'), meaning that it does not accept the exact of temporal graphs that satisfy sp.
B.6 Proof of Theorem [1
In the following result, we utilise time2vec functions 22 in the constructed TGNN. formal definition can be found in Appendix(A) We remark that in the following result we exclusively utilise the (-th element of t2v functions <h indicating that the result is independent of the exact form of activation used in these functions.
Theorem 11. La I Toioo Mmsgg QtimeZvec: [|].
19

---

Proof. Let E L2 and let
PI..... (m: fm Pm+1:...::p
be an enumeration of the subformulas of y such that all atomic formulas are the , Pm and Pi E sub(pp) implies i S j. In particular, we consider an enumeration such that (nn = 4.
The global (in time) TGNN T' (M, o, out) E Tglob Mmag, Qtime2vec; [I]. where ái is some t2v function with Wy 1,
0, meaning the O-th element is the identity, and out(21...... (2n)) (r We note that M _Mmsg which means that aggregation given by Σ (x). where msg is realised by some one layer FÑN Nmsg with
activation. The MPNN M is
build such that for each (o there is layer ( in the same manner done in Theorem 6 However, each layer has input dimension n and output dimension n, which stands in contrast to previous constructions. This is due the fact that, the semantics previous or past timestamps respected via aggregation. This works as follows.
Assume that ye Boolean. Then, is handled layer (0) exactly as shown in the proof of Theorem In the case of 9o; = Qtù with Q {Y,P), P), due to the way L2 is defined, these subformulas must occur in form of Q For modal subformulas O we therefore distinguish three cases, namely that Y0 POPj, or something else. In the case that YoPj.. we build msg, represented by N Nmsg. such that it maps dimension j identically if ())) - 1; otherwise, maps dimension j to In the case POyjj we build Nosg such that maps dimension j identically if (()) < 11; otherwise, it maps dimension j to O. In the third case, we build Nmsg such that it maps dimension j identically if Φ(() O: otherwise, it maps dimension j to O. We remark that this involves simple FNN constructions as done in other studies such as [36]. Informally, the way we construct N Nmsg is to filter the correct temporal information. Otherwise, O is handled as seen in Theorem 6
Correctness is again shown via induction over time and subformulae. The key insight here is that, while we do not directly evaluate formulas of the form Q² with Q E LY,P), the definition of La ensures that such formulas are the form Q Regarding Qo the interactions between ø and msg ensure that only the information from the previous (in the case of Q Y) or all previous (in the case Q = P) timepoints is considered in the aggregation. Other than this, the arguments are the same as in Theorem e
20

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
The claims made in the abstract and introduction are covered by our core results. The detailed results outlined in the "Our contribution." subsection of the introduction.
Justification:
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
It is fine to include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: See Section as well as remarks in the pre- posttext of specific results and definitions. This especially includes the fact that all models and logics are defined rigorously.
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or speech-to-text system might not be used reliably provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't acknowledged
the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
21

---

Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
Justification: For each result, we included proof sketch in the main body and full proof in the appendix. Furthermore, we defined each model and framework rigorously.
Guidelines:
The answer NA means that the paper does not include theoretical results. All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, a No answer to this question will not perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to model. In general. releasing code and data often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
specific model and empirical evaluation, may
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (c.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
22

---

5. Open access to data and code
Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, described in supplemental material?
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips.co
for more details.
While encourage the release of code and data, understand that this might not be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https for more details.
7 //nips.
The authors should provide instructions data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
23

---

The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
should be clear whether the error bar is the standard deviation or the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables figures symmetric error bars that would yield results that are out range (c.g. negative emror rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't 't make it into the paper).
9. Code ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics htttps/s/horris...cpppptt///tei
Answer: [Yes]
Justification:
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.

---

The conference expects that many papers will be foundational research and not tied particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms monitor how system learns from feedback over time, improving the efficiency and accessibility of MI..
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Lieenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper. properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (c.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode. com com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
25

---

If this information is not available online, the authors are encouraged to reach out to the asset's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/mmoel as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question:
Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
16. Declaration of LLM usage
26

---

Does the paper describe the usage of LLMs if it is important, original, or non-standard component of the core methods this research? Note that if the LLM used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs any important, original, non-standard components.
Please refer to our LLM policy for what should or should not be described.
27


Reviews:
[{"review_id": "88rkgbQk7t", "reviewer": "Reviewer_v7Dk", "summary": "This paper investigates the expressive power of Temporal Graph Neural Networks (TGNNs) using two-dimensional product logics, which combine temporal and modal logics. The authors characterize the logical expressiveness of three classes of TGNNs—recursive, time-and-graph, and global TGNNs—by connecting them to fragments of these logics. They show that recursive TGNNs can express all properties definable in the product logic, while time-and-graph and global TGNNs are limited to specific fragments due to constraints on how temporal and spatial operators interact. These results provide foundational insights into the capabilities of different TGNN architectures and establish relative expressiveness relationships between them.", "questions": "1. How can the proposed method be extended to provide edge-specific or global confidence scores to enhance interpretability?\n2. What is the time complexity (or computational cost) of extracting logical rules from a TGNN?", "limitations": "The discussion on limitations, while present, could be more detailed, particularly regarding the assumptions and their impact on real-world applications.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "## Strengths\n\n1. The paper presents a novel and rigorous logical characterization of temporal graph neural networks (TGNNs) using two-dimensional product logics, effectively bridging a gap in the literature.\n2. The theoretical results are well-supported by detailed proofs and clearly defined concepts, enhancing the paper’s credibility and rigor.\n3. The work provides practical insights into the expressive power of different TGNN architectures, which could inform model selection for specific tasks.\n\n## Weaknesses\n\n1. The proposed method can derive logical interpretations for TGNNs but does not provide edge-specific or global weights (e.g., confidence scores), limiting interpretability at a granular level.\n2. The paper lacks empirical validation, which could have strengthened the practical applicability of its theoretical findings.mpirical validation, which could have strengthened the practical relevance of the theoretical findings.\n3. The technical complexity of the proofs and logical frameworks might limit accessibility for readers without a strong background in formal logics.", "was_revised": true, "final_justification": "Thank you to the authors for providing discussions on several issues in the rebuttal. I believe these directions are worth further exploration in future work. However, as these discussions do not affect my evaluation of the paper, I have decided to maintain my rating.", "rebuttal": "Thank you for taking the time to review our paper. We will focus on addressing your specific questions. \n\n--- \n\n> How can the proposed method be extended to provide edge-specific or global confidence scores to enhance interpretability? \n\nYou are correct that our proposed method aims not only to characterise the expressive capabilities of TGNNs, but also to pave the way for rigorous verification or interpretation methods based on logic. Combining interpretability methods, such as computing a global confidence score, with our approach of deriving logical characterisations seems to require connecting TGNNs with tailored \"less-classical\" logics, presumably those that include metric as well as probabilistic expressions.\n\nWe can see several interesting research directions that could address this: (i) focus on establishing further characterisations (other classical temporal logics, other TGNN models, etc.), (ii) investigate verification/interpretation methods based on these, such as extracting equivalent formulas from TGNNs as surrogates; and (iii, your idea!) then proceed to combine logics with existing interpretation methods.\n\n> What is the time complexity (or computational cost) of extracting logical rules from a TGNN?\n\nPlease notice that our proofs are constructive, as they provide algorithms for translating one formalism into another. However, there is no guarantee that our algorithms are optimal. Establishing tight computational complexity of translations between GNNs and logics is a very interesting task indeed. However, it is challenging, and so far it has not been fully addressed even in the conceptualy simpler case of static GNNs.\n\nHowever, some results for static GNNs are known, and there is an ongoing research in this direction. Assume we are interested in finding a formula $\\varphi$ which exactly captures the classification of a static GNN $M$. Naive translations usually lead to an exponential size of $\\varphi$. See for example [1]. However, there are substantial efforts in finding subclasses of static GNNs or certain verification problems, for which the translation is polynomial (like in [2]) or where verification is manageable despite a high worst-case complexity, see [3]. Solving the problem for static GNNs seems to be essential to make a progress for TGNNS, but it is reasonable to assume that similar research will be soon addressed also for TGNNs. \n\nFurthermore, if we assume that the formula $\\varphi$ does not perfectly align with $M$ and only corresponds to it to a certain, but sufficient degree, then the time complexity might indeed be polynomial. This, however, is more related to approximation of one formalism with another, which we find as another very interesting direction!\n\n\n--- \n- [1] Michael Benedikt, Chia-Hsuan Lu, Boris Motik, Tony Tan:Decidability of Graph Neural Networks via Logical Characterizations. ICALP 2024\n- [2] Pierre Nunn, Marco Sälzer, François Schwarzentruber, Nicolas Troquard:\nA Logic for Reasoning about Aggregate-Combine Graph Neural Networks. IJCAI 2024\n- [3] Marco Sälzer, François Schwarzentruber, Nicolas Troquard:\nVerifying Quantized Graph Neural Networks is PSPACE-complete. CoRR abs/2502.16244 (2025)"}, {"review_id": "ZeGdFaTbz5", "reviewer": "Reviewer_kogE", "summary": "In this paper, the authors study the expressiveness of temporal graph\nneural networks (TGNNs).\n\nA GNN is defined by a sequence of aggregation and combination\nfunctions that are applied to a graph G = (V, E, c), where c is a\nfunction that maps each vertex in V to a vector in R^k. A temporal\ngraph is defined as (G_1, t_1), (G_2, t_2), ..., (G_n, t_n), where\neach t_i is a timestamp and t_1 < t_2 < ... < t_n. Then, a TGNN is an\nextension of a GNN that takes as input a temporal graph (G_1, t_1),\n(G_2, t_2), ..., (G_n, t_n), processes each graph G_i as a GNN, but\nassigns to each node u in (G_{i+1}, t_{i+1}) a label that is defined\nas the concatenation of the label of u in G_{i+1} with the resulting\nlabel from the execution on G_i.\n\nThe paper considers different classes of TGNNs, with the class of\nrecursive TGNNs being the most expressive. To study the expressiveness\nof these classes, the paper considers different product logics, the\nmost expressive being defined as the product of path temporal logic\nPTL_{P,Y}, with operators \"yesterday\" (Y) and \"sometime in the past\"\n(P), with the modal logic K. Then, the authors prove that each formula\nin PTL_{P,Y} × K can be expressed by a recursive TGNN. Moreover, the\nauthors consider less expressive TGNNs and identify fragments of\nPTL_{P,Y} × K that are and are not contained in them. As a corollary\nof these results, they provide separations in terms of expressive\npower between the different classes of TGNNs considered in the paper.", "questions": "Q1 What are the complexities of the translations presented in the\npaper? This information is important, for example, to determine\nwhether a TGNN is exponentially more succinct than a product logic.", "limitations": "Yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\nS1 Understanding the expressive power of a TGNN is a fundamental\nproblem. In particular, understanding what cannot be expressed by a\nclass of TGNNs helps to understand not only the limitations of such an\narchitecture but also to identify what needs to be added to the\narchitecture to increase its expressive power.\n\nS2 The paper provides some non-trivial results about the\nexpressiveness of some classes of TGNNs, which help in understanding\nthe expressiveness of these classes.\n\nWeaknesses:\n\nW1 The inexpressibility results presented in the paper are\ninteresting, as they help us understand what a class of TGNNs cannot\nexpress. However, the authors do not make an effort to explain such\ninexpressibility results in a way that the reader can clearly\nunderstand the limitations of a class of TGNNs.\n\nW2 The paper does not provide convincing evidence that product logics\nare the right formalism to study the expressive power of TGNNs. In\nparticular, they do not clearly explain why the expressiveness of\nTGNNs cannot be studied in terms of temporal extensions of first-order\nlogic.\n\nW3 The paper does not identify any logic that exactly captures the\nexpressive power of any of the classes of TGNNs studied. Notice that\nthis has been done for (non-temporal) GNNs.", "was_revised": true, "final_justification": "The answer of the authors is only partially satisfactory, in particular as they do not comment on the fact that the paper does not identify any logic that exactly captures the expressive power of any of the classes of TGNNs studied. I keep my score.", "rebuttal": "Thank you for dedicating your time to providing a review of our paper. We focus addressing your direct question. \n\n----\n\n> What are the complexities of the translations presented in the paper? This information is important, for example, to determine whether a TGNN is exponentially more succinct than a product logic.\n\nYou are absolutely right that it is an interesting information to include in the paper. Please notice that all our translations are constructive and, thus, open to analyse their complexity. \n\nIn particular, it is given that all of them are feasible in polynomial time. Indeed, all of our translations are based on enumeration of all (linearly many) subformulas of the formula to be translated, and then creating a single layer of a TGNN (or of its MPNN component, to be more specific) per subformula. This leads to a polynomial time procedure.\n\nThank you for this comment! We will ensure to clarify and emphasise it in the revised version of the paper. We are certain that this observation will strengthen our results indeed."}, {"review_id": "ohKJpyRv8a", "reviewer": "Reviewer_PQun", "summary": "The paper presents an expressivity investigations for a temporal extension of Graph Neural Networks (GNN) hereinafter referred to as TGNNs. Instead of simply dealing with the topology of a graph as in GNNs, the model adds a temporal dimension considering a sequence of graphs marked by a timestamp. The paper recall the definition of GNN and then presents three different ways of extending their semantics to the temporal dimension given rise to the three classes of Recursive TGNNs, Time-and-graph TGNNs and Global TGNNs. The different way for including the temporal information (basically the way the embeddings on previous graphs are used to fix the embedding in the following ones) affects the expressiveness of corresponding classes. Following an idea  already successfully adopted in the literature for GNNs the expressiveness is compared by using a logical approach: which properties (expressed by a suitable logic) can be recognized by the considered class. In particular the logic exploited in the paper is a suitable product combination of a standard Past Linear Time Logic (for the temporal dimension) and the K logic (but also a fragment of CTL would suit as well) for the spatial dimension. The main result is that the logic is subsumed by Recursive TGNNs but not by Time-and-graph TGNNs and Global TGNNs. In addition, for by Time-and-graph TGNNs and Global TGNNs, the paper propose fragments of the product logic which are respectively subsumed.", "questions": "Page 3. Definition of Temporal Graph. The sequence of graphs in a temporal graph shares the same set of nodes. No constraint is required on the set of edges admitting different structures over the same set of nodes. Authors should spend some word on this point.\nThe logic K used in combination with PLTL allows only to express a modality for neighborhood. What would be the effects if a modality for reachability were considered (something like EF in CTL)?\nThe weakness of Global TGNNs seems to be the fact that they are not able to focus on specific instants or intervals on the past. Is there any significant class able to interact in more selective way with the past (not only the immediately preceding instant)?", "limitations": "yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strength.  From the theoretical viewpoint, the paper focus on a relevant and interesting topic extending the expressiveness investigation on the temporal aspects of Timed GNN. The investigation provides an initial picture on the topic. Some aspects in the adopted technique are original (e.g. the adoption of the product logic). The technical machinery is appropriate and seems to be sound. The paper is clearly written even if some technical definitions needed to understand the paper are confined to the appendix.\nWeakeness. Some results seems to immediately derive from corresponding results of the untimed case (e.g. Theorem 2 concerning presburger quantification). Quoting from the abstract: “These results  yields the first logical characterizations of temporal GNNs”.  Usually to have a “characterization” one has to prove that two formalisms are equivalent in some sense, so that claim should be removed. The correct claim is that stated by the title. If there had been a technical characterization the results would have assumed a much greater theoretical significance. The authors should explain more convincingly the usefulness of the temporal dimension.", "was_revised": true, "final_justification": "I thank  the authors for their detailed discussions in the rebuttal. Indeed, there are some interesting future work directions opening up. As these discussions do not affect my evaluation of the paper, I will keep my score.", "rebuttal": "Thank you for taking the time to thoroughly review our paper and posing the insightful questions that we address below. We focus on responding to your specific queries below.\n\n--- \n\n> Definition of Temporal Graph. The sequence of graphs in a temporal graph shares the same set of nodes. No constraint is required on the set of edges admitting different structures over the same set of nodes. Authors should spend some word on this point. \n\nWe will add a clarification of these assumptions in the revised version of the paper. We appreciate your attention to this matter!\n\n\n> The logic K used in combination with PLTL allows only to express a modality for neighborhood. What would be the effects if a modality for reachability were considered (something like EF in CTL)? \n\nInteresting point! Our study focuses on TGNNs, where the static graphs or snapshots of a temporal graph are processed by message-passing neural networks (MPNNs). In their standard, local-only form, these can only access the local neighbourhood of a node (the size of which depends on the depth of the MPNN). Thus, the exact classes of TGNNs we considered cannot capture modalities that express reachability.\n\nTo capture \"reachability\", these MPNN components must somehow be able to access global information. This could be achieved by using recursive MPNN components, which have no fixed depth, or to some degree by MPNN components that allow for global access, sometimes referred to as global aggregation or global readout. Both kinds of MPNN exist (see [1, 2]), but are to the best of our knowledge not yet considered in the context of TGNNs. Similarly, a large part of TGNNs do not use MPNN-esque components to process static or temporal aspects of temporal graphs, but use attention mechanisms (see, for example, [3]). These may also capture modalities requiring global information.\n\n\n>The weakness of Global TGNNs seems to be the fact that they are not able to focus on specific instants or intervals on the past. Is there any significant class able to interact in more selective way with the past (not only the immediately preceding instant)?\n\nYour questions address the core challenge of navigating the TGNN landscape: it can be quite difficult to discern which models exist and how they differ in their capabilities. (To tackle this problem, we propose this study as a starting point to understand these differences with formal rigour.)\n\nRegarding global TGNNs, we note that certain types may indeed be capable of doing exactly what you are asking for. This necessitates that the way temporal information is combined with label information (in our paper realised by the $\\circ$ operation and time function $\\phi$) allows for Boolean-esque capabilities. Specifically, all label information corresponding to timepoints outside the interval we are interested in should be \"ignored\". In typical MPNN components, this is equivalent to mapping them to the all-zero vector, since aggregation is usually performed via summation. However, this assumes very specific conditions regarding the instantiation of the class of global TGNNs, namely $\\circ$ and $\\phi$, and it remains to be seen whether these conditions occur naturally in training processes. Nevertheless, these kinds of architectures generally permit the capabilities you are asking about.\n\n\n\n--- \n- [1] Veeti Ahvonen, Damian Heiman, Antti Kuusisto, Carsten Lutz:\nLogical characterizations of recurrent graph neural networks with reals and floats. NeurIPS 2024\n- [2] Michael Benedikt, Chia-Hsuan Lu, Boris Motik, Tony Tan:Decidability of Graph Neural Networks via Logical Characterizations. ICALP 2024\n- [3] Emanuele Rossi, Ben Chamberlain, Fabrizio Frasca, Davide Eynard, Federico Monti, Michael M. Bronstein:\nTemporal Graph Networks for Deep Learning on Dynamic Graphs. CoRR abs/2006.10637 (2020)"}, {"review_id": "3eK3g6oN70", "reviewer": "Reviewer_Hkih", "summary": "This work proposes to use two-dimensional product logics to analyze the logical expressiveness of Temporal Graph Neural Networks (TGNNs).\nThe paper analyzes the expressiveness of three types of TGNNs: recursive, time-and-graph, and global TGNNs, using two types of logic: propositional temporal logic (PTL) and modal logic (K).\nTheoretical results show that recursive TGNNs can express at least $PTL_{P,Y}\\times K$, and that time-and-graph and global TGNNs can express fragments of $PTL_{P,Y}\\times K$.", "questions": "- How could the theoretical results be utilized in practice? For example, could they be used to design more expressive TGNNs?\n- Is there a reason for the use of truncated ReLU? I imagine those are not used in practice, and other activation functions such as sigmoid would be more common.\n- Why do you only consider the operators $P$ and $Y$? Are there other past-time temporal logic operators that you could consider, such as ``always in the past''?\n- More background details regarding some parts of the paper would be helpful, such as K^{\\#} and time2vec.  While I understand they are given in the appendix, it would greatly help the readability of the paper if some details were included in the main text.", "limitations": "yes", "rating": 4, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths: \n- The paper is the first to analyze the logical expressiveness of TGNNs using two-dimensional product logics.\n- The paper has strong theoretical results, showing which TGNNs can express what type of logic.\n- Overall, the paper is well-written and easy to follow.\n\nWeaknesses: \n- The discussion on how the theoretical results could be utilized in practice is limited, despite the paper not including any experimental results.\n- Reasoning behind the use of $PTL_{P,Y}$ is not stated clearly.", "was_revised": true, "final_justification": "I appreciate the authors' response to the review.  \nI understand that this is a theory paper, but still have an impression that it is rather limited due to the lack of experimental progress.  I have already put a rather (weakly) positive score, which I feel is appropriate.", "rebuttal": "Thank you for thoroughly reviewing our paper and posing several questions, which we happily address below. We focus on responding to the questions you asked. \n\n--- \n\n> How could the theoretical results be utilized in practice? For example, could they be used to design more expressive TGNNs?\n\nExactly! We highlight three key uses of our research in practice:\n\n1. It guides model selection, as some TGNN architectures are by design better suited for certain tasks than others.\n2. Understanding the limitations of existing TGNN architectures, as initiated with our study, guides the design of more expressive types. However, practitioners must determine which capabilities are desirable.\n3. Connecting TGNNs with logic paves the way for formal verification and interpretation of these models, for example, by extracting logical formulas from them.\n\nHowever, you're right that we could emphasise these key contributions even more. We plan to do so in the overview section of our results in a potential final version.\n\n> Is there a reason for the use of truncated ReLU? I imagine those are not used in practice, and other activation functions such as sigmoid would be more common.\n\nPlease notice that all our established results also hold for the standard ReLU, as these can replicate the behaviour of truncated ReLU with only a linear increase in complexity.\n\nWe have focused on truncated ReLU primarily to simplify proofs. Just as a sidenote: that it is a standard approach in papers relating the expressive power of GNNs with logics as those we considered as related work. \n\n> Why do you only consider the operators P and Y? Are there other past-time temporal logic operators that you could consider, such as ``always in the past''?\n\nThank you for this comment! Actually our results apply also to \"always in the past\" operator.\n\nThis is because \"always in the past'' is expressible using negation and operator P. In particular, \"always in the past $\\varphi$'' is equivalent to: $\\neg P \\neg \\varphi$. For simplicity of presentation and to make proofs easier (less operators to consider), we used the common approach to not include temporal operators which can expressed using combination of others.\n\nPlease observe that for the same reason our presentation of the modal logic K mentions only $\\Diamond$ among modal operators. However, the logic also allows to express the dual opeator $\\Box\\varphi$, as it is expressible as $\\neg \\Diamond \\neg \\varphi$.\n\nWe will emphasise the above in the paper, which we believe can strengthen our results. Thank you for that!\n\n\n> More background details regarding some parts of the paper would be helpful, such as K^{#} and time2vec. While I understand they are given in the appendix, it would greatly help the readability of the paper if some details were included in the main text.\n\nThank you for the comment. Limited amount of space requires moving some parts to the appendix, and it is the only reason why we have not provided full description of the above mentioned. We aim for a better explanation / intuitions about them in the revised version of the paper, especially Section 5."}]

Author rebuttal:

Meta-review: (a) Summary of scientific claims and findings

This paper studies the expressive power of temporal graph neural networks (TGNNs) by connecting them to two-dimensional product logics, combining propositional temporal logic (PTL) and modal logic K. The main result is that recursive TGNNs can capture all properties definable in PTL × K, while other classes such as time-and-graph TGNNs and global TGNNs are limited to syntactically constrained fragments. This provides the first logical characterizations of TGNNs and clarifies their relative expressiveness.

(b) Strengths

- Provides a rigorous and novel theoretical framework linking TGNNs to product logics.
- Establishes clear separations in expressive power between different TGNN architectures.
- Proofs are constructive, with translations running in polynomial time.
- Potentially useful for guiding model selection, architecture design, and verification.

(c) Weaknesses

- No empirical validation or experiments, limiting the practical impact for applied audiences.
- Some results (e.g., fragments derivable from static GNN expressiveness) could be seen as incremental extensions.

(d) Reasons for decision

I recommend acceptance as a poster. The theoretical contribution is sound, original, and relevant to the NeurIPS theory community. The paper advances our understanding of TGNN expressiveness, and while not groundbreaking enough for a spotlight or oral (due to lack of experiments, incremental nature of some parts, and partial scope), it is nonetheless a meaningful and rigorous step in an emerging area.

(e) Discussion and rebuttal period

During the discussion, reviewers raised concerns about interpretability extensions, computational complexity, the choice of formalism, missing exact characterizations, assumptions on temporal graphs, and practical relevance of the results. The authors clarified that their translations are constructive and polynomial time, explained architectural limitations tied to reachability, justified operator and activation choices, and outlined how their work connects to verification and model design. While the rebuttal effectively addressed technical questions, broader conceptual and scope-related concerns remained. Overall, reviewers converged on borderline positive evaluations, and the paper is judged solid enough for poster acceptance.
Decision: Accept (poster)