A Characterization Theorem for a Modal Description Logic

1 Introduction

Modal description logics extend the static knowledge model of standard description logics by adding modalities capturing, e.g., the temporal evolution of the state of the world or the dependence of knowledge on the information available to individual agents. Their semantics is typically two-dimensional [Gabbay et al., 2003], i.e. it is defined over interpretations involving two sets of individuals and worlds, respectively, and concepts are interpreted as subsets of the Cartesian product of these two sets. For instance, temporal description logics (surveyed, e.g., by Lutz et al. [2008]) have a frame structure on the set of worlds, in the same way as in the semantics of standard temporal logics such as CTL; they support statements such as 'every person that is currently a child will eventually become an adult in the future'.

A simpler variant of the same idea is to give up directedness of temporal evolution and instead introduce a modality that reads 'at some other point in time', so that, continuing the previous example, one can express only that that every person that is currently a child is an adult at some other time. This coarser granularity buys a simplification of the semantics in which the set of worlds is just a set (equivalently, a frame whose transition relation is an equivalence), i.e. a model of the modal logic S5. Modal description logics with an S5 modality have been used prominently as description logics of change, and are able to encode a restricted form of temporal entityrelationship models if the description logic is strong enough (specifically, contains ALCQI) [Artale et al., 2007].

∗Work forms part of DFG project ProbDL2 (SCHR 1118/6-2)

One of the simplest description logics of change in this sense is S5ALC, i.e. the extension of the standard description logic ALC [Baader et al., 2003] with an S5 change modality. In fact, there are many other readings for the S5 modality. In particular, S5 modalities standardly feature in epistemic logics, and indeed S5ALC was originally introduced as an epistemic description logic [Wolter and Zakharyaschev, 1999b]. As a variant of this view, S5ALC and its EL fragment have been considered as a corner case of probabilistic description logics for subjective uncertainty, with probabilities mentioned in concepts restricted to 0 or 1 [Guti´errez-Basulto et al., 2017]. In the current work, we focus on S5ALC as one of the most basic modal description logics, and use it as a starting point for the correspondence theory of modal description logics.

Specifically, S5ALC embeds as a fragment into the modal first-order logic S5FOL, which extends standard first-order logic with an S5 modality and lives over the same type of semantic structures as S5ALC. This situation is analogous to the one with ALC itself, which embeds as a fragment into ordinary first-order logic (FOL). For ALC, it is straightforward to check that its concepts are bisimulation-invariant, i.e. bisimilar individuals satisfy the same ALC-concepts. This constitutes in effect an upper bound on the expressivity of ALC: any property that fails to be bisimulation-invariant (such as 'individual x is related to itself under role r') is not expressible in ALC. Remarkably, it can be shown that this is also a lower bound: every bisimulation-invariant first-order property can be expressed in ALC, a fact first proved by van Benthem [1976] and later shown to hold true also over finite structures by Rosen [1997]. In other words, ALC is precisely the bisimulation-invariant fragment of FOL; we refer to theorems of this type as modal characterization theorems. In this terminology, the object of this paper is to establish a modal characterization theorem for S5loc ALC , the fragment of S5ALC determined by admitting only local (i.e. non-modalized) roles: We show that both over unrestricted and over finite interpretations, S5loc ALC is precisely the bisimulation-invariant fragment of S5FOL, where both bisimulation invariance and equivalence to a modal formula are understood over two-dimensional interpretations. Technically, we follow a generic recipe suggested by Otto [2004], which relies on locality w.r.t. Gaifman distance. In fact, the main challenge in our proof is to identify a suitable notion of Gaifman distance for S5FOL, and relate it to numbers of rounds played in bisimulation games (Remark 4.3). Summing up, we pin down the exact expressivity of S5loc ALC as a fragment of S5FOL; to our best knowledge, this is the first time a modal characterization theorem is obtained for a many-dimensional modal logic or a modal description logic.

Proofs are sometimes omitted or only sketched; see [Wild and Schr¨oder, 2017] for a full version.

Related Work In the one-dimensional case, the original van Benthem / Rosen characterization theorem has been extended in various directions, e.g. for logics with frame conditions [Dawar and Otto, 2005], coalgebraic modal logics [Schr¨oder et al., 2015], fragments of XPath [ten Cate et al., 2010; Figueira et al., 2015; Abriola et al., 2017], neighbourhood logic [Hansen et al., 2009], modal and first order logic with team semantics [Kontinen et al., 2015], modal µ-calculi (within monadic second order logics) [Janin and Walukiewicz, 1995; Enqvist et al., 2015], and PDL (within weak chain logic) [Carreiro, 2015].

In the many-dimensional setting, all existing characterization results that we are aware of look in the other direction, from the perspective of modal first-order logics: they characterize modal first-order logics as fragments of even more expressive two-sorted first order logics that make the worlds explicit. Specifically, van Benthem [2001] proves this for unrestricted frames in the modal dimension, i.e., in the nomenclature scheme we use here, for KFOL, while Sturm and Wolter [2001] characterize S5FOL as as a fragment of two-sorted FOL; in both cases, the relevant notion of equivalence is essentially bisimilarity in the modal dimension, and Ehrenfeucht-Fra¨ıss´e equivalence in the first-order dimension. Both results are proved only over unrestricted models, and their proofs rely on compactness. The characterization theorem for S5FOL can in fact be combined with our characterization of S5ALC as a fragment of S5FOL to obtain, over unrestricted models, a stronger characterization of S5ALC as the bisimulation-invariant fragment of the two-sorted first-order correspondence language (Corollary 4.13 below).

2 S5-modalized ALC and FOL

We recall the syntax of modalized ALC as introduced by Wolter and Zakharyaschev [1999b], restricting to a single modality: Concepts C, D of S5loc ALC (S5-modalized ALC with only local roles) are given by the grammar

where as usual A ranges over a set NC of (atomic) concept names and r over a set NR of role names. The remaining Boolean connectives ⊤, ⊥, ⊔, as well as universal restrictions ∀r. C, are encoded as usual. The rank of an S5loc ALC -concept C is the maximal nesting depth of modalities □ and existential restrictions ∃r in C (e.g. ∃r. □A has rank 2).

An S5-interpretation

consists of nonempty sets W I , ∆I of of worlds and individuals, respectively, and for each world w ∈ W I a standard ALC interpretation (-)I,w over ∆I , i.e. for each concept name A ∈ NC a subset AI,w ⊆ ∆I , and for each role name r ∈ NR a binary relation rI,w ⊆ ∆I × ∆I . We refer to ∆I as the domain of I. The interpretation C I,w ⊆ ∆I of a composite concept C at a world w is then defined recursively by the usual clauses for the ALC constructs ((¬C)I,w = ∆I \C I,w , (C ⊓D)I,w = C I,w ∩DI,w , (∃r. C)I,w = {d ∈ ∆I | ∃e ∈ C I,w . (d, e) ∈ rI,w }), and by

In words, □C denotes the set of individuals that belong to C in all worlds. As usual, we write ♦ for the dual of □, i.e. ♦C abbreviates ¬□¬C and denotes the set of all individuals that belong to C in some world. We write I,w, d |= C if d ∈ C I,w .

S5-interpretations are two-dimensional in the sense that concepts are effectively interpreted as subsets of Cartesian products W I ×∆I , and the modalities □ and ∃r are interpreted by relations that move only in one dimension of the product: □ moves only in the world dimension and keeps the individual fixed, and vice versa for ∃r. Thus, S5loc ALC and S5ALC (Remark 2.2) are examples of many-dimensional modal logics [Marx and Venema, 1996; Gabbay et al., 2003].

As indicated in the introduction, there are various readings that can be attached to the modality □. E.g. if we see □ as a change modality [Artale et al., 2007], and, for variety, consider spatial rather than temporal change, then the concept

describes persons married to fugitives from the law, i.e. to persons that are wanted by the police in some place but not here. As an example where we read □ as an epistemic modality 'I know that' [Wolter and Zakharyaschev, 1999b; Gabbay et al., 2003], the concept

applies to people who I know are armed with a concealed gun that as far as I knowmight be loaded.

A more expressive modal language is S5-modalized firstorder logic with constant domains, which we briefly refer to as S5FOL. Formulas φ, ψ of S5FOL are given by the grammar

where x, y and the xi are variables from a fixed countably infinite reservoir and R is an n-ary predicate from an underlying language of predicate symbols with given arities. The quantifier ∃x binds the variable x, and we have the usual notions of free and bound variables in formulas. The rank of a formula φ is the maximal nesting depth of modalities □ and quantifiers ∃x in φ; e.g. ∃x. □(∀y. r(x, y)) has rank 3. This is exactly the S5 modal first-order logic called QML by Sturm and Wolter [2001]. From now on we fix the language to be the correspondence language of S5ALC, which has a unary predicate symbol A for each concept name A and a binary predicate symbol r for each role name r. The semantics of S5FOL is then defined over S5-interpretations, like S5loc ALC . It is given in terms of a satisfaction relation |= that relates an interpretation I, a world w ∈ W I , and a valuation η assigning a value η(x) ∈ ∆I to every variable x on the one hand to a formula φ on the other hand. The relation |= is defined by the expected clauses for Boolean connectives, and

(where η[x ↦→ d] denotes the valuation that maps x to d and otherwise behaves like η). That is, the semantics of the firstorder constructs is as usual, and that of □ is as in S5ALC. We often write valuations as vectors ¯ d = (d1, . . . , dn) ∈ (∆I )n , which list the values assigned to variables x1, . . . , xn if the free variables of φ are contained in {x1, . . . , xn}.

To formalize the obvious fact that S5loc ALC is a fragment of S5FOL, we extend the usual standard translation to S5ALC: a translation STx that maps S5ALC-concepts C to S5FOLformulas STx(C) with a single free variable x is given by

and commutation with all other constructs. Then STx preserves the semantics, i.e.

Lemma 2.1. For every S5loc ALC -concept C, interpretation I, w ∈ W I , and d ∈ ∆I , we have

Remark 2.2. Modalized ALC has been extended with modalized roles [Wolter and Zakharyaschev, 1999a], i.e. roles of the form□r or ♦r, interpreted as

The S5-modalized description logic in this extended sense has been termed S5ALC by Gabbay et al. [2003]; so in our notation S5loc ALC is the fragment of S5ALC without modalized roles. Since modalized roles □r, ♦r have an interpretation that is independent of the world while that of basic roles r varies between worlds, the latter are called local roles, explaining the slightly verbose terminology used above. We will see that S5ALC fails to be bisimulation-invariant, and is therefore strictly more expressive than S5loc ALC .

3 Bisimulation and Invariance

We proceed to introduce the relevant notion of bisimulation for S5-interpretations. This is just the usual notion of bisimilarity, specialized to the two-dimensional shape of S5-interpretations and the S5 structure of the world dimension; explicitly:

Definition 3.1 (Bisimulation). A bisimulation between interpretations I, J is a relation

such that whenever (w, d)R(v, e), then

1. d ∈ AI,w iff e ∈ AJ,v for all A ∈ NC;
2. for every w′ ∈ W I there is v′ ∈ W J such that (w′ , d)R(v′ , e);
3. Same with the roles of I and J interchanged.
4. for every (d, d′ ) ∈ rI,w (r ∈ NR) there is e′ such that (e, e′ ) ∈ rJ ,v and (w, d′ )R(v, e′ )
5. Same with the roles of I and J interchanged.

We say that I, w, d and J , v, e are bisimilar, and write

if there exists a bisimulation R such that (w, d)R(v, e).

We record explicitly that S5loc ALC is bisimulation-invariant, a fact that is immediate from bisimulation invariance of basic multi-modal logic (over all interpretations, including S5interpretations). As a general manner of speaking, whenever P is any property that applies to triples I, w, d consisting of an S5-interpretation I, w ∈ W I , and d ∈ ∆I (e.g. P could be an S5loc ALC -concept or an S5FOL-formula with one free variable), then we say that P is bisimulation-invariant, or just ≈-invariant, if whenever I, w, d ≈ J , v, e then I, w, d has property P iff J , v, e has property P. We will extend this terminology without further comment to other notions of equivalence that we introduce later, such as bisimilarity up to finite depth and Ehrenfeucht-Fra¨ıss´e equivalence. Moreover, we will consider restrictions of these notions to finite S5-interpretations; e.g. bisimulation-invariance over finite S5interpretations of a property P is defined like bisimulationinvariance of P above but with I and J assumed to be finite. In these terms, we have

Lemma 3.2 (Bisimulation invariance). Every S5loc ALC -concept is ≈-invariant.

Example 3.3. As indicated in the introduction, bisimulation invariance is an upper bound on the expressivity of S5ALC. As an extremely simple example, the formula r(x, x) of S5FOL fails to be ≈-invariant and is therefore, by Lemma 3.2, not equivalent to (the standard translation of) any S5loc ALC - concept. Bisimulation invariance also separates S5loc ALC from S5ALC (Remark 2.2): the S5ALC-concept ∃♦r.A fails to be ≈-invariant and is therefore not expressible in S5loc ALC .

Bisimulation games As usual, bisimilarity can equivalently be captured in terms of games. Explicitly:

Definition 3.4 (Bisimulation game). Let I, J be S5interpretations, and let (w0, d0) ∈ W I × ∆I , (v0, e0) ∈ W J ×∆J . The bisimulation game for I, w0, d0 and J , v0, e0 is played by players S (Spoiler) and D (Duplicator), where D means to establish bisimilarity and S aims to disprove it. A configuration of the game is a quadruple ((w, d), (v, e)) ∈ (W I × ∆I ) × (W J × ∆J ), with ((w0, d0), (v0, e0)) being the initial configuration. A round consists of one move by S and a subsequent move by D, with the following alternatives in the current configuration ((w, d), (v, e)):

1. S may pick a world w′ ∈ W I , and D then needs to pick a world v′ ∈ W J ; the new configuration then is ((w′ , d), (v′ , e)).

1. Same with the roles of I and J interchanged.
2. S may pick a role r ∈ NR and an individual d′ ∈ ∆I such that (d, d′ ) ∈ rI,w . Then D needs to pick an individual e′ ∈ ∆J such that (e, e′ ) ∈ rJ ,v ; the new configuration reached is ((w, d′ ), (v, e′ )).
3. Same with the roles of I and J interchanged.

We will call the first two kinds of moves W-moves and the other two kinds ∆-moves. If one of the players cannot move, then the other one wins. A configuration ((w, d), (v, e)) is winning for S if d ∈ AI,w and e /∈ AJ,v for some concept name A ∈ NC, or vice versa; and S wins if a winning configuration for S is reached. Infinite plays that do not visit a winning configuration for S are won by D.

The following is then standard:

Lemma 3.5. We have I, w, d ≈ J , v, e iff D wins the bisimulation game for I, w, d and J , v, e.

The bisimulation game can be restricted to a finite number of rounds, capturing bisimulation up to finite depth:

Definition 3.6 (Finite-depth bisimulation). The n-round bisimulation game for n ≥ 0 is played in the same way as the bisimulation game but only for at most n rounds. The winning conditions are the same as in the bisimulation game except that D now wins if no winning configuration for S has been reached after n rounds. We say that I, w, d and J , v, e are depth-n bisimilar, and write

if D wins the n-round bisimulation game for I,w, d and J , v, e.

Again, the following is standard:

Lemma 3.7 (Invariance under finite-depth bisimulation). Every S5loc ALC -concept C of rank at most n is ≈n-invariant.

For technical purposes, we shall need a normalization of the bisimulation game based on the observation that due to the S5 structure of the worlds, S can never gain an advantage from playing more than one consecutive W-move. Formally:

Definition 3.8 (Alternating bisimulation game). The alternating bisimulation game is played like the bisimulation game but with a restriction on the sequence of moves: Each round in the alternating bisimulation game consists of two phases,

1. S may decide to make a W-move, and in this case D also makes a W-move, according to Item 1 or Item 2 of Definition 3.4, and then
2. S and D each play exactly one ∆-move according to Item 3 or Item 4 of Definition 3.4

(where D needs to avoid winning configurations for S at all times). The alternating bisimulation game also comes in two variants, the unbounded and the n-round game, with the proviso that at the end of an n-round game, there may be one extra phase of type 1 above. We write

if D has a winning strategy in the alternating and in the nround alternating bisimulation game for I, w, d and J , v, e, respectively.

The unrestricted game is equivalent to the alternating game in the following sense:

Lemma 3.9. For interpretations I, J and (w, d) ∈ W I ×∆I , (v, e) ∈ W J ×∆J :

1. If I,w, d ≈2n+1 J , v, e, then I,w, d ≈alt n J , v, e.
2. If I,w, d ≈alt n J , v, e, then I,w, d ≈n J , v, e.
3. I,w, d ≈ J , v, e iff I,w, d ≈alt J , v, e.

4 The Modal Characterization Theorem

We proceed to state our main result and sketch its proof: S5loc ALC is the bisimulation-invariant fragment of S5FOL, both over finite and over unrestricted S5-interpretations. Formally,

Theorem 4.1 (Modal characterization). Let φ = φ(x) be an S5FOL-formula with one free variable x. If φ is ≈-invariant (over finite S5-interpretations), then there exists an S5loc ALC - concept C such that φ is logically equivalent to STx(C) (over finite S5-interpretations). Moreover, the rank of C is exponentially bounded in the rank of φ.

While modal characterization theorems over unrestricted structures can often be proved using model-theoretic tools such as compactness [van Benthem, 1976], proofs that apply also to finite structures typically need to work with some form of locality [Otto, 2004]. In the basic, one-dimensional case, this is Gaifman locality [Gaifman, 1982], which is based on the notion of Gaifman distance in a first-order model: The Gaifman graph of the model connects two of its points if they occur together in some tuple that is in the interpretation of some relation in the model, and the Gaifman distance is then just the graph distance in the Gaifman graph. We adapt these notions for our purposes as follows.

Definition 4.2. The Gaifman graph of an S5-interpretation I is the undirected graph with vertex set ∆I that has an edge between d and e iff d ̸= e and either (d, e) ∈ rI,w or (e, d) ∈ rI,w for some role name r and some w ∈ W I . The Gaifman distance D : ∆I × ∆I → N ∪ {∞} is just graph distance (length of the shortest connecting path) in the Gaifman graph, and for any tuple ¯ d = (d1, . . . , dk) ∈ (∆I )k , the neighbourhood U ℓ ( ¯ d) of ¯ d with radius ℓ is given by

Remark 4.3. It may be slightly surprising that Gaifman graphs for S5-interpretations live only in the individual dimension, so that implicit steps between worlds are effectively discounted (a point where the S5 structure on worlds becomes important). The technical reason for this is that it does not seem easily possible to include the worlds in the Gaifman graph without creating unduly short paths. The fact that world steps count 0 in the Gaifman distance creates a certain amount of tension with the fact that bisimulation games do feature explicit W-moves (Definition 3.4). Our alternating bisimulation games (Definition 3.8) serve mainly to address this point.

Definition 4.4 (Locality). The restriction I|U of an S5interpretation I to a subset U ⊆ ∆I is given by W I|U = W I , ∆I|U = U, AI|U,w = AI,w ∩ U for A ∈ NC, and rI|U,w = rI,w ∩ (U ×U) for r ∈ NR. An S5FOL-formula φ with k free variables is ℓ-local for ℓ ≥ 0 if for every S5-interpretation I, w ∈W I , and and ¯ d ∈ (∆I )k ,

In these terms, we organize the proof of our main result as follows, following a generic strategy proposed by Otto [2004]:

Proof of Theorem 4.1 (Sketch). For φ ≈-invariant of rank n, we prove the following steps in order:

• φ is ℓ-local, where ℓ = 3n (Lemma 4.7).
• φ is ≈2ℓ+1-invariant (Lemma 4.9).
• φ is equivalent to a concept of rank 2ℓ+1 (Lemma 4.12).

(The locality bound is slightly generous, for simplicity.)

Standard FOL comes with its own notion of invariance, with respect to Ehrenfeucht-Fra¨ıss´e equivalence [Libkin, 2004]. This notion has been extended to S5FOL by complementing it with bisimilarity in the world dimension [van Benthem, 2001; Sturm and Wolter, 2001]. Here, we introduce a bounded version of this equivalence, which we phrase in game-theoretic terms; this will be instrumental in the proof of locality:

Definition 4.5 (Bounded Ehrenfeucht-Fra¨ıss´e game for S5FOL). Let I, J be S5-interpretations, let (w0, d0) ∈ W I × ∆I , (v0, e0) ∈ W J × ∆J , and let n ≥ 0. The nround Ehrenfeucht-Fra¨ıss´e game for I, w0, d0 and J , v0, e0 is played by players S and D. The configurations are quadruples ((w, ¯ d), (v, ¯ e)), where w ∈ W I , v ∈ W J and ¯ d and ¯ e are finite sequences over ∆I and ∆J , respectively. The initial configuration is ((w0, d0), (v0, e0)). The possible moves from configuration ((w, ¯ d), (v, ¯ e)) are:

1. S may pick a world w′ ∈ W I , and D then needs to pick a world v′ ∈ W J ; the new configuration is ((w′ , ¯ d), (v′ , ¯ e)).
2. Same with the roles of I and J interchanged.
3. S may pick some d ∈ ∆I and D then needs to pick e ∈ ∆J . The new configuration is ((w, ¯ dd), (v, ¯ ee)).
4. Same with the roles of I and J interchanged.

The winning conditions are as in the n-round bisimulation game, except that a configuration is now winning for S if it fails to be a partial isomorphism. Here, ((w, (d0, . . . , dk)), (v, (e0, . . . , ek))) is a partial isomorphism if

• for all 0 ≤ i, j ≤ k, di = dj ⇔ ei = ej; and
• for all 0 ≤ i1, . . . , im ≤ k and m-ary relation symbols R, (di1 , . . . , dim ) ∈ RI,w ⇔ (ei1 , . . . , eim ) ∈ RJ ,v .

We say that I,w0, d0 and J , v0, e0 are S5-EhrenfeuchtFra¨ıss´e equivalent up to depth n, and write

if D has a winning strategy in this game.

As announced, S5FOL is invariant under S5-EhrenfeuchtFra¨ıss´e equivalence. For the unbounded variant, this has been shown in earlier work [Sturm and Wolter, 2001]; for our bounded variant, invariance takes the following shape:

Lemma 4.6 (Bounded S5-Ehrenfeucht-Fra¨ıss´e invariance). Every S5FOL-formula of rank at most n with one free variable is ∼=n-invariant.

We use this to prove locality:

Lemma 4.7. Let φ be a ≈-invariant S5FOL-formula of rank n. Then φ is ℓ-local for ℓ = 3n .

Proof (sketch). Let I be an S5-interpretation and (w0, d0) ∈ W I × ∆I . Put J = I|U ℓ (d0); we need to show that I,w0, d0 |= φ ⇔ J ,w0, d0 |= φ. By ≈-invariance, we can disjointly extend the domains of I and J without affecting satisfaction of φ. We thus extend both I and J with n copies of both I and J each, obtaining I ′ and J ′ , respectively.

By Lemma 4.6, it suffices to show that I ′ ,w0, d0 ∼=n J ′ ,w0, d0. The winning strategy for D is to maintain the following invariant, where we put ℓi = 3n-i for 0 ≤ i ≤ n:

If ((w, ¯ d), (v, ¯ e)) is the current configuration, with ¯ d = (d0, . . . , di), ¯ e = (e0, . . . , ei), then w = v and there is an isomorphism between I ′ |U ℓi ( ¯ d) and J ′ |U ℓi (¯ e) mapping each dj to ej.

D maintains the invariant as follows: Whenever S picks a new world in either interpretation, D can just pick the same world in the other interpretation, as I ′ and J ′ have the same set of worlds. Whenever S picks a new individual d in U 2ℓi+1 ( ¯ d) or U 2ℓi+1 (¯ e) (where ¯ d = (d0, . . . , di) and ¯ e = (e0, . . . , ei)), then d is in the domain or range of the isomorphism in the invariant, and D picks his response according to the isomorphism. Otherwise, D picks a 'fresh' copy of the appropriate type (I or J , depending on where d lies) in the other interpretation and responds with d in that copy.

Having proved locality of ≈-invariant formulas, we next establish invariance even under finite-depth bisimilarity. To this end, we need tree unravellings of S5-interpretations:

Definition 4.8 (Tree unravelling). Let I be an interpretation and d0 ∈ ∆I . The tree unravelling I ∗ d0 of I is the interpretation with set W I ∗ d0 = W I of worlds; with domain ∆I ∗ d0 consisting of all paths of the form (d0, . . . , dk) such that for each i ∈ {0, . . . , k - 1}, (di, di+1) ∈ rI,w for some role name r and some world w; and with the following interpretations of concept and role names:

where π : (d0, . . . , dk) ↦→ dk is projection to the last entry.

It is then easy to show that I,w, d ≈ I ∗ d ,w, d. In fact, a bisimulation is given by the function π (and identity on the set of worlds). Also, I ∗ d , w, d ≈alt ℓ I ∗ d |U ℓ (d), w, d.

Lemma 4.9. Let φ = φ(x) be ≈-invariant and ℓ-local. Then φ is ≈2ℓ+1-invariant.

Proof (sketch). Let I,w, d ≈2ℓ+1 J , v, e and I,w, d |= φ. We need to show that J , v, e |= φ. By Lemma 3.9, I,w, d ≈alt ℓ J , v, e. By ≈-invariance of φ, we may pass from I and J to their unravellings, and by ℓ-locality of φ, we may then restrict those to the radius ℓ neighbourhoods of d and e, respectively. The resulting interpretations I ∗ d |U ℓ (d) and J ∗ e |U ℓ (e) then are trees of height at most ℓ in the individual dimension.

Now I ∗ d |U ℓ (d), w, d ≈alt ℓ J ∗ e |U ℓ (e), v, e, i.e. D wins the alternating ℓ-round bisimulation game. Due to the tree structure on the domains, D's winning strategy is also winning for the unbounded alternating bisimulation game, as eventually a leaf node will be reached and S will not have a legal move in the second phase of a round. So, using Lemma 3.9 again, D wins the unbounded ordinary bisimulation game, and therefore J , v, e |= φ by ≈-invariance of φ.

Remark 4.10. In the case of finite interpretations (the 'Rosen' part of the characterization theorem), there is a caveat: the tree unravelling of a finite interpretation is not finite in general, so we cannot use ≈-invariance over finite interpretations to pass from interpretations to their unravellings. To remedy this, we work with partial unravellings up to level ℓ instead. Such a partial unravelling is constructed by restricting the tree unravelling I ∗ d0 to the radius ℓ + 1 neighbourhood of d0 and then identifying each leaf node ¯ d with the corresponding element π( ¯ d) in a fresh disjoint copy of I. The resulting interpretation is clearly finite if I is finite, and readily shown to be bisimilar to I. Also, the radius ℓ neighbourhood of d0 in the partial unravelling is a tree.

Finally, we construct an equivalent S5ALC-concept for a given formula that is invariant under finite-depth bisimulation. We will make use of normal forms, as introduced by Fine [1975].

Since the formula φ is fixed, we can assume w.l.o.g. that NC and NR are finite sets NC = {A1, . . . ,As} and NR = {r1, . . . , rt}.

Definition 4.11. The sets nfk and atk of normal forms and atoms of rank k ≥ 0, respectively, are defined by induction:

and nfk is the set of finite conjunctions of the form ∧B∈atk εBB (according to some fixed total ordering on atk) where each εB is either nothing or negation. Moreover, nf-1 = ∅ for convenience.

These normal forms have the following properties:

• For any I,w, d, there is exactly one normal formC k I,w,d of rank k such that I, w, d |= C k I,w,d .
• We have I, w, d ≈k J , v, e iff C k I,w,d = C kJ ,v,e .

Lemma 4.12. Every≈k-invariant S5FOL-formula φwith one free variable x can be expressed as an S5loc ALC -concept of rank k, namely

Proof. First, note that the above disjunction is finite, even though there may be infinitely many interpretations satisfying φ. We denote the arising S5loc ALC -concept by C.

For the implication from φ to STx(C), just note that if I,w, d |= φ, then C k I,w,d is one of the disjuncts in C.

For the reverse implication, let I, w, d |= C and let C kJ ,v,e be a disjunct in C such that I, w, d |= C kJ ,v,e . By the above properties of normal forms, it follows that C k I,w,d = C kJ ,v,e and therefore I, w, d ≈k J , v, e. By definition, J , v, e |= φ, so I, w, d |= φ by ≈k-invariance of φ, as desired.

This completes the proof of Theorem 4.1 as outlined above.

Characterization within two-sorted FOL The natural first-order correspondence language for S5FOL [Sturm and Wolter, 2001] is a two-sorted language with sorts domain and world; for every n-ary predicate R in the S5FOL language, the two-sorted language has an n + 1-ary predicate R with n arguments of sort domain and one additional argument of sort world. This language SL is interpreted in the standard way over two-sorted first-order structures; for the twosorted language induced by the correspondence language of S5loc ALC , these are just S5-interpretations. One has a translation (-)†v of S5FOL into the two-sorted first-order language, given by R(x1, . . . , xn)†v = R(x1, . . . , xn, v) and (□φ)†v = ∀v. (φ†v ), and commutation with all other constructs, where v is a variable of sort world. Sturm and Wolter [2001] show that S5FOL is, over unrestricted S5interpretations, precisely the fragment of SL that is determined by invariance under potential S5-isomorphisms, i.e. unbounded S5-Ehrenfeucht-Fra¨ıss´e equivalence, defined as above but without a bound on the number of rounds. Since every potential S5-isomorphism is a bisimulation, we can combine this result with Theorem 4.1 to obtain that S5loc ALC is the bisimulation-invariant fragment of SL:

Corollary 4.13 (Modal characterization within SL). Let φ = φ(x, v) be a ≈-invariant formula with one variable x of sort domain and one free variable v of sort world, in the twosorted first-order language SL. Then there exists an S5loc ALC - concept C such that φ is logically equivalent to (STx(C))†v .

(Unlike for Theorem 4.1, there is as yet no version of Corollary 4.13 for finite S5-interpretations, as the characterization of S5FOL within SL is known only for the unrestricted case.)

5 Conclusions

We have proved a modal characterization theorem for the modal description logic S5loc ALC , i.e. S5ALC [Gabbay et al., 2003] with only local roles. Specifically, we have shown that S5loc ALC , one of the modal description logics originally introduced by Wolter and Zakharyaschev [1999b], is, both over finite and over unrestricted models, the bisimulationinvariant fragment of S5-modal first-order logic. By a result of Sturm and Wolter [2001], it follows moreover that S5loc ALC is, over unrestricted models, the bisimulation-invariant fragment of two-sorted FOL with explicit worlds. To our knowledge, these are the first modal characterization theorems in modal description logic.

It remains a topic of interest to obtain similar characterization theorems for other modal description logics or manydimensional modal logics. Notably, this concerns logics whose modal dimension differs from the comparatively simple structure of S5, e.g. KALC. Also, one may investigate the possibility of a modal characterization of full S5ALC, then of course with respect to a different notion of equivalence.