We study preservation theorems for modal logics over finite structures with respect to three fundamental semantic relations: embeddings, injective homomorphisms, and homomorphisms. We focus on classes of pointed Kripke models that are invariant under bounded unravellings, a natural locality condition satisfied by modal logics and by graph neural networks (GNNs). We show that preservation under embeddings coincides with definability in existential graded modal logic; preservation under injective homomorphisms with definability in existential positive graded modal logic; and preservation under homomorphisms with definability in existential positive modal logic. A key technical contribution is a structural well-quasi-ordering result. We prove that the embedding relation on classes of tree-shaped models of uniformly bounded height forms a well-quasi-order, and that the bounded-height assumption is essential. This well-quasi-ordering yields a finite minimal-tree argument leading to explicit syntactic characterisations via finite disjunctions of (graded) modal formulae. As an application, we derive consequences for the expressive power of GNNs. Using our preservation theorem for injective homomorphisms, we obtain a new logical characterisation of monotonic GNNs, showing that they capture exactly existential-positive graded modal logic, while monotonic GNNs with MAX aggregation correspond precisely to existential-positive modal logic.

翻译：我们研究了有限结构上模态逻辑相对于三种基本语义关系（嵌入、单射同态和同态）的保持定理。重点关注在有界展开下不变的带标记克里普克模型类，这是一种由模态逻辑和图神经网络（GNNs）共同满足的自然局部性条件。我们证明：在嵌入下的保持性等价于可被存在分次模态逻辑定义；在单射同态下的保持性等价于可被存在正分次模态逻辑定义；在同态下的保持性等价于可被存在正模态逻辑定义。一个关键的技术贡献是结构性的良拟序结果。我们证明了在具有一致有界高度的树形模型类上，嵌入关系构成良拟序，且高度有界的假设是本质性的。该良拟序性质通过有限最小树论证，导出了通过（分次）模态公式的有限析取实现的显式语法刻画。作为应用，我们推导了关于图神经网络表达能力的推论。利用单射同态保持定理，我们获得了单调图神经网络的新逻辑刻画，证明其恰好捕获存在正分次模态逻辑，而采用MAX聚合的单调图神经网络则精确对应存在正模态逻辑。