Modal Logic with Relations over Paths: a Theoretical Development through Comonadic Semantics

TL;DR

This work introduces Path Predicate Modal Logic ${\rm PPML}$, a modal language that allows relation symbols of arbitrary arity as atoms, enabling modal reasoning on general relational structures and data-aware logics. It develops a comprehensive comonadic semantics via a family of idempotent comonads ${\mathbb{C}}_k$, equipping ${\rm PPML}$ with a tree-like model theory, a tree-model property, and a Hennessy–Milner style correspondence through resource-bounded bisimulations. By establishing an arboreal-category framework and a translation functor ${K}$, the paper links ${\rm PPML}$ to Basic Modal Logic and First-Order Logic fragments (bounded quantifier rank and bounded variable count), enabling polynomial reductions for k-bisimilarity, model checking, and satisfiability, and showing DataGL to be equi-expressive within this setting. It further demonstrates that ${\rm PPML}$ provides a flexible framework for designing data-aware logics, captures DataGL by embedding data into equal-data relations, and opens avenues for extending to other data-aware logics and relative comonads. Overall, the work unifies modal, comonadic, and data-aware logics into a coherent theory with concrete complexity and model-theoretic consequences, while suggesting practical reductions and new directions for logic design and semantic methodology.

Abstract

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.

Figures (5)

• Figure 1: Two pointed $\sigma$-structures for $\sigma=\{E, S\}$, where $S$ is binary, given by $E^\mathcal{A} = \{a\}\times\{a_1,a_2,a_3,a_4\}$, $S^\mathcal{A} = \{(a,a_3),(a_3,a),(a,a_4),(a_4,a)\}$, $E^\mathcal{B} = \{b\}\times\{b_1,b_2,b_3\}$ and $S^\mathcal{B} = \{(b,b_2),(b_2,b)\}$. $E$ is represented by bold arrows, while $S$, being symmetric in these example structures, is represented by two-headed dotted arrows. Below, we depict a $2$-bisimulation $(Z_i)_{i\leq 2}$ between witnessing that ${(\mathcal{A}, a)} \mathrel{\underline{~~}\space{\leftrightarrow}}_2 {(\mathcal{B}, b)}$. Each node of the tree contains a pair of sequences and the nested boxes represent the nested relations of the bisimulation.
• Figure 2: The structures $\mathcal{A}$ and $\mathcal{B}$ from Figure \ref{['fig:example_bisimilar_structures']} and their ${\rm PPML}$-unravellings $\mathbb{C}_2 {(\mathcal{A}, a)}$ and $\mathbb{C}_2 {(\mathcal{B}, b)}$.
• Figure 3: A span of bounded morphisms between the unravellings $\mathbb{C}_2(\mathcal{A},a)$ and $\mathbb{C}_2(\mathcal{B},b)$ of the structures ${(\mathcal{A}, a)}$, ${(\mathcal{B}, b)}$ as in Figures \ref{['fig:example_bisimilar_structures']} and \ref{['fig:pptrees']}. The left leg of the span is an isomorphism (there are two possible choices), while the dashed arrows indicate how the right leg acts on each point. By Corollary \ref{['coro:full_logical_equivalence']}, the existence of this span of bounded morphisms shows that ${(\mathcal{A}, a)} \equiv_2 {(\mathcal{B}, b)}$.
• Figure 4: a) An example of a ${\rm DataGL}$ model $\mathfrak{M}$ (in particular a data tree) with $\text{PROP} = \{p, q\}$ and $\mathbb{D}$ equal to the set of integers. Notice how $\mathfrak{M}$ is a valid ${\rm DataGL}$ model (Def. \ref{['def:datagl_model_and_semantics']}) since $R$ is the transitive closure of the accessibility relation of a tree, and hence it is transitive irreflexive. b) The corresponding $\sigma_{\rm DGL}$-structure ${t \, \mathfrak{M}}$ (Def. \ref{['def:datagl_model_to_sigma_structure']}), where each point is labelled with the set of unary relation symbols that are true at that point.
• Figure 5: $\sigma_{\rm DGL}$-structures which are $k$-bisimilar for all $k$. Bold arrows represent $E$ and dotted arrows represent $R_=$. $\psi_1 \coloneqq \Diamond (\lnot R_= \land \Diamond (\lnot R_= \land \lnot T))$ is true in ${(\mathcal{A}, a)}$ but false in ${(\mathcal{B}, b)}$, hence $\psi_1$ is not expressible in $\sigma_{\rm DGL}$-${\rm PPML}$.

Theorems & Definitions (136)

• Definition 1
• Remark 2
• Definition 3
• Example 4
• Definition 5
• Remark 6
• Remark 7
• Definition 8
• Example 9
• proof