Model checking with temporal graphs and their derivative

TL;DR

This work delivers the first algorithmic meta-theorems for temporal graphs that do not bound the lifetime. It presents MSOT-based model checking with an FPT guarantee parameterized by formula size and expanded tree-width $\mathop{tw}_{\rightarrow}(\mathcal{G})$, and extends to a weaker fragment $\textsf{FOT}_1^\Delta$ with FPT time under bounded expanded twin-width $\mathop{dtww}_{\Delta}(\mathcal{G})$, via a derivative (sliding-window) framework. The key technique is transforming temporal formulas to MSO on appropriately augmented structures and leveraging Gaifman locality to relate local neighborhoods to global width bounds. The derivative notion further refines width control by analyzing $\Delta$-slices, enabling tractable model checking for additional temporal properties, including $\Delta$-cliques and temporal matchings, with potential applications to time series databases and community-structure queries.

Abstract

Temporal graphs are graphs where the presence or properties of their vertices and edges change over time. When time is discrete, a temporal graph can be defined as a sequence of static graphs over a discrete time span, called lifetime, or as a single graph where each edge is associated with a specific set of time instants where the edge is alive. For static graphs, Courcelle's Theorem asserts that any graph problem expressible in monadic second-order logic can be solved in linear time on graphs of bounded tree-width. We propose the first adaptation of Courcelle's Theorem for monadic second-order logic on temporal graphs that does not explicitly rely on the lifetime as a parameter. We then introduce the notion of derivative over a sliding time window of a chosen size, and define the tree-width and twin-width of the temporal graph's derivative. We exemplify its usefulness with meta theorems with respect to a temporal variant of first-order logic. The resulting logic expresses a wide range of temporal graph problems including a version of temporal cliques, an important notion when querying time series databases for community structures.

Figures (4)

• Figure 1: (left, black edges) A temporal graph $\mathcal{G}$; (left, purple edges) some relations of its $\sigma_1$-structure $\lceil \mathcal{G}\rceil$, its static expansion graph is pictured when taking both black and dashed edges; (right) the union graph of $\mathcal{G}$.
• Figure 2: (left) A temporal static expanded graph $\mathcal{G}_\rightarrow$; (right) Its associated structure $\langle \mathcal{G} \rangle$; (right, blue edges) Its predicate $\operatorname{adj}$; (right, dashed edges) Its predicate $\operatorname{succ}$.
• Figure 3: The nodes $u(\mathcal{G})$, $w_1(\mathcal{G})$, $w_2(\mathcal{G})$ and $w_3(\mathcal{G})$. Thick black edges show the relation $\operatorname{adj}$, and dashed arrows the relation $\operatorname{succ}$. Red edge shows non homogeneity in the contraction sequence of $\mathcal{G}_\rightarrow$.
• Figure 4: (blue vertices) The $r$-neighbourhood $\mathcal{N}^{r}(a)$ of $a$, for $\Delta = 2$ and $r = 2$; (black edges) The edges of the original graph $\mathcal{G}$; (dashed edges) The edges which represent $\operatorname{succ}$; (green edges) The edges which represent $\operatorname{sim}_\Delta$. In $G^r(a)$, green edges are not considered.

Theorems & Definitions (21)

• Theorem 1: Courcelle90:graphrewriting
• Theorem 2
• Theorem 3
• Theorem 4
• Lemma 5
• Lemma 6
• Theorem 7
• Corollary 8
• Theorem 9
• Theorem 10