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.
Following [
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 [
We start with a recap of notions from category theory [
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 ::= r ::=
A | {o}, C ::= B | ¬C | C ⊓ C | ∃s.C | ∃s.Self 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 individual names to elements of ∆ ℐ , concept names to subsets of ∆ ℐ , and role names to subsets of 1It 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 diference), nominals () and the Self operator (Self). ℒ-concepts for other sublogics ℒ of ℒSelf ℐb are defined similarly. We stress here that role union/intersection/diference, 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 diferent 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ℐ ⊕ sℐ 2 Self op. ∃s.Self {d | (d, d) ∈ sℐ }
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 ∅.
We assume familiarity with basic concepts such as categories, functors or natural transformations. 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 [
Let be a vocabulary. Following [
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ℐ if e = o ”. • If Self ∈ Φ , then we extend the definition of -harmony with a condition “for all r ∈ we have that (d, d) ∈ r ℐ if (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 [
(a) If (d, ′e) then d ∈ Cℐ if 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ℐ if e = o . (e) If Self ∈ Φ , then (d, ′e) implies (d, d) ∈ r ℐ if (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) if 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 [
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).
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 S elf ≜ ∪ {CSelf.r | r ∈ }. By the self-enrichment of a ≜ ( , , )-interpretation ℐ we mean the Self ≜ ( , S elf , )-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) if she has a winning strategy in a -round ℒ()-bisimulation game on (fSelf (ℐ), d; fSelf ( ), e). 3i.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 S elf 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 inverseenrichment 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) if 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 benrichment 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) if 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 substructure 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 subinterpretations 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 shortest 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, . . . , ddoisto− 1 to ∆ ′ and employ the fresh role name ro, whose interpretation will contains precisely the pairs (d, do1), (do1, do2), . . . , (ddoisto− 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) if 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) if 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.
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 sufices
to translate the work done in [
• 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(ℐ,) if ℐ ∈ Cℐ . • For role names r ∈ , we put (, ) ∈ r DL(ℐ,) if 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 suficient 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.
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 ≺ if (, ) ∈ 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 diferent kinds of embeddings, essential to characterize plays.
Definition 4.4. A morphism in ℛ*() is an embedding if it is an injective strong homomorphism. 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(ℐ, ), ⊑).
Given suficient 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 (ℐ, ) ↔D L ( , ) 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 (ℐ, ; , ) if 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 (ℐ, ; , ) if (ℐ, ) ↔D L ( , ).
The above theorem with aforementioned definitions were just slight variations of theorems
and notions presented in [
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 if 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 (ℐ, ) ↔D L ( , ). 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 [
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 reductions 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 if 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 ℛ* (Self ) ℐ ℛ* (Selfℐ ) b ℛ* (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 , )-reductionfunctors 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 sufices 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Φ ( , ).
• (ℐ, ) ↔
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 [
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.