Game comonads give a categorical semantics for comparison games in Finite Model Theory, thus providing an abstract characterisation of logical equivalence for a wide range of logics, each one captured through a specific choice of comonad. However, data-aware logics such as CoreDataXPath present sophisticated notions of bisimulation which defy a straightforward comonadic encoding. In this work we begin the comonadic treatment of data-aware logics by introducing a generalisation of Modal Logic that allows relation symbols of arbitrary arity as atoms of the syntax, which we call Path Predicate Modal Logic or PPML. We motivate this logic as arising from a shift in perspective on a already studied restricted version of CoreDataXPath, called DataGL, and prove that PPML recovers DataGL for a specific choice of signature. We argue that this shift in perspective allows the capturing and designing of new data-aware logics. On the other hand, PPML enjoys an intrinsic motivation in that it extends Modal Logic to predicate over more general models. Having defined the simulation and bisimulation games for PPML and having proven a Hennessy-Milner-type theorem, we define the PPML comonad and prove that it captures these games, following analogous results in the literature. Our treatment is novel in that we explicitly prove that our comonad satisfies the axioms of arboreal categories and arboreal covers. Using the comonadic machinery, we immediately obtain a tree-model property for PPML. Finally, we define a translation functor from relational structures into Kripke structures and use its properties to prove a series of polynomial-time reductions from PPML problems to their Basic Modal Logic counterparts. Our results explain precisely in what sense PPML lets us view general relational structures through the modal lens.

翻译：博弈共单子为有限模型理论中的比较博弈提供了范畴语义，从而为广泛逻辑（每种逻辑通过特定的共单子选择来刻画）的逻辑等价性给出了抽象特征。然而，像CoreDataXPath这类数据感知逻辑提出了复杂的互模拟概念，难以直接进行共单子编码。在本工作中，我们通过引入一种允许任意元数关系符号作为语法原子的模态逻辑推广（称为路径谓词模态逻辑即PPML），开启了数据感知逻辑的共单子化处理。我们论证了该逻辑源于对已有受限制版CoreDataXPath（称为DataGL）的视角转换，并证明PPML在特定签名选择下可还原为DataGL。我们主张这种视角转换能够捕获和设计新的数据感知逻辑。另一方面，PPML具有内在动因：它将模态逻辑扩展为对更一般模型进行谓词化。在定义PPML的模拟博弈和互模拟博弈并证明Hennessy-Milner型定理后，我们定义了PPML共单子，并依据文献中的类比结果证明该共单子捕获了这些博弈。本工作的新颖之处在于明确证明了我们的共单子满足树状范畴与树状覆盖的公理。利用共单子机制，我们立即得到PPML的树模型性质。最后，我们定义了从关系结构到Kripke结构的翻译函子，并利用其性质证明了从PPML问题到基本模态逻辑对应问题的一系列多项式时间归约。我们的结果精确阐明了PPML如何让我们通过模态透镜来观察一般关系结构。