Abstract Game comonads provide categorical semantics for comparison games in Finite Model Theory, thus providing an abstract characterization 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 generalization 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. On the other hand, PPML enjoys an intrinsic motivation in that it extends Modal Logic to predicate over more general models. Having introduced resource-bounded simulation and bisimulation games for PPML together with a proof of the Hennessy–Milner property relating bisimilarity and logical equivalence, we define the PPML comonad, which essentially amounts to an unravelling construction on models of PPML, and prove that it captures these games, following analogous results in the literature. However, we depart from the literature in our proof strategy, since we draw upon the axiomatic framework of arboreal categories, giving intuition for the axioms involved and supplying detailed verifications. Subsequently, 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 characterization 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.
Figueira et al. (Fri,) studied this question.