--- title: "A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic" authors: - "Paul Wild" - "Lutz Schröder" - "Dirk Pattinson" - "Barbara König" doi: "10.24963/ijcai.2019/263" url: "https://ijcai.org/proceedings/2019/263" pdf: "https://ijcai.org/proceedings/2019/0263.pdf" venue: "Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence" year: 2019 pages: "1900-1906" track: "Main track" keywords: - "Knowledge Representation and Reasoning: Non-classical Logics for Knowledge Representation" - "Uncertainty in AI: Uncertainty in AI" - "Knowledge Representation and Reasoning: Reasoning about Knowlege and Belief" - "Knowledge Representation and Reasoning: Description Logics and Ontologies" --- # A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König *Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence*, pages 1900-1906. DOI: [10.24963/ijcai.2019/263](https://doi.org/10.24963/ijcai.2019/263) ## Abstract The fuzzy modality probably is interpreted over probabilistic type spaces by taking expected truth values. The arising probabilistic fuzzy description logic is invariant under probabilistic bisimilarity; more informatively, it is non-expansive wrt. a suitable notion of behavioural distance. In the present paper, we provide a characterization of the expressive power of this logic based on this observation: We prove a probabilistic analogue of the classical van Benthem theorem, which states that modal logic is precisely the bisimulation-invariant fragment of first-order logic. Specifically, we show that every formula in probabilistic fuzzy first-order logic that is non-expansive wrt. behavioural distance can be approximated by concepts of bounded rank in probabilistic fuzzy description logic. ## Full text ## 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. ## References 1. [Baldan et al., 2014] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral metrics via func- tor lifting. In Found. Software Tech. Theor. Comput. Sci., FSTTCS 2014, volume 29 of LIPIcs, pages 403-415, 2014. 2. [Barr, 1993] Michael Barr. Terminal coalgebras in well- founded set theory. Theor. Comp. Sci., 114:299-315, 1993. 3. [Burgess, 1969] John Burgess. Probability logic. J. Symb. Log., 34:264-274, 1969. 4. [Desharnais et al., 2004] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318:323- 354, 2004. 5. [Desharnais et al., 2008] Josée Desharnais, Franc ¸ois Lavio- lette, and Mathieu Tracol. Approximate analysis of proba- bilistic processes: Logic, simulation and games. In Quan- titative Evaluation of Systems, QEST 2008, pages 264- 273. IEEE, 2008. 6. [Dudley, 2002] Richard Dudley. Real Analysis and Proba- bility. Cambridge University Press, 2nd edition, 2002. 7. [Figueira et al., 2015] Diego Figueira, Santiago Figueira, and Carlos Areces. Model theory of XPath on data trees. Part I: Bisimulation and characterization. J. Artif. Intell. Res. (JAIR), 53:271-314, 2015. 8. [Flaminio and Godo, 2007] Tommaso Flaminio and Lluis Godo. A logic for reasoning about the probability of fuzzy events. Fuzzy Sets and Systems, 158(6):625-638, 2007. 9. [Gaifman, 1982] Haim Gaifman. On local and non-local properties. In Logic Colloq. 1981, pages 105-135, 1982. 10. [Giacalone et al., 1990] Alessandro Giacalone, Chi Jou, and Scott Smolka. Algebraic reasoning for probabilistic con- current systems. In Programming Concepts and Methods, pages 443-458. North-Holland, 1990. 11. [Hájek, 2007] Petr Hájek. Complexity of fuzzy probability logics II. Fuzzy Sets and Systems, 158:2605-2611, 2007. 12. [Halpern and Rabin, 1987] Joseph Halpern and Michael Ra- bin. A logic to reason about likelihood. Artif. Intell., 32:379-405, 1987. 13. [Halpern, 1990] Joseph Halpern. An analysis of first-order logics of probability. Artif. Intell., 46:311-350, 1990. 14. [Hamblin, 1959] Charles Hamblin. The modal 'probably'. Mind, 68:234-240, 1959. 15. [Heifetz and Mongin, 2001] Aviad Heifetz and Philippe Mongin. Probabilistic logic for type spaces. Games Econ. Behav., 35:31-53, 2001. 16. [Hennessy and Milner, 1985] Matthew Hennessy and Robin Milner. Algebraic laws for non-determinism and concur- rency. J. ACM, 32:137-161, 1985. 17. [Herzig, 2003] Andreas Herzig. Modal probability, belief, and actions. Fund. Inf., 57:323-344, 2003. 18. [Huth and Kwiatkowska, 1997] Michael Huth and Marta Kwiatkowska. Quantitative analysis and model checking. In Logic in Computer Science, LICS 1997, pages 111-122. IEEE, 1997. 19. [Janin and Walukiewicz, 1995] David Janin and Igor Walukiewicz. Automata for the modal µ-calculus and related results. In Mathematical Foundations of Computer Science, MFCS 1995, volume 969 of LNCS, pages 552-562. Springer, 1995. 20. [Kozen, 1985] Dexter Kozen. A probabilistic PDL. J. Com- put. Sys. Sci., 30(2):162-178, 1985. 21. [Larsen and Skou, 1991] Kim Larsen and Arne Skou. Bisim- ulation through probabilistic testing. Inf. Comput., 94:1- 28, 1991. 22. [Litak et al., 2018] Tadeusz Litak, Dirk Pattinson, Katsuhiko Sano, and Lutz Schröder. Model theory and proof theory of coalgebraic predicate logic. Log. Meth. Comput. Sci., 14(1), 2018. 23. [Lukasiewicz and Straccia, 2008] Thomas Lukasiewicz and Umberto Straccia. Managing uncertainty and vagueness in description logics for the semantic web. J. Web Sem., 6:291-308, 2008. 24. [Makowsky and Ziegler, 1980] Johann Makowsky and Mar- tin Ziegler. Topological model theory with an interior op- erator: consistency properties and back -and forth argu- ments. Arch. math. Logik, 20:27-54, 1980. 25. [Otto, 2004] Martin Otto. Elementary proof of the van Benthem-Rosen characterisation theorem. Technical Re- port 2342, TU Darmstadt, 2004. 26. [Rosen, 1997] Eric Rosen. Modal logic over finite structures. J. Logic Lang. Inform., 6(4):427-439, 1997. 27. [Schröder and Pattinson, 2011] Lutz Schröder and Dirk Pat- tinson. Description logics and fuzzy probability. In IJCAI 2011, pages 1075-1081, 2011. 28. [Schröder et al., 2017] Lutz Schröder, Dirk Pattinson, and Tadeusz Litak. A van Benthem/Rosen theorem for coalge- braic predicate logic. J. Log. Comput., 27:749-773, 2017. 29. [Sturm and Wolter, 2001] Holger Sturm and Frank Wolter. First-order expressivity for S5-models: Modal vs. two- sorted languages. J. Philos. Logic, 30:571-591, 2001. 30. [van Benthem, 1976] Johan van Benthem. Modal Corre- spondence Theory. PhD thesis, Univ. of Amsterdam, 1976. 31. [van Breugel and Worrell, 2005] Franck van Breugel and James Worrell. A behavioural pseudometric for probabilis- tic transition systems. Theor. Comput. Sci., 331:115-142, 2005. 32. [Wild and Schröder, 2017] Paul Wild and Lutz Schröder. A characterization theorem for a modal description logic. In IJCAI 2017, pages 1304-1310, 2017. 33. [Wild et al., 2018] Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König. A van Benthem theorem for fuzzy modal logic. In Logic in Computer Science, LICS 2018, pages 909-918. ACM, 2018. 34. [Zadeh, 1968] Lotfi Zadeh. Probability measures of fuzzy events. J. Math. Anal. Appl., 23:421-427, 1968.