English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Game comonads give a categorical semantics for comparison games in FiniteModel Theory, thus providing an abstract characterisation of logicalequivalence for a wide range of logics, each one captured through a specificchoice of comonad. However, data-aware logics such as CoreDataXPath presentsophisticated notions of bisimulation which defy a straightforward comonadicencoding. In this work we begin the comonadic treatment of data-aware logics byintroducing a generalisation of Modal Logic that allows relation symbols ofarbitrary arity as atoms of the syntax, which we call Path Predicate ModalLogic or PPML. We motivate this logic as arising from a shift in perspective ona already studied restricted version of CoreDataXPath, called DataGL, and provethat PPML recovers DataGL for a specific choice of signature. We argue thatthis shift in perspective allows the capturing and designing of new data-awarelogics. On the other hand, PPML enjoys an intrinsic motivation in that itextends Modal Logic to predicate over more general models. Having defined thesimulation and bisimulation games for PPML and having proven aHennessy-Milner-type theorem, we define the PPML comonad and prove that itcaptures these games, following analogous results in the literature. Ourtreatment is novel in that we explicitly prove that our comonad satisfies theaxioms of arboreal categories and arboreal covers. Using the comonadicmachinery, we immediately obtain a tree-model property for PPML. Finally, wedefine a translation functor from relational structures into Kripke structuresand use its properties to prove a series of polynomial-time reductions fromPPML problems to their Basic Modal Logic counterparts. Our results explainprecisely in what sense PPML lets us view general relational structures throughthe modal lens.

A Modal Logic with n-ary Relations Over Paths: Comonadic Semantics and Expressivity