A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic

1 Introduction

In the representation of uncertain knowledge, one will often wish to avoid mention of exact numerical probabilities, e.g. when these are not precisely known or not relevant to the representation task at hand - as a typical example, a medical practitioner will rarely name a numerical threshold for the likelihood of a diagnosis, and instead qualify the diagnosis as, say, 'suspected' or 'probable'. This has led to efforts aimed at formalizing a modality probably, used alternatively to modalities 'with probability at least p' [Larsen and Skou, 1991; Heifetz and Mongin, 2001]. Such a formalization may be approached in a two-valued setting via qualitative axiomatizations of likelihood [Burgess, 1969; Halpern and Rabin, 1987] or via threshold probabilities [Hamblin, 1959; Herzig, 2003]. In a fuzzy setting, 'probably' leads a natural life as a fuzzy modality P, whose truth value just increases as its argument becomes more probable (this modality thus connects the otherwise well-distinguished worlds of fuzziness and probability [Lukasiewicz and Straccia, 2008]). The semantics of this operator, first defined by Zadeh [1968], interprets Pφ as the expected truth value of φ. It appears in various fuzzy propositional [H´ajek, 2007; Flaminio and Godo, 2007], modal [Desharnais et al., 2004; van Breugel and Worrell, 2005], fixpoint [Kozen, 1985; Huth and Kwiatkowska, 1997], and description logics [Schr¨oder and Pattinson, 2011].

In the present paper, we pin down the exact expressiveness of the basic description logic of probably, which we briefly refer to as probabilistic fuzzy ALC or ALC(P), within a natural ambient probabilistic fuzzy first-order logic FO(P), by providing a modal characterization theorem. The prototype of such characterization theorems is van Benthem's theorem [1976], which states that (classical) modal logic is precisely the bisimulation-invariant fragment of first-order logic. It has been noted that in systems with numerical values, behavioural pseudometrics offer a more fine-grained measure of equivalence than two-valued bisimilarity [Giacalone et al., 1990; Desharnais et al., 2004; van Breugel and Worrell, 2005; Desharnais et al., 2008; Baldan et al., 2014]. When propositional connectives are equipped with Zadeh semantics, ALC(P) is non-expansive wrt. behavioural distance; we continue to refer to this property as bisimulation invariance. In previous work [Wild et al., 2018] we have shown that relational fuzzy modal logic is the bisimulation-invariant fragment of fuzzy FOL, more precisely that every bisimulationinvariant fuzzy FO formula can be approximated by fuzzy modal formulae of bounded rank. The bound on the rank is key; without it, the statement turns into a form of the (much simpler) Hennessy-Milner theorem [Hennessy and Milner, 1985] (which classically states that non-bisimilar states in finitely branching systems can be distinguished by modal formulae), and indeed does not need to assume FO definability of the given bisimulation-invariant property [van Breugel and Worrell, 2005]. Here, we establish a corresponding result for the rather more involved probabilistic setting: We show that every bisimulation-invariant formula in probabilistic fuzzy FOL can be approximated in bounded rank in probabilistic fuzzy ALC. This means not only that, up to approximation, ALC(P) is as powerful as FO(P) on bisimulation-invariant properties, but also that ALC(P) provides effective syntax for bisimulation-invariant FO(P), which FO(P) itself does not.

A full version is available at http://arxiv.org/abs/1906. 00784.

RelatedWork There is widespread interest in modal characterization theorems in many areas, including concurrency [Janin and Walukiewicz, 1995] as well as AI and database theory [Sturm and Wolter, 2001; Figueira et al., 2015; Wild and Schr¨oder, 2017; Wild et al., 2018]. The overall structure of our proof builds partly on that of our modal characterization theorem for relational fuzzy modal logic [Wild et al., 2018] (in turn based ultimately on a strategy due to Otto [2004]) but deals with a much more involved logic, which instead of just the lattice structure of the unit interval involves its full arithmetic structure, via the use of probabilities and expected values, necessitating, e.g., the use of Kantorovich-Rubinstein duality. Notable contributions of our proof include new forms of probabilistic bisimulation games up-to-ϵ (different from games introduced by Desharnais et al. [2008], which characterize a different metric) and Ehrenfeucht-Fra¨ıss´e games, related to two-valued games considered in the context of topological FOL [Makowsky and Ziegler, 1980]. (For lack of space, we omit discussion of quantitative Hennessy-Milner type results beyond the mentioned result by van Breugel and Worrell [2005].)

FO(P) may be seen as a fuzzy variant of Halpern's [1990] type-1 (i.e. statistical) two-valued probabilistic FOL, and uses a syntax related to coalgebraic predicate logic [Litak et al., 2018]. Van-Benthem style theorems for two-valued coalgebraic modal logic [Schr¨oder et al., 2017] instantiate to twovalued probabilistic modal logic, then establishing expressibility of bisimulation-invariant probabilistic FO formulae by probabilistic modal formulae with infinite conjunction but of bounded rank, in an apparent analogy to bounded-rank approximation in the fuzzy setting.

2 Fuzzy Probabilistic Logics

We proceed to introduce the logics featuring in our main result. We fix (w.l.o.g., finite) sets NC of atomic concepts and NR of roles; concepts C,D of quantitative probabilistic ALC (ALC(P)) are defined by the grammar

where q ∈ Q ∩ [0, 1], A ∈ NC and r ∈ NR. The intended reading of P is 'probably'; we give examples below. Slightly deviating from standard practice, we define the rank rk(C) of a concept C as the maximal nesting depth of the P and atomic concepts in C; e.g. rk((Pr. Ps.A)⊓(Pr.B)) = 3. We denote the set of all concepts of rank at most n by ALC(P)n.

Concepts are interpreted over probabilistic structures to which we neutrally refer as interpretations or, briefly, models. We allow infinite models but restrict to discrete probability distributions over successors at each state. A model

consists of a domain ∆I of states or individuals, and interpretations AI : ∆I → [0, 1], rI : ∆I × ∆I → [0, 1] of atomic concepts A and roles r such that for each a ∈ ∆I , the map

is either zero or a probability mass function on ∆I , i.e.

(implying that the support {a′ ∈ ∆I | ra(a′ ) > 0} of ra is at most countable). We call a state a r-blocking if ∑a′∈∆I ra(a′ ) = 0. At non-blocking states a, ra thus acts as a probabilistic accessibility relation; we abuse ra to denote also the probability measure defined by ra.

The interpretation C I : ∆I → [0, 1] of concepts is defined recursively, extending that of atomic concepts, by

At non-blocking a, (Pr.C)I (a) is thus the expected truth value of C for a random r-successor of a. We define disjunction ⊔ as the dual of ⊓ as usual, so ⊔ takes maxima. We use Zadeh semantics for the propositional operators, which will later ensure non-expansiveness wrt. behavioural distance; see additional comments in Section 7.

Up to minor variations, our models correspond to Markov chains or, in an epistemic reading, type spaces (e.g. [Heifetz and Mongin, 2001]). The logic ALC(P) was considered (with Łukasiewicz semantics) by Schr¨oder and Pattinson [2011], and resembles van Breugel and Worrell's quantitative probabilistic modal logic [2005]. E.g., in a reading of ∆I as consisting of real-world individuals, the concept

describes noises you hear in your tent at night as being loud and probably coming from the large and probably angry animal whose shadow just crossed the tent roof. (In this view, P can be usefully combined with crisp or fuzzy relational modalities, using off-the-shelf compositionality mechanisms [Schr¨oder and Pattinson, 2011].) In an epistemic reading where the elements of ∆I are possible worlds, and the roles are understood as epistemic agents, the concept

denotes the degree to which player believes she is successfully bluffing by letting opponent overestimate player's hand.

For readability, we will restrict the technical treatment to a single role r, omitted in the syntax, from now on, noting that covering multiple roles amounts to no more than additional indexing. As the first-order correspondence language of quantitative probabilistic ALC we introduce quantitative probabilistic first-order logic (FO(P)), with formulae φ, ψ, . . . defined by the grammar

where x and y range over a fixed countably infinite reservoir of variables. The reading of xP⌈y : φ⌉ is the expected truth value of φ at a random successor y of x. (In particular, when φ is crisp, then xP⌈y : φ⌉ is just the probability of y satisfying φ, similar to the weights wy(φ) in Halpern's type-1 probabilistic FOL [1990].) We have the expected notions of free and bound variables, under the additional proviso that y (but not x!) is bound in xP⌈y : φ⌉. The (quantifier) rank qr(φ) of a formula φ is the maximal nesting depth of the variable-binding operators ∃ and P and propositional atoms A in φ; e.g. ∃x. xP⌈y : A(y)⌉ has rank 3.

Given a model I = (∆I , (AI )A∈NC , rI ) and a vector ¯a = (a1, . . . , an) ∈ (∆I )n of values, the semantics of the logic assigns a truth value φ(¯a) ∈ [0, 1] to a formula φ(x1, . . . , xn) with free variables at most x1, . . . , xn. We define φ(¯a) recursively by essentially the same clauses as in ALC(P) for the propositional constructs, and

where ∨ takes suprema. Moreover, equality is two-valued, i.e. (xi = xj)(¯a) is 1 if ai = aj , and 0 otherwise.

E.g. the formula xP⌈z : z = y⌉ ('the successor of x is probably y') denotes the access probability from x to y, xP⌈z : zP⌈w : w = y⌉⌉ the probability of reaching y from x in two independently distributed steps, and ∃y. xP⌈z : z = y⌉ the probability of the most probable successor of x.

We have a standard translation STx from ALC(P) into FO(P), indexed over a variable x naming the current state. Following Litak et al. [2018], we define STx recursively by

and by commutation with all other constructs.

Lemma 2.1. For every ALC(P)-concept C and state a, C(a) = STx(C)(a).

ST thus identifies ALC(P) as a fragment of FO(P).

3 Behavioural Distances and Games

We next discuss several notions of behavioural distance between states: via fixed point iteration `a la Wasserstein/Kantorovich, via games and via the logic. We focus mostly on depth-n distances. Only for one version, we define also the unbounded distance, which will feature in the modal characterization result. We show in Section 4 that at finite depth, all these distances coincide. It has been shown in previous work [Desharnais et al., 2004; van Breugel and Worrell, 2005] that the unbounded-depth distances defined via Kantorovich fixed point iteration and via the logic, respectively, coincide in very similar settings; such results can be seen as probabilistic variants of the Hennessy-Milner theorem.

We recall standard notions on pseudometric spaces:

Definition 3.1 (Pseudometric spaces, non-expansive maps). A (bounded) pseudometric on a set X is a function d: X × X → [0, 1] such that for x, y, z ∈ X, the following axioms hold: d(x, x) = 0 (reflexivity), d(x, y) = d(y, x) (symmetry), d(x, z) ≤ d(x, y) + d(y, z) (triangle inequality). If additionally d(x, y) = 0 implies x = y, then d is a metric. A (pseudo)metric space (X, d) consists of a set X and a (pseudo)metric d on X.

A map f : X → [0, 1] is non-expansive wrt. a pseudometric d if |f(x) - f(y)| ≤ d(x, y) for all x, y ∈ X. The space of these non-expansive functions, denoted Pred(X, d), is equipped with the supremum (pseudo)metric d∞,

We denote by Bϵ(x) = {y ∈ X | d(x, y) ≤ ϵ} the ball of radius ϵ around x in (X, d). The space (X, d) is totally bounded if for every ϵ > 0 there exists a finite ϵ-cover, i.e. finitely many elements x1, . . . , xn ∈ X such that X = ⋃ni=1 Bϵ(xi).

Recall that a metric space is compact iff it is complete and totally bounded.

We next introduce the Wasserstein and Kantorovich distances, which coincide according to Kantorovich-Rubinstein duality. To this end, we first need the notion of a coupling of two probability distributions, from which the original distributions are factored out as marginals.

Definition 3.2. Let π1 and π2 be discrete probability measures on A and B, respectively. We denote by Cpl(π1, π2) the set of couplings of π1 and π2, i.e. probability measures µ on A × B such that π1 and π2 are marginals of µ:

• for all a ∈ A, ∑b∈B µ(a, b) = π1(a);
• for all b ∈ B, ∑a∈A µ(a, b) = π2(b).

Definition 3.3 (Wasserstein and Kantorovich distances). Let (X, d) be a pseudometric space. We generally write

DX

for the set of discrete probability distributions on X. We define two pseudometrics on DX, the Kantorovich distance d↑ and the Wasserstein distance d↓ :

where ∧ takes meets (and ∨ suprema). We extend these distances without further mention to zero functions (like the functions ra at blocking states a) by decreeing that the zero function has distance 1 from all probability distributions.

The notation d↑ , d↓ is meant as a mnemonic for the fact that these distances are obtained via suprema respectively via infima. If (X, d) is separable (contains a countable dense subset), these pseudometrics coincide, a fact known as the Kantorovich-Rubinstein duality (e.g. [Dudley, 2002]):

Lemma 3.4 (Kantorovich-Rubinstein duality). Let (X, d) be a separable pseudometric space. Then for all π1, π2 ∈ DX,

The above notions of lifting a distance on X to a distance on distributions over X can be used to give fixed point equations for behavioural distances on models.

Definition 3.5 (Fixed point iteration `a la Wasserstein/Kantorovich). Given a model I, we define the chains (dKn ), (dWn ) of depth-n Kantorovich and Wasserstein distances, respectively, via fixed point iteration:

where ∨ is binary join. We extend this to states a, b in different models I, J by taking the disjoint union of I, J .

In both cases, we start with the zero pseudometric, and in the next iteration lift the pseudometric dn from the previous step via Wasserstein/Kantorovich. This lifted metric is then applied to the probability distributions πa, πb associated with a, b. In addition we take the maximum with the supremum over the distances for all atomic A ∈ NC.

We now introduce a key tool for our technical development, a new up-to-ϵ bisimulation game inspired by the definition of the Wasserstein distance.

Definition 3.6 (Bisimulation game). Given models I, J , a0 ∈ ∆I , b0 ∈ ∆J , and ϵ0 ∈ [0, 1], the ϵ0-bisimulation game for a0 and b0 is played by Spoiler (S) and Duplicator (D), with rules as follows:

• Configurations: triples (a, b, ϵ), with states a ∈ ∆I , b ∈ ∆J and maximal allowed deviation ϵ ∈ [0, 1]. The initial configuration is (a0, b0, ϵ0).
• Moves: In each round, D first picks a probability measure µ ∈ Cpl(πa, πb). Then, D distributes the deviation ϵ over all pairs (a′ , b′ ) of successors, i.e. picks a function ϵ′ : ∆I ×∆J → [0, 1] such that Eµ(ϵ′ ) ≤ ϵ. Finally, S picks a pair (a′ , b′ ) with µ(a′ , b′ ) > 0; the new configuration is then (a′ , b′ , ϵ′ (a′ , b′ )).
• D wins if both states are blocking or ϵ = 1.
• S wins if exactly one state is blocking and ϵ < 1.
• Winning condition: |AI (a)-AJ (b)| ≤ ϵ for all A ∈ NC.

The game comes in two variants, the (unbounded) bisimulation game and the n-round bisimulation game, where n ≥ 0. Player D wins if the winning condition holds before every round, otherwise S wins. More precisely, D wins the unbounded game if she can force an infinite play and the nround game once n rounds have been played (the winning condition is not checked after the last round, so in particular, any 0-round game is an immediate win for D).

Remark 3.7. The above bisimulation game differs from bisimulation games in the literature (e.g. [Desharnais et al., 2008]) in a number of salient features. A particularly striking aspect is that D's moves are not similar to those of S, and moreover D in fact moves before S. Intuitively, D is required to commit beforehand to a strategy that she will use to respond to S's next move. Note also that the precision ϵ changes as the game is being played, a complication forced by the arithmetic nature of models.

This leads to notions of game distance:

Definition 3.8. depth-n game distance dGn and (unboundeddepth) game distance dG are defined as

where G(a, b, ϵ) and Gn(a, b, ϵ) denote the the bisimulation game and the n-round bisimulation game on (a, b, ϵ), respectively.

Finally we define the depth-n logical distance via ALC(P), restricting to concepts of rank at most n:

Definition 3.9. The depth-n logical distance dLn (a, b) of states a, b in models I, J is defined as

The equivalence of the four bounded-depth behavioural distances introduced above will be shown in Theorem 4.3.

Behavioural distance forms the yardstick for our notion of bisimulation invariance; for definiteness:

Definition 3.10. A quantitative, i.e. [0, 1]-valued, property Q of states, or a formula or concept defining such a property, is bisimulation-invariant if Q is non-expansive wrt. game distance, i.e. for states a, b in models I, J , respectively,

Similarly, Q is depth-n bisimulation invariant, or finite-depth bisimulation invariant if mention of n is omitted, if Q is nonexpansive wrt. dGn in the same sense.

It is easy to see that ALC(P)-concepts are bisimulationinvariant. More precisely, ALC(P)-concepts of rank at most n are depth-n bisimulation invariant (a stronger invariance since clearly dGn ≤ dG), as shown by routine induction. In contrast, many other properties of states are expressible in FO(P) but not in ALC(P), as they fail to be bisimulationinvariant. Examples include xP⌈y : x = y⌉ (probability of a self-transition) and ∃z. xP⌈y : y = z⌉ (highest transition probability to a successor).

We are now ready to formally state our main theorem (a proof will be given in Section 6):

Theorem3.11 (Modal characterization). Every bisimulationinvariant FO(P)-formula of rank at most n can be approximated (uniformly across all models) by ALC(P)-concepts of rank at most 3n .

(The exponential bound on the rank features also in the full statement of van Benthem's theorem.)

4 Modal Approximation at Finite Depth

We now establish the most important stepping stone on the way to the eventual proof of the modal characterization theorem: We show that every depth-n bisimulation-invariant property of states can be approximated by ALC(P)-concepts of rank at most n. We prove this simultaneously with coincidence of the various finite-depth behavioural pseudometrics defined in the previous section. To begin,

Lemma 4.1. The game-based pseudometric dGn coincides with the Wasserstein pseudometric dWn ,

We note next that the modality P is non-expansive: We extend P to act on [0, 1]-valued functions f : ∆I → [0, 1] by

Lemma 4.2. The map f ↦→ Pf is non-expansive wrt. the supremum metric, that is ‖Pf - Pg‖∞ ≤ ‖f - g‖∞ for all f, g : ∆I → [0, 1].

Following our previous work [Wild et al., 2018], we prove coincidence of the remaining pseudometrics in one big induction, along with total boundedness (needed later to apply a variant of the Arzel`a-Ascoli theorem and the KantorovichRubinstein duality) and modal approximability of depth-n bisimulation-invariant properties. We phrase the latter as density of the (semantics of) ALC(P)-concepts of rank at most n in the non-expansive function space (Definition 3.1):

Theorem 4.3. Let I be a model. Then for all n ≥ 0,

1. we have dGn = dWn = dKn = dLn =: dn on I;
2. the pseudometric space (∆I , dn) is totally bounded;
3. ALC(P)n is a dense subset of Pred(∆I , dn).

Proof sketch. By simultaneous induction on n.

In the base case n = 0, all the behavioural distances are the zero pseudometric, so that total boundedness follows trivially and the density claim follows because non-expansive maps are just constants in [0, 1] and the syntax of ALC(P) includes truth constants q ∈ Q ∩ [0, 1].

For the inductive step, let I be a model and n > 0, and assume as the inductive hypothesis that all claims in Theorem 4.3 hold for all n′ < n. We begin with Item 1; dGn = dWn is already proved (Lemma 4.1).

• dWn = dKn follows by Kantorovich-Rubinstein duality (Lemma 3.4), since every totally bounded pseudometric space is separable.
• dKn = dLn : By Lemma 4.2 and the inductive hypothesis, P[ALC(P)n-1] is dense in P[Pred(∆I , dn-1)]. Thus, the supremum in the definition of dKn does not change when it is taken only over the concepts in ALC(P)n-1 instead of all nonexpansive properties. The proof is finished by a simple induction over propositional combinations of concepts.

Item 2: By the inductive hypothesis, the space (∆I , dn-1) is totally bounded. By the Arzel`a-Ascoli theorem (in a version for totally bounded spaces and non-expansive maps, cf. [Wild et al., 2018]), it follows that Pred(∆I , dn-1) is totally bounded wrt. the supremum pseudometric. This implies that depth-n distances can be approximated up to ϵ by examining differences at only finitely many, say m, concepts. As ([0, 1]m, d∞) is totally bounded, (∆I , dn) is, too.

Item 3: By the Stone-Weierstraß theorem (again in a version for totally bounded spaces and non-expansive maps [Wild et al., 2018]) it suffices to give, for each ϵ > 0, each non-expansive map f ∈ Pred(∆I , dn), and each pair of states a, b ∈ ∆I a concept C ∈ ALC(P)n such that

To construct such a C, we note that |f(a) - f(b)| ≤ dLn (a, b) (by non-expansiveness), so there exists some D ∈ ALC(P)n such that |DI (a)-DI (b)| ≥ |f(a)-f(b)|-ϵ. FromD, we can construct C using truncated subtraction ⊖.

This completes the proof of Theorem 4.3. Now that we can approximate depth-k bisimulation-invariant properties by ALC(P)-concepts of rank k on any fixed model, we need to make the approximation uniform across all models. We achieve this by means of a final model, i.e. one that realizes all behaviours. Formally:

Definition 4.4. A (probabilistic) bounded morphism between models I, J is a map f : ∆I → ∆J such that AI = f -1 [AJ ] for each A ∈ NC and rf(a)(B) = ra(f -1 [B]) for all B ⊆ ∆J , a ∈ ∆I (implying that a is blocking iff f(a) is blocking). A model F is final if for every model I, there exists a unique bounded morphism I → F.

It follows from standard results in coalgebra [Barr, 1993] that a final model exists. Bounded morphisms preserve behaviour on-the-nose, that is:

Lemma 4.5. Let f : I → J be a bounded morphism. Then, for any a ∈ ∆I , dG(a, f (a)) = 0.

This entails the following lemma, which will enable us to use approximants on the final model as uniform approximants across all models:

Lemma 4.6. Let F be a final model, and let φ and ψ be bisimulation-invariant first-order properties. Then, for any model I, ‖φ - ψ‖I∞ ≤ ‖φ - ψ‖F∞.

5 Locality

The proof of the modal characterization theorem now further proceeds by first establishing that every bisimulationinvariant first-order formula φ is local in a sense to be made precise shortly, and subsequently that φ is in fact even finitedepth bisimulation invariant, for a depth that is exponential in the rank of φ. Locality refers to a probabilistic variant of Gaifman graphs [Gaifman, 1982]:

Definition 5.1. Let I be a model.

• The Gaifman graph of I is the undirected graph on the set ∆I of vertices that has an edge for every pair (a, b) with rI (a, b) > 0 or rI (b, a) > 0.
• The Gaifman distance D: ∆I × ∆I → N ∪ {∞} is graph distance in the Gaifman graph: For every a, b ∈ ∆I , the distance D(a, b) is the least number of edges on any path from a to b, if such a path exists, and ∞ otherwise.
• For a ∈ ∆I and k ≥ 0, the radius k neighbourhood U k (a) = {b ∈ ∆I | D(a, b) ≤ k} of a consists of the states reachable from a in at most k steps.
• The restriction of I to U k (a) is the model I k a with set U k (a) of states, and

The restriction to U k (a) thus makes all states at distance k blocking. Restricted models have the expected relationship with games of bounded depth:

Lemma 5.2. Let a be a state in a model I. Then D wins the k-round 0-bisimulation game for I, a and I k a , a.

Locality of a formula now means that its truth values only depend on the neighbourhood of the state in question:

Definition 5.3. A formula φ(x) is k-local for a radius k if for every model I and every a ∈ ∆I , φI (a) = φI k a (a).

As ALC(P)-concepts are bisimulation-invariant, Lemma 5.2 implies

Lemma 5.4. Every ALC(P)-concept of rank at most k is klocal.

To prove locality of bisimulation-invariant FO(P)-formulae, we require a model-theoretic tool, an adaptation of Ehrenfeucht-Fra¨ıss´e equivalence to the probabilistic setting:

Definition 5.5. Let I, J be models, and let ¯a0 and ¯b0 be vectors of equal length over ∆I and ∆J , respectively. The Ehrenfeucht-Fra¨ıss´e game for I, ¯a0 and J ,¯b0, played by Spoiler (S) and Duplicator (D), is given as follows.

• Configurations: pairs (¯a,¯b) of vectors ¯a over ∆I and ¯b over ∆J ; the initial configuration is (¯a0, ¯b0).
• Moves: Each round can be played in one of two ways, chosen by S:
• Standard round: S selects a state in one model, say a ∈ ∆I , and D then has to select a state in the other model, say b ∈ ∆J , reaching the configuration (¯aa, ¯bb).
• Probabilistic round: S selects an index i and a fuzzy subset in one model, say φA : ∆I → [0, 1]. D then has to select a fuzzy subset in the other model, say φB : ∆J → [0, 1], such that Erai (φA) = Erbi (φB). Then, S selects an element on one side, say a ∈ ∆I , such that rai (a) > 0, and D subsequently selects an element on the other side, say b ∈ ∆J , such that φA(a) = φB(b) and rbi (b) > 0, reaching the configuration (¯aa, ¯bb).
• Winning conditions: Any player who cannot move loses. S wins if a configuration is reached (including the initial configuration) that fails to be a partial isomorphism. Here, a configuration (¯a, ¯b) is a partial isomorphism if

• AI (ai) = AJ (bi) for all i and all A ∈ NC
• rI (ai, aj) = rJ (bi, bj) for all i, j.

Player D wins if she reaches the n-th round (maintaining configurations that are not winning for S).

For our purposes, we need only soundness of EhrenfeuchtFra¨ıss´e equivalence:

Lemma 5.6 (Ehrenfeucht-Fra¨ıss´e invariance). Let I, J be models, and let ¯a0,¯b0 be vectors of length m over ∆I and ∆J , respectively, such that D wins the n-round EhrenfeuchtFra¨ıss´e game on ¯a0, ¯b0. Then for every FO(P)-formula φ with qr(φ) ≤ n and free variables at most x1, . . . , xm,

Since embeddings into disjoint unions of models are bounded morphisms, the following is immediate from Lemma 4.5:

Lemma 5.7. Every bisimulation-invariant formula is also invariant under disjoint union.

We are now in a position to prove our desired locality result: Lemma 5.8 (Locality). Let φ(x) be a bisimulation-invariant FO(P)-formula of rank n with one free variable x. Then φ is k-local for k = 3n .

Proof sketch. Let a be a state in a model I. We need to show φI (a) = φI k a (a). Construct models J ,K that extend I and I k a , respectively, by adding n disjoint copies of both I and I k a . We finish the proof by showing that

The first and third equality follow by bisimulation invariance of φ (Lemma 5.7), and the second using Lemma 5.6, by giving a winning invariant for D in the n-round EhrenfeuchtFra¨ıss´e game for J , a and K, a.

6 Proof of the Main Result

Having established locality of bisimulation-invariant firstorder formulae and modal approximability of finite-depth bisimulation-invariant properties, we now discharge the last remaining steps in our programme: We show by means of an unravelling construction that bisimulation-invariant first-order formulae are already finite-depth bisimulationinvariant, and then conclude the proof of our main result, the modal characterization theorem.

Definition 6.1. Let I be a model. The unravelling I ∗ of I is a model with non-empty finite sequences ¯a ∈ (∆I )+ as states, where atomic concepts and roles are interpreted by

for ¯a ∈ (∆I )+ and a ∈ ∆I , where last takes last elements.

As usual, models are bisimilar to their unravellings:

Lemma 6.2. For any model I and a ∈ ∆I , D has a winning strategy in the 0-bisimulation game for I, a and I ∗ , a.

We next show that locality and bisimulation invariance imply finite-depth bisimulation invariance:

Lemma 6.3. Let φ be bisimulation invariant and k-local. Then φ is depth-k bisimulation invariant.

Proof sketch. By unravelling (Lemma 6.2) and locality (Lemma 5.2), we need only consider depth-k tree models. On such models, winning strategies in k-round bisimulation games automatically win also the unrestricted game.

This allows us to wrap up the proof of our main result:

Proof of Theorem 3.11. Let φ be a probabilistic first-order formula of rank n. By Lemma 5.8 and Lemma 6.3, φ is depthk bisimulation-invariant for k = 3n . By Theorem 4.3, for every ϵ > 0, there exists an ALC(P) concept Cϵ of rank at most k such that ‖φF -C F ϵ ‖∞ ≤ ϵ on the final model F. By Lemma 4.6, this approximation works over all models.

7 Conclusions

We have established a modal characterization result for a probabilistic fuzzy DL ALC(P), stating that every formula of quantitative probabilistic FOL that is bisimulation-invariant, i.e. non-expansive wrt. a natural notion of behavioural distance, can be approximated by ALC(P)-concepts of bounded modal rank, the bound being exponential in the rank of the original formula. As discussed in the introduction, the bound on the modal rank is the crucial feature making this result into a van-Benthem (rather than Hennessy-Milner) type theorem.

It remains open whether our main result can be sharpened to make do without approximation. (Similar open problems persist for the case of fuzzy modal logic [Wild et al., 2018] and two-valued probabilistic modal logic [Schr¨oder et al., 2017].) Further directions for future research include a treatment of Łukasiewicz semantics of the propositional connectives (for which non-expansiveness in fact fails). Moreover, the version of our main result that restricts the semantics to finite models, in analogy to Rosen's finite-model version of van Benthem's theorem [Rosen, 1997], remains open.