Game comonads provide 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. Motivated by the goal of applying comonadic tools to the study of data-aware logics such as CoreDataXPath, in this work we introduce 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 previously studied fragment 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. We introduce resource-bounded simulation and bisimulation games for PPML and show the Hennessy-Milner property relating bisimilarity and logical equivalence. We define the PPML comonad and prove that it captures these games. We develop the model-theoretical understanding of PPML by making systematic use of the comonadic framework. This includes results such as a tree-model property and an alternative proof of the one-way Hennessy-Milner property using a correspondence between positive PPML formulas and canonical models. We also use the comonadic perspective to establish connections with other logics, such as bounded quantifier rank and bounded variable number fragments of First Order Logic on one side and Basic Modal Logic on the other, and show how the PPML comonad induces a syntax-free characterisation of logical equivalence for DataGL, our original motivation. With respect to Basic Modal Logic, a functorial assignment from PPML unravellings into Kripke trees enables us to obtain polynomial-time reductions from PPML problems to their Basic Modal Logic counterparts.

翻译：博弈余单子为有限模型论中的比较博弈提供了范畴语义，从而为广泛逻辑的逻辑等价性提供了抽象刻画，每种逻辑通过特定余单子的选择得以捕获。受将余单子工具应用于数据感知逻辑（如CoreDataXPath）研究的目标驱动，本文引入一种模态逻辑的泛化形式，允许任意元数关系符号作为语法原子，我们称之为路径谓词模态逻辑（PPML）。我们通过视角转换论证该逻辑源于先前研究的CoreDataXPath片段DataGL，并证明对于特定签名选择，PPML可还原为DataGL。我们认为这种视角转换有助于捕获和设计新的数据感知逻辑。我们为PPML引入资源有界模拟与互模拟博弈，并建立关联互模拟性与逻辑等价的Hennessy-Milner性质。我们定义PPML余单子并证明其可捕获这些博弈。通过系统运用余单子框架，我们发展了PPML的模型理论理解，包括树模型性质等结果，以及利用正PPML公式与典范模型对应关系对单向Hennessy-Milner性质的替代证明。我们还借助余单子视角建立与其他逻辑的关联：一方面与有界量词秩及有界变量数一阶逻辑片段，另一方面与基本模态逻辑，并展示PPML余单子如何为原始动机DataGL诱导出无语法的逻辑等价刻画。相对于基本模态逻辑，从PPML展开到Kripke树的函子化赋值使我们能够将PPML问题多项式时间归约至对应的基本模态逻辑问题。