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 (VIM) width and tree-interval-membership (TIM) width, parameters which 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 degree to the parameters VIM and TIM width, 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.

翻译：算法元定理为展示在由结构限制定义的图类上图问题的可处理性提供了重要工具。尽管此类结果在静态图上已得到充分确立，但针对时态图的相应框架相对有限。在本工作中，我们重新审视了逻辑元定理在时态图中的过往应用，并发展了一个扩展的统一逻辑框架。我们的首要贡献是引入了顶点区间隶属度（VIM）宽度和树区间隶属度（TIM）宽度参数的逻辑编码，这些参数捕捉了顶点和组件随时间活动的特征。在此基础上，我们将现有的针对有限生命周期和时态度的单子二阶逻辑（MSO）元定理扩展至VIM和TIM宽度参数，并为所有四个参数建立了新颖的一阶逻辑（FO）元定理。最后，我们为广泛的时态图问题构建了一个模块化的、可复用的FO与MSO公式词典，并给出了一个示例。该词典允许以组合方式表达新问题，并直接在我们考虑的四个参数上产生固定参数可处理性结果。