FO and MSO Model Checking on Temporal Graphs

Döring, Michelle; Enright, Jessica; Larios-Jones, Laura; Skretas, George

doi:10.4230/LIPIcs.SAND.2026.9

FO and MSO Model Checking on Temporal Graphs

Michelle Döring

Hasso Plattner Institute, University of Potsdam, Germany Jessica Enright

School of Computing Science, University of Glasgow, UK Laura Larios-Jones

School of Computing Science, University of Glasgow, UK George Skretas

Hasso Plattner Institute, University of Potsdam, Germany

Abstract

Algorithmic meta-theorems provide an important tool for showing tractability of graph problems on graph classes defined by structural restrictions. While such results are well established for static graphs, corresponding frameworks for temporal graphs are comparatively limited.

In this work, we revisit past applications of logical meta-theorems to temporal graphs and develop an extended unifying logical framework. Our first contribution is the introduction of logical encodings for the parameters vertex-interval-membership width ( $\mathsf{vim}$ ) and tree-interval-membership width ( $\mathsf{tim}$ ), parameters that capture the signature of vertex and component activity over time. Building on this, we extend existing monadic second-order (MSO) meta-theorems for bounded lifetime and temporal total degree to the parameters $\mathsf{vim}$ and $\mathsf{tim}$ , and establish novel first-order (FO) meta-theorems for all four parameters.

Finally, we signpost a modular lexicon of reusable FO and MSO formulas for a broad range of temporal graph problems, and give an example. This lexicon allows new problems to be expressed compositionally and directly yields fixed-parameter tractability results across the four parameters we consider.

Keywords and phrases:

temporal graphs, dynamic graphs, time-varying graphs, parameterized complexity, logic, meta-theorems, monadic second-order logic, first-order logic, treewidth, planar, nowhere dense, lifetime, temporal total degree, vertex-interval membership width, tree-interval membership width

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic ; Mathematics of computing

\rightarrow

Graph algorithms ; Theory of computation

\rightarrow

Fixed parameter tractability

Acknowledgements:

We thank Sebastian Siebertz for his valuable feedback.

DOI:

10.4230/LIPIcs.SAND.2026.9

Event:

5th Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2026)

Editors:

George B. Mertzios and Andréa W. Richa

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Many networks of interest, such as public-transport systems or communication and interaction networks, consist of time-sensitive connections. A standard abstraction of such networks is a temporal graph $\mathcal{G}=(V,E,\lambda)$ , that is, a static graph $G=(V,E)$ as footprint together with an edge labelling $\lambda\colon E\rightarrow 2^{\mathbb{N}}$ assigning to each edge the time steps at which it is available. This model strictly generalises static graphs, which are recovered as the special case in which all edges are available at all times. While temporal graphs are more expressive, this comes at a computational costs: many problems that are polynomial-time solvable on static graphs are computationally hard on temporal graphs (see e. g., the survey [24, Section 3]), motivating an extensive line of work in parameterised complexity (e. g., [33, 22, 6, 23, 35]).

The core question in parameterised complexity is whether a problem is fixed-parameter tractable ( $\mathtt{FPT}$ ) when parameterised by some measure that captures relevant properties of the input. For static graphs, one of the most studied parameters is treewidth ( $\mathsf{tw}$ ). Two standard approaches to obtain $\mathtt{FPT}$ algorithms parameterised by treewidth are: (i) developing a dynamic program (see [11, Section 7.3]), or (ii) expressing the problem in a suitable logic and applying a logical meta-theorem.

First-order (FO) logic and monadic-second order (MSO) logic provide formal languages that can be used for expressing combinatorial problems on graphs. A key benefit of this logical perspective is that it allows for logical meta-theorems which unify algorithmic results by establishing tractability for entire classes of problems on entire classes of graphs, often based on the fragment of logic required. The most prominent example is Courcelle’s theorem [9], which implies that every property definable in MSO logic can be decided in linear time on graphs of bounded treewidth. On sparse graphs, FO model checking has a long history on increasingly general graph classes, culminating in the result of Grohe, Kreutzer, and Siebertz [26] showing that FO model checking is fixed-parameter tractable on nowhere dense graph classes – a broad notion of sparsity that, in particular, includes planar graphs and graph classes of bounded treewidth, degree, or expansion. For a detailed background on logic and algorithmic meta-theorems we refer to the surveys [25, 30].

For temporal graphs, applications of logical meta-theorems so far exclusively use MSO formulations to obtain $\mathtt{FPT}$ results under bounded treewidth combined with lifetime (largest time label) or temporal degree (number of temporal edges incident to one vertex) [12, 13, 20, 21, 24, 27, 31, 35]. In contrast, the FO meta-theorem route on planar or nowhere dense graphs has not yet been considered for temporal graphs. Moreover, it is still common to obtain $\mathtt{FPT}$ results via problem-specific dynamic programs with long technical proofs (see, e.g., [8, 28]), even in settings where a logical approach could yield a simpler and more modular proof. Here, we provide a unifying framework for encoding temporal graphs along with example associated formulas. We also extend existing applications of logical meta-theorems to temporal graphs beyond bounded treewidth by enabling applications of FO meta-theorems for nowhere-dense footprints.

Beyond proof techniques, a central question is which parameters meaningfully capture temporal and structural complexity. Recently, two new parameters have been introduced that are sensitive to the order of snapshots and thus capture temporal structure more intrinsically: vertex-interval-membership width ( $\mathsf{vim}$ ) by Bumpus and Meeks [3], and tree-interval-membership width ( $\mathsf{tim}$ ) by Enright, Hand, Larios-Jones and Meeks [19]. The latter work studies parameterised complexity with respect to $\mathsf{vim}$ and $\mathsf{tim}$ , and proposes a general procedure for deriving dynamic programs. Concretely, any problem satisfying certain locality properties admits a dynamic program on graphs with bounded $\mathsf{vim}$ , and under even more restrictive locality requirements on graphs with bounded $\mathsf{tim}$ . A drawback of their approach is that verifying the locality properties is quite involved for $\mathsf{vim}$ and becomes even more demanding for $\mathsf{tim}$ . Since bounded $\mathsf{vim}$ and $\mathsf{tim}$ imply bounded treewidth of the footprint, it is a question whether these parameters support logical meta-theorems as for $\mathsf{tw}+\Lambda$ and $\mathsf{tw}+\Delta^{t}$ . We answer this affirmatively: we show that $\mathsf{vim}$ and $\mathsf{tim}$ admit encodings within our framework that preserve the structure needed to apply FO and MSO meta-theorems, yielding the first such results for purely temporal parameters.

1.1 Our contribution

We provide a unifying framework including the pre-existing encodings for lifetime ( $\Lambda$ ) and temporal total degree ( $\Delta^{t}$ ), and introduce novel encodings for the parameters $\mathsf{vim}$ and $\mathsf{tim}$ . These encodings are given in Section 3.

In Section 4, we show that all four encodings admit the application of FO and MSO meta-theorems. Concretely, we analyse the Gaifman graph induced by each encoding and prove that its structure is bounded by the respective parameter. This allows us to lift the static meta-theorems to temporal graphs, yielding the following temporal meta-theorems: any property expressible in FO/MSO logic over the corresponding encoding yields an $\mathtt{FPT}$ algorithm parameterised by the respective parameter.

Theorem 1.

MSO Model Checking on a temporal graph $\mathcal{G}=(G,\lambda)$ is $\mathtt{FPT}$ when parameterised by (i) $\mathsf{tw}+\Lambda$ , (ii) $\mathsf{tw}+\Delta^{t}$ , (iii) $\mathsf{vim}$ , or (iv) $\mathsf{tim}$ .

Theorem 2.

FO Model Checking on a temporal graph $\mathcal{G}=(G,\lambda)$ is $\mathtt{FPT}$ when parameterised by (i) $\Lambda$ if the footprint $G$ is nowhere dense, (ii) $\Delta^{t}$ , (iii) $\mathsf{vim}$ , or (iv) $\mathsf{tim}$ .

Finally, we provide the Logic Cookbook (see Section 5 in the full version): a collection of FO and MSO formulas for over a dozen temporal graph problems studied in the literature. Besides serving as a reusable reference for future work, this section highlights the simplicity and modularity of this logical tool. For example, in each of [3, 7, 8, 19, 28], a substantial contribution is an $\mathtt{FPT}$ result proven via a specialised dynamic program and lengthy correctness arguments; in our cookbook, the same $\mathtt{FPT}$ result follows from a compact formula combined with the meta-theorem.

Some results and proofs are omitted due to space constraints and can be found in the full version of the paper.

1.2 Related Work

The first work in logic that bears resemblance to temporal graph encodings is by [1] who provided an alternative proof of Courcelle’s MSO meta-theorem and considered, in particular, edge-labelled static graphs. This perspective was later adopted by [35] to obtain an $\mathtt{FPT}$ algorithm for Temporal $(s,z)$ -Separator parameterised by $\mathsf{tw}+\Lambda$ , introducing what we call the lifetime encoding.

Independently, [32] studied different models of time-varying graphs (including temporal graphs) with bounded lifetime and proposed an encoding that was claimed to extend the MSO and FO meta-theorems of Courcelle and Frick–Grohe to this setting. However, their encoding contains a fundamental flaw, which was later identified and shown to be irreparable in the survey by [24]. That survey gives a comprehensive exploration of possible notions of treewidth for temporal graphs (since no singular temporal treewidth definition exists), discussing both the lifetime and degree encodings in detail. The degree encoding was introduced by [20]. They used it to show that Temporal Reachability Edge Deletion is in $\mathtt{FPT}$ with respect to $\mathsf{tw}$ , $\Delta^{t}$ and solution size combined.

Subsequent work that uses an MSO approach: [27] prove $\mathtt{FPT}$ by $\mathsf{tw}+\Lambda$ for Temporal Feedback Edge/Connection Set; [31] show $\mathtt{FPT}$ by $\mathsf{tw}+\Lambda$ for Temporal Reachability Dominating Set; [21] show $\mathtt{FPT}$ by $\mathsf{tw}+\Delta^{t}$ for Counting Temporal Paths via a counting variant of MSO; [13] show $\mathtt{FPT}$ by $\mathsf{tw}+\Lambda$ and by $\mathsf{tw}+\Delta^{t}$ for Open and Closed Temporal Connected Component; [33] use Courcelle-type reasoning over a static MSO formulation on the footprint for Temporal Graph Realization with Fixed Stretch; and [14] show $\mathtt{FPT}$ by $\mathsf{tw}$ plus maximum deadline $D$ for ReachFast using an MSO encoding which is similar to the lifetime encoding but tailored specifically to this label-shifting problem.

Concurrently to our work, [2] obtain MSO and restricted-FO meta-theorems for temporal graphs by encoding the static expansion graph $\mathcal{G}_{\rightarrow}$ as a relational structure, with treewidth and twin-width of $\mathcal{G}_{\rightarrow}$ as the respective parameters. They define a custom temporal logic ( $\mathsf{MSOT}_{2}$ , $\mathsf{FOT}_{1}^{\Delta}$ ) which can equivalently be defined as a relational encoding of the static expansion within our framework. They also study a local time-window variant (differentials), yielding meta-theorems parameterised by the maximum treewidth or twin-width over sliding windows. In the full version, we discuss in how their results fit into our framework.

2 Preliminaries

A temporal graph $\mathcal{G}=(V,E,\lambda)$ consists of a static graph $G=(V,E)$ , known as the footprint, and a labelling function $\lambda\colon E\rightarrow 2^{\mathbb{N}}$ assigning to every static edge $e$ a finite set of time labels $\lambda(e)$ . The largest value assigned by $\lambda$ is referred to as the lifetime $\Lambda$ . Alternatively, a temporal graph can be defined as a sequence $\mathcal{G}=\big(G_{t}=(V,E_{t})\big)_{t\in\Lambda}$ of static snapshots $G_{t}$ . A temporal graph is (un)directed if the footprint is (un)directed. A pair $(e,t)$ , where $e\in E$ and $t\in\lambda(e)$ , is a temporal edge with label $t$ . We denote the set of all temporal edges of $\mathcal{G}$ by $\mathcal{E}$ . A temporal path of length $\ell$ is a sequence of temporal edges $\langle{(e_{i},t_{i})}\rangle_{i\in[\ell]}$ where $\langle{e_{i}}\rangle$ forms a path in the footprint and the time labels $\langle{t_{i}}\rangle$ are non-decreasing. If the time labels are strictly increasing, the path is strict; otherwise, it is non-strict. If there is a temporal path from $u$ to $v$ , we say $u$ reaches $v$ . A temporal graph is temporally connected if for all $u,v\in V$ , $u$ reaches $v$ and vice versa. A temporal graph where reachability is considered exclusively using (non-)strict paths is called a (non-)strict temporal graph.¹¹1Formally, strictness is a property of the path model rather than of the temporal graph itself. We use this terminology, analogously to speaking of weighted or unit-weight static graphs, as a convention about the travel time of temporal edges: one in the strict case and zero in the non-strict case.

We distinguish two families of parameters for temporal graphs: static parameters, which constrain the structure of the (undirected) footprint, and temporal parameters, which bound the temporal structure locally or the activity over time. See Table 1 for an overview.

Static graph parameters.

The static degree of a vertex $v$ is defined as $\delta^{s}(v)=\lvert\{e\in E\colon v\in e\}\rvert$ and $\Delta^{s}=\max_{v\in V}\delta(v)$ denotes the maximum static degree of $\mathcal{G}$ . The treewidth of a graph measures how structurally close it is to being a tree. Small treewidth means that the graph can be organised into small, overlapping pieces with a tree-like skeleton. The treewidth of a temporal graph always refers to the undirected footprint; for directed temporal graphs we take the treewidth of the underlying undirected graph of the directed footprint.

Definition 3 (Tree Decomposition, Treewidth [11]).

Let $G=(V,E)$ be an undirected static graph. A tree decomposition of $G$ is a pair $\mathcal{T}=(T,\{B_{u}\colon u\in V(T)\})$ consisting of a tree $T$ and a family of bags $B_{u}\subseteq V$ such that (i) $\bigcup_{u\in V(T)}B_{u}=V$ , (ii) for every $e\in E$ there exists $u\in V(T)$ with $e\subseteq B_{u}$ , and (iii) for every $v\in V$ , the set $\{u\in V(T)\colon v\in B_{u}\}$ induces a connected subtree of $T$ . The width of $\mathcal{T}$ is defined as $width(\mathcal{T}):=\max_{u\in V(T)}\lvert B_{u}\rvert-1$ . The treewidth of a static graph $G$ is $\mathsf{tw}(G):=\min\{width(\mathcal{T})\colon\mathcal{T}\text{ is a tree % decomposition of }G\}$ .

A path decomposition is a tree decomposition in which the underlying tree $T$ is restricted to be a path; the pathwidth $\mathsf{pw}(G)$ is defined analogously as the minimum width over all path decompositions of $G$ . Since every path is a tree, we have $\mathsf{pw}(G)\geq\mathsf{tw}(G)$ for all graphs $G$ . A class of graphs has bounded treewidth (respectively bounded pathwidth) if there exists a constant $k$ such that every graph in the class satisfies $\mathsf{tw}(G)<k$ (resp. $\mathsf{pw}(G)<k$ ).

Table 1: Overview of the parameters considered in this paper.

Symbol	Name	Family	What it controls
$\Delta^{s}$	static degree	static	#static edges locally
$\mathsf{pw}$	pathwidth	static	footprint path-likeness
$\mathsf{tw}$	treewidth	static	footprint tree-likeness
$\mathsf{d}$	denseness function	static	sparsity measure
$\Lambda$	lifetime	temporal	largest time label
$\Delta^{t}$	temporal total degree	temporal	#temporal edges locally
$\mathsf{vim}$	vertex-interval membership width	temporal	#relevant vertices at a time
$\mathsf{tim}$	tree-interval membership width	temporal	#relevant vertices connected at a time

We use standard notions from topological minor theory; for details we refer to the book [34]. Two graphs $G$ and $H$ are isomorphic if there is a bijection between $V(G)$ and $V(H)$ that preserves adjacency. For $r\in\mathbb{N}$ , an $r$ -subdivision of $H$ is obtained by selecting an arbitrary subset of edges and replacing each edge of that set by a path of length at most $r+1$ such that all paths are pairwise internally vertex-disjoint. The graph $H$ is a depth- $r$ topological minor of $G$ , denoted $H\preceq^{t}_{r}G$ , if some $r$ -subdivision²²2The standard definition uses a $2r$ -subdivision. We drop the factor $2$ for notational simplicity; this only rescales the depth parameter by a constant factor and yields an equivalent notion. of $H$ is isomorphic to a subgraph of $G$ (the $t$ in $\preceq^{t}_{r}$ stands for topological and should not be confused with a time step $t\in[\Lambda]$ ). A graph class $\mathcal{C}$ is nowhere dense if there exists a function $\mathsf{d}\colon\mathbb{N}\Rightarrow\mathbb{N}$ such that for every $r\in\mathbb{N}$ and every $G\in\mathcal{C}$ we have $K_{\mathsf{d}(r)}\not\preceq^{t}_{r}G$ . We call $\mathsf{d}$ a denseness-function of $\mathcal{C}$ .

Temporal graph parameters.

The lifetime $\Lambda$ of a temporal graph is its largest time label. The temporal total degree of a vertex $v$ at time $t$ is defined as $\delta^{t}(v)=\lvert\{(e,t)\colon v\in e,\;t\in\lambda(e)\}\rvert$ and $\Delta^{t}=\max_{v\in V}\delta^{t}(v)$ denotes the maximum temporal total degree of $\mathcal{G}$ . The vertex-interval membership (VIM) width and tree-interval membership (TIM) width capture the maximum number of vertices that are simultaneously “participating” in the temporal graph. Both measures use the activity-interval of a vertex $v$ , which starts at the first time at which $v$ has an incident edge and ends after the last time at which $v$ has an incident edge. For every snapshot outside this interval, $v$ does not interact with the rest of the graph.

Definition 4 (Activity-interval).

For $v\in V$ , let $t_{min}(v)=\min\{\lambda(e)\colon e\in E,v\in e\}$ and $t_{max}(v)=\max\{\lambda(e)\colon e\in E,v\in e\}$ . The activity-interval of vertex $v$ is defined as $A(v)=\left[t_{min}(v),t_{max}(v)\right]$ and the activity-interval of a static edge $e\in E$ as $A(e)=\left[\min\lambda(e),\max\lambda(e)\right]$ . We say $v$ or $e$ is alive at time $t$ if $t\in A(v)$ or $t\in A(e)$ , respectively.

Note that an edge $e\in E$ can be alive at time $t$ without being active (i. e., $t\in A(e)$ and $t\notin\lambda(e)$ ), but not vice versa.

The VIM decomposition of a temporal graph consists of a path with one bag per time step containing exactly the vertices that are alive at that time. Note that every temporal graph has a unique VIM decomposition and that a temporally connected graph has VIM width exactly $n$ . See Figure 1 left for an illustration of a VIM decomposition.

Definition 5 (Vertex-Interval-Membership Width (Bumpus and Meeks [3])).

The vertex-interval-membership (VIM) decomposition of a temporal graph $\mathcal{G}$ is a sequence $(\pi_{t})_{t\in[\Lambda]}$ of bags with $\pi_{t}=\{v\in V:t\in A(v)\}$ . The vertex-interval-membership width of a temporal graph $\mathcal{G}$ is $\mathsf{vim}(\mathcal{G})=\max_{t\in[\Lambda]}\,\lvert\pi_{t}\rvert$ .

The TIM width parameter generalises VIM width from a decomposition as a path over time to a tree. This is motivated by the fact that for many temporal problems, vertices that are alive at the same time but far from one another in the graph can be considered independently. The bags of a TIM decomposition have the property that any connected component of a snapshot is entirely contained in a bag at that time. Each bag at time $t$ is connected to the bags at time $t-1$ and $t+1$ with which it shares vertices. This forms a tree-shape (see Figure 1 right). Since the complexity of computing a minimum-width TIM decomposition is unknown, we have a trade off between time required to decompose the temporal graph and size of the decomposition. For this reason, we discuss both parameters in this work despite similarities in the proofs for each.

Figure 1: Example from [19] of a VIM decomposition (A) and a TIM decomposition (B) of a temporal graph

\mathcal{G}

.

Definition 6 (Tree-Interval-Membership Width [19]).

A tree-interval-membership (TIM) decomposition of a temporal graph $\mathcal{G}$ is a triple $\mathcal{T}=(T,{\Pi},\tau)$ consisting of a labelled directed tree $T$ , a family of bags ${\Pi}=\{\pi_{i}\colon i\in V(T)\}$ , and a node labelling function $\tau\colon V(T)\Rightarrow[\Lambda]$ such that:

(i)

for every $v\in V(\mathcal{G})$ and $t\in[\Lambda]$ there exists a unique $i\in V(T)$ with $\tau(i)=t$ and $v\in\pi_{i}$ ,
(ii)

for every $(uv,t)\in\mathcal{E}(\mathcal{G})$ there exists an $i\in V(T)$ with $\tau(i)=t$ and $\{u,v\}\subseteq\pi_{i}$ , and
(iii)

the directed edges of $T$ are $E(T)=\{(i,j):\pi_{i}\cap\pi_{j}\neq\emptyset\text{ and }\tau(i)+1=\tau(j)\}$ .

The width of a TIM decomposition is defined as $width(T):=\max\{|\pi_{i}|\colon i\in V(T)\}$ . The TIM width of a temporal graph $\mathcal{G}$ is $\mathsf{tim}(\mathcal{G}):=\min\{width(\mathcal{T})\colon\mathcal{T}\text{ is % a TIM decomposition of }\mathcal{G}\}$ .

Since the VIM bags form a (not necessarily optimal) path decomposition of the undirected footprint, it follows that $\mathsf{pw}(\mathcal{G})\leq\mathsf{vim}(\mathcal{G})$ (and hence $\mathsf{tw}(\mathcal{G})\leq\mathsf{pw}(\mathcal{G})\leq\mathsf{vim}(\mathcal{% G})$ ). Analogously, the TIM bags form a tree decomposition of the undirected footprint, and thus $\mathsf{tw}(\mathcal{G})\leq\mathsf{tim}(\mathcal{G})$ .

2.1 Logic in Static Graphs

First-order (FO) logic and monadic second-order (MSO) logic provide a uniform language to express graph properties and, in turn, define whole graph classes. Since we only recall the basic notions needed in this paper, we point the reader to [30] as an accessible entry point with a focus on meta-theorems and a concise introduction to FO and MSO logic. For a more detailed treatment of FO and MSO logic, we refer to [10, 16, 17].

To reason about graphs using logic, each graph is represented as a relational structure: An undirected graph $G=(V,E)$ is encoded with universe $U:=V\cup E$ and an incidence relation $\mathsf{inc}\subseteq E\times V$ satisfying $\mathsf{inc}(uv,x)$ if and only if $x\in\{u,v\}$ . A directed graph $D=(V,A)$ is encoded with universe $U:=V\cup A$ and relations $\mathsf{source},\mathsf{target}\subseteq A\times V$ satisfying $\mathsf{source}((u,v),x)$ if and only if $x=u$ , and $\mathsf{target}((u,v),x)$ if and only if $x=v$ .

An FO formula $\varphi$ uses element variables $x,y,\dots$ ranging over the universe $U$ and builds formulas from atomic predicates $x=y$ or $R(x_{1},x_{2},\dots)$ via the logical connectives $\neg,\wedge,\vee,\Rightarrow,\Leftrightarrow$ , the existential quantifier $\exists$ , and the universal quantifier $\forall$ . An MSO formula is an FO formula which can additionally use set variables $X,Y,\dots\subseteq U$ , the membership relation $x\in X$ , and is allowed to quantify over sets.

A formula $\varphi$ is interpreted in a relational structure $\lfloor G\rfloor$ of a graph $G$ in the natural way: $=$ denotes equality of elements or sets, $R(x_{1},\dots,x_{k})$ denotes containment in the relation $R$ , $\in$ denotes set containment, and $\neg,\vee,\wedge,\Rightarrow,\Leftrightarrow$ denote negation, disjunction, conjunction, implication, and biimplication, respectively. Furthermore, $\exists x(\varphi(x))$ is true in $\lfloor G\rfloor$ if and only if there is an element in the universe $b\in U$ such that $\varphi$ is true in $\lfloor G\rfloor$ when $x$ is interpreted by $b$ . Analogously, $\forall x(\varphi(x))$ is true in $\lfloor G\rfloor$ if and only if $\varphi$ is true in $\lfloor G\rfloor$ for all interpretations of $x$ by elements $b\in U$ in the universe. For MSO formulas, $\exists X(\varphi(X))$ and $\forall X(\varphi(X))$ are analogously defined for sets $B\subseteq U$ by which $X$ is interpreted. A formula $\varphi$ is satisfied by a $G$ if $\varphi$ is true interpreted in $\lfloor G\rfloor$ . The algorithmic task of deciding whether a given graph satisfies a specific formula is the model checking problem.

Model Checking (MC)

Input:	A static graph $G$ and a logical formulas $\varphi$ .
Problem:	Does $G$ satisfy $\varphi$ ?

For FO and MSO there exist general meta-theorems that characterise the static graph classes on which their respective MC problem is tractable.

Theorem 7 (Grohe–Kreutzer–Siebertz: FO MC on nowhere dense [26]).

Let $\mathcal{C}$ be a graph class with denseness function $\mathsf{d}\colon\mathbb{N}\to\mathbb{N}$ , i.e., $K_{\mathsf{d}(r)}\not\preceq^{t}_{r}G$ for all $r\in\mathbb{N}$ and all $G\in\mathcal{C}$ . Then for every $\varepsilon>0$ there exists a computable function $f$ and a computable radius function $r(\cdot)$ such that, given a graph $G\in\mathcal{C}$ and an FO formula $\varphi$ , one can decide whether $G$ satifies $\varphi$ in time $f\bigl(|\varphi|,\varepsilon,\mathsf{d}(r(\varphi))\bigr)\cdot|V(G)|^{1+\varepsilon}$ .

Theorem 8 (Courcelle: MSO MC on bounded treewidth, [10]).

There exists a computable function $f$ such that, given a graph $G$ of treewidth $\mathsf{tw}$ and an MSO formula $\varphi$ , one can decide whether $G$ satisfies $\varphi$ in time $f(\lvert\varphi\rvert,\mathsf{tw})\cdot(|V|+|E|)$ .

3 Temporal Graph Encodings

To apply logical meta-theorems to temporal graphs, we encode them as relational structures resembling the static graph encoding with additional structure to represent time. Different encodings make different aspects of the temporal structure explicit and directly influence the structure of the resulting representation as well as the expressive power of any logic.

We present four relational encodings – two known (the lifetime encoding [27] and the degree encoding [20]) and two novel (the VIM and TIM encodings, introduced in this work) – each tailored to a specific notion of static or temporal sparsity. These encodings serve as the foundation for the temporal meta-theorems in Section 4, yielding tractability of FO and MSO model checking under bounded (i) $\Lambda$ , (ii) $\Delta^{t}$ , (iii) $\mathsf{vim}$ , and (iv) $\mathsf{tim}$ , possibly combined with static parameters. All encodings are presented for strict, undirected temporal graphs. Directed variants can be obtained by replacing the incidence relation with source and target relations. Non-strict reachability is obtained via adapting the successor relation in the degree encoding, or on the formula level for the lifetime, VIM, and TIM encoding.

The lifetime encoding represents a temporal graph as a time-labelled static graph, mirroring the standard mathematical definition. The universe contains the vertices, temporal edges, and time steps. An incidence relation identifies the endpoints of each temporal edge, while a presence relation records when a temporal edge is present. A total linear order on the time steps encodes the global timeline.

Definition 9 (lifetime encoding).

Let $\mathcal{G}=(V,\mathcal{E})$ be an undirected strict temporal graph with lifetime $\Lambda$ , and let $L:=[\Lambda]$ . The lifetime encoding $\lfloor\mathcal{G}\rfloor_{\Lambda}$ is the relational structure defined as:

universe $U=V\cup\mathcal{E}\cup L$

unary relations $V\subseteq U,\mathcal{E}\subseteq U,L\subseteq U$

binary relations

$\blacksquare$

$\mathsf{inc}\subseteq\mathcal{E}\times V$ where $\mathsf{inc}((uv,t),x)\Leftrightarrow x=u\text{ or }x=v$ ,
$\blacksquare$

$\mathsf{pres}\subseteq\mathcal{E}\times L$ where $\mathsf{pres}((uv,t),t^{\prime})\Leftrightarrow t^{\prime}=t$ ,
$\blacksquare$

$<^{T}\subseteq L\times L$ where $t_{1}<^{T}t_{2}\Leftrightarrow t_{1}<t_{2}$ .

Figure 2: Illustration of the lifetime encoding

\lfloor\mathcal{G}\rfloor_{\Lambda}

. Each temporal edge

(e,t)\in\mathcal{E}

between two vertices (empty circles) is represented by a temporal-edge node (filled circles), which is connected via the presence relation (orange) to the time-node

t\in L

for which

\varepsilon=(e,t)\in\mathcal{E}

. The total order

<^{T}

induces a clique

K_{\Lambda}

of size

\Lambda

.

Figure 3: Illustration of the degree encoding

\lfloor\mathcal{G}\rfloor_{\Delta^{t}}

. Each temporal edge

(e,t)\in\mathcal{E}

between two vertices (empty circles) is represented by a temporal-edge node (filled circles), which is connected via the possible-successor relation (orange) to every temporal-edge-node with whom it shares an endpoint and satisfies the temporal order.

The degree encoding abstracts away from the concrete time labels of edges and instead focuses on the relative order of neighbouring temporal edges. Rather than representing when an edge appears, the encoding captures which temporal edges can be taken consecutively along a temporal path. In contrast to static graphs – where succession is determined simply by shared endpoints – this relation additionally depends on the order at which the edges are present. As a result, the encoding directly represents temporal reachability via a partial order on temporal edges.

Definition 10 (degree encoding).

Let $\mathcal{G}=(V,\mathcal{E})$ be an undirected strict temporal graph with temporal total degree $\Delta^{t}$ . The degree encoding $\lfloor\mathcal{G}\rfloor_{\Delta^{t}}$ is the relational structure defined as:

universe $U=V\cup\mathcal{E}$

unary relations $V\subseteq U,\mathcal{E}\subseteq U$

binary relations

$\blacksquare$

$\mathsf{inc}\subseteq\mathcal{E}\times V$ , where $\mathsf{inc}((uv,t),x)\Leftrightarrow x=u\text{ or }x=v$ ,
$\blacksquare$

$\mathsf{psuc}\subseteq\mathcal{E}\times\mathcal{E}$ , where $\mathsf{psuc}((e_{1},t_{1}),(e_{2},t_{2}))\Leftrightarrow t_{1}<t_{2}$ and there
exists $v\in V$ such that $\mathsf{inc}(e_{1},v)$ and $\mathsf{inc}(e_{2},v)$ .

The VIM encoding directly represents the VIM decomposition of the temporal graph at the level of the relational structure. The encoding contains a sequence of bag elements, one for each bag of the VIM decomposition. Vertices and temporal edges are related to the bag elements in which they are alive, and successive bags are connected by a linear successor relation. In contrast to the lifetime encoding, the bags are not pairwise adjacent; this avoids introducing a clique over time and ensures that the density of the structure is bounded by the VIM width of the graph.

Definition 11 (VIM encoding).

Let $\mathcal{G}=(V,\mathcal{E})$ be an undirected strict temporal graph with VIM decomposition $(\pi_{t})_{t\in[\Lambda]}$ . The relational VIM structure $\lfloor\mathcal{G}\rfloor_{\mathsf{vim}}$ is defined as:

universe $U=V\cup\mathcal{E}\cup{\Pi}$

unary relations $V\subseteq U,\mathcal{E}\subseteq U,{\Pi}\subseteq U$

binary relations

$\blacksquare$

$\mathsf{inc}\subseteq\mathcal{E}\times V$ where $\mathsf{inc}((uv,t),x)\Leftrightarrow x=u\text{ or }x=v$ ,
$\blacksquare$

$\mathsf{bag}\subseteq V\times{\Pi}$ where $\mathsf{bag}(v,\pi_{t})\Leftrightarrow v\in\pi_{t}$ ,
$\blacksquare$

$\mathsf{pres}\subseteq\mathcal{E}\times{\Pi}$ where $\mathsf{pres}((uv,t),\pi_{i})\Leftrightarrow i=t\text{ and }u,v\in\pi_{i}$ ,
$\blacksquare$

$\mathsf{next}\subseteq{\Pi}\times{\Pi}$ where $\mathsf{next}(\pi_{i},\pi_{j})\Leftrightarrow i+1=j$ .

Figure 4: Illustration of the VIM encoding

\lfloor\mathcal{G}\rfloor_{\mathsf{vim}}

(left) and the TIM encoding

\lfloor\mathcal{G}\rfloor_{\mathsf{tim}}

(right). Each temporal edge

(e,t)\in\mathcal{E}

between two vertices (empty circles) is represented by a temporal-edge node (filled circles). Vertices are connected via the bag relation (solid blue) to every bag in which they are alive. Temporal-edge-nodes are connected analogously via the presence relation (dotted orange). The relation

\mathsf{next}

induces a path (left), resp. tree (right), over the bag-nodes

\Pi

.

The TIM encoding is a generalisation of the VIM encoding. In a TIM decomposition, vertices in the same connected component of a snapshot must be in the same bag at that time, while those in different connected components may be in different bags.

Definition 12 (TIM encoding).

Let $\mathcal{G}=(V,\mathcal{E})$ be an undirected strict temporal graph with TIM decomposition $(T,{\Pi},\tau)$ . The relational TIM structure $\lfloor\mathcal{G}\rfloor_{\mathsf{tim}}$ is defined as:

universe $U=V\cup\mathcal{E}\cup{\Pi}$

unary relations $V\subseteq U,\mathcal{E}\subseteq U,{\Pi}\subseteq U$

binary relations

$\blacksquare$

$\mathsf{inc}\subseteq\mathcal{E}\times V$ where $\mathsf{inc}((uv,t),x)\Leftrightarrow x=u\text{ or }x=v$ ,
$\blacksquare$

$\mathsf{bag}\subseteq V\times{\Pi}$ where $\mathsf{bag}(v,\pi_{i})\Leftrightarrow v\in\pi_{i}$ ,
$\blacksquare$

$\mathsf{pres}\subseteq\mathcal{E}\times{\Pi}$ where $\mathsf{pres}((uv,t),\pi_{i})\Leftrightarrow\tau(i)=t\text{ and }u,v\in\pi_{i}$ ,
$\blacksquare$

$\mathsf{next}\subseteq{\Pi}\times{\Pi}$ where $\mathsf{next}(\pi_{i},\pi_{j})\Leftrightarrow\tau(i)+1=\tau(j)\text{ and }\\ \phantom{XXXXXXXXXXXXXXXXXX}(\pi_{i},\pi_{j})\in E(T)$ .

4 Temporal Meta–Theorems

In this section, we establish meta-theorems for FO and MSO model checking on temporal graphs. Using the relational encodings from Section 3, we show that FO/MSO-definable temporal properties are fixed-parameter tractable under bounded (i) $\Lambda$ , (ii) $\Delta^{t}$ , (iii) $\mathsf{vim}$ , or (iv) $\mathsf{tim}$ , possibly in combination with structural assumptions on the footprint. See 1 See 2 Both results are obtained by analysing the Gaifman graph $\operatorname{Gf}(\mathcal{S})$ of a relational structure.

Definition 13 (Gaifman graph).

Let $\mathcal{S}$ be any finite relational structure with universe $U$ and some set of relations $\mathfrak{R}=\{R_{1},R_{2},\dots\}$ . The Gaifman graph $\operatorname{Gf}(\mathcal{S})$ is a static, simple, undirected graph with vertex set $U$ and an edge $\{a,b\}$ if and only if (i) $a\neq b$ and (ii) there exist a relation $R\in\mathfrak{R}$ with $k\geq 2$ arguments and a tuple $(a_{1},\dots,a_{k})\in R$ such that $a,b\in\{a_{1},\dots,a_{k}\}$ .

The illustrations in Figures 3, 3, 4, and 4 depict the Gaifman graphs of the four encodings. The static meta-theorems (Theorems 8 and 7) apply to relational structures via their Gaifman graphs: bounded treewidth of $\operatorname{Gf}(\mathcal{S})$ yields $\mathtt{FPT}$ MSO MC on $\mathcal{S}$ by Courcelle’s theorem, and nowhere denseness of $\operatorname{Gf}(\mathcal{S})$ yields $\mathtt{FPT}$ FO MC on $\mathcal{S}$ by the Grohe–Kreutzer–Siebertz theorem. Since each encoding $\lfloor\mathcal{G}\rfloor$ is a relational structure, it suffices to show that $\operatorname{Gf}(\lfloor\mathcal{G}\rfloor)$ has bounded treewidth, respectively is nowhere dense, as a function of the corresponding parameter.

4.1 Temporal Encodings preserve Treewidth

MSO model checking is fixed-parameter tractable on graph classes of bounded treewidth. We show that the Gaifman graph of each encoding has bounded treewidth whenever the corresponding parameter $\Lambda$ , $\Delta^{t}$ , $\mathsf{vim}$ or $\mathsf{tim}$ is bounded. This has previously been established for the lifetime encoding [27] and the degree encoding [20]; we provide proofs for completeness and unified notation in the full version. For the VIM encoding and TIM encoding introduced in this work, we give novel proofs.

All results in this section are proven with a similar technique. Starting from a tree, VIM, or TIM decomposition of the temporal graph $\mathcal{G}$ , the bags are enlarged with temporal elements specific to each encoding to obtain a tree decomposition of the Gaifman graph.

Lemma 14 ([27]).

Let $\mathcal{G}$ be a temporal graph with treewidth $\mathsf{tw}(\mathcal{G})$ and lifetime $\Lambda$ . Then $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Lambda})\big)\ % \leq\ \Lambda+\Lambda\mathsf{tw}(\mathcal{G})^{2}+\mathsf{tw}(\mathcal{G})$ and, consequently, $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Lambda})\big)\in% \mathcal{O}(\mathsf{tw}(\mathcal{G})^{2}\Lambda)$ .

Lemma 15 ([20]).

Let $\mathcal{G}$ be a temporal graph with treewidth $\mathsf{tw}(\mathcal{G})$ and maximum temporal total degree $\Delta^{t}$ . Then $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Delta^{t}})\big)% \ \leq\ (\Delta^{t}+1)(\mathsf{tw}(\mathcal{G})+1)$ and, consequently, $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Delta^{t}})\big)% \in\mathcal{O}(\mathsf{tw}(\mathcal{G})\cdot\Delta^{t})$ .

Lemma 16.

Let $\mathcal{G}$ be a temporal graph with VIM width $\mathsf{vim}(\mathcal{G})$ . Then $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{vim}})% \big)\ \leq\ \mathsf{vim}(\mathcal{G})+2\mathsf{vim}(\mathcal{G})^{2}$ and, consequently, $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{vim}})% \big)\in\mathcal{O}(\mathsf{vim}(\mathcal{G})^{2})$ .

Proof.

Let ${\Pi}=(\pi_{t})_{t\in[\Lambda]}$ be the VIM decomposition of $\mathcal{G}$ , so $\pi_{t}=\{v\in V:t\in A(v)\}$ and $\max_{t\in[\Lambda]}|\pi_{t}|=\mathsf{vim}$ . Recall that the VIM decomposition forms a (not necessarily optimal) path decomposition of the footprint $G$ of $\mathcal{G}$ . We build a path decomposition $(T,\{B_{t}:t\in[\Lambda]\})$ of $\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{vim}})$ as follows. To avoid confusion, we refer to the bags $\pi_{t}$ of the VIM decompositions of $\mathcal{G}$ as VIM-bags and the bags $B_{t}$ of the path decomposition of $\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{vim}})$ as simply bags. For notational convenience, let $\pi_{\Lambda+1}:=\emptyset$ . For each $t\in V(T)=[\Lambda]$ , define the bag

\displaystyle B_{t}\ :=\

\displaystyle\underbrace{\{v:v\in\pi_{t}\}}_{\text{$t$-alive vertices}}\ \cup% \ \underbrace{\{\varepsilon\in\mathcal{E}:\varepsilon=(e,t)\}}_{\text{temporal% edges in $G_{t}$}}\ \cup\ \underbrace{\{\pi_{t},\pi_{t+1}\}}_{\text{current % and next VIM-bag}}.

We show that this forms a path decomposition. Recall that the universe of $\lfloor\mathcal{G}\rfloor_{\mathsf{vim}}$ is $U=V\cup\mathcal{E}\cup{\Pi}$ .

(i)
First, we show $\bigcup_{t\in[\Lambda]}B_{t}=U$ :
- $\blacksquare$
  
  A vertex $v\in V$ lies in every $B_{t}$ with $t\in A(v)$ .
- $\blacksquare$
  
  A temporal edge $\varepsilon\in\mathcal{E}$ lies in $B_{t}$ where $\varepsilon=(e,t)$ for some static edge $e$ .
- $\blacksquare$
  
  A VIM-bag $\pi_{t}\in{\Pi}$ lies in the bags $B_{t}$ and $B_{t-1}$ .
(ii)
Every edge of the Gaifman graph is covered by some bag:
- $\blacksquare$
  
  $\mathsf{inc}\subseteq\mathcal{E}\times V$ : if $v$ is an endpoint of $\varepsilon=(e,t)$ then $t\in A(v)$ and we must have $\varepsilon,v\in B_{t}$ .
- $\blacksquare$
  
  $\mathsf{pres}\subseteq\mathcal{E}\times{\Pi}$ : if $\mathsf{pres}(\varepsilon,\pi_{t})$ , then $\varepsilon,\pi_{t}\in B_{t}$ .
- $\blacksquare$
  
  $\mathsf{bag}\subseteq V\times{\Pi}$ : if $\mathsf{bag}(v,\pi_{t})$ , then $v,\pi_{t}\in B_{t}$ .
- $\blacksquare$
  
  $\mathsf{next}\subseteq{\Pi}\times{\Pi}$ : for any $t\in[\Lambda)$ , we have $\pi_{t},\pi_{t+1}\in B_{t}$ and $B_{t+1}$ .
(iii)
For each element of $U$ , the indices of bags containing it form a connected subtree of $T$ :
- $\blacksquare$
  
  $v\in V$ occurs precisely in the bags $B_{t}$ where $t\in A(v)$ . Since $A(v)$ is a contiguous interval, this must be a subpath of the decomposition.
- $\blacksquare$
  
  $\varepsilon=(e,t)\in\mathcal{E}$ occurs only in the bag $B_{t}$ . This must trivially induce a connected subpath of the decomposition.
- $\blacksquare$
  
  $\pi_{t}\in F$ occurs only in $B_{t}$ and $B_{t-1}$ , which are adjacent in the decomposition.

Lastly, we bound the width. For any $t\in[\Lambda]$ , we have $|\pi_{t}|\leq\mathsf{vim}$ . Every temporal edge in $B_{t}$ has both endpoints in $\pi_{t}$ , so there are at most $|\pi_{t}|^{2}\leq\mathsf{vim}^{2}$ such edges. Thus $|B_{t}|\leq 1+|\pi_{t}|+|\pi_{t}|^{2}\leq 1+\mathsf{vim}+\mathsf{vim}^{2}$ , and hence $\mathsf{tw}(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{vim}}))\in% \mathcal{O}(\mathsf{vim}(\mathcal{G})^{2})$ . $\hfill\blacktriangleleft$

For the TIM encoding, recall that $\mathsf{tim}(\mathcal{G})\geq\mathsf{tw}(\mathcal{G})$ .

Lemma 17.

Let $\mathcal{G}$ be a temporal graph with TIM width $\mathsf{tim}(\mathcal{G})$ . Then $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{tim}})% \big)\ \leq\ \mathsf{tim}(\mathcal{G})^{2}+3\mathsf{tim}(\mathcal{G})-1$ and, consequently, $\mathsf{tw}\big(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{tim}})% \big)\in\mathcal{O}(\mathsf{tim}(\mathcal{G})^{2})$ .

Proof.

Let $(T,{\Pi}=\{\pi_{i}\colon i\in V(T)\},\tau)$ be a TIM decomposition of $\mathcal{G}$ . We build a tree decomposition $(T,\{B_{i}:i\in V(T)\})$ of $\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{tim}})$ as follows. To avoid confusion, we refer to the bags $\pi_{i}$ of the TIM decomposition as TIM-bags and the bags $B_{i}$ of the tree decomposition as simply bags. For each $i\in V(T)$ , define the bag

\displaystyle B_{i}:=

\displaystyle\underbrace{\{v\in\pi_{i}\}}_{\text{vertices in TIM-bag}}\cup\ % \underbrace{\{\varepsilon=(e,t)\in\mathcal{E}:\tau(i)=t,\ \varepsilon[0],% \varepsilon[1]\in\pi_{i}\}}_{\text{temporal edges with endpoints in TIM-bag}}% \ \cup\underbrace{\{\pi_{i},p(\pi_{i})\}}_{\text{TIM-bag and parent}},

where $p(\pi_{i})$ is the parent TIM-bag of $\pi_{i}$ in the TIM decomposition. We show that this forms a tree decomposition. Recall that the universe of $\lfloor\mathcal{G}\rfloor_{\mathsf{tim}}$ is $U=V\cup E\cup{\Pi}$ .

(i)
First, we show $\bigcup_{i\in V(T)}B_{i}=U$ :
- $\blacksquare$
  
  A vertex $v\in V$ lies in every $B_{i}$ with $v\in\pi_{i}$ . By definition of a TIM decomposition there exists at least one such TIM-bag for every vertex.
- $\blacksquare$
  
  A temporal edge $\varepsilon=(e,t)\in\mathcal{E}$ lies in $B_{i}$ where $\tau(i)=t$ and $\varepsilon[0],\varepsilon[1]\in\pi_{i}$ . By definition of a TIM decomposition, there exists at least one such TIM-bag for every temporal edge.
- $\blacksquare$
  
  A TIM-bag $\pi_{i}\in{\Pi}$ lies in $B_{i}$ .
(ii)
Every edge of the Gaifman graph is covered by some bag:
- $\blacksquare$
  
  $\mathsf{inc}\subseteq\mathcal{E}\times V$ : if $v$ is an endpoint of $\varepsilon=(e,t)$ , then there exists $i\in V(T)$ with $\tau(i)=t$ and $\varepsilon[0],\varepsilon[1]\in\pi_{i}$ ; hence $\varepsilon,v\in B_{i}$ .
- $\blacksquare$
  
  $\mathsf{bag}\subseteq V\times{\Pi}$ : for $v\in\pi_{i}$ we have $v,\pi_{i}\in B_{i}$ .
- $\blacksquare$
  
  $\mathsf{pres}\subseteq\mathcal{E}\times{\Pi}$ : if $\mathsf{pres}(\varepsilon,\pi_{i})$ , then $\varepsilon,\pi_{i}\in B_{i}$ .
- $\blacksquare$
  
  $\mathsf{next}\subseteq{\Pi}\times{\Pi}$ : for $(i,j)\in E(T)$ , we have that $\pi_{j}$ is the parent of $\pi_{i}$ in $T$ by definition of the TIM encoding. By construction of our bags, we have $\pi_{i}\in B_{i}$ and $p(\pi_{i})=\pi_{j}\in B_{i}$ . Hence $\pi_{i}$ and $\pi_{j}$ occur together in the bag $B_{i}$ .
(iii)
For each element of $U$ , the indices of bags containing it form a connected subtree of $T$ :
- $\blacksquare$
  
  $v\in V$ appears in the bag $B_{i}$ if and only if $v\in\pi_{i}$ . By the definition of a TIM decomposition, the subtree of $T$ induced by TIM-bags containing $v$ must form a directed path. Since the TIM decomposition and this tree decomposition are indexed by the same tree, the bags containing $v$ form a subpath of $T$ .
- $\blacksquare$
  
  $\varepsilon=(e,t)\in\mathcal{E}$ appears in the bag $B_{i}$ if and only if both endpoints of $\varepsilon$ are in $\pi_{i}$ and $\tau(i)=t$ . This occurs in exactly one bag of the decomposition. Therefore, the subtree induced by the bags of $(T,\mathcal{B})$ containing $\varepsilon$ is connected and non-empty.
- $\blacksquare$
  
  $\pi_{i}\in{\Pi}$ appears in $B_{i}$ and all bags of its children, which induce a connected subtree of $T$ . Since the tree decomposition and the TIM decomposition are indexed by the same tree, the claim follows.

Lastly, we show the width bound. Since $|\pi_{i}|\leq\mathsf{tim}$ for $i\in V(T)$ , we have $|B_{i}|\ \leq|\pi_{i}|\ +\ |\mathcal{E}_{i}|\ +\ |N_{T}(\pi_{i})|\ \leq\ 3% \mathsf{tim}+\mathsf{tim}^{2}$ , hence $\mathsf{tw}(\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{tim}}))\in% \mathcal{O}(\mathsf{tim}(\mathcal{G})^{2})$ . $\hfill\blacktriangleleft$

4.2 Temporal Encodings preserve Nowhere Denseness

FO model checking is fixed-parameter tractable on nowhere dense graph classes, a broad family that includes, e. g., planar graphs, graphs of bounded expansion and of bounded treewidth. We show that the Gaifman graphs arising from our relational encodings form nowhere dense graph classes.

To the best our knowledge, FO meta-theorems have previously been considered for temporal graphs only by Mans and Mathieson [32] who studied a (flawed) variant of the lifetime encoding. They had essentially the same goal as in this paper: to design an encoding whose Gaifman graphs allow efficient FO model checking which, at the time, was only known for the class of graphs with bounded expansion. A flaw in their encoding and the associated argument was later identified by Fluschnik et al. [24]: Mans and Mathieson consider a generalisation of temporal graphs where the vertex set also varies over time. Their universe therefore contains an element for every vertex appearance (a temporal vertex), in contrast to our encoding which contains one element per static vertex. They claimed one could identify whether two temporal vertices belong to the same underlying vertex using a constant-length formula, but this would imply the existence of a constant-length formula for 3-colourability on constant-treewidth graphs [24], which would contradict $P\neq NP$ .

In what follows, we show that all four encodings preserve nowhere denseness when their respective parameter is bounded. Among the four encodings, the lifetime encoding requires the most care and we first give additional definitions for depth- $r$ topological minors.

Depth- $𝒓$ topological minors via models.

Recall that for static graphs $G$ and $H$ , we write $H\preceq^{t}_{r}G$ , if some $r$ -subdivision of $H$ is isomorphic to a subgraph of $G$ . An $r$ -subdivision is obtained by replacing a set of edges in $H$ by paths of length at most $r+1$ such that the internal vertices (all but the endpoints) of all paths are disjoint. Equivalently, $H\preceq^{t}_{r}G$ holds if $G$ contains a depth- $r$ model of $H$ , which is a pair $\eta=(\eta_{V},\eta_{E})$ where $\eta_{V}\colon V(H)\Rightarrow V(G)$ is an injective mapping, and for every edge $ab\in E(H)$ , $\eta_{E}(ab)$ is a simple path in $G$ , called model-path, of length at most $r+1$ that connects $\eta_{V}(a)$ and $\eta_{V}(b)$ , such that for all distinct edges $ab,cd\in E(H)$ , the paths $\eta_{E}(ab)$ and $\eta_{E}(cd)$ are internally vertex-disjoint, and no internal vertex of any path $\eta_{E}(ab)$ lies in $\eta_{V}(V(H))$ . The vertices in $\eta_{V}(V(H))$ are called the branch-vertices of the model. Intuitively, the model represents how the graph $H$ can be “found” inside $G$ after stretching each edge of $H$ into a path of length at most $r+1$ . The process of contracting an edge $u v$ yields the graph $G/uv$ obtained by identifying $u$ and $v$ into a new vertex that is adjacent to every vertex that was adjacent to $u$ or $v$ in $G$ , and then deleting self-loops and parallel edges (so that the result remains simple).

Lemma 18.

Let $\mathcal{C}$ be a nowhere dense class of static graphs with denseness-function $\mathsf{d}$ , and consider the class of all temporal graphs $\mathcal{C^{\prime}}$ with footprint in $\mathcal{C}$ and maximum lifetime $\Lambda$ . Then the class of Gaifman graphs $\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Lambda})$ for each $\mathcal{G}\in\mathcal{C^{\prime}}$ is nowhere dense. In particular, the function $g(r):=\mathsf{d}(\lceil r/2\rceil)+2\Lambda$ is a denseness-function for this class.

Proof.

Let $\mathcal{C}$ be a nowhere dense static graph class with denseness-function $\mathsf{d}$ , and let $\mathcal{C^{\prime}}$ be the class of all temporal graphs $\mathcal{G}=(G,\lambda)$ with lifetime at most $\Lambda$ and whose footprint $G$ lies in $\mathcal{C}$ . We analyze the class of Gaifman graphs $\{\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Lambda})\colon\mathcal{G}\in% \mathcal{C^{\prime}}\}$ .

Fix $\mathcal{G}\in\mathcal{C^{\prime}}$ , let $G_{\operatorname{Gf}}:=\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Lambda})$ . We will refer to a vertex $a\in V\cup\mathcal{E}\cup L$ of $G_{\operatorname{Gf}}$ as vertex node, temporal-edge node, or time node, respectively.

Step 1: $G_{\operatorname{Gf}}-L$ is nowhere dense with $\mathsf{d}_{\operatorname{Gf}-L}(r):=\mathsf{d}(\lceil r/2\rceil)$ .

Consider $G_{\operatorname{Gf}}-L$ . This graph can be obtained from the footprint $G$ by subdividing every edge $uv\in E(G)$ once (resulting in a temporal-edge node $\varepsilon$ ) and multiplying this $u-\varepsilon-v$ path for every temporal edge $(uv,t)\in\mathcal{E}$ . Conversely, $G$ can be obtained from $G_{\operatorname{Gf}}-L$ by contracting every temporal-edge node with one of its neighbours.

We show that if we can find an $r$ -subdivision of a clique $K_{q}$ in $G_{\operatorname{Gf}}-L$ , then there is an $\lceil r/2\rceil$ -subdivision of $K_{q}$ in $G$ . From this we conclude that $\mathsf{d}_{\operatorname{Gf}-L}(r):=\mathsf{d}(\lceil r/2\rceil)$ is a denseness function of $G_{\operatorname{Gf}}-L$ .

Fix $r\in\mathbb{N}$ and $q\geq 4$ , and assume that $K_{q}\preceq^{t}_{r}(G_{\operatorname{Gf}}-L)$ . Let $\eta$ be a depth- $r$ model of $K_{q}$ in $G_{\operatorname{Gf}}-L$ . In $G_{\operatorname{Gf}}-L$ , every temporal-edge node $\varepsilon=(uv,t)\in\mathcal{E}$ has degree 2 and is adjacent exactly to the nodes $u$ and $v$ . Consequently, no temporal-edge node in $\mathcal{E}$ can be a branch-vertex of a depth- $r$ clique model when $q\geq 4$ , and hence all branch-vertices must lie in $V$ . Additionally, each model-path of length $\ell$ in $G_{\operatorname{Gf}}-L$ must alternate between $V$ and $\mathcal{E}$ , and therefore becomes a path of length at most $\lceil\ell/2\rceil$ on $V$ in $G$ (after contracting all temporal-edge nodes with one of its neighbours). Internal vertex-disjointness of the model-paths is preserved under contraction. Thus, we obtain a depth- $\lceil r/2\rceil$ model of $K_{q}$ in $G$ , and therefore $K_{q}\preceq_{\lceil r/2\rceil}G$ .

By definition of $\mathsf{d}$ as a denseness-function for $\mathcal{C}$ , we have $K_{\mathsf{d}(\lceil r/2\rceil)}\not\preceq_{\lceil r/2\rceil}G$ for all $r$ . By our arguments above, this implies $K_{\mathsf{d}_{\operatorname{Gf}-L}(r)}=K_{\mathsf{d}(\lceil r/2\rceil)}\not% \preceq^{t}_{r}(G_{\operatorname{Gf}}-L)$ for all $r\in\mathbb{N}$ , and hence $\mathsf{d}_{\operatorname{Gf}-L}(r)=\mathsf{d}(\lceil r/2\rceil)$ is a denseness-function for the class of all such graphs $G_{\operatorname{Gf}}-L$ .

Step 2: $G_{\operatorname{Gf}}$ is nowhere dense with $\mathsf{d}_{\operatorname{Gf}}(r):=\mathsf{d}_{\operatorname{Gf}-L}(r)+2\Lambda$ .

Towards contradiction assume $K_{\ell}\preceq^{t}_{r}G_{\operatorname{Gf}}$ for $\ell:=\mathsf{d}_{\operatorname{Gf}-L}(r)+2\Lambda$ , and let $\eta$ be a depth- $r$ model of $K_{\ell}$ in $G_{\operatorname{Gf}}$ .

Step 1 shows that $G_{\operatorname{Gf}}-L$ cannot contain a depth- $r$ topological minor isomorphic to $K_{\mathsf{d}_{\operatorname{Gf}-L}(r)}$ . Thus, the only way the model $\eta$ can “beat” this bound is by exploiting clique of time nodes $L$ . Importantly, $L$ can help in two ways: (i) by hosting branch-vertices, and (ii) by serving as internal vertices on model-paths for clique edges. We show that both effects are limited by $|L|=\Lambda$ .

First, we consider the time nodes in $L$ that are branch-vertices. Let $B$ be the set of branch-vertices of $\eta$ and denote by $B_{L}:=B\cap L$ the branch-vertices in $L$ and by $B_{\neg L}:=B\setminus L$ the branch-vertices in $G_{\operatorname{Gf}}-L$ . Since $|L|=\Lambda$ , we have $|B_{L}|\leq\Lambda$ and therefore $\lvert B_{\neg L}\rvert\geq\ell-\Lambda=\mathsf{d}_{\operatorname{Gf}-L}(r)+\Lambda$ .

Next, we consider the time nodes in $L$ that are used by model-paths. Let $F$ be the set of clique edges $x y$ whose model path contains a time node of $L$ as an internal vertex. Since model-paths have to be internally disjoint, each time node in $L$ can be used by the model-path of at most one clique edge, and therefore $\lvert F\rvert\leq\lvert L\setminus B_{L}\rvert\leq\Lambda$ . Let $S$ be the set of endpoints (in $B_{\neg L}$ ) of the edges in $F$ . Then $\lvert S\rvert\leq 2\lvert F\rvert\leq 2\Lambda$ .

Define $B^{\prime}:=B_{\neg L}\setminus S$ as the set of branch vertices outside $L$ whose model-paths do not use $L$ . It holds $\lvert B^{\prime}\rvert\geq\lvert B_{\neg L}\rvert-2\Lambda\geq\mathsf{d}_{% \operatorname{Gf}-L}(r)$ . We claim that restricting $\eta$ to the branch-vertices $B^{\prime}$ yields a depth- $r$ model of $K_{\lvert B^{\prime}\rvert}$ in $G_{\operatorname{Gf}}-L$ . To that end, consider any two distinct $x,y\in B^{\prime}$ . Then $x,y\notin L$ and $xy\notin F$ (otherwise $x\in S$ or $y\in S$ ). Hence the model-path for $x y$ does not go through $L$ and must lie entirely in $G_{\operatorname{Gf}}-L$ . Thus, $G_{\operatorname{Gf}}-L$ contains $K_{|B^{\prime}|}$ as a depth- $r$ topological minor, and in particular contains $K_{\mathsf{d}_{\operatorname{Gf}-L}(r)}$ as a depth- $r$ topological minor. This contradicts $\mathsf{d}_{\operatorname{Gf}-L}$ being a denseness-function for $G_{\operatorname{Gf}}-L$ .

Consequently, $K_{\mathsf{d}_{\operatorname{Gf}-L}(r)+2\Lambda}\not\preceq^{t}_{r}G_{% \operatorname{Gf}}$ for all $r\in\mathbb{N}$ , and hence $g(r)=\mathsf{d}_{\operatorname{Gf}-L}(r)+2\Lambda$ is a denseness-function for the class of all such graphs $G_{\operatorname{Gf}}$ . $\hfill\blacktriangleleft$

For the degree encoding, we show a stronger result, namely that the maximum static degree of the Gaifman graph is bounded by the temporal total degree of $\mathcal{G}$ . Since graph classes of bounded maximum degree are nowhere dense, this immediately implies the desired result.

Lemma 19.

Let $\mathcal{C}$ be a nowhere dense class of static graphs with denseness-function $\mathsf{d}$ , and consider the class of all temporal graphs $\mathcal{C^{\prime}}$ with footprint in $\mathcal{C}$ and maximum temporal total degree $\Delta^{t}$ . For $\mathcal{G}\in\mathcal{C^{\prime}}$ , let $H:=\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Delta^{t}})$ be the Gaifman graph of the degree encoding of $\mathcal{G}$ . Then $\Delta(H)\leq 2\Delta^{t}$ and, consequently, the class of all such graphs $H$ is nowhere dense.

Proof.

Let $G_{\operatorname{Gf}}:=\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\Delta^{t}})$ be the Gaifman graph of the degree encoding $\lfloor\mathcal{G}\rfloor_{\Delta^{t}}$ . Recall from the degree encoding that the vertices of $G_{\operatorname{Gf}}$ are $V\cup\mathcal{E}$ , where $\mathcal{E}$ is the set of temporal edges. The binary relations are: $\mathsf{source}((e,t),v)$ and $\mathsf{target}((e,t),v)$ , connecting every temporal edge to its endpoints; and $\mathsf{psuc}((e_{1},t_{1}),(e_{2},t_{2}))$ , which holds if and only if the two temporal edges share an endpoint and $t_{1}\prec t_{2}$ . Thus, in the Gaifman graph $G_{\operatorname{Gf}}$ : each temporal edge $(e,t)$ is adjacent to its two endpoints; and two temporal edges $(e_{1},t_{1})$ and $(e_{2},t_{2})$ are adjacent if and only if they share a vertex in $V$ and their times are comparable (which is always the case, since $\prec$ is a total order). We now bound the maximum degree of $G_{\operatorname{Gf}}$ in terms of the maximum temporal total degree $\Delta^{t}$ .

Let $v\in V$ . By definition of $\Delta^{t}$ , there are at most $\Delta^{t}$ temporal edges incident with $v$ , so in $G_{\operatorname{Gf}}$ the vertex $v$ has at most $\Delta^{t}$ neighbours (all of them in $\mathcal{E}$ ). There are no edges in $G_{\operatorname{Gf}}$ between two vertices of $V$ . Hence $\deg_{H}(v)\leq\Delta^{t}$ . Let $\varepsilon=(e,t)\in\mathcal{E}$ where $e$ has endpoints $u,v\in V$ (for directed graphs, $u$ is the source and $v$ the target; the argument is identical). Then the neighbours of $\varepsilon$ in $G_{\operatorname{Gf}}$ are (1) its endpoints $u$ and $v$ (two vertices in $V$ ); and (2) all other temporal edges incident with $u$ or with $v$ (the $\mathsf{psuc}$ -neighbours). By the definition of $\Delta^{t}$ , there are at most $\Delta^{t}-1$ temporal edges at $u$ different from $(e,t)$ , and at most $\Delta^{t}-1$ such edges at $v$ . Therefore $\varepsilon$ has at most $(\Delta^{t}-1)+(\Delta^{t}-1)$ neighbours in $\mathcal{E}$ , plus its two endpoint vertices. In particular, $\deg_{H}(x)\leq 2+2(\Delta^{t}-1)\leq 2\Delta^{t}$ .

Combining both cases, the maximum degree of $G_{\operatorname{Gf}}$ is bounded by $\Delta(G_{\operatorname{Gf}})\leq 2\Delta^{t}$ . $\hfill\blacktriangleleft$

For the VIM encoding and the TIM encoding the nowhere dense preservation also follows from a stronger result: the parameters $\mathsf{vim}$ and $\mathsf{tim}$ bound the treewidth of the footprint of a temporal graph. Since graph classes with bounded treewidth are nowhere dense, the desired result follows directly from the treewidth bounds established in Lemmas 16 and 17.

Corollary 20.

Let $\mathbf{C}$ be a class of temporal graph with VIM width at most $\mathsf{vim}$ . Then the class of all Gaifman graphs $\{\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{vim}})\,\colon\,% \mathcal{G}\in\mathbf{C}\}$ is nowhere dense. Equivalently, let $\mathbf{C^{\prime}}$ be a class of temporal graph with TIM width at most $\mathsf{tim}$ . Then the class of all Gaifman graphs $\{\operatorname{Gf}(\lfloor\mathcal{G}\rfloor_{\mathsf{tim}})\,\colon\,% \mathcal{G}\in\mathbf{C^{\prime}}\}$ is nowhere dense.

5 Logic Cookbook (see full version)

A major motivation of our framework is reusability: in the full version, we provide a modular lexicon of FO/MSO formulas for temporal-graph properties across all four encodings (and, by design, extendable to future encodings). The cookbook covers over a dozen problems considered in the temporal graph literature including reachability notions (temporal path, reachability, restless path), reachability-based problems (separator/cut, connected component, temporal spanner), covering problems (matching, edge/vertex cover, dominating set), classic subgraph problems (temporal clique and independent set, colouring), and temporal parameters (feedback edge number, temporal path number). For each problem, we provide (i) a formal definition; (ii) a modular logic formula; (iii) metadata such as the supported encodings, the logical fragment (FO/MSO), and formula length.

As an illustration, we give the formula for Temporal Spanner (see [5, 29]) which is a sparse subgraph of a temporal graph that preserves temporal connectivity.

MSO Formula 5.3.13 temporal spanner

Purpose: there exists a set $X\subseteq\mathcal{E}$ such that for every $u,v\in V$ there is a temporal $u$ - $v$ path in $\mathcal{G}$ if and only if there is a temporal $u$ - $v$ path only traversing temporal edges in $X$

Logic:

MSO

Length:

constant

Encodings:

\Lambda

,

\Delta^{t}

,

\mathsf{vim}

,

\mathsf{tim}

\displaystyle\varphi_{\text{tspanner}}()=\exists X\subseteq\mathcal{E}\,% \forall u,v\in V\colon\big(\varphi_{\text{path}}(u,v)\leftrightarrow\varphi_{% \text{Epath}}(u,v,X)\big)

where $\varphi_{\text{path}}(u,v)$ checks if there is a temporal path from $u$ to $v$ and $\varphi_{\text{Epath}}(u,v,X)$ checks if there is a temporal path from $u$ to $v$ only traversing temporal edges in $X$ .

6 Future Work

Several directions for future research exist on the use of logic for temporal graphs.

With respect to temporal encodings, a natural direction is to identify other temporal parameters for which similar preservation and meta-theorems can be obtained. Possible candidates include the temporal feedback vertex number [27], the temporal cliquewidth [18], or a combination of underlying cliquewidth with lifetime or temporal total degree.

In the work introducing the TIM width, Enright et al. [19] present two meta-algorithms that characterise the classes of computational problems that are $\mathtt{FPT}$ with respect to $\mathsf{vim}$ and $\mathsf{tim}$ . For $\mathsf{vim}$ , tractability is tied to a notion of temporal locality, while for $\mathsf{tim}$ this locality is further structurally restricted. This perspective reminds of first-order logic which is inherently limited to see only local properties of a graph. An interesting question is whether these classes of problems admit a precise logical characterisation, e. g., by a suitable fragment of FO or MSO logic, and how such a characterisation relates to the VIM and TIM encodings.

Finally, a broader direction is to investigate logical tools beyond FO and MSO meta-theorems, such as logical transductions, game-based techniques, and methods inspired by the Weisfeiler–Leman framework. Such tools may provide alternative ways to compare temporal graph classes and to reason about their structural and algorithmic properties. Recent work has begun to study isomorphisms for temporal graphs under reachability notions [4, 15]; an intriguing next step is to explore whether transductions or related techniques can be used to further compare temporal graph classes, in particular with respect to structural parameters and the computational complexity of temporal graph problems.

References

[1] Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12(2):308–340, 1991. doi:10.1016/0196-6774(91)90006-K.
[2] Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, and Nathalie Sznajder. Model checking with temporal graphs and their derivative, 2026. doi:10.48550/arXiv.2602.12446.
[3] Benjamin Merlin Bumpus and Kitty Meeks. Edge Exploration of Temporal Graphs. Algorithmica, 85(3):688–716, 2023. doi:10.1007/s00453-022-01018-7.
[4] Arnaud Casteigts, Timothée Corsini, and Writika Sarkar. Simple, Strict, Proper, Happy: A Study of Reachability in Temporal Graphs. Theoretical Computer Science, 991:114434, 2024. doi:10.1016/j.tcs.2024.114434.
[5] Arnaud Casteigts, Anne-Sophie Himmel, Hendrik Molter, and Philipp Zschoche. Finding Temporal Paths Under Waiting Time Constraints. Algorithmica, 83(9):2754–2802, 2021. doi:10.1007/s00453-021-00831-w.
[6] Arnaud Casteigts, Nils Morawietz, and Petra Wolf. Distance to Transitivity: New Parameters for Taming Reachability in Temporal Graphs. In Rastislav Královič and Antonín Kučera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, volume 306, pages 36:1–36:17, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. ISSN: 1868-8969. doi:10.4230/LIPIcs.MFCS.2024.36.
[7] Justine Cauvi and Laurent Viennot. Parameterized Restless Temporal Path, 2025. doi:10.48550/arXiv.2507.05760.
[8] Dibyayan Chakraborty, Antoine Dailly, Florent Foucaud, and Ralf Klasing. Algorithms and Complexity for Path Covers of Temporal Dags, 2024. URL: https://hal.science/hal-04493029.
[9] Bruno Courcelle. Graph Rewriting: An Algebraic and Logic Approach. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 193–242. Elsevier, 1990. doi:10.1016/B978-0-444-88074-1.50010-X.
[10] Professor Bruno Courcelle and Dr Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press, USA, 1st edition, 2012.
[11] Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Daniel Marx, Marcin Pilipczuk, and Michał Pilipczuk. Parameterized Algorithms, volume 5. Springer, a edition, 2015.
[12] Tom Davot, Jessica Enright, and Laura Larios-Jones. Parameterised algorithms for temporally satisfying reconfiguration problems. In International Symposium on Algorithmics of Wireless Networks, pages 89–103. Springer, 2025. doi:10.1007/978-3-032-09120-8_7.
[13] Argyrios Deligkas, Michelle Döring, Eduard Eiben, Tiger-Lily Goldsmith, George Skretas, and Georg Tennigkeit. Parameterized Complexity of Temporal Connected Components: Treewidth and Temporal Path Number, 2025. doi:10.48550/arXiv.2510.05806.
[14] Argyrios Deligkas, Eduard Eiben, and George Skretas. Minimizing Reachability Times on Temporal Graphs via Shifting Labels. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, volume 5, pages 5333–5340, 2023. doi:10.24963/ijcai.2023/592.
[15] Michelle Döring. Simple, Strict, Proper, and Directed: Comparing Reachability in Directed and Undirected Temporal Graphs. In The 36th International Symposium on Algorithms and Computation, ISAAC 2025, volume 359, pages 27:1–27:21, Tainan, Taiwan, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025). doi:10.4230/LIPIcs.ISAAC.2025.27.
[16] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Springer, New York, NY, 1994. doi:10.1007/978-1-4757-2355-7.
[17] Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer Science & Business Media, 1999.
[18] Jessica Enright, Samuel D. Hand, Laura Larios-Jones, and Kitty Meeks. Structural Parameters for Dense Temporal Graphs. LIPIcs, Volume 306, MFCS 2024, 306:52:1–52:15, 2024. doi:10.4230/LIPIcs.MFCS.2024.52.
[19] Jessica Enright, Samuel D. Hand, Laura Larios-Jones, and Kitty Meeks. Families of Tractable Problems with Respect to Vertex-Interval-Membership Width and Its Generalisations, 2025. doi:10.48550/arXiv.2505.15699.
[20] Jessica Enright, Kitty Meeks, George B. Mertzios, and Viktor Zamaraev. Deleting Edges to Restrict the Size of an Epidemic in Temporal Networks. Journal of Computer and System Sciences, 119:60–77, 2021. doi:10.1016/j.jcss.2021.01.007.
[21] Jessica Enright, Kitty Meeks, and Hendrik Molter. Counting Temporal Paths. Algorithmica, 87(5):736–782, 2025. doi:10.1007/s00453-025-01301-3.
[22] Thomas Erlebach, Nils Morawietz, and Petra Wolf. Parameterized Algorithms for Multi-Label Periodic Temporal Graph Realization. Theoretical Computer Science, page 115412, 2025. Publisher: Elsevier. doi:10.1016/j.tcs.2025.115412.
[23] Thomas Erlebach and Jakob T. Spooner. Parameterised Temporal Exploration Problems. Journal of Computer and System Sciences, 135:73–88, 2023. doi:10.1016/j.jcss.2023.01.003.
[24] Till Fluschnik, Hendrik Molter, Rolf Niedermeier, Malte Renken, and Philipp Zschoche. As Time Goes By: Reflections on Treewidth for Temporal Graphs. In Fedor V. Fomin, Stefan Kratsch, and Erik Jan Van Leeuwen, editors, Treewidth, Kernels, and Algorithms, volume 12160 of Lecture Notes in Computer Science, pages 49–77. Springer International Publishing, Cham, 2020. doi:10.1007/978-3-030-42071-0_6.
[25] Martin Grohe. Logic, Graphs, and Algorithms. Logic and Automata, pages 2 : 357–422, 2008.
[26] Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding First-Order Properties of Nowhere Dense Graphs. J. ACM, 64(3):17:1–17:32, 2017. doi:10.1145/3051095.
[27] Roman Haag, Hendrik Molter, Rolf Niedermeier, and Malte Renken. Feedback Edge Sets in Temporal Graphs. Discrete Applied Mathematics, 307:65–78, 2022. Publisher: Elsevier. doi:10.1016/j.dam.2021.09.029.
[28] Anton Herrmann, Christian Komusiewicz, Nils Morawietz, and Frank Sommer. Timeline Problems in Temporal Graphs: Vertex Cover vs. Dominating Set. In Akanksha Agrawal and Erik Jan van Leeuwen, editors, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025), volume 358 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1–12:18, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.IPEC.2025.12.
[29] David Kempe, Jon Kleinberg, and Amit Kumar. Connectivity and Inference Problems for Temporal Networks. Journal of Computer and System Sciences, 64(4):820–842, 2002. doi:10.1006/jcss.2002.1829.
[30] Stephan Kreutzer. Algorithmic meta-theorems. In Finite and Algorithmic Model Theory, London Mathematical Society Lecture Note Series, pages 177–270. Cambridge University Press, 2011. editors: J. Esparza, C. Michaux, and C. Steinhorn.
[31] David C. Kutner and Laura Larios-Jones. Temporal Reachability Dominating Sets: Contagion in Temporal Graphs. Journal of Computer and System Sciences, 155:101–116, 2023. doi:10.1007/978-3-031-48882-5_8.
[32] Bernard Mans and Luke Mathieson. On the Treewidth of Dynamic Graphs. Theoretical Computer Science, 554:217–228, 2014. doi:10.1016/j.tcs.2013.12.024.
[33] George B. Mertzios, Hendrik Molter, Nils Morawietz, and Paul G. Spirakis. Temporal Graph Realization With Bounded Stretch. In 50th International Symposium on Mathematical Foundations of Computer Science, volume 345, pages 75:1–75:19, Dagstuhl, Germany, 2025. Leibniz International Proceedings in Informatics (LIPIcs). doi:10.4230/LIPIcs.MFCS.2025.75.
[34] Jaroslav Nešetřil and Patrice Ossona De Mendez. Sparsity: Graphs, Structures, and Algorithms, volume 28 of Algorithms and Combinatorics. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. doi:10.1007/978-3-642-27875-4.
[35] Philipp Zschoche, Till Fluschnik, Hendrik Molter, and Rolf Niedermeier. The Complexity of Finding Small Separators in Temporal Graphs. Journal of Computer and System Sciences, 107:72–92, 2020. doi:10.1016/j.jcss.2019.07.006.

[bib.bib1] [1] Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12(2):308–340, 1991. doi:10.1016/0196-6774(91)90006-K.

[bib.bib2] [2] Binh-Minh Bui-Xuan, Florent Krasnopol, Bruno Monasson, and Nathalie Sznajder. Model checking with temporal graphs and their derivative, 2026. doi:10.48550/arXiv.2602.12446.

[bib.bib3] [3] Benjamin Merlin Bumpus and Kitty Meeks. Edge Exploration of Temporal Graphs. Algorithmica, 85(3):688–716, 2023. doi:10.1007/s00453-022-01018-7.

[bib.bib4] [4] Arnaud Casteigts, Timothée Corsini, and Writika Sarkar. Simple, Strict, Proper, Happy: A Study of Reachability in Temporal Graphs. Theoretical Computer Science, 991:114434, 2024. doi:10.1016/j.tcs.2024.114434.

[bib.bib5] [5] Arnaud Casteigts, Anne-Sophie Himmel, Hendrik Molter, and Philipp Zschoche. Finding Temporal Paths Under Waiting Time Constraints. Algorithmica, 83(9):2754–2802, 2021. doi:10.1007/s00453-021-00831-w.

[bib.bib6] [6] Arnaud Casteigts, Nils Morawietz, and Petra Wolf. Distance to Transitivity: New Parameters for Taming Reachability in Temporal Graphs. In Rastislav Královič and Antonín Kučera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, volume 306, pages 36:1–36:17, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. ISSN: 1868-8969. doi:10.4230/LIPIcs.MFCS.2024.36.

[bib.bib7] [7] Justine Cauvi and Laurent Viennot. Parameterized Restless Temporal Path, 2025. doi:10.48550/arXiv.2507.05760.

[bib.bib8] [8] Dibyayan Chakraborty, Antoine Dailly, Florent Foucaud, and Ralf Klasing. Algorithms and Complexity for Path Covers of Temporal Dags, 2024. URL: https://hal.science/hal-04493029.

[bib.bib9] [9] Bruno Courcelle. Graph Rewriting: An Algebraic and Logic Approach. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 193–242. Elsevier, 1990. doi:10.1016/B978-0-444-88074-1.50010-X.

[bib.bib10] [10] Professor Bruno Courcelle and Dr Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press, USA, 1st edition, 2012.

[bib.bib11] [11] Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Daniel Marx, Marcin Pilipczuk, and Michał Pilipczuk. Parameterized Algorithms, volume 5. Springer, a edition, 2015.

[bib.bib12] [12] Tom Davot, Jessica Enright, and Laura Larios-Jones. Parameterised algorithms for temporally satisfying reconfiguration problems. In International Symposium on Algorithmics of Wireless Networks, pages 89–103. Springer, 2025. doi:10.1007/978-3-032-09120-8_7.

[bib.bib13] [13] Argyrios Deligkas, Michelle Döring, Eduard Eiben, Tiger-Lily Goldsmith, George Skretas, and Georg Tennigkeit. Parameterized Complexity of Temporal Connected Components: Treewidth and Temporal Path Number, 2025. doi:10.48550/arXiv.2510.05806.

[bib.bib14] [14] Argyrios Deligkas, Eduard Eiben, and George Skretas. Minimizing Reachability Times on Temporal Graphs via Shifting Labels. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, volume 5, pages 5333–5340, 2023. doi:10.24963/ijcai.2023/592.

[bib.bib15] [15] Michelle Döring. Simple, Strict, Proper, and Directed: Comparing Reachability in Directed and Undirected Temporal Graphs. In The 36th International Symposium on Algorithms and Computation, ISAAC 2025, volume 359, pages 27:1–27:21, Tainan, Taiwan, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025). doi:10.4230/LIPIcs.ISAAC.2025.27.

[bib.bib16] [16] H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Springer, New York, NY, 1994. doi:10.1007/978-1-4757-2355-7.

[bib.bib17] [17] Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer Science & Business Media, 1999.

[bib.bib18] [18] Jessica Enright, Samuel D. Hand, Laura Larios-Jones, and Kitty Meeks. Structural Parameters for Dense Temporal Graphs. LIPIcs, Volume 306, MFCS 2024, 306:52:1–52:15, 2024. doi:10.4230/LIPIcs.MFCS.2024.52.

[bib.bib19] [19] Jessica Enright, Samuel D. Hand, Laura Larios-Jones, and Kitty Meeks. Families of Tractable Problems with Respect to Vertex-Interval-Membership Width and Its Generalisations, 2025. doi:10.48550/arXiv.2505.15699.

[bib.bib20] [20] Jessica Enright, Kitty Meeks, George B. Mertzios, and Viktor Zamaraev. Deleting Edges to Restrict the Size of an Epidemic in Temporal Networks. Journal of Computer and System Sciences, 119:60–77, 2021. doi:10.1016/j.jcss.2021.01.007.

[bib.bib21] [21] Jessica Enright, Kitty Meeks, and Hendrik Molter. Counting Temporal Paths. Algorithmica, 87(5):736–782, 2025. doi:10.1007/s00453-025-01301-3.

[bib.bib22] [22] Thomas Erlebach, Nils Morawietz, and Petra Wolf. Parameterized Algorithms for Multi-Label Periodic Temporal Graph Realization. Theoretical Computer Science, page 115412, 2025. Publisher: Elsevier. doi:10.1016/j.tcs.2025.115412.

[bib.bib23] [23] Thomas Erlebach and Jakob T. Spooner. Parameterised Temporal Exploration Problems. Journal of Computer and System Sciences, 135:73–88, 2023. doi:10.1016/j.jcss.2023.01.003.

[bib.bib24] [24] Till Fluschnik, Hendrik Molter, Rolf Niedermeier, Malte Renken, and Philipp Zschoche. As Time Goes By: Reflections on Treewidth for Temporal Graphs. In Fedor V. Fomin, Stefan Kratsch, and Erik Jan Van Leeuwen, editors, Treewidth, Kernels, and Algorithms, volume 12160 of Lecture Notes in Computer Science, pages 49–77. Springer International Publishing, Cham, 2020. doi:10.1007/978-3-030-42071-0_6.

[bib.bib25] [25] Martin Grohe. Logic, Graphs, and Algorithms. Logic and Automata, pages 2 : 357–422, 2008.

[bib.bib26] [26] Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding First-Order Properties of Nowhere Dense Graphs. J. ACM, 64(3):17:1–17:32, 2017. doi:10.1145/3051095.

[bib.bib27] [27] Roman Haag, Hendrik Molter, Rolf Niedermeier, and Malte Renken. Feedback Edge Sets in Temporal Graphs. Discrete Applied Mathematics, 307:65–78, 2022. Publisher: Elsevier. doi:10.1016/j.dam.2021.09.029.

[bib.bib28] [28] Anton Herrmann, Christian Komusiewicz, Nils Morawietz, and Frank Sommer. Timeline Problems in Temporal Graphs: Vertex Cover vs. Dominating Set. In Akanksha Agrawal and Erik Jan van Leeuwen, editors, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025), volume 358 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1–12:18, Dagstuhl, Germany, 2025. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.IPEC.2025.12.

[bib.bib29] [29] David Kempe, Jon Kleinberg, and Amit Kumar. Connectivity and Inference Problems for Temporal Networks. Journal of Computer and System Sciences, 64(4):820–842, 2002. doi:10.1006/jcss.2002.1829.

[bib.bib30] [30] Stephan Kreutzer. Algorithmic meta-theorems. In Finite and Algorithmic Model Theory, London Mathematical Society Lecture Note Series, pages 177–270. Cambridge University Press, 2011. editors: J. Esparza, C. Michaux, and C. Steinhorn.

[bib.bib31] [31] David C. Kutner and Laura Larios-Jones. Temporal Reachability Dominating Sets: Contagion in Temporal Graphs. Journal of Computer and System Sciences, 155:101–116, 2023. doi:10.1007/978-3-031-48882-5_8.

[bib.bib32] [32] Bernard Mans and Luke Mathieson. On the Treewidth of Dynamic Graphs. Theoretical Computer Science, 554:217–228, 2014. doi:10.1016/j.tcs.2013.12.024.

[bib.bib33] [33] George B. Mertzios, Hendrik Molter, Nils Morawietz, and Paul G. Spirakis. Temporal Graph Realization With Bounded Stretch. In 50th International Symposium on Mathematical Foundations of Computer Science, volume 345, pages 75:1–75:19, Dagstuhl, Germany, 2025. Leibniz International Proceedings in Informatics (LIPIcs). doi:10.4230/LIPIcs.MFCS.2025.75.

[bib.bib34] [34] Jaroslav Nešetřil and Patrice Ossona De Mendez. Sparsity: Graphs, Structures, and Algorithms, volume 28 of Algorithms and Combinatorics. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. doi:10.1007/978-3-642-27875-4.

[bib.bib35] [35] Philipp Zschoche, Till Fluschnik, Hendrik Molter, and Rolf Niedermeier. The Complexity of Finding Small Separators in Temporal Graphs. Journal of Computer and System Sciences, 107:72–92, 2020. doi:10.1016/j.jcss.2019.07.006.

FO and MSO Model Checking on Temporal Graphs

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

1.1 Our contribution

Theorem 1.

Theorem 2.

1.2 Related Work

2 Preliminaries

Static graph parameters.

Definition 3 (Tree Decomposition, Treewidth [11]).

Temporal graph parameters.

Definition 4 (Activity-interval).

Definition 5 (Vertex-Interval-Membership Width (Bumpus and Meeks [3])).

Definition 6 (Tree-Interval-Membership Width [19]).

2.1 Logic in Static Graphs

Theorem 7 (Grohe–Kreutzer–Siebertz: FO MC on nowhere dense [26]).

Theorem 8 (Courcelle: MSO MC on bounded treewidth, [10]).

3 Temporal Graph Encodings

Definition 9 (lifetime encoding).

Definition 10 (degree encoding).

Definition 11 (VIM encoding).

Definition 12 (TIM encoding).

4 Temporal Meta–Theorems

Definition 13 (Gaifman graph).

4.1 Temporal Encodings preserve Treewidth

Lemma 14 ([27]).

Lemma 15 ([20]).

Lemma 16.

Proof.

Lemma 17.

Proof.

4.2 Temporal Encodings preserve Nowhere Denseness

Depth-𝒓 topological minors via models.

Lemma 18.

Proof.

Step 1: 𝑮𝐆𝐟−𝑳 is nowhere dense with 𝗱𝐆𝐟−𝑳⁢(𝒓):=𝗱⁢(⌈𝒓/𝟐⌉).

Step 2: 𝑮𝐆𝐟 is nowhere dense with 𝗱𝐆𝐟⁢(𝒓):=𝗱𝐆𝐟−𝑳⁢(𝒓)+𝟐⁢𝚲.

Lemma 19.

Proof.

Corollary 20.

5 Logic Cookbook (see full version)

6 Future Work

References

Depth- $𝒓$ topological minors via models.

Step 1: $G_{\operatorname{Gf}}-L$ is nowhere dense with $\mathsf{d}_{\operatorname{Gf}-L}(r):=\mathsf{d}(\lceil r/2\rceil)$ .

Step 2: $G_{\operatorname{Gf}}$ is nowhere dense with $\mathsf{d}_{\operatorname{Gf}}(r):=\mathsf{d}_{\operatorname{Gf}-L}(r)+2\Lambda$ .