=Paper=
{{Paper
|id=Vol-3263/paper-5
|storemode=property
|title=Comonadic Semantics for Description Logics Games
|pdfUrl=https://ceur-ws.org/Vol-3263/paper-5.pdf
|volume=Vol-3263
|authors=Bartosz Bednarczyk,Mateusz Urbańczyk
|dblpUrl=https://dblp.org/rec/conf/dlog/BednarczykU22
}}
==Comonadic Semantics for Description Logics Games==
<pdf width="1500px">https://ceur-ws.org/Vol-3263/paper-5.pdf</pdf>
<pre>
Comonadic Semantics for Description Logic Games
Bartosz Bednarczyk1,2 , Mateusz Urbańczyk2
1
    Computational Logic Group, Technische Universität Dresden, Germany
2
    Institute of Computer Science, University of Wrocław, Poland


                                         Abstract
                                         A categorical approach to study model comparison games in terms of comonads was recently initiated by
                                         Abramsky et al. In this work, we analyse games that appear naturally in the context of description logics
                                         and supplement them with suitable game comonads. More precisely, we consider expressive sublogics
                                         of 𝒜ℒ𝒞 Self ℐb𝒪, namely, the logics that extend 𝒜ℒ𝒞 with any combination of inverses, nominals, safe
                                         boolean roles combinations and the Self operator. Our construction augments and modifies the so-called
                                         modal comonad by Abramsky and Shah. The approach that we took heavily relies on the use of relative
                                         comonads, which we leverage to encapsulate additional capabilities within the bisimulation games in a
                                         compositional manner.

                                         Keywords
                                         comonads, category theory, bisimulations, expressive power, games, coalgebraic semantics




1. Introduction
Following [1], there are two different views on the fundamental features of computation, that
can be summarised as “structure” and “power” as follows:
                  • Structure: Compositionality and semantics, addressing the question of mastering the
                    complexity of computer systems and software.
                  • Power: Expressiveness and complexity, addressing the question of how we can harness
                    the power of computation and recognize its limits.
It turned out that there are almost disjoint communities of researchers studying Structure and
Power, with seemingly no common technical language and tools. To encounter this issue, Samson
Abramsky and Anuj Dawar started a project, whose goal is to provide category-theoretical
toolkit to reason about finite model theory. Their approach, described e.g. in [2], employs
comonads on the category of relational structures in order to capture model comparison games
such as Ehrenfeucht-Fraissé, pebbling, and bisimulation games [2] as well as games for Hybrid
logics [3] and Guarded Fragment [4]. The structure allows us to leverage the tool of category
theory, and apply it to generalise known established theorems, as it was done in [5, 6].
   In this paper, we continue the exploration of suitable game comonads by incorporating the
comonadic semantics for description logics games, namely, for expressive description logics
  DL 2022: 35th International Workshop on Description Logics, August 7–10, 2022, Haifa, Israel
" bartosz.bednarczyk@cs.uni.wroc.pl (B. Bednarczyk); mateusz.urbanczyk97@gmail.com (M. Urbańczyk)
~ https://bartoszjanbednarczyk.github.io/ (B. Bednarczyk)
 0000-0002-8267-7554 (B. Bednarczyk)
                                       © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)
between 𝒜ℒ𝒞 and 𝒜ℒ𝒞 Self ℐb𝒪.1 It is also worth mentioning a parallel research that defines
categorical semantics for 𝒜ℒ𝒞 [7, 8], however, the approach is much different from ours, as we
focus solely on games and leave 𝒜ℒ𝒞 in the standard set-theoretic semantics.

1.1. Our Results
In what follows, we change setting established in the previous work from the category of
relational structures, to a category of pointed interpretations that are parametrised by subsets
of role names, concept names and individual names.
   We start with defining comonadic semantics for 𝒜ℒ𝒞-bisimulation-games. It is well-known
that 𝒜ℒ𝒞 is a notational variant of a multi-modal logic; hence, we employ this observation to
take the full advantage of existing results on modal logic from [2] and use them as the base for
our further investigations. In order to define comonadic semantics for DLs ℒ ⊆ 𝒜ℒ𝒞 Self ℐb𝒪,
instead of providing it directly for them (and thus repeating all the required proofs from [2]),
we follow a different route. We provide a family of game reductions from ℒ to weaker sublogics,
ending up on 𝒜ℒ𝒞, which transform interpretations in such a way that a winning strategy
in ℒ-bisimulation-game is equivalent to a winning strategy in 𝒜ℒ𝒞-bisimulation-game for a
suitably transformed interpretations. From a categorical point of view, we introduce a comonad
for 𝒜ℒ𝒞 logic and reductions shall be defined by functors, on which we will build relative
comonads to encapsulate the additional capabilities available in an ℒ-bisimulation-game. By
composing the reduction functors together, we shall obtain comonadic semantics for all of the
games for considered logics.


2. Preliminaries
We start with a recap of notions from category theory [9, 10], such as comonads, as well as
from description logics, for which we define their syntax, semantics and bisimulations [11]. By
doing so, we would like to unify the context for readers from different backgrounds.

2.1. Preliminaries on DLs
We fix infinite mutually disjoint sets of individual names NI , concept names NC , and role
names NR . We will briefly recap syntax and semantics of 𝒜ℒ𝒞 Self ℐb𝒪-concepts and as well
as ℒ-concepts for relevant sublogics ℒ of 𝒜ℒ𝒞 Self ℐb𝒪. The following EBNF grammar defines
atomic concepts B, concepts C, atomic roles r , simple roles s with o ∈ NI , A ∈ NC , p ∈ NR :

                      B ::= A | {o}, C ::= B | ¬C | C ⊓ C | ∃s.C | ∃s.Self
                      r ::= p | p − , s ::= r | s ∩ s | s ∪ s | s ∖ s

   The semantics of 𝒜ℒ𝒞 Self ℐb𝒪-concepts is defined via interpretations ℐ = (∆ℐ , ·ℐ ) composed
of a non-empty set ∆ℐ called the domain of ℐ and an interpretation function ·ℐ mapping indi-
vidual names to elements of ∆ℐ , concept names to subsets of ∆ℐ , and role names to subsets of

1
    It will become clear why we write 𝒜ℒ𝒞 Self ℐb𝒪 instead of 𝒜ℒ𝒞𝒪ℐbSelf later.
∆ℐ × ∆ℐ . This mapping is then extended to complex concepts and roles (cf. Table 1). The rank
of a concept is the maximal nesting-depth of ∃-restrictions.
   The 𝒜ℒ𝒞-concepts are obtained by dropping from the syntax the inversions of roles (ℐ),
safe boolean combination of roles (b) (i.e. union, intersection and difference), nominals (𝒪)
and the Self operator (Self). ℒ-concepts for other sublogics ℒ of 𝒜ℒ𝒞 Self ℐb𝒪 are defined
similarly. We stress here that role union/intersection/difference, the Self operator, role inverse
·− and nominals {·} are operators and they do not introduce neither new role names nor new
concept names. We will find it convenient to employ expressions of the form 𝒜ℒ𝒞Φ or ℒΦ with
Φ ⊆ {𝒪, ℐ, Self, b} to speak collectively about different expressive sublogics of 𝒜ℒ𝒞 Self ℐb𝒪.

         Name                                  Syntax Semantics
         conc. negation                       ¬C        ∆ℐ ∖ Cℐ
         conc. intersection                 C⊓D         Cℐ ∩ Dℐ
         exist. restriction                  ∃r .C      { d | ∃e.(d, e) ∈ r ℐ ∧ e ∈ Cℐ }
         nominal op.                          {o}       {oℐ }
         inverse role op.                     p−        {(d, e) | (e, d) ∈ p ℐ }
         role boolean op. for ⊕ ∈ {∪, ∩, ∖} s1 ⊕ s2     s1ℐ ⊕ s2ℐ
         Self op.                           ∃s.Self     {d | (d, d) ∈ s ℐ }

                         Table 1: Concepts and roles in 𝒜ℒ𝒞 Self ℐb𝒪.

  Any triple 𝒱 ≜ (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟 ) from NI × NC × NR having finite components will be called
a vocabulary. We often speak about ℒ(𝒱)-concepts i.e. those ℒ-concepts that employ only
symbols from 𝒱. For a pointed interpretation (ℐ, d) we say that it satisfies a concept C (written:
(ℐ, d) |= C) if d ∈ Cℐ . An 𝒱-pointed-interpretation (ℐ, d) is a partial interpretation, where all
indv-names outside 𝒱 are left undefined while other other symbols outside 𝒱 are interpreted as ∅.

2.2. Preliminaries on Category Theory
We assume familiarity with basic concepts such as categories, functors or natural transforma-
tions. Let C and D be categories. We write |C| to denote morphisms (arrows) of C and 𝑓 ∈ |C|
to indicate that 𝑓 is a morphism in C. Let 𝐺 : C → C be a functor and 𝜀 : C ⇒ 1C a natural
transformation, with 1C being the identity functor on C. A comonad 𝐺 is a triple (𝐺, 𝜀, (·)* ),
where 𝜀 is called the counit of 𝐺 that for each object 𝐴 it gives us an arrow 𝜀𝐴 : 𝐺𝐴 → 𝐴,
while (·)* , called the Kleisli coextension of 𝐺, is an operator sending each arrow 𝑓 : 𝐺𝐴 → 𝐵
to 𝑓 * : 𝐺𝐴 → 𝐺𝐵. These has to satisfy, for all 𝑓 : 𝐺𝐴 → 𝐵 and 𝑔 : 𝐺𝐵 → 𝐶, the equations:

          𝜀*𝐴 = 1𝐺𝐴 ,                𝜀𝐵 ∘ 𝑓 * = 𝑓,                (𝑔 ∘ 𝑓 * )* = 𝑔 * ∘ 𝑓 *

Furthermore, we define coKleisli category Kl(𝐺), with objects from C and arrows from 𝐴 to 𝐵
given by the arrows in C of the form 𝐺𝐴 → 𝐵, where composition 𝑔 ∙ 𝑓 is given by 𝑔 ∘ 𝑓 * .
   We shall also need the notion of relative comonads [12]. Given a functor 𝐽 : C → D, and
a comonad 𝐺 on D, we obtain a relative comonad on C, whose coKleisli category is defined
as follows. A morphism from 𝐴 to 𝐵, for objects 𝐴, 𝐵 of C, is a D-arrow 𝐺𝐽𝐴 → 𝐽𝐵. The
counit at 𝐴 is 𝜀𝐽𝐴 , using the counit of 𝐺 at 𝐽𝐴. Given 𝑓 : 𝐺𝐽𝐴 → 𝐽𝐵, the Kleisli coextension
𝑓 * : 𝐺𝐽𝐴 → 𝐺𝐽𝐵 is the Kleisli coextension of G. Since G is a comonad, these operations
satisfy the equations for a comonad in Kleisli form. We write this as (𝐺 ∘ 𝐽)-relative-comonad.

2.3. Bisimulation Games
Let 𝒱 be a vocabulary. Following [13], we recap the notion of bisimulation games for 𝒜ℒ𝒞 and
its extensions. Call d ∈ ∆ℐ and e ∈ ∆𝒥 to be in 𝒱-harmony 2 if for all concept names C ∈ 𝜎𝑐 we
have that d ∈ Cℐ iff e ∈ C𝒥 . The 𝒜ℒ𝒞(𝒱)-bisimulation game is played by two players, Spoiler
(he) and Duplicator (she), on two pointed interpretations (ℐ, d0 ) and (𝒥 , e0 ). A configuration
of a game is a quartet of the form (ℐ, 𝑠; 𝒥 , 𝑠′ ), where 𝑠 and 𝑠′ are words from, respectively,
∆ℐ (𝜎𝑟 ∆ℐ )* and ∆𝒥 (𝜎𝑟 ∆𝒥 )* . Intuitively, configurations encode not only the current position
of the play, but also its full play history. The initial configuration is simply (ℐ, d0 ; 𝒥 , e0 ). The
0-th round of the game starts in the initial configuration and we require that d0 and e0 are in
𝒱-harmony. If not, then immediately Spoiler wins. For any configuration (ℐ, 𝑠d; 𝒥 , 𝑠′ e) (where
the sequences 𝑠, 𝑠′ may be empty) in the game, the following rules apply:
     (a) In each round, Spoiler picks one of the two interpretations, say ℐ. Then he picks a role
         name r ∈ 𝜎𝑟 and takes an element d′ ∈ ∆ℐ such that (♡): (d, d′ ) ∈ r ℐ . If there is no
         such role name r and an element d′ , then Duplicator wins.
     (b) Duplicator responds in the other interpretation, 𝒥 , by picking the same role name r ∈ 𝜎𝑟
         as Spoiler did and an element e′ ∈ ∆ℐ in 𝒱-harmony with d′ , witnessing (♣): (e, e′ ) ∈ r 𝒥 .
         If there is no such role name r or an element e′ , Spoiler wins.
The game continues from the position (ℐ, 𝑠dr d′ ; 𝒥 , 𝑠′ er e′ ). Duplicator has a winning strategy
in the game on (ℐ, d0 ; 𝒥 , e0 ) if she can respond to every move of Spoiler so that she either wins
the game or can survive 𝜔 rounds. We define winning strategies in 𝑘-round games analogously.
   The above game is adjusted to the case of expressive sublogics ℒΦ of 𝒜ℒ𝒞 Self ℐb𝒪 as follows.
        • If 𝒪 ∈ Φ, then we extend the definition of 𝒱-harmony with a condition “for all o ∈ 𝜎𝑖
          we have that d = oℐ iff e = o𝒥 ”.
        • If Self ∈ Φ, then we extend the definition of 𝒱-harmony with a condition “for all r ∈ 𝜎𝑟
          we have that (d, d) ∈ r ℐ iff (e, e) ∈ r 𝒥 ”.
        • If ℐ ∈ Φ, then in Spoiler’s move the condition (♡) additionally allows for (d′ , d) ∈ r ℐ .
          Then in the corresponding move of Duplicator, the condition (♣) imposes (e′ , e) ∈ r 𝒥 .
        • If b ∈ Φ, then for the element e′ we additionally extend (♣) in order to fulfil the equality
          {r ∈ 𝜎𝑟 | (d, d′ ) ∈ r ℐ } = {r ∈ 𝜎𝑟 | (e, e′ ) ∈ r 𝒥 }. Moreover, in case of ℐ ∈ Φ, then also
          {r ∈ 𝜎𝑟 | (d′ , d) ∈ r ℐ } = {r ∈ 𝜎𝑟 | (e′ , e) ∈ r 𝒥 } must hold.
   To simplify reasoning about bisimulation games, we employ the well-known notion of
bisimulation, which can be seen as the “encoding” of winning strategies of Duplicator. Let ℒΦ
be an expressive sublogic of 𝒜ℒ𝒞 Self ℐb𝒪⋃︀and 𝑘 ∈ N ∪ {𝜔}. Following [14], the ℒΦ(𝒱)-𝑘-
bisimulation between ℐ and 𝒥 is a set 𝒵 ⊆ 𝑘ℓ=0 (∆ℐ )𝑘 × (∆𝒥 )𝑘 satisfying the following seven
conditions for all o ∈ 𝜎𝑖 , C ∈ 𝜎𝑐 , r ∈ 𝜎𝑟 , d, d′ ∈ ∆ℐ , 𝑠 ∈ (∆ℐ )* and e, e′ ∈ ∆𝒥 , 𝑠′ ∈ (∆𝒥 )* :
2
    For 𝒜ℒ𝒞 we do not actually use 𝜎𝑖 and 𝜎𝑟 , but they will be useful for other logics.
      (a) If 𝒵(𝑠d, 𝑠′ e) then d ∈ Cℐ iff e ∈ C𝒥 .
     (b) If 𝒵(𝑠d, 𝑠′ e) and (d, d′ ) ∈ r ℐ then there is e′ ∈ ∆𝒥 s.t. (e, e′ ) ∈ r 𝒥 and 𝒵(𝑠dd′ , 𝑠′ ee′ ).
      (c) If 𝒵(𝑠d, 𝑠′ e) and (e, e′ ) ∈ r 𝒥 then there is d′ ∈ ∆𝒥 s.t. (d, d′ ) ∈ r ℐ and 𝒵(𝑠dd′ , 𝑠′ ee′ ).
     (d) If 𝒪 ∈ Φ, then 𝒵(𝑠d, 𝑠′ e) implies d = oℐ iff e = o𝒥 .
      (e) If Self ∈ Φ, then 𝒵(𝑠d, 𝑠′ e) implies (d, d) ∈ r ℐ iff (e, e) ∈ r 𝒥 .
      (f) If ℐ ∈ Φ, then 𝒵(𝑠d, 𝑠′ e) and (d′ , d) ∈ r ℐ implies that there is e′ ∈ ∆𝒥 s.t. (e′ , e) ∈ r 𝒥
          and 𝒵(𝑠dd′ , 𝑠′ ee′ ).
     (g) If b ∈ Φ, then if 𝒵(𝑠d, 𝑠′ e) and (d, d′ ) ∈ r ℐ implies that there is e′ ∈ ∆𝒥 satisfying
         𝒵(𝑠dd′ , 𝑠′ ee′ ) and {r ∈ 𝜎𝑟 | (d, d′ ) ∈ r ℐ } = {r ∈ 𝜎𝑟 | (e, e′ ) ∈ r 𝒥 } . If ℐ ∈ Φ, then
         also {r ∈ 𝜎𝑟 | (d′ , d) ∈ r ℐ } = {r ∈ 𝜎𝑟 | (e′ , e) ∈ r 𝒥 }.
                          ℒΦ(𝒱)
We write (ℐ, d) ≡𝑘        (𝒥 , e) iff d and e satisfy the same ℒΦ(𝒱)-concepts of rank at most
𝑘 (as before, here 𝑘 can be also 𝜔). The following fact for most of considered logics is either
well-known (see [13], in particular Prop. 2.1.3 and related chapters) or can be established by
tiny modifications of existing proofs.

Fact 2.1. For any 𝑘 ∈ N ∪ {𝜔} and a logic ℒΦ between 𝒜ℒ𝒞 and 𝒜ℒ𝒞 Self ℐb𝒪, t.f.a.e.:

        • Duplicator has the winning strategy in the 𝑘-round ℒΦ(𝒱)-bisim-game on (ℐ, d; 𝒥 , e),
        • There is an ℒΦ(𝒱)-𝑘-bisimulation 𝒵 between ℐ and 𝒥 such that 𝒵(d, e),
                     ℒΦ(𝒱)
        • (ℐ, d) ≡𝑘          (𝒥 , e).


3. Reductions Between Games and Logics
Herein we establish reductions, based on appropriate model transformations, that will allow us
for transferring winning strategies of Duplicator from richer logics to weaker ones, ending up
on 𝒜ℒ𝒞. All of them, except the case of nominals, will be trivial. Such transformation will be
essential in Section 5, where we will employ them in the construction of relative comonads.
   We will denote the game reductions for logic extensions Φ by fΦ , which has two components
fΦ and f*Φ , that define actions on, respectively, the interpretation and the distinguished element.
 ℐ

   We first handle the Self operator. Let 𝜎𝑐Self ≜ 𝜎𝑐 ∪ {CSelf.r | r ∈ 𝜎𝑟 }. By the self-enrichment
of a 𝒱 ≜ (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟 )-interpretation ℐ we mean the 𝒱 Self ≜ (𝜎𝑖 , 𝜎𝑐Self , 𝜎𝑟 )-interpretation ℐSelf ,
where the (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟 )-reduct3 of ℐSelf is equal to ℐ, and the interpretation of CSelf.r concepts
is defined as (CSelf.r )ℐSelf = (∃r .Self)ℐ . Let fSelf be the described transformation, mapping ℐ
to ℐSelf . The following proposition is immediate from the semantics of Self:

Proposition 3.1. Let 𝑘 ∈ N ∪ {𝜔} and let ℒ be a DL satisfying 𝒜ℒ𝒞 ⊆ ℒ ⊆ 𝒜ℒ𝒞ℐb𝒪. Then
Duplicator has a winning strategy in a 𝑘-round ℒSelf (𝒱)-bisimulation game on (ℐ, d; 𝒥 , e) iff
she has a winning strategy in a 𝑘-round ℒ(𝒱)-bisimulation game on (fSelf (ℐ), d; fSelf (𝒥 ), e).


3
    i.e. the interpretation obtained from ℐSelf by omitting the interpretation of symbols outside 𝜎𝑖 ∪ 𝜎𝑐 ∪ 𝜎𝑟 .
Proof. Employ Fact 2.1 after observing that due to the choice of 𝜎𝑐Self the ℒSelf (𝒱)-𝑘-bisimulation
between ℐ and 𝒥 is a ℒ(𝒱 Self )-𝑘-bisimulation between fSelf (ℐ) and fSelf (𝒥 ) and vice-versa.

   Our next goal is to incorporate inverses of roles. Let 𝜎𝑟ℐ ≜ 𝜎𝑟 ∪ {rinv | r ∈ 𝜎𝑟 } By the inverse-
enrichment of a 𝒱 ≜ (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟 )-interpretation ℐ we mean the 𝒱 ℐ ≜ (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟ℐ )-interpretation
ℐℐ , where the (𝜎𝑖 , 𝜎𝑐 , ∅)-reducts of ℐ and ℐℐ are equal, and the interpretations of role names
rinv are defined as (rinv )ℐℐ = (r − )ℐ . Let fℐ be the described transformation, mapping ℐ to ℐℐ .
The following follows analogously to Proposition 3.1:

Proposition 3.2. Let 𝑘 ∈ N ∪ {𝜔} and let ℒ be a DL satisfying 𝒜ℒ𝒞 ⊆ ℒ ⊆ 𝒜ℒ𝒞𝒪b. Then
Duplicator has a winning strategy in a 𝑘-round ℒℐ(𝒱)-bisimulation game on (ℐ, d; 𝒥 , e) iff she
has a winning strategy in a 𝑘-round ℒ(𝒱 ℐ )-bisimulation game on (fℐ (ℐ), d; fℐ (𝒥 ), e).

   We focus next on safe boolean combination of roles. Given a finite 𝜎𝑟 ⊆ NR , let 𝜎𝑟b be
composed of role names having the form r𝑆 , where 𝑆 is any non empty subset of 𝜎𝑟 . By the b-
enrichment of a 𝒱 ≜ (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟 )-interpretation ℐ we mean the 𝒱 b ≜ (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟b )-interpretation
ℐb , where the (𝜎𝑖 , 𝜎𝑐 , ∅)-reducts of ℐ and ℐb are equal and the interpretation of role names r𝑆 ∈
𝜎𝑟b is defined as {(d, e) | {r ∈ 𝜎𝑟 | (d, e) ∈ r ℐ } = 𝑆}. Let fb be the described transformation,
mapping ℐ to ℐb . Once more, the following proposition is straightforward:

Proposition 3.3. Let 𝑘 ∈ N ∪ {𝜔} and let ℒ be a DL satisfying 𝒜ℒ𝒞 ⊆ ℒ ⊆ 𝒜ℒ𝒞𝒪. Then
Duplicator has a winning strategy in a 𝑘-round ℒb(𝒱)-bisimulation-game on (ℐ, d; 𝒥 , e) iff she
has a winning strategy in a 𝑘-round ℒ(𝒱 b )-bisimulation-game on (fb (ℐ), d; fb (𝒥 ), e).

   Finally, we proceed with the case of nominals. In this case we need to be extra careful, as the
comonads introduces in the next section will act as unravelling on interpretations, and we do
not want to create multiple copies of a nominal. Recall that the Gaifman graph Gℐ = (𝑉ℐ , 𝐸ℐ )
of an interpretation ℐ is a simple undirected graph whose nodes are domain elements from ∆ℐ
and an edge exist between two nodes when there is a role that connects them in ℐ.
   Let 𝜎𝑐𝒪 ≜ 𝜎𝑐 ∪ {Co,r | o ∈ 𝜎𝑖 , r ∈ 𝜎𝑟 } and 𝜎𝑟𝒪 ≜ 𝜎𝑟 ∪ {ro | o ∈ 𝜎𝑖 }. By the
nominal-enrichment of a 𝒱 ≜ (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟 )-interpretation ℐ we mean the 𝒱 𝒪 ≜ (𝜎𝑖 , 𝜎𝑐𝒪 , 𝜎𝑟𝒪 )-
interpretation ℐ𝒪 defined in the following steps:

    • First, we get rid of unreachable elements from ℐ. More precisely, let 𝒥 to be the substruc-
      ture of ℐ restricted to the set of all elements reachable in (finitely-many steps) from d in
      Gℐ . W.l.o.g., assume that all oℐ for o ∈ 𝜎𝑖 are reachable.
    • For every o ∈ 𝜎𝑖 and every d ∈ ∆ℐ for which there is an r -connection between d
      and oℐ , we insert a “trampoline” element labelled by the unique concept name Co,r and
      we r -connect it with d. Trampoline elements are used to bookkeep information about
      connections between elements and named elements. Let 𝒥 be the resulting interpretation.
    • We next divide 𝒥 into components. Let 𝒥d and 𝒥o for o ∈ 𝜎𝑖 be induced subinter-
      pretations of 𝒥 obtained by removing all elements {oℐ | o ∈ 𝜎𝑖 } from 𝒥 except the
      element mentioned in the subscript (that serve the role of distinguished elements of the
      components). Take 𝒥 ′ to be the disjoint sum of the components.
       • Finally, we will link components. For all o ∈ 𝜎𝑖 , take disto be the length of the short-
                                                                                   ′
         est path from d to oℐ in Gℐ . We will connect d to o𝒥 by a dummy path of length
                                                                                                         ′
         precisely disto . Thus, we introduce dummy elements do1 , . . . , dodisto −1 to ∆𝒥 and em-
         ploy the fresh role name ro , whose interpretation will contains precisely the pairs
                                                          ′
         (d, do1 ), (do1 , do2 ), . . . , (dodisto −1 , o𝒥 ). The resulting interpretation is the desired ℐ𝒪 .
      Let f𝒪 be the described transformation, mapping ℐ to ℐ𝒪 . In Appendix we show that
Lemma 3.4. Let 𝑘 ∈ N ∪ {𝜔}. Duplicator has a winning strategy in a 𝑘-round 𝒜ℒ𝒞𝒪(𝒱)-
bisimulation game on (ℐ, d) and (𝒥 , e) iff she has a winning strategy in a 𝑘-round 𝒜ℒ𝒞(𝒱 𝒪 )-
bisimulation game on (f𝒪 (ℐ), d) and (f𝒪 (𝒥 ), e).
  We wrap up the above reductions, with a goal that the winning strategy of Duplicator in
an ℒΦ-bisimulation game is equivalent to the winning strategy in a certain 𝒜ℒ𝒞-bisimulation
game. Note that the order of applications of reduction matters, e.g. we should apply first the fℐ
reduction, and only then fb ; otherwise we will not get all possible combinations of roles with
inverse. Hence, we first proceed with fSelf reduction, then with fℐ , with fb and finally with f𝒪 .
Let fΦ be a composition of reductions for extensions Φ ∈ {Self, ℐ, b, 𝒪} in the above order.
Theorem 3.5. Let 𝑘 ∈ N ∪ {𝜔} and ℒΦ satisfy 𝒜ℒ𝒞 ⊆ ℒΦ ⊆ 𝒜ℒ𝒞 Self ℐb𝒪. Then Duplicator
has a winning strategy in a 𝑘-round ℒΦ(𝒱)-bisimulation game on (ℐ, d) and (𝒥 , e) iff she has a
winning strategy in a 𝑘-round ℒ(𝒱 Φ )-bisimulation game on (fΦ (ℐ), d) and (fΦ (𝒥 ), e).
Proof. The key idea here is grounded on the composition of the reduction functions. Given Φ,
we simply apply consecutively Propositions 3.1–3.3 and Lemma 3.4.


4. Game Comonads
Having defined a family of game reductions, we are going to start employing basic category
theory primitives to define denotational semantics for bisimulation games. In this section, we
focus on vanilla 𝒜ℒ𝒞. Since 𝒜ℒ𝒞 is a notational variant of the multi-modal logic, it suffices
to translate the work done in [2] to the description logic setting. Subsequently, we prove that
such definition of a “generalised game” coincides with our definition of 𝒜ℒ𝒞(𝒱)-bisimulation
game defined in Section 2.3. In what follows, we shall work in the category of pointed inter-
pretations ℛ* (𝒱) over a vocabulary 𝒱, where objects (ℐ, 𝑑) are 𝒱-pointed-interpretations, and
morphisms ℎ : (ℐ, 𝑑) → (𝒥 , 𝑒) are homomorphisms between interpretations that preserve the
distinguished element. With DLΦ  𝑘 , we will denote the corresponding game comonad, where 𝑘 is
the depth parameter and Φ ⊆ {Self, ℐ, b, 𝒪} parametrizes the set of language extensions. We
                                                       {ℐ,𝒪}                                {}
will be a bit careless and write DLℐ𝒪𝑘 in place of DL𝑘       , or likewise, DL𝑘 to denote DL𝑘 .

4.1. Comonad for 𝒜ℒ𝒞
We start with introducing the comonad for 𝒜ℒ𝒞, which will be the base for our further comonads.
Definition 4.1 (𝒜ℒ𝒞-comonad). For every 𝑘 ≥ 0, we define a comonad DL𝑘 on ℛ* (∅, 𝜎𝑐 , 𝜎𝑟 ),4
where DL𝑘 unravels (ℐ, d) from d, up to depth 𝑘. 5 More precisely:
4
    Notice ∅ in place of 𝜎𝑖 . This is because 𝒜ℒ𝒞-concepts cannot speak about individual names.
5
    For the notion of unravelling consult e.g. [11, Definition 3.21].
    • The domain of DL𝑘 (ℐ, 𝑑) is composed of sequences [𝑎0 , r0 , 𝑎1 , r2 , . . .] ∈ ∆ℐ (𝜎𝑟 ∆ℐ )* ,
      where we additionally require that (𝑎𝑖 , 𝑎𝑖+1 ) ∈ r𝑖ℐ and 𝑎0 = d. The singleton sequence
      [d] serves as the distinguished element of DL𝑘 (ℐ, 𝑑).
    • The functorial action on morphisms for DL𝑘 satisfies:
                        DL𝑘 (ℎ : (ℐ, 𝑑) → (𝒥 , 𝑒)) : DL𝑘 (ℐ, 𝑑) → DL𝑘 (𝒥 , 𝑒)
                     (DL𝑘 ℎ)[𝑎0 , 𝛼1 , 𝑎1 , ..., 𝛼𝑗 , 𝑎𝑗 ] = [ℎ 𝑎0 , 𝛼1 , ℎ 𝑎1 , ..., 𝛼𝑗 , ℎ 𝑎𝑗 ]
    • The map 𝜀ℐ : DL𝑘 (ℐ, 𝑑) → (ℐ, 𝑑) sends a sequence to its last element.
    • Concept names C ∈ 𝜎𝑐 are interpreted such that 𝑠 ∈ CDL𝑘 (ℐ,𝑑) iff 𝜀ℐ 𝑠 ∈ Cℐ .
    • For role names r ∈ 𝜎𝑟 , we put (𝑠, 𝑡) ∈ r DL𝑘 (ℐ,𝑑) iff there is 𝑑′ ∈ ∆ℐ so that 𝑡 = 𝑠[r , 𝑑′ ].
    • For a morphism ℎ : DL𝑘 (ℐ, 𝑑) → (𝒥 , 𝑒), we define Kleisli coextension ℎ* : DL𝑘 (ℐ, 𝑑) →
      DL𝑘 (𝒥 , 𝑒) recursively by ℎ* [𝑑] = [𝑒] and ℎ* (𝑠[𝛼, 𝑑′ ]) = ℎ* (𝑠)[𝛼, ℎ(𝑠[𝛼, 𝑑′ ])]).

Proposition 4.2. The triple (DL𝑘 , 𝜀, (·)* ) is a comonad in Kleisli form on ℛ* (∅, 𝜎𝑐 , 𝜎𝑟 ).

   Having the 𝒜ℒ𝒞-comonad defined, as the next step we introduce sufficient categorical
background required to define bisimulation games in an abstract-enough way. This may be a
bit heavy for readers not familiar enough with category theory.

4.2. Tree-like Structures, Paths and Embeddings
A covering relation ≺ for a partial order ≤ is a relation satisfying 𝑥 ≺ 𝑦 ≜ 𝑥 ≤ 𝑦 ∧ 𝑥 ̸=
𝑦 ∧ (∀𝑧.𝑥 ≤ 𝑧 ≤ 𝑦 =⇒ 𝑧 = 𝑥 ∨ 𝑧 = 𝑦). This is employed to define tree-like structures below,
that will intuitively serve as the description of bisimulation game strategies.

Definition 4.3. A ordered interpretation (ℐ, 𝑑, ≤) is a pointed interpretation (ℐ, d) equipped
with a partial order on ∆ℐ such that ↑ (𝑑) ≜ {𝑑′ ∈ ∆ℐ | 𝑑 ≤ 𝑑′ } is a tree order that satisfies
the following condition (D) for 𝑥, 𝑦 ∈ ↑ (𝑑), we have 𝑥 ≺ 𝑦 iff (𝑥, 𝑦) ∈ r ℐ for some r ∈ 𝜎𝑟 .
Morphisms between ordered interpretations preserve the covering relation. We put ℛ𝐷    *𝑘 (𝒱) to be
the category of ordered interpretation as objects with 𝑘 bounding the height of the underlying tree.

  We next define different kinds of embeddings, essential to characterize plays.

Definition 4.4. A morphism in ℛ𝐷    *𝑘 (𝒱) is an embedding if it is an injective strong homomor-
phism. We write 𝑒 : ℐ ↣ 𝒥 to mean that 𝑒 is an embedding. Now, we define a subcategory Paths
of ℛ* (𝒱) whose objects have tree orders that are linear, so they comprise a single branch. We say
that 𝑒 : 𝑃 ↣ ℐ is a path embedding if 𝑃 is a path. A morphism 𝑓 : ℐ → 𝒥 ∈ |ℛ𝐷           *𝑘 (𝒱)| is a
pathwise embedding if for any path embedding 𝑒 : 𝑃 ↣ ℐ, 𝑓 ∘ 𝑒 is a path embedding.

  Let ⊑ being be the lexicographical order on sequences from ∆ℐ . From the construction of
 *𝑘 (𝒱), we can extract a free functor, for which construction is justified in the Appendix:
ℛ𝐷

Lemma 4.5. There exists a canonical functor 𝐹𝑘 ℐ = (DL𝑘 (ℐ, 𝑑), ⊑).
4.3. A Categorical View on Games
Given sufficient background, we can move on to the main result, namely, to the characterisation
of ≡𝒜ℒ𝒞 𝑘 in the language of category-theory. We start with defining what does it mean for a
morphism in 𝑓 : ℐ → 𝒥 ∈ |ℛ𝐷   *𝑘 (𝒱)| to be open. This holds if, whenever we have a commutative
square (LHS) then there is an embedding 𝑄 ↣ ℐ such that the diagram on the RHS commutes.
                    𝑃         𝑄                                       𝑃         𝑄


                    ℐ     𝑓
                               𝒥                                        ℐ    𝑓
                                                                                  𝒥
  Finally, we can define back-and-forth equivalence (ℐ, 𝑑) ↔DL    𝑘  (𝒥 , 𝑒) between objects in
ℛ* (𝒱), intuitively corresponding to conditions (b) and (c) from the definition of a bisimulation.
This holds if there is an object 𝑅 in ℛ𝐷
                                       *𝑘 (𝒱) and a span of open pathwise embeddings such that:


                                                𝑅


                               𝐹𝑘 (ℐ, 𝑑)                   𝐹𝑘 (𝒥 , 𝑒)

    We shall now define a back-and-forth game 𝒢𝑘Φ (ℐ, 𝑑; 𝒥 , 𝑒) played between the interpretations
(ℐ, 𝑑) and (𝒥 , 𝑒). Positions of the game are pairs (𝑠, 𝑡) ∈ DLΦ𝑘 (ℐ, 𝑑) × DL𝑘 (𝒥 , 𝑒). We define a
                                                                              Φ

relation 𝑊 (ℐ, 𝑑; 𝒥 , 𝑒) ⊆ DL𝑘 (ℐ, 𝑑) × DL𝑘 (𝒥 , 𝑒) as follows. A pair (𝑠, 𝑡) is in 𝑊 (ℐ, 𝑑; 𝒥 , 𝑒)
                                Φ             Φ

iff for some path 𝑃 , path embeddings 𝑒1 : 𝑃 ↣ ℐ and 𝑒2 : 𝑃 ↣ 𝒥 , and 𝑝 ∈ 𝑃 , 𝑠 = 𝑒1 𝑝 and
𝑡 = 𝑒2 𝑝. The intention is that 𝑊 (ℐ, 𝑑; 𝒥 , 𝑒) picks out the winning positions for Duplicator. At
the start of each round of the game, the position is specified by (𝑠, 𝑡) ∈ DLΦ             Φ
                                                                             𝑘 (ℐ, 𝑑) × DL𝑘 (𝒥 , 𝑒).
The initial position is ([𝑑], [𝑒]). The round proceeds as follows. Spoiler either chooses 𝑠′ ≻ 𝑠,
and Duplicator must respond with 𝑡′ ≻ 𝑡, producing the new position (𝑠′ , 𝑡′ ); or Spoiler
chooses 𝑡′′ ≻ 𝑡, and Duplicator must respond with 𝑠′′ ≻ 𝑠, producing the new position (𝑠′′ , 𝑡′′ ).
Duplicator wins the round if she is able to respond, and the new position is in 𝑊 (ℐ, 𝑑; 𝒥 , 𝑒).
We follow the same notation convention as for DLΦ     𝑘 with respect to extensions Φ of game 𝒢𝑘 .
                                                                                                  Φ

The following theorem follows from [2, Theorem 10.1].

Theorem 4.6. Duplicator has a winning strategy in 𝒢𝑘 (ℐ, 𝑑; 𝒥 , 𝑒) iff (ℐ, 𝑑) ↔DL
                                                                               𝑘 (𝒥 , 𝑒).

  The above theorem with aforementioned definitions were just slight variations of theorems
and notions presented in [2]. We have accommodated them to the description logic setting and
now we will glue them together with our definition of the bisimulation game from Section 2.3.

Theorem 4.7. Given interpretations (ℐ, 𝑑) and (𝒥 , 𝑒), the 𝒢𝑘 (ℐ, 𝑑; 𝒥 , 𝑒) game for the DL𝑘
comonad is equivalent to the 𝑘-round 𝒜ℒ𝒞(𝒱)-bisimulation game between (ℐ, 𝑑) and (𝒥 , 𝑒).

Proof. First note that configurations and the moves are structurally the same in both games.
Hence, by induction over 𝑘 it suffices to show that the winning conditions coincide.
Base. Let 𝑘 = 0 and suppose ([𝑑], [𝑒]) ∈ 𝑊 (ℐ, 𝑑; 𝒥 , 𝑒). That holds iff there are path embeddings
𝑒1 : 𝑃 ↣ ℐ, 𝑒2 : 𝑃 ↣ 𝒥 and 𝑝 ∈ 𝑃 such that 𝑒1 𝑝 = [𝑑] and 𝑒2 𝑝 = [𝑒]. By strong
homomorphism property, 𝑑 is in 𝒱-harmony with 𝑝, which in turn is in 𝒱-harmony with 𝑑,
which by transitivity of 𝒱-harmony concludes this case.
Step. Assume that the proposition holds for all 𝑖 ≤ 𝑘. We need to show that the winning
conditions coincide for games of length 𝑘 + 1. Suppose 𝑠 = 𝑠′ [𝛼𝑠 , 𝑑′ ], 𝑡 = 𝑡′ [𝛼𝑡 , 𝑒′ ] and (𝑠, 𝑡) ∈
𝑊 (ℐ, 𝑑; 𝒥 , 𝑒). That holds iff there are path embeddings 𝑒1 : 𝑃 ↣ ℐ, 𝑒2 : 𝑃 ↣ 𝒥 and
𝑝 ∈ 𝑃 such that 𝑒1 𝑝 = 𝑠 and 𝑒2 𝑝 = 𝑡. By definition of 𝑊 (ℐ, 𝑑; 𝒥 , 𝑒) relation, we get
that (𝑠′ , 𝑡′ ) ∈ 𝑊 (ℐ, 𝑑; 𝒥 , 𝑒) and hence, by induction hypothesis, 𝑠, 𝑡 are a valid winning
configuration in 𝒜ℒ𝒞 game. It remains to show that [𝛼𝑠 , 𝑑′ ] and [𝛼𝑡 , 𝑒′ ] are valid moves leading
to winning positions. From 𝑒1 𝑝 = 𝑠 and 𝑒2 𝑝 = 𝑡 we immediately get that 𝛼𝑠 = 𝛼𝑡 and since
𝑒1 , 𝑒2 are embeddings we have that 𝑑′ is in 𝒱-harmony with 𝑝 which in turn is in 𝒱-harmony
with 𝑒′ , hence by transitivity of 𝒱-harmony, we are done.

  By applying Theorem 4.6, Theorem 4.7 and Fact 2.1, we derive our first result on comonadic
semantics for description logic games, namely:

Theorem 4.8. We have that (ℐ, 𝑑) ≡𝒜ℒ𝒞 𝑘 (𝒥 , 𝑒) if and only if (ℐ, 𝑑) ↔DL
                                                                       𝑘 (𝒥 , 𝑒).


5. Comonads for Extensions of 𝒜ℒ𝒞
We can now proceed with definitions of game comonads for extensions of 𝒜ℒ𝒞.
   The approach that we undertook relies on an observation that we had based on how 𝐼-
morphisms were incorporated in [2]. In our case, relative comonads serve as a tool to start
within the base category where our objects live, and then to enrich the interpretations encoding
the additional capabilities available in bisimulation games for richer logics. We do this via the
already-presented reductions from Section 3, followed by the notion of unravelling using DL𝑘
defined in Section 4, all established in a generalised framework using relative comonads.

Definition 5.1. A vocabulary-map 𝛿 is triple (𝛿𝑖 , 𝛿𝑐 , 𝛿𝑟 ) : NI × NC × NR → NI × NC × NR
that maps the vocabulary (𝜎𝑖 , 𝜎𝑐 , 𝜎𝑟 ) ↦−→ (𝛿𝑖 (𝜎𝑖 ), 𝛿𝑐 (𝜎𝑐 ), 𝛿𝑟 (𝜎𝑟 )).

Proposition 5.2. Let 𝛿 be a vocabulary map and f a game reduction. A (f, 𝛿)-reduction-functor
is a full and faithful [9, Def 7.1] functor 𝐽 : ℛ* (𝒱) → ℛ* (𝛿 𝒱) acting (ℐ, 𝑑) ↦−→ (fℐ ℐ, f* 𝑑).

    While Proposition 5.2 is stated in a very general setting, we strictly only consider the reduc-
tions from Section 3. Knowing that, 𝐽 is clearly a functor. The full and faithful property comes
from the bidirectional nature of our reduction games, i.e. reductions are defined in a reversible
way and as such the reduction-functor encodes a full subcategory. Thus, we obtain a family of
(f𝜃 , 𝛿𝜃 )-reduction-functors, where 𝜃 ∈ {Self, ℐ, b, 𝒪} are considered logic extensions.

Definition 5.3. Let 𝛿, 𝛿 ′ be a vocabulary-maps. We say that a functor 𝐹 : ℛ* (𝒱) → ℛ* (𝛿 𝒱) is
invariant over vocabulary-maps iff for any 𝛿 ′ it can be lifted to 𝐹 : ℛ* (𝛿 ′ 𝒱) → ℛ* (𝛿 (𝛿 ′ 𝒱))

   What want to capture by this that such a functor acting on ℛ* (𝒱) category is natural in 𝒱,
i.e. does not depend on the contents of the concepts or roles. It is easy to see the following fact:

Observation 5.4. DL𝑘 and (f𝜃 , 𝛿𝜃 )-reduction-functors are invariant over vocabulary-maps.
  In order to obtain richer semantics, we shall leverage the functor composition, following the
same order as defined for the game reductions in Section 3:
              𝐽Self                      𝐽ℐ                   𝐽b                    𝐽𝒪
    ℛ* (𝒱)                ℛ* (𝒱 Self )        ℛ* (𝒱 Selfℐ )        ℛ* (𝒱 Selfℐb )        ℛ* (𝒱 Selfℐb𝒪 )

  In Appendix we show that:
Lemma 5.5. Reduction-functors are closed under composition.

5.1. Comonadic Semantics for Extensions of 𝒜ℒ𝒞
Having defined appropriate notions and tools, we now present the way to obtain game semantics
for an arbitrary sublogic 𝒜ℒ𝒞 ⊆ ℒΦ ⊆ 𝒜ℒ𝒞 Self ℐb𝒪 by the use of relative comonads.
  Let 𝐽Φ ≜ i𝜃∈Φ 𝐽𝜃 be a family of functors indexed by Φ where 𝐽𝜃 are (f𝜃 , 𝛿𝜃 )-reduction-
functors and the operator iiterates over the extensions and composes the functors together in
(Self, ℐ, b, 𝒪) order. It follows from Lemma 5.5 that 𝐽Φ functors are also reduction-functors.
Proposition 5.6 (𝒜ℒ𝒞Φ-comonad). The game comonad DLΦ
                                                   𝑘 is a (DL𝑘 ∘𝐽Φ )-relative-comonad.

Proof. We know that 𝐽Φ is a functor. From Proposition 4.2 and Observation 5.4 we get that DL𝑘
is a comonad on the codomain of 𝐽Φ . Hence, by definition, DLΦ 𝑘 is a relative comonad.

  With that, we arrive at the concluding lemma which shall guide us to the final result.
Lemma 5.7. Let 𝑘 ∈ N ∪ {𝜔} and let Φ ⊆ {Self, ℐ, b, 𝒪}. Given pointed interpretations (ℐ, 𝑑)
and (𝒥 , 𝑒), the 𝒢𝑘Φ (ℐ, 𝑑; 𝒥 , 𝑒) game for the DLΦ
                                                  𝑘 relative comonad is equivalent to the 𝑘-round
𝒜ℒ𝒞Φ(𝒱)-bisimulation game played on (ℐ, 𝑑) and (𝒥 , 𝑒).
Proof. By Theorem 3.5, it suffices to show that 𝒢𝑘Φ (ℐ, 𝑑; 𝒥 , 𝑒) is equivalent to 𝒜ℒ𝒞(𝒱 Φ )-
bisimulation game between (fℐΦ ℐ, f*Φ 𝑑) and (fℐΦ 𝒥 , f*Φ 𝑒). Recall that the positions in the
𝒢𝑘Φ (ℐ, 𝑑; 𝒥 , 𝑒) are pairs (𝑠, 𝑡) ∈ DLΦ
                                       𝑘 (ℐ, 𝑑) × DL𝑘 (𝒥 , 𝑒). By unfolding the definition of DL𝑘 ,
                                                         Φ                                      Φ

we get that it corresponds to a product of unravelings (fΦ ℐ, 𝑑) × (fΦ 𝒥 , 𝑒). Hence, 𝑠 and 𝑡
are sequences of the form [𝑎0 , 𝛼1 , 𝑎1 , ..., 𝛼𝑗 , 𝑎𝑗 ], where 𝛼𝑖 ∈ 𝜎𝑟Φ and 𝑎𝑖 ∈ ∆ℐ ∨ 𝑎𝑖 ∈ ∆𝒥
for 1 ≤ 𝑖 ≤ 𝑗. An attentive reader can already notice that it is the same as positions in the
𝒜ℒ𝒞(𝒱)-bisimulation game by definition in Section 2.3. What remains to be shown is that
the winning conditions coincide. Note that after applying Theorem 3.5 we are playing the
𝒜ℒ𝒞-bisimulation game, and thus the same inductive reasoning applies as in Theorem 4.7.

  We have finally arrived at the hearth of our result. This is summarised by the following
theorem, which is an immediate corollary from Fact 2.1, Lemma 5.7 and Theorem 4.6.
Theorem 5.8. For any 𝑘 ∈ N ∪ {𝜔} and a logic ℒΦ between 𝒜ℒ𝒞 and 𝒜ℒ𝒞 Self ℐb𝒪, t.f.a.e.:
    • Duplicator has the winning strategy in the 𝑘-round ℒΦ(𝒱)-bisim-game on (ℐ, d; 𝒥 , e),
    • There is an ℒΦ(𝒱)-𝑘-bisimulation 𝒵 between ℐ and 𝒥 such that 𝒵(d, e),
                ℒΦ(𝒱)
    • (ℐ, d) ≡𝑘             (𝒥 , e),
                      Φ
    • (ℐ, 𝑑) ↔DL
              𝑘  (𝒥 , 𝑒).
6. Conclusions
This paper provides yet another view on bisimulation games used in the description logic
setting, via the lenses of comonadic semantics, as well as another nail for the comonads hammer
developed in recent years. There are several directions for future work. One of them involves
the analysis of other known DL extensions, e.g. the number restrictions or the universal role,
where we believe that our approach can be useful. Another research direction is to investigate
combinatorial properties arising from comonads [15, 2, 16], e.g. the coalgebra numbers, or deep
dive into transcribing known theorems using the developed comonadic structure, as in [5, 6].


Acknowledgements
Results from this paper will be included in the master thesis of M. Urbańczyk, written under
an informal supervision of B. Bednarczyk. B. Bednarczyk was supported by the ERC Grant
No. 771779, while M. Urbańczyk received generous financial support from the University of
Wrocław and from the DL Workshop’s student grant.


References
 [1] S. Abramsky, Whither semantics?, Theor. Comput. Sci. 2020 .
 [2] S. Abramsky, N. Shah, Relating structure and power: Comonadic semantics for computa-
     tional resources, J. Log. Comput. 2021 .
 [3] S. Abramsky, D. Marsden, Comonadic semantics for hybrid logic and bounded fragments,
     arXiV 2021 .
 [4] S. Abramsky, D. Marsden, Comonadic semantics for guarded fragments, LICS 2021 .
 [5] A. Dawar, T. Jakl, L. Reggio, Lovász-Type Theorems and Game Comonads, LICS 2021 .
 [6] S. Abramsky, L. Reggio, Arboreal Categories and Resources, ICALP 2021 .
 [7] C. L. Duc, Category-theoretical Semantics of the Description Logic ALC, arXiv 2021 .
 [8] L. Brieulle, C. L. Duc, P. Vaillant, Reasoning in the Description Logic ALC under Category
     Semantics, arXiv 2022 .
 [9] S. Awodey, Category Theory, Ebsco Publishing, 2006.
[10] S. MacLane, Categories for the Working Mathematician, Springer-Verlag, 1971.
[11] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
     University Press, 2017.
[12] T. Altenkirch, J. Chapman, T. Uustalu, Monads need not be endofunctors, Log. Methods
     Comput. Sci. 2015 11 (1).
[13] R. Piro, Model-theoretic characterisations of description logics, Ph.D. thesis, University of
     Liverpool, UK, 2012.
[14] A. R. Divroodi, L. A. Nguyen, On bisimulations for description logics, Inf. Sci. 2015 .
[15] S. Abramsky, A. Dawar, P. Wang, The pebbling comonad in Finite Model Theory, LICS
     2017 .
[16] S. Abramsky, T. Jakl, T. Paine, Discrete density comonads and graph parameters, arXiV
     2022 .

</pre>