Algorithmic meta-theorems (AMTs) are general algorithmic results applying to a whole range of problems, rather than just to a single problem alone. They often have a logical and a structural component, that is, they are results of the form: every computational problem that can be formalised in a given logic $\mathcal{L}$ can be solved efficiently on every class $\mathcal{C}$ of structures satisfying certain conditions. — Stephan Kreutzer

This page summarizes the logical meta-theorem framework for temporal graphs, showing how to obtain broad fixed-parameter tractability (FPT) results by expressing computational problems in FO or MSO over suitable relational encodings of a temporal graph to utilize the AMTs that exist for static graphs.

Logic on Static Graphs

History on AMTs for Temporal Graphs

Logic on Temporal Graphs

There are three steps to using AMTs on temporal graphs:

1. Define an encoding of an arbitrary temporal graph as a relational structure — a universe of elements joined together by a set of relations (such as incidence or adjacency relation)
2. Proof that the Gaifman graph of this encoding has the bounded graph structure needed for the AMT (such as bounded treewidth, twin width, etc).
3. Formulate the desired computational problem with the desired logic, using the encoding.

Known AMTs for Temporal Graphs

Temporal Algorithmic Meta Theorems

Known Temporal Graph Encodings

All encodings represent a temporal graph with a different perspective — they all contain (at least) static vertices and temporal edges; and differ in how they represent time and temporal constraints.

Below are the strict and undirected variants; to obtain directed encodings replace the incidence relation by source and target relations; non-strict reachability is handled by adapting the successor relation or at the formula level depending on the encoding.

1) Lifetime encoding $\lfloor \mathcal{G}\rfloor_\Lambda$

Based on the lifetime $\Lambda$ of the temporal graph. The encoding is a direct analogue to the classical definition of a temporal graph as a labeled graph.

Key effect: the time-order induces a clique on time nodes, so structural bounds typically are impacted by factor of $\Lambda$.

2) Degree encoding $\lfloor \mathcal{G}\rfloor_{\Delta_t}$

Based on the temporal degree $\Delta^t$ of the temporal graph. The temporal information is stored between touching edges — using an order instead of specific time steps.

Key effect: no representation of explicit time steps; structure is impacted by a factor of $\Delta_t$.