A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic

TL;DR

This paper establishes a probabilistic analogue of the van Benthem theorem for fuzzy description logic, characterizing its expressive power through invariance under probabilistic bisimilarity and behavioral distance.

Contribution

It proves that non-expansive probabilistic fuzzy first-order formulas can be approximated by bounded rank concepts in probabilistic fuzzy description logic, extending classical modal logic results.

Findings

Probabilistic fuzzy description logic is invariant under probabilistic bisimilarity.

Non-expansive formulas can be approximated by bounded rank concepts.

The paper provides a probabilistic van Benthem theorem analogue.

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. For a modal logic perspective on the same result, see arXiv:1810.04722.

Equations

$$C,D::=q\mid A\mid C\ominus q\mid \neg C\mid C\sqcap D\mid \text{P}r.C$$

$$\mathcal{I}=({\Delta }^{\mathcal{I}},(A^{\mathcal{I}}{)}_{A\in {\mathsf{N}}_{\mathsf{C}}},(r^{\mathcal{I}}{)}_{r\in {\mathsf{N}}_{\mathsf{R}}})$$

$$r_a:{\Delta }^{\mathcal{I}}\to [0,1],r_a(a^{\prime })=r^{\mathcal{I}}(a,a^{\prime })$$

$${\sum }_{a^{\prime }\in {\Delta }^{\mathcal{I}}}{r}_a(a^{\prime })\in \{0,1\}$$

$$q^{\mathcal{I}}(a)$$

$$(C\ominus q{)}^{\mathcal{I}}(a)$$

$$(\neg C{)}^{\mathcal{I}}(a)$$

$$(C\sqcap D{)}^{\mathcal{I}}(a)$$

$$(\text{P}r.C{)}^{\mathcal{I}}(a)$$

$$\mathsf{Loud}\sqcap \text{P}\mathsf{hasSource}.(\mathsf{Large}\sqcap \text{P}\mathsf{hasMood}.\mathsf{Angry})$$

$$\neg \mathsf{GoodHand}\sqcap \text{P}\mathsf{player}.\text{P}\mathsf{opponent}.\mathsf{GoodHand}$$

$$\begin{gathered} \varphi ,\psi ::=q\mid A(x)\mid x=y\mid \varphi \ominus q\mid \neg \varphi \mid \varphi \sqcap \psi \mid \exists x.\varphi \\ \mid x\text{P}\lceil y:\varphi \rceil (q\in \mathbb{Q}\cap [0,1],A\in {\mathsf{N}}_{\mathsf{C}}) \end{gathered}$$

$$A(x_i)(\bar{a})$$

$$(\exists x_0.\varphi (x_0,x_1,\dots ,x_n))(\bar{a})$$

$$(x_i\text{P}\lceil y:\varphi (y,x_1,\dots ,x_n)\rceil )(\bar{a})$$

$${\mathsf{ST}}_x(A)$$

$${\mathsf{ST}}_x(\text{P}C)$$

$$d_{\infty }(f,g)=\Vert f-g{\Vert }_{\infty }={\bigvee }_{x\in X}|f(x)-g(x)|.$$

$$\mathcal{D}X$$

$$d^{\uparrow }({\pi }_1,{\pi }_2)=\bigvee \{|E_{{\pi }_1}(f)-E_{{\pi }_2}(f)|\mid f\in \mathrm{Pred}(X,d)\}$$

$$d^{\downarrow }({\pi }_1,{\pi }_2)=\bigwedge \{E_{\mu }(d)\mid \mu \in \mathrm{Cpl}({\pi }_1,{\pi }_2)\}$$

$$d^{\uparrow }({\pi }_1,{\pi }_2)=d^{\downarrow }({\pi }_1,{\pi }_2).$$

$$d_0^W(a,b)=d_0^K(a,b)=0$$

$$d_{n+1}^W(a,b)={\bigvee }_{A\in {\mathsf{N}}_{\mathsf{C}}}|A^{\mathcal{I}}(a)-A^{\mathcal{I}}(b)|\vee (d_n^W{)}^{\downarrow }({\pi }_a,{\pi }_b)$$

$$d_{n+1}^K(a,b)={\bigvee }_{A\in {\mathsf{N}}_{\mathsf{C}}}|A^{\mathcal{I}}(a)-A^{\mathcal{I}}(b)|\vee (d_n^K{)}^{\uparrow }({\pi }_a,{\pi }_b)$$

$$d_n^G(a,b)$$

$$d^G(a,b)$$

$$d_n^L(a,b)=\bigvee \{|C^{\mathcal{I}}(a)-C^{\mathcal{J}}(b)|\mid \mathrm{rk}(C)\le n\}.$$

$$|Q(a)-Q(b)|\le d^G(a,b).$$

$$(\text{P}f)(a)$$

$$\max (|f(a)-C^{\mathcal{I}}(a)|,|f(b)-C^{\mathcal{I}}(b)|)\le ϵ.$$

$$A^{{\mathcal{I}}_a^k}(b)$$

$$\varphi ({\bar{a}}_0)=\varphi ({\bar{b}}_0).$$

$${\varphi }^{\mathcal{I}}(a)={\varphi }^{\mathcal{J}}(a)={\varphi }^{\mathcal{K}}(a)={\varphi }^{{\mathcal{I}}_a^k}(a).$$

$$A^{{\mathcal{I}}^{\ast }}(\bar{a})=A^{\mathcal{I}}(\mathsf{last}(\bar{a}))r^{{\mathcal{I}}^{\ast }}(\bar{a},\bar{a}a)=r^{\mathcal{I}}(\mathsf{last}(\bar{a}),a),$$

$$Ff(\xi (a))=\zeta (f(a))$$

Full text

For a modal logic perspective on the same result, see Wild et al. (2018b).

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); Lutz and Schröder (2010). 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 Zadeh (1968), interprets $\textsf{P}\,\phi$ as the expected truth value of $\phi$. It appears in various fuzzy propositional Hájek (2007); Flaminio and Godo (2007), modal Desharnais et al. (1999); van Breugel and Worrell (2005), fixpoint Kozen (1985); Huth and Kwiatkowska (1997), and description logics Schröder 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 $\mathcal{ALC}$ or $\mathcal{ALC}(\textsf{P})$, within a natural ambient probabilistic fuzzy first-order logic $\mathsf{FO}(\textsf{P})$, by providing a modal characterization theorem. The prototype of such characterization theorems is van Benthem’s theorem van Benthem (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. (1999); van Breugel and Worrell (2005); Desharnais et al. (2008); Baldan et al. (2014). When propositional connectives are equipped with Zadeh semantics, $\mathcal{ALC}(\textsf{P})$ is non-expansive wrt. behavioural distance; we continue to refer to this property as bisimulation invariance. In previous work Wild et al. (2018a) we have shown that relational fuzzy modal logic is the bisimulation-invariant fragment of fuzzy FOL, more precisely that every bisimulation-invariant 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 $\mathcal{ALC}$. This means not only that, up to approximation, $\mathcal{ALC}(\textsf{P})$ is as powerful as $\mathsf{FO}(\textsf{P})$ on bisimulation-invariant properties, but also that $\mathcal{ALC}(\textsf{P})$ provides effective syntax for bisimulation-invariant $\mathsf{FO}(\textsf{P})$, which $\mathsf{FO}(\textsf{P})$ itself does not Otto (2006).

Proofs are mostly omitted or only sketched; full proofs are in the appendix.

Related Work

There is widespread interest in modal characterization theorems in modal logic Dawar and Otto (2005), database theory Figueira et al. (2015), concurrency Janin and Walukiewicz (1995); Carreiro (2015), and AI Sturm and Wolter (2001); Wild and Schröder (2017); Wild et al. (2018a). The overall structure of our proof builds partly on that of our modal characterization theorem for relational fuzzy modal logic Wild et al. (2018a) (in turn based ultimately on a strategy due to Otto 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-$\epsilon$ (different from games introduced by Desharnais et al. Desharnais et al. (2008), which characterize a different metric) and Ehrenfeucht-Fraïssé 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 van Breugel and Worrell (2005).)

$\mathsf{FO}(\textsf{P})$ may be seen as a fuzzy variant of Halpern’s Halpern (1990) type-1 (i.e. statistical) two-valued probabilistic FOL, and uses a syntax related to coalgebraic predicate logic Litak et al. (2018) and, ultimately, Chang’s modal predicate logic Chang (1973). Van-Benthem style theorems for two-valued coalgebraic modal logic Schröder et al. (2017) instantiate to two-valued 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 $\mathsf{N}_{\mathsf{C}}$ of atomic concepts and ${\mathsf{N}_{\mathsf{R}}}$ of roles; concepts $C,D$ of quantitative probabilistic $\mathcal{ALC}$ ($\mathcal{ALC}(\textsf{P})$) are defined by the grammar

[TABLE]

where $q\in\mathbb{Q}\cap[0,1]$, $A\in\mathsf{N}_{\mathsf{C}}$ and $r\in{\mathsf{N}_{\mathsf{R}}}$. The intended reading of P is ‘probably’; we give examples below. Slightly deviating from standard practice, we define the rank $\operatorname{\mathsf{rk}}(C)$ of a concept $C$ as the maximal nesting depth of the P and atomic concepts in $C$; e.g. $\operatorname{\mathsf{rk}}((\textsf{P}\,r.\,\textsf{P}\,s.\,A)\mathop{\sqcap}(\textsf{P}\,r.\,B))=3$. We denote the set of all concepts of rank at most $n$ by $\mathcal{ALC}(\textsf{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

[TABLE]

consists of a domain $\Delta^{\mathcal{I}}$ of states or individuals, and interpretations $A^{\mathcal{I}}\colon\Delta^{\mathcal{I}}\to[0,1]$, $r^{\mathcal{I}}\colon\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}\to[0,1]$ of atomic concepts $A$ and roles $r$ such that for each $a\in\Delta^{\mathcal{I}}$, the map

[TABLE]

is either zero or a probability mass function on $\Delta^{\mathcal{I}}$, i.e.

[TABLE]

(implying that the support $\{a^{\prime}\in\Delta^{\mathcal{I}}\mid r_{a}(a^{\prime})>0\}$ of $r_{a}$ is at most countable). We call a state $a$ $r$-blocking if $\sum_{a^{\prime}\in\Delta^{\mathcal{I}}}r_{a}(a^{\prime})=0$. At non-blocking states $a$, $r_{a}$ thus acts as a probabilistic accessibility relation; we abuse $r_{a}$ to denote also the probability measure defined by $r_{a}$.

The interpretation $C^{\mathcal{I}}\colon\Delta^{\mathcal{I}}\to[0,1]$ of concepts is defined recursively, extending that of atomic concepts, by

[TABLE]

At non-blocking $a$, $(\textsf{P}\,r.\,C)^{\mathcal{I}}(a)$ is thus the expected truth value of $C$ for a random $r$-successor of $a$. We define disjunction $\mathop{\sqcup}$ as the dual of $\mathop{\sqcap}$ as usual, so $\mathop{\sqcup}$ 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 $\mathcal{ALC}(\textsf{P})$ was considered (with Łukasiewicz semantics) by Schröder and Pattinson Schröder and Pattinson (2011), and resembles van Breugel and Worrell’s quantitative probabilistic modal logic van Breugel and Worrell (2005). E.g., in a reading of $\Delta^{\mathcal{I}}$ as consisting of real-world individuals, the concept

[TABLE]

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öder and Pattinson (2011).) In an epistemic reading where the elements of $\Delta^{\mathcal{I}}$ are possible worlds, and the roles are understood as epistemic agents, the concept

[TABLE]

denotes the degree to which $\mathsf{player}$ believes she is successfully bluffing by letting $\mathsf{opponent}$ overestimate $\mathsf{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 $\mathcal{ALC}$ we introduce quantitative probabilistic first-order logic ($\mathsf{FO}(\textsf{P})$), with formulae $\phi,\psi,\dots$ defined by the grammar

[TABLE]

where $x$ and $y$ range over a fixed countably infinite reservoir of variables. The reading of $x\textsf{P}\lceil y:\phi\rceil$ is the expected truth value of $\phi$ at a random successor $y$ of $x$. (In particular, when $\phi$ is crisp, then $x\textsf{P}\lceil y:\phi\rceil$ is just the probability of $y$ satisfying $\phi$, similar to the weights $w_{y}(\phi)$ in Halpern’s type-1 probabilistic FOL Halpern (1990).) We have the expected notions of free and bound variables, under the additional proviso that $y$ (but not $x$!) is bound in $x\textsf{P}\lceil y:\phi\rceil$. The (quantifier) rank $\mathsf{qr}(\phi)$ of a formula $\phi$ is the maximal nesting depth of the variable-binding operators $\exists$ and P and propositional atoms $A$ in $\phi$; e.g. $\exists x.\,x\textsf{P}\lceil y:A(y)\rceil$ has rank $3$.

Given a model $\mathcal{I}=(\Delta^{\mathcal{I}},(A^{\mathcal{I}})_{A\in\mathsf{N}_{\mathsf{C}}},r^{\mathcal{I}})$ and a vector $\bar{a}=(a_{1},\dots,a_{n})\in(\Delta^{\mathcal{I}})^{n}$ of values, the semantics of the logic assigns a truth value $\phi(\bar{a})\in[0,1]$ to a formula $\phi(x_{1},\dots,x_{n})$ with free variables at most $x_{1},\dots,x_{n}$. We define $\phi(\bar{a})$ recursively by essentially the same clauses as in $\mathcal{ALC}(\textsf{P})$ for the propositional constructs, and

[TABLE]

where $\bigvee$ takes suprema. Moreover, equality is two-valued, i.e. $(x_{i}=x_{j})(\bar{a})$ is $1$ if $a_{i}=a_{j}$, and [math] otherwise.

E.g. the formula $x\textsf{P}\lceil z:z=y\rceil$ (‘the successor of $x$ is probably $y$’) denotes the access probability from $x$ to $y$, $x\textsf{P}\lceil z:z\textsf{P}\lceil w:w=y\rceil\rceil$ the probability of reaching $y$ from $x$ in two independently distributed steps, and $\exists y.\,x\textsf{P}\lceil z:z=y\rceil$ the probability of the most probable successor of $x$.

We have a standard translation $\mathsf{ST}_{x}$ from $\mathcal{ALC}(\textsf{P})$ into $\mathsf{FO}(\textsf{P})$, indexed over a variable $x$ naming the current state. Following Litak et al. Litak et al. (2018), we define $\mathsf{ST}_{x}$ recursively by

[TABLE]

and by commutation with all other constructs.

Lemma 2.1**.**

For every $\mathcal{ALC}(\textsf{P})$-concept $C$ and state $a$, $C(a)=\mathsf{ST}_{x}(C)(a)$.

$\mathsf{ST}$ thus identifies $\mathcal{ALC}(\textsf{P})$ as a fragment of $\mathsf{FO}(\textsf{P})$.

3 Behavioural Distances and Games

We next discuss several notions of behavioural distance between states: via fixed point iteration à 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\colon X\times X\to[0,1]$ such that for $x,y,z\in X$, the following axioms hold: $d(x,x)=0$ (reflexivity), $d(x,y)=d(y,x)$ (symmetry), $d(x,z)\leq 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\colon X\to[0,1]$ is non-expansive wrt. a pseudometric $d$ if $|f(x)-f(y)|\leq d(x,y)$ for all $x,y\in X$. The space of these non-expansive functions, denoted $\operatorname{Pred}(X,d)$, is equipped with the supremum (pseudo)metric $d_{\infty}$,

[TABLE]

We denote by $B_{\epsilon}({x})=\{y\in X\mid d(x,y)\leq\epsilon\}$ the ball of radius $\epsilon$ around $x$ in $(X,d)$. The space $(X,d)$ is totally bounded if for every $\epsilon>0$ there exists a finite $\epsilon$-cover, i.e. finitely many elements $x_{1},\dots,x_{n}\in X$ such that $X=\bigcup_{i=1}^{n}B_{\epsilon}({x_{i}})$.

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 $\pi_{1}$ and $\pi_{2}$ be discrete probability measures on $A$ and $B$, respectively. We denote by $\operatorname{Cpl}(\pi_{1},\pi_{2})$ the set of couplings of $\pi_{1}$ and $\pi_{2}$, i.e. probability measures $\mu$ on $A\times B$ such that $\pi_{1}$ and $\pi_{2}$ are marginals of $\mu$:

• •

for all $a\in A$, $\sum_{b\in B}\mu(a,b)=\pi_{1}(a)$;

• •

for all $b\in B$, $\sum_{a\in A}\mu(a,b)=\pi_{2}(b)$.

Definition 3.3** (Wasserstein and Kantorovich distances).**

Let $(X,d)$ be a pseudometric space. We generally write

[TABLE]

for the set of discrete probability distributions on $X$. We define two pseudometrics on $\mathcal{D}X$, the Kantorovich distance $d^{\uparrow}$ and the Wasserstein distance $d^{\downarrow}$:

[TABLE]

where $\bigwedge$ takes meets (and $\bigvee$ suprema). We extend these distances without further mention to zero functions (like the functions $r_{a}$ at blocking states $a$) by decreeing that the zero function has distance $1$ from all probability distributions.

The notation $d^{\uparrow},d^{\downarrow}$ 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 $\pi_{1},\pi_{2}\in\mathcal{D}X$,

[TABLE]

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 à la Wasserstein/Kantorovich).**

Given a model $\mathcal{I}$, we define the chains $(d^{K}_{n})$, $(d^{W}_{n})$ of depth-$n$ Kantorovich and Wasserstein distances, respectively, via fixed point iteration:

[TABLE]

where $\vee$ is binary join. We extend this to states $a,b$ in different models $\mathcal{I}$, $\mathcal{J}$ by taking the disjoint union of $\mathcal{I}$, $\mathcal{J}$.

In both cases, we start with the zero pseudometric, and in the next iteration lift the pseudometric $d_{n}$ from the previous step via Wasserstein/Kantorovich. This lifted metric is then applied to the probability distributions $\pi_{a},\pi_{b}$ associated with $a,b$. In addition we take the maximum with the supremum over the distances for all atomic $A\in\mathsf{N}_{\mathsf{C}}$.

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

Definition 3.6** (Bisimulation game).**

Given models $\mathcal{I},\mathcal{J}$, $a_{0}\in\Delta^{\mathcal{I}},b_{0}\in\Delta^{\mathcal{J}}$, and $\epsilon_{0}\in[0,1]$, the $\epsilon_{0}$-bisimulation game for $a_{0}$ and $b_{0}$ is played by Spoiler ($S$) and Duplicator ($D$), with rules as follows:

• •

Configurations: triples $(a,b,\epsilon)$, with states $a\in\Delta^{\mathcal{I}}$, $b\in\Delta^{\mathcal{J}}$ and maximal allowed deviation $\epsilon\in[0,1]$. The initial configuration is $(a_{0},b_{0},\epsilon_{0})$.

• •

Moves: In each round, $D$ first picks a probability measure $\mu\in\operatorname{Cpl}(\pi_{a},\pi_{b})$. Then, $D$ distributes the deviation $\epsilon$ over all pairs $(a^{\prime},b^{\prime})$ of successors, i.e. picks a function $\epsilon^{\prime}\colon\Delta^{\mathcal{I}}\times\Delta^{\mathcal{J}}\to[0,1]$ such that $\operatorname{E}_{\mu}(\epsilon^{\prime})\leq\epsilon$. Finally, $S$ picks a pair $(a^{\prime},b^{\prime})$ with $\mu(a^{\prime},b^{\prime})>0$; the new configuration is then $(a^{\prime},b^{\prime},\epsilon^{\prime}(a^{\prime},b^{\prime}))$.

• •

$D$ wins if both states are blocking or $\epsilon=1$.

• •

$S$ wins if exactly one state is blocking and $\epsilon<1$.

• •

Winning condition: $|A^{\mathcal{I}}(a)-A^{\mathcal{J}}(b)|\leq\epsilon$ for all $A\in\mathsf{N}_{\mathsf{C}}$.

The game comes in two variants, the (unbounded) bisimulation game and the $n$-round bisimulation game, where $n\geq 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 $n$-round game once $n$ rounds have been played (the winning condition is not checked after the last round, so in particular, any [math]-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 $\epsilon$ 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 $d^{G}_{n}$ and (unbounded-depth) game distance $d^{G}$ are defined as

[TABLE]

where $\mathsf{G}(a,b,\epsilon)$ and $\mathsf{G}_{n}(a,b,\epsilon)$ denote the the bisimulation game and the $n$-round bisimulation game on $(a,b,\epsilon)$, respectively.

Finally we define the depth-$n$ logical distance via $\mathcal{ALC}(\textsf{P})$, restricting to concepts of rank at most $n$:

Definition 3.9**.**

The depth-$n$ logical distance $d^{L}_{n}(a,b)$ of states $a$, $b$ in models $\mathcal{I}$, $\mathcal{J}$ is defined as

[TABLE]

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 $\mathcal{I},\mathcal{J}$, respectively,

[TABLE]

Similarly, $Q$ is depth-$n$ bisimulation invariant, or finite-depth bisimulation invariant if mention of $n$ is omitted, if $Q$ is non-expansive wrt. $d^{G}_{n}$ in the same sense.

It is easy to see that $\mathcal{ALC}(\textsf{P})$-concepts are bisimulation-invariant. More precisely, $\mathcal{ALC}(\textsf{P})$-concepts of rank at most $n$ are depth-$n$ bisimulation invariant (a stronger invariance since clearly $d^{G}_{n}\leq d^{G}$), as shown by routine induction. In contrast, many other properties of states are expressible in $\mathsf{FO}(\textsf{P})$ but not in $\mathcal{ALC}(\textsf{P})$, as they fail to be bisimulation-invariant. Examples include $x\textsf{P}\lceil y:x=y\rceil$ (probability of a self-transition) and $\exists z.\,x\textsf{P}\lceil y:y=z\rceil$ (highest transition probability to a successor).

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

Theorem 3.11** (Modal characterization).**

Every bisimulation-invariant $\mathsf{FO}(\textsf{P})$-formula of rank at most $n$ can be approximated (uniformly across all models) by $\mathcal{ALC}(\textsf{P})$-concepts of rank at most $3^{n}$.

(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 $\mathcal{ALC}(\textsf{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 $d^{G}_{n}$ coincides with the Wasserstein pseudometric $d^{W}_{n}$,

We note next that the modality P is non-expansive: We extend P to act on $[0,1]$-valued functions $f\colon\Delta^{\mathcal{I}}\to[0,1]$ by

[TABLE]

Lemma 4.2**.**

The map $f\mapsto\textsf{P}f$ is non-expansive wrt. the supremum metric, that is $\lVert\textsf{P}f-\textsf{P}g\rVert_{\infty}\leq\lVert f-g\rVert_{\infty}$ for all $f,g\colon\Delta^{\mathcal{I}}\to[0,1]$.

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

Theorem 4.3**.**

Let $\mathcal{I}$ be a model. Then for all $n\geq 0$,

we have $d^{G}_{n}=d^{W}_{n}=d^{K}_{n}=d^{L}_{n}=:d_{n}$ on $\mathcal{I}$; 2. 2.

the pseudometric space $(\Delta^{\mathcal{I}},d_{n})$ is totally bounded; 3. 3.

$\mathcal{ALC}(\textsf{P})_{n}$* is a dense subset of $\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n})$.*

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 $\mathcal{ALC}(\textsf{P})$ includes truth constants $q\in\mathbb{Q}\cap[0,1]$.

For the inductive step, let $\mathcal{I}$ be a model and $n>0$, and assume as the inductive hypothesis that all claims in Theorem 4.3 hold for all $n^{\prime}<n$. We begin with Item 1; $d^{G}_{n}=d^{W}_{n}$ is already proved (Lemma 4.1).

• •

$d^{W}_{n}=d^{K}_{n}$ follows by Kantorovich-Rubinstein duality (Lemma 3.4), since every totally bounded pseudometric space is separable.

• •

$d^{K}_{n}=d^{L}_{n}$: By Lemma 4.2 and the inductive hypothesis, $\textsf{P}[\mathcal{ALC}(\textsf{P})_{n-1}]$ is dense in $\textsf{P}[\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n-1})]$. Thus, the supremum in the definition of $d^{K}_{n}$ does not change when it is taken only over the concepts in $\mathcal{ALC}(\textsf{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 $(\Delta^{\mathcal{I}},d_{n-1})$ is totally bounded. By the Arzelà-Ascoli theorem (in a version for totally bounded spaces and non-expansive maps, cf. Wild et al. (2018a)), it follows that $\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n-1})$ is totally bounded wrt. the supremum pseudometric. This implies that depth-$n$ distances can be approximated up to $\epsilon$ by examining differences at only finitely many, say $m$, concepts. As $([0,1]^{m},d_{\infty})$ is totally bounded, $(\Delta^{\mathcal{I}},d_{n})$ is, too.

Item 3: By the Stone-Weierstraß theorem (again in a version for totally bounded spaces and non-expansive maps Wild et al. (2018a)) it suffices to give, for each $\epsilon>0$, each non-expansive map $f\in\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n})$, and each pair of states $a,b\in\Delta^{\mathcal{I}}$ a concept $C\in\mathcal{ALC}(\textsf{P})_{n}$ such that

[TABLE]

To construct such a $C$, we note that $|f(a)-f(b)|\leq d^{L}_{n}(a,b)$ (by non-expansiveness), so there exists some $D\in\mathcal{ALC}(\textsf{P})_{n}$ such that $|D^{\mathcal{I}}(a)-D^{\mathcal{I}}(b)|\geq|f(a)-f(b)|-\epsilon$. From $D$, we can construct $C$ using truncated subtraction $\ominus$. ∎

This completes the proof of Theorem 4.3. Now that we can approximate depth-$k$ bisimulation-invariant properties by $\mathcal{ALC}(\textsf{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 $\mathcal{I}$, $\mathcal{J}$ is a map $f:\Delta^{\mathcal{I}}\to\Delta^{\mathcal{J}}$ such that $A^{\mathcal{I}}=f^{-1}[A^{\mathcal{J}}]$ for each $A\in\mathsf{N}_{\mathsf{C}}$ and $r_{f(a)}(B)=r_{a}(f^{-1}[B])$ for all $B\subseteq\Delta^{\mathcal{J}}$, $a\in\Delta^{\mathcal{I}}$ (implying that $a$ is blocking iff $f(a)$ is blocking). A model $\mathcal{F}$ is final if for every model $\mathcal{I}$, there exists a unique bounded morphism $\mathcal{I}\to\mathcal{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\colon\mathcal{I}\to\mathcal{J}$ be a bounded morphism. Then, for any $a\in\Delta^{\mathcal{I}}$, $d^{G}(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 $\mathcal{F}$ be a final model, and let $\phi$ and $\psi$ be bisimulation-invariant first-order properties. Then, for any model $\mathcal{I}$, $\lVert\phi-\psi\rVert_{\infty}^{\mathcal{I}}\leq\lVert\phi-\psi\rVert_{\infty}^{\mathcal{F}}$.

5 Locality

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

Definition 5.1**.**

Let $\mathcal{I}$ be a model.

• •

The Gaifman graph of $\mathcal{I}$ is the undirected graph on the set $\Delta^{\mathcal{I}}$ of vertices that has an edge for every pair $(a,b)$ with $r^{\mathcal{I}}(a,b)>0$ or $r^{\mathcal{I}}(b,a)>0$.

• •

The Gaifman distance $D\colon\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}\to\mathbb{N}\cup\{\infty\}$ is graph distance in the Gaifman graph: For every $a,b\in\Delta^{\mathcal{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 $\infty$ otherwise.

• •

For $a\in\Delta^{\mathcal{I}}$ and $k\geq 0$, the radius $k$ neighbourhood $U^{k}(a)=\{b\in\Delta^{\mathcal{I}}\mid D(a,b)\leq k\}$ of $a$ consists of the states reachable from $a$ in at most $k$ steps.

• •

The restriction of $\mathcal{I}$ to $U^{k}(a)$ is the model $\mathcal{I}^{k}_{a}$ with set $U^{k}(a)$ of states, and

[TABLE]

for $A\in\mathsf{N}_{\mathsf{C}}$ and $b,c\in U^{k}(a)$.

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 $\mathcal{I}$. Then $D$ wins the $k$-round [math]-bisimulation game for $\mathcal{I},a$ and $\mathcal{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 $\phi(x)$ is $k$-local for a radius $k$ if for every model $\mathcal{I}$ and every $a\in\Delta^{\mathcal{I}}$, $\phi^{\mathcal{I}}(a)=\phi^{\mathcal{I}^{k}_{a}}(a)$.

As $\mathcal{ALC}(\textsf{P})$-concepts are bisimulation-invariant, Lemma 5.2 implies

Lemma 5.4**.**

Every $\mathcal{ALC}(\textsf{P})$-concept of rank at most $k$ is $k$-local.

To prove locality of bisimulation-invariant $\mathsf{FO}(\textsf{P})$-formulae, we require a model-theoretic tool, an adaptation of Ehrenfeucht-Fraïssé equivalence to the probabilistic setting:

Definition 5.5**.**

Let $\mathcal{I},\mathcal{J}$ be models, and let $\bar{a}_{0}$ and $\bar{b}_{0}$ be vectors of equal length over $\Delta^{\mathcal{I}}$ and $\Delta^{\mathcal{J}}$, respectively. The Ehrenfeucht-Fraïssé game for $\mathcal{I},\bar{a}_{0}$ and $\mathcal{J},\bar{b}_{0}$, played by Spoiler ($S$) and Duplicator ($D$), is given as follows.

• •

Configurations: pairs $(\bar{a},\bar{b})$ of vectors $\bar{a}$ over $\Delta^{\mathcal{I}}$ and $\bar{b}$ over $\Delta^{\mathcal{J}}$; the initial configuration is $(\bar{a}_{0},\bar{b}_{0})$.

• •

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\in\Delta^{\mathcal{I}}$, and $D$ then has to select a state in the other model, say $b\in\Delta^{\mathcal{J}}$, reaching the configuration $(\bar{a}a,\bar{b}b)$.

• –

Probabilistic round: $S$ selects an index $i$ and a fuzzy subset in one model, say $\phi_{A}\colon\Delta^{\mathcal{I}}\to[0,1]$. $D$ then has to select a fuzzy subset in the other model, say $\phi_{B}\colon\Delta^{\mathcal{J}}\to[0,1]$, such that $\operatorname{E}_{r_{a_{i}}}(\phi_{A})=\operatorname{E}_{r_{b_{i}}}(\phi_{B})$. Then, $S$ selects an element on one side, say $a\in\Delta^{\mathcal{I}}$, such that $r_{a_{i}}(a)>0$, and $D$ subsequently selects an element on the other side, say $b\in\Delta^{\mathcal{J}}$, such that $\phi_{A}(a)=\phi_{B}(b)$ and $r_{b_{i}}(b)>0$, reaching the configuration $(\bar{a}a,\bar{b}b)$.

• •

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 $(\bar{a},\bar{b})$ is a partial isomorphism if

• –

$a_{i}=a_{j}\iff b_{i}=b_{j}$

• –

$A^{\mathcal{I}}(a_{i})=A^{\mathcal{J}}(b_{i})$ for all $i$ and all $A\in\mathsf{N}_{\mathsf{C}}$

• –

$r^{\mathcal{I}}(a_{i},a_{j})=r^{\mathcal{J}}(b_{i},b_{j})$ 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 Ehrenfeucht-Fraïssé equivalence:

Lemma 5.6** (Ehrenfeucht-Fraïssé invariance).**

Let $\mathcal{I},\mathcal{J}$ be models, and let $\bar{a}_{0},\bar{b}_{0}$ be vectors of length $m$ over $\Delta^{\mathcal{I}}$ and $\Delta^{\mathcal{J}}$, respectively, such that $D$ wins the $n$-round Ehrenfeucht-Fraïssé game on $\bar{a}_{0},\bar{b}_{0}$. Then for every $\mathsf{FO}(\textsf{P})$-formula $\phi$ with $\mathsf{qr}(\phi)\leq n$ and free variables at most $x_{1},\dots,x_{m}$,

[TABLE]

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 $\phi(x)$ be a bisimulation-invariant $\mathsf{FO}(\textsf{P})$-formula of rank $n$ with one free variable $x$. Then $\phi$ is $k$-local for $k=3^{n}$.

Proof sketch.

Let $a$ be a state in a model $\mathcal{I}$. We need to show $\phi^{\mathcal{I}}(a)=\phi^{\mathcal{I}^{k}_{a}}(a)$. Construct models  $\mathcal{J},\mathcal{K}$ that extend $\mathcal{I}$ and $\mathcal{I}^{k}_{a}$, respectively, by adding $n$ disjoint copies of both $\mathcal{I}$ and $\mathcal{I}^{k}_{a}$. We finish the proof by showing that

[TABLE]

The first and third equality follow by bisimulation invariance of $\phi$ (Lemma 5.7), and the second using Lemma 5.6, by giving a winning invariant for $D$ in the $n$-round Ehrenfeucht-Fraïssé game for $\mathcal{J},a$ and $\mathcal{K},a$. ∎

6 Proof of the Main Result

Having established locality of bisimulation-invariant first-order 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 bisimulation-invariant, and then conclude the proof of our main result, the modal characterization theorem.

Definition 6.1**.**

Let $\mathcal{I}$ be a model. The unravelling $\mathcal{I}^{\ast}$ of $\mathcal{I}$ is a model with non-empty finite sequences $\bar{a}\in(\Delta^{\mathcal{I}})^{+}$ as states, where atomic concepts and roles are interpreted by

[TABLE]

for $\bar{a}\in(\Delta^{\mathcal{I}})^{+}$ and $a\in\Delta^{\mathcal{I}}$, where $\mathsf{last}$ takes last elements.

As usual, models are bisimilar to their unravellings:

Lemma 6.2**.**

For any model $\mathcal{I}$ and $a\in\Delta^{\mathcal{I}}$, $D$ has a winning strategy in the [math]-bisimulation game for $\mathcal{I},a$ and $\mathcal{I}^{\ast},a$.

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

Lemma 6.3**.**

Let $\phi$ be bisimulation invariant and $k$-local. Then $\phi$ 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 $\phi$ be a probabilistic first-order formula of rank $n$. By Lemma 5.8 and Lemma 6.3, $\phi$ is depth-$k$ bisimulation-invariant for $k=3^{n}$. By Theorem 4.3, for every $\epsilon>0$, there exists an $\mathcal{ALC}(\textsf{P})$ concept $C_{\epsilon}$ of rank at most $k$ such that $\lVert\phi^{\mathcal{F}}-C^{\mathcal{F}}_{\epsilon}\rVert_{\infty}\leq\epsilon$ on the final model $\mathcal{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 $\mathcal{ALC}(\textsf{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 $\mathcal{ALC}(\textsf{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. (2018a) and two-valued probabilistic modal logic Schröder 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.

Appendix A Appendix

A.1 Coalgebraic Modelling

Universal coalgebra Rutten (2000) serves as a generic framework for modelling state-based systems, with the system type encapsulated as a set functor. Although we are only concerned with a concrete system type in the present paper, we do need coalgebraic methods to some degree. In particular, the requisite background on behavioural distances van Breugel and Worrell (2005); Baldan et al. (2014) is largely based on coalgebraic techniques, and moreover we will need the final coalgebra at one point in the development. We require only basic definitions, which we recapitulate here and then instantiate to the case of our notion of model.

Recall first that a set functor $F:\mathsf{Set}\to\mathsf{Set}$ consists of an assignment of a set $FX$ to every set $X$ and a map $Ff:FX\to FY$ to every map $f:X\to Y$, preserving identities and composition. The core example of a functor for the present purposes is the distribution functor $\mathcal{D}$, which assigns to a set $X$ the set $\mathcal{D}X$ of discrete probability measures on $X$, and to a map $f:X\to Y$ the map $\mathcal{D}f:\mathcal{D}X\to\mathcal{D}Y$ that takes image measures; explicitly, $\mathcal{D}f(\mu)$ is the image measure of $\mu$ along $f$, given by $\mathcal{D}f(\mu)(A)=\mu(f^{-1}[A])$. Functors can be combined by taking products and sums: Given set functors $F,G:\mathsf{Set}\to\mathsf{Set}$, the set functors $F\times G,F+G:\mathsf{Set}\to\mathsf{Set}$ are given by $(F\times G)X=FX\times GX$ and $(F+G)X=FX+GX$, respectively, with the evident action on maps in both cases; here, $+$ denotes disjoint union as usual. Every set $C$ induces a constant functor, also denoted $C$ and given by $CX=C$ and $Cf=\mathsf{id}_{C}$ for every set $X$ and every map $f$. Moreover, the identity functor $\mathsf{id}$ is given by $\mathsf{id}\,X=X$ and $\mathsf{id}\,f=f$ for all sets $X$ and all maps $f$.

An $F$-coalgebra $(A,\xi)$ for a set functor $F$ consists of a set $X$ of states and a transition map $\xi:A\to FA$, thought of as assigning to each state $a\in A$ a structured collection $\xi(a)$ of successors. A $\mathcal{D}$-coalgebra $(A,\xi)$, for instance, is just a Markov chain: its transition map $\xi:A\to\mathcal{D}A$ assigns to each state a distribution over successor states. Similarly, models in the sense defined above are coalgebras $(A,\xi)$ for the set functor $[0,1]^{\mathsf{N}_{\mathsf{C}}}\times(\mathcal{D}+1)$: If $\xi(a)=(f,\pi)$, then $f:\mathsf{N}_{\mathsf{C}}\to[0,1]$ determines the truth values of the atomic concepts at the state $a$, and $\pi$ is either a discrete probability measure determining the successors of $a$ or a designated value denoting termination. The probabilistic transition systems considered by van Breugel and Worrell van Breugel and Worrell (2005), which indexes probabilistic transition relations over a set $\mathsf{Act}$ of actions and moreover uses unrestricted subdistributions, corresponds to coalgebras $(A,\xi)$ for the set functor $\mathcal{D}(\mathsf{id}+1)^{\mathsf{Act}}$ – given a state $a$ and an action $c\in\mathsf{Act}$, $\xi(a)(c)\in\mathcal{D}(A+1)$ is a subdistribution over successor states of $a$, with the summand $1$ serving to absorb the weight missing to obtain total weight $1$.

A morphism $f:(A,\xi)\to(B,\zeta)$ between $F$-coalgebras $(A,\xi)$ and $(B,\zeta)$ is a map $f:A\to B$ such that

[TABLE]

for all states $a\in A$. Morphisms should be thought of as behaviour-preserving maps or functional bisimulations. E.g. $f:A\to B$ is a morphism of $\mathcal{D}$-coalgebras (i.e. Markov chains) $(A,\xi)$ and $(B,\zeta)$ if for each set $Y\subseteq B$ and each state $a\in A$,

[TABLE]

i.e. the probability of reaching $Y$ from $f(a)$ is the same as that of reaching $f^{-1}[Y]$ from $a$. Morphisms of probabilistic transition systems, viewed as coalgebras, satisfy a similar condition for the successor distributions, and additionally preserve the truth values of atomic concepts.

An $F$-coalgebra $(Z,\zeta)$ is final if for every $F$-coalgebra $(A,\xi)$ there exists exactly one morphism $(A,\xi)\to(Z,\zeta)$. Final coalgebras are unique up to isomorphism if they exist, and should be thought of as having as states all possible behaviours of states in $F$-coalgebras. For our present purposes, we do not need an explicit description of the final coalgebra; it suffices to know that since the functor describing probabilistic transition systems is accessible (more precisely $\omega_{1}$-accessible), a final coalgebra for it, i.e. a final probabilistic transition system, exists Barr (1993).

A.2 Omitted Proofs

A.2.1 Proof of Lemma 3.4

We make use of the following version of the Kantorovich-Rubinstein duality (Dudley, 2002, Proposition 11.8.1):

Lemma A.1** (Kantorovich-Rubinstein duality).**

Let $(X,d)$ be a separable metric space, and let $\mathcal{P}_{1}(X)$ denote the space of probability measures $\mu\colon\mathcal{B}(X)\to[0,1]$ on the Borel $\sigma$-algebra $\mathcal{B}(X)$ such that $\textstyle{\int}d(x,\,\cdot\,)\,\mathrm{d}\mu<\infty$ for some $x\in X$. Then for $\mu_{1},\mu_{2}\in\mathcal{P}_{1}(X)$,

[TABLE]

Essentially, we only need to transfer this version of Kantorovich-Rubinstein duality to the slightly more general case of pseudometrics.

First, note that the relation $x\sim y:\iff d(x,y)=0$ is an equivalence relation on $X$. The quotient set $Y:=X/{\sim}$ is made into a metric space $(Y,d^{\prime})$, the metric quotient of $(X,d)$, by taking $d^{\prime}([x],[y])=d(x,y)$. Let $p\colon A\to B$ be the projection map. By construction, $p$ is an isometry. Both the Kantorovich and the Wasserstein lifting preserve isometries Baldan et al. (2014), so for all discrete probability measures $\mu_{1},\mu_{2}$ on $X$,

[TABLE]

In the second step we have applied Lemma A.1 to the metric space $(Y,d^{\prime})$, noting that every discrete probability measure can be defined on the Borel $\sigma$-algebra.

A.2.2 Proof of Lemma 4.1.

Induction over $n$. The base case $n=0$ is clear: the [math]-round game is an immediate win for $D$, so $d^{G}_{0}=d^{W}_{0}=0$. We proceed with the inductive step from $n$ to $n+1$.

So let $a$ and $b$ be states in a model $\mathcal{I}$. If $a$ and $b$ are both blocking, then $d^{G}_{n+1}(a,b)=d^{W}_{n+1}(a,b)=0$. If exactly one of $a,b$ is blocking, then $d^{G}_{n+1}(a,b)=d^{W}_{n+1}(a,b)=1$. Now assume that both $a$ and $b$ are non-blocking.

“$\geq$”: Let $d^{G}_{n+1}(a,b)\leq\epsilon$, so $D$ wins the $(n+1)$-round bisimulation game on $(a,b,\epsilon)$. We show that $d^{W}_{n+1}(a,b)\leq\epsilon$. First, for every $A\in\mathsf{N}_{\mathsf{C}}$, $|A^{\mathcal{I}}(a)-A^{\mathcal{I}}(b)|\leq\epsilon$ by the winning condition. Second, suppose $D$ chooses $\mu\in\operatorname{Cpl}(r_{a},r_{b})$ and $\epsilon^{\prime}\colon\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}\rightarrow[0,1]$ in the first turn. By assumption, $D$ wins the $n$-round bisimulation game on $(a^{\prime},b^{\prime},\epsilon^{\prime}(a^{\prime},b^{\prime}))$ for every $a^{\prime},b^{\prime}\in\Delta^{\mathcal{I}}$, so $d^{W}_{n}=d^{G}_{n}\leq\epsilon^{\prime}$ by induction, and thus $\operatorname{E}_{\mu}(d^{W}_{n})\leq\operatorname{E}_{\mu}(\epsilon^{\prime})\leq\epsilon$.

“$\leq$”: Let $d^{W}_{n+1}(a,b)<\epsilon$. It suffices to give a winning strategy for $D$ in the $(n+1)$-round bisimulation game on $(a,b,\epsilon)$ (implying $d^{G}_{n+1}(a,b)\leq\epsilon$). The winning condition in the initial configuration follows immediately from the assumption. Also by the assumption, there exists $\mu\in\operatorname{Cpl}(r_{a},r_{b})$ such that $\operatorname{E}_{\mu}(d^{W}_{n})<\epsilon$. As $r_{a}$ and $r_{b}$ are discrete, the set

[TABLE]

is countable; so we can write $R=\{(a_{1},b_{1}),(a_{2},b_{2}),\dots\}$. Now put $\delta=\epsilon-\operatorname{E}_{\mu}(d^{W}_{n})$ and define

[TABLE]

for $(a_{i},b_{i})\in R$ and $\epsilon^{\prime}(a^{\prime},b^{\prime})=0$ for $(a^{\prime},b^{\prime})\notin R$. Then

[TABLE]

so playing $\mu$ and $\epsilon^{\prime}$ constitutes a legal move for $D$. Now, since $\mu\in\operatorname{Cpl}(r_{a},r_{b})$, $\mu(a^{\prime},b^{\prime})=0$ for all $(a^{\prime},b^{\prime})\notin R$. This means that $S$ must pick some $(a_{i},b_{i})\in R$. Then

[TABLE]

so $D$ wins the $n$-round game on $(a_{i},b_{i},\epsilon^{\prime}(a_{i},b_{i}))$.

A.2.3 Proof of Lemma 4.2.

Let $\lVert f-g\rVert_{\infty}\leq\epsilon$; we have to show $\lVert\textsf{P}f-\textsf{P}g\rVert_{\infty}\leq\epsilon$. So let $a\in\Delta^{\mathcal{I}}$; then

[TABLE]

as required.

A.2.4 Proof of Theorem 4.3.

We proceed by simultaneous induction on $n$.

In the base case $n=0$, all the behavioural distances are the zero pseudometric: $d^{G}_{0}=0$ because by the rules of the game each [math]-round game is an immediate win for $D$; $d^{W}_{0}=d^{K}_{0}=0$ by definition; and $d^{L}_{0}=0$ because each rank-[math] concept is a propositional combination of truth constants and therefore constant. Total boundedness follows directly from the fact that under the zero pseudometric every $\epsilon$-ball is the entire space, regardless of $\epsilon$. Finally, the density claim follows because non-expansive maps under the zero pseudometric are just constants in $[0,1]$ and the syntax of $\mathcal{ALC}(\textsf{P})$ includes truth constants $q\in\mathbb{Q}\cap[0,1]$.

For the inductive step, let $\mathcal{I}$ be a model and $n>0$, and assume as the inductive hypothesis that all claims in Theorem 4.3 hold for all $n^{\prime}<n$. We begin with Item 1:

• •

$d^{G}_{n}=d^{W}_{n}$ is Lemma 4.1.

• •

$d^{W}_{n}=d^{K}_{n}$ follows by Kantorovich-Rubinstein duality (Lemma 3.4), since every totally bounded pseudometric space is separable.

• •

$d^{K}_{n}=d^{L}_{n}$: Let $a,b\in\Delta^{\mathcal{I}}$ and consider the map

[TABLE]

Then $G$ is a continuous function because all of its constituents are continuous (in particular, P is continuous by Lemma 4.2).

By the induction hypothesis, and because density is preserved by continuous maps, $G[\mathcal{ALC}(\textsf{P})_{n-1}]$ is a dense subset of $G[\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n-1})]$. Thus,

[TABLE]

To prove the penultimate step, we first note that “$\leq$” follows immediately. To see “$\geq$”, we proceed by induction over the propositional combinations of atomic concepts $A\in\mathsf{N}_{\mathsf{C}}$ and concepts $\textsf{P}C$, where $C\in\mathcal{ALC}(\textsf{P})_{n-1}$, using that for any concepts $C,D$ and $q\in\mathbb{Q}\cap[0,1]$:

[TABLE]

Item 2: We make use of the following version of the Arzelà-Ascoli theorem Wild et al. (2018a) where function spaces are restricted to non-expansive functions instead of the more general continuous functions, but the underlying spaces are only required to be totally bounded instead of compact:

Lemma A.2** **(Arzelà-Ascoli for totally bounded

spaces).

Let $(X,d)$ be a totally bounded pseudometric space. Then the space $\operatorname{Pred}(X,d)$, equipped with the supremum pseudometric, is totally bounded.

By Lemma A.2, applied to the inductive hypothesis, we know that the space $\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n-1})$ is totally bounded wrt. the supremum pseudometric.

Let $\epsilon>0$. As $\mathcal{ALC}(\textsf{P})_{n-1}$ is dense in $\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n-1})$, there exist finitely many $C_{1},\dots,C_{m}\in\mathcal{ALC}(\textsf{P})_{n-1}$ such that

[TABLE]

From these concepts, together with the atomic concepts $A_{1},\dots,A_{k}$, we can construct the map

[TABLE]

Note that we assume here that the set of atomic concepts is a finite set $\mathsf{N}_{\mathsf{C}}=\{A_{1},\dots,A_{k}\}$. This is without loss of generality for the modal characterization theorem, because every formula of $\mathsf{FO}(\textsf{P})$ can only contain finitely many propositional atoms, so $\mathsf{N}_{\mathsf{C}}$ can be restricted to just those atoms.

It turns out that $I$ is an $\frac{\epsilon}{4}$-isometry, that is

[TABLE]

for all $a,b\in\Delta^{\mathcal{I}}$. Thus, by the triangle inequality, we can take preimages to turn a finite $\frac{\epsilon}{4}$-cover of $[0,1]^{k+m}$ (a compact, hence totally bounded space) into a finite $\epsilon$-cover of $(\Delta^{\mathcal{I}},d_{n})$.

Item 3: We make use of the following Stone-Weierstraß theorem  Wild et al. (2018a) (again in a version for totally bounded spaces and non-expansive maps):

Lemma A.3** (Stone-Weierstraß for totally bounded spaces).**

Let $(X,d)$ be a totally bounded pseudometric space, and let $L$ be a subset of $\operatorname{Pred}(X,d)$ such that $f_{1},f_{2}\in L$ implies $\min(f_{1},f_{2}),\max(f_{1},f_{2})\in L$. Then $L$ is dense in $\operatorname{Pred}(X,d)$ if each $f\in\operatorname{Pred}(X,d)$ can be approximated at each pair of points by functions in $L$; that is for all $\epsilon>0$ and all $x_{1},x_{2}\in X$ there exists $g\in L$ such that

[TABLE]

We apply Lemma A.3 to $(\Delta^{\mathcal{I}},d_{n})$ with $L:=\mathcal{ALC}(\textsf{P})_{n}$. Clearly $L$ is closed under $\min$ and $\max$ so, to finish the proof, it suffices to give, for each $\epsilon>0$, each non-expansive map $f\in\operatorname{Pred}(\Delta^{\mathcal{I}},d_{n})$ and each pair of states $a,b\in\Delta^{\mathcal{I}}$ a concept $C\in\mathcal{ALC}(\textsf{P})_{n}$ such that

[TABLE]

To construct such a $C$, we note that $|f(a)-f(b)|\leq d^{L}_{n}(a,b)$ (by non-expansiveness), so there exists some $D\in\mathcal{ALC}(\textsf{P})_{n}$ such that $|D^{\mathcal{I}}(a)-D^{\mathcal{I}}(b)|\geq|f(a)-f(b)|-\epsilon$. From $D$, we can construct $C$ using truncated subtraction $\ominus$.

A.2.5 Proof of Lemma 4.5.

We show that $D$ wins the bisimulation game for $(a_{0},f(a_{0}),0)$ by maintaining the invariant that the current configuration is of the form $(a,b,0)$ with $b=f(a)$, which ensures that the winning condition always holds. It remains to show that $D$ can maintain the invariant.

In each round, $D$ begins by picking $\mu(a^{\prime},b^{\prime})=r_{a}(a^{\prime})$ if $b^{\prime}=f(a^{\prime})$ and [math] otherwise, and $\epsilon^{\prime}=0$. We can see that $\mu\in\operatorname{Cpl}(r_{a},r_{b})$, because

[TABLE]

and

[TABLE]

for all $a^{\prime}\in\Delta^{\mathcal{I}}$ and $b^{\prime}\in\Delta^{\mathcal{J}}$. Also, clearly $\operatorname{E}_{\mu}(\epsilon^{\prime})=0$. Now any choice by $S$ leads to another configuration $(a^{\prime},b^{\prime},0)$ with $b^{\prime}=f(a^{\prime})$.

A.2.6 Proof of Lemma 4.6.

Let $\mathcal{I}$ be a model, and let $h\colon\mathcal{I}\to\mathcal{F}$ be the unique morphism. Let $a\in\Delta^{\mathcal{I}}$. Then $d^{G}(a,h(a))=0$ by Lemma 4.5, and thus $\phi^{\mathcal{I}}(a)=\phi^{\mathcal{F}}(h(a))$ and $\psi^{\mathcal{I}}(a)=\psi^{\mathcal{F}}(h(a))$ by bisimulation invariance. So

[TABLE]

A.2.7 Proof of Lemma 5.2.

Player $D$ wins by maintaining the invariant that whenever $i$ rounds have been played, the current configuration is of the form $(a_{i},a_{i},0)$ for some $a_{i}\in\Delta^{\mathcal{I}}$ with $D(a,a_{i})\leq i$. For $i<k$, no configuration of this kind can be winning for $S$, because the two states in this configuration represent the same state in different models (recall that the winning conditions are not checked after the last round has been played).

It remains to give a strategy for $D$ that maintains the invariant. It clearly holds at the start of the game, with $a_{0}=a$. When the $(i+1)$-th round is played, $D$ can pick $\mu\in\operatorname{Cpl}(r_{a_{i}},r_{a_{i}})$ and $\epsilon^{\prime}\colon\Delta^{\mathcal{I}}\times U^{k}(a)\to[0,1]$ as follows:

[TABLE]

Clearly, $\operatorname{E}_{\mu}(\epsilon^{\prime})=0$, so this is a legal move. Now the new configuration chosen by $S$ necessarily satisfies the invariant.

A.2.8 Proof of Lemma 5.6.

We proceed by induction over formulae.

• •

The cases $A(x_{i})$ and $x_{i}=x_{j}$ (with $A\in\mathsf{N}_{\mathsf{C}}$) follow immediately from the fact that the initial configuration is a partial isomorphism.

• •

The Boolean cases ($q,\phi\ominus q,\neg\phi,\phi\mathop{\sqcap}\psi$) follow directly by the inductive hypothesis.

• •

$\exists x.\,\phi$: Let $(\bar{a},\bar{b})$ be the current configuration. Let $\delta>0$, let $a$ be such that

[TABLE]

and let $b$ be the winning answer for $D$ in reply to $S$ choosing $a$. By induction, $\phi(\bar{a}a)=\phi(\bar{b}b)$, so

[TABLE]

Because $\delta>0$ was arbitrary, it follows that $(\exists x.\,\phi)(\bar{b})\geq(\exists x.\,\phi)(\bar{a})$. We can symmetrically show that $(\exists x.\,\phi)(\bar{a})\geq(\exists x.\,\phi)(\bar{b})$, which proves this case.

• •

$x_{i}\textsf{P}\lceil x_{m+1}:\phi\rceil$: Let $(\bar{a},\bar{b})$ be the current configuration. Suppose that $S$ picks the index $i$ and the fuzzy subset

[TABLE]

and $D$’s winning reply is $\psi_{B}\colon\Delta^{\mathcal{J}}\to[0,1]$. We show that on the support of $r_{b_{i}}$, $\psi_{B}$ must be equal to

[TABLE]

Suppose there exists some $b\in\Delta^{\mathcal{J}}$ with $r(b_{i},b)>0$ and $\phi_{B}(b)\neq\psi_{B}(b)$. Then $D$ has a winning reply $a\in\Delta^{\mathcal{I}}$ in case $S$ picks this $b$, which means, by the rules of the game, that $r(a_{i},a)>0$ and $\phi_{A}(a)=\psi_{B}(b)$. However, it is also true that $\phi_{A}(a)=\phi_{B}(b)$, by the inductive hypothesis. This is a contradiction.

Now, because $\psi_{B}$ was a winning reply, we obtain

[TABLE]

A.2.9 Proof of Lemma 5.8.

Let $a$ be a state in a model $\mathcal{I}$. We need to show $\phi^{\mathcal{I}}(a)=\phi^{\mathcal{I}^{k}_{a}}(a)$. Let $\mathcal{J}$ be a new model that extends $\mathcal{I}$ by adding $n$ disjoint copies of both $\mathcal{I}$ and $\mathcal{I}^{k}_{a}$. Let $\mathcal{K}$ be the model that extends $\mathcal{I}^{k}_{a}$ likewise. We finish the proof by showing that

[TABLE]

The first and third equality follow by bisimulation invariance of $\phi$ (Lemma 5.7). The second equality follows by Ehrenfeucht-Fraïssé invariance (Lemma 5.6) once we show that $D$ has a winning strategy in the $n$-round Ehrenfeucht-Fraïssé game for $\mathcal{J},a$ and $\mathcal{K},a$.

Such a winning strategy can be described as follows: For $\bar{a}=(a_{1},\dots,a_{n})$, put $U^{k}(\bar{a})=\bigcup_{i\leq n}U^{k}(a_{i})$. Then $D$ maintains the invariant that, if the configuration reached after $i$ rounds is $(\bar{b},\bar{c})$, then there exists an isomorphism $f_{i}$ between $U^{k_{i}}(\bar{b})$ and $U^{k_{i}}(\bar{c})$ that maps each $b_{j}$ to the corresponding $c_{j}$, where $k_{i}=3^{n-i}$.

The invariant holds at the start of the game, because the neighbourhoods on both sides are just $U^{k}(a)$. Similarly, whenever the invariant holds, the current configuration is a partial isomorphism by restriction of the given isomorphism to the two vectors of the configuration.

Now we consider what happens during the rounds. Suppose that $i$ rounds have been played, and the current configuration is $(\bar{b},\bar{c})$. If $S$ decides to play a standard round, playing some $b\in\Delta^{\mathcal{J}}$, then there are two cases:

• •

$b\in U^{2k_{i+1}}(\bar{b})$: In this case, the radius-$k_{i+1}$ neighbourhood $U^{k_{i+1}}(b)$ of $b$ is fully contained in the domain $U^{k_{i}}(\bar{b})$ of $f_{i}$ – this follows by the triangle inequality, as $2k_{i+1}+k_{i+1}=3k_{i+1}=k_{i}$. Now $D$ can just reply with $c:=f_{i}(b)$, and an isomorphism $f_{i+1}$ between $U^{k_{i+1}}(\bar{b}b)$ and $U^{k_{i+1}}(\bar{c}c)$ is formed by restricting the domain and codomain of $f_{i}$ appropriately.

• •

$b\notin U^{2k_{i+1}}(\bar{b})$: In this case, the radius-$k_{i+1}$ neighbourhoods $U^{k_{i+1}}(b)$ of $b$ and $U^{k_{i+1}}(\bar{b})$ of $\bar{b}$ do not intersect – this too follows from the triangle inequality. Now $D$ can pick a fresh copy of $\mathcal{I}$ or $\mathcal{I}^{k}_{a}$ in $\mathcal{K}$ (depending on which kind of copy $b$ lies in); her reply $c$ is then just $b$ in that copy. Here, a fresh copy is one that was never visited on any of the previous rounds. By construction of $\mathcal{J}$ and $\mathcal{K}$, such a copy is always available. This means that we now have two isomorphisms, one between $U^{k_{i+1}}(\bar{b})$ and $U^{k_{i+1}}(\bar{c})$ (by restriction of $f_{i}$), and one between $U^{k_{i+1}}(b)$ and $U^{k_{i+1}}(c)$ (by isomorphism of the respective copies of $\mathcal{I}$ or $\mathcal{I}^{k}_{a}$). Because these isomorphisms have disjoint domains and codomains, we can combine them to form the desired isomorphism $f_{i+1}$.

If $S$ plays a standard round with some $c\in\Delta^{\mathcal{K}}$ instead, the same argument applies.

Finally, if $S$ starts a probabilistic round by picking an index $0\leq j\leq i$ and playing some $\phi_{B}\colon\Delta^{\mathcal{J}}\to[0,1]$, then we first note that, by the rules of the game, the support of $\phi_{B}$ must be contained in $U^{1}(\bar{b})$, which in turn must be contained in the domain of $f_{i}$. This means that $D$ can construct $\phi_{C}\colon\Delta^{\mathcal{K}}\to[0,1]$ by mapping along $f_{i}$, i.e. $\phi_{C}(c)=\phi_{B}(f_{i}^{-1}(c))$ for all successors $c$ of $c_{j}$, and $\phi_{C}(c)=0$ otherwise. Now, whichever $b$ or $c$ is picked by $S$, $D$ can just reply with $c:=f_{i}(b)$ or $b:=f_{i}^{-1}(c)$ and $f_{i+1}$ is formed as in the first case of a standard round. Again, the same argument applies if $S$ picks a fuzzy subset $\phi_{C}$ on the other side.

A.2.10 Proof of Lemma 6.2.

$D$ wins by maintaining the invariant that the configuration of the game is of the form $(\bar{a},\mathsf{last}(\bar{a}),0)$ for some $\bar{a}\in(\Delta^{\mathcal{I}})^{+}$. To do so, she can put $\mu(\bar{a}a,a)=\pi_{\bar{a}}(\bar{a}a)=\pi_{\mathsf{last}(\bar{a})}(a)$ for all $a\in(\Delta^{\mathcal{I}})^{+}$, all other values of $\mu$ are [math], and $\epsilon^{\prime}=0$. Then any move by $S$ leads to a configuration where the invariant holds.

A.2.11 Proof of Lemma 6.3.

Let $\mathcal{I}$ and $\mathcal{J}$ be two models and let $a\in\Delta^{\mathcal{I}}$ and $b\in\Delta^{\mathcal{J}}$ be two states such that $d_{k}^{G}(a,b)<\epsilon$. It is enough to show that $|\phi^{\mathcal{I}}(a)-\phi^{\mathcal{J}}(b)|\leq\epsilon$.

We denote by $a^{\prime}$ and $a^{\prime\prime}$ the copies of $a$ in $\mathcal{I}^{\ast}$ and $(\mathcal{I}^{\ast})^{k}_{a}$, respectively. Similarly, $b^{\prime}$ and $b^{\prime\prime}$ denote the copies of $b$ in $\mathcal{J}^{\ast}$ and $(\mathcal{J}^{\ast})^{k}_{b}$. By Lemma 6.2, $D$ wins the [math]-bisimulation-game for $\mathcal{I},a$ and $\mathcal{I}^{\ast},a^{\prime}$ (similarly for $\mathcal{J}$) and by Lemma 5.2, she also wins the $k$-round [math]-bisimulation game for $\mathcal{I}^{\ast},a^{\prime}$ and $(\mathcal{I}^{\ast})^{k}_{a},a^{\prime\prime}$ (similarly for $\mathcal{J}$). Because behavioural distance $d^{G}_{k}$ is a pseudometric, this means that

[TABLE]

so $D$ has a winning strategy in the $k$-round $\epsilon$-bisimulation game for $(\mathcal{I}^{\ast})^{k}_{a},a^{\prime\prime}$ and $(\mathcal{J}^{\ast})^{k}_{b},b^{\prime\prime}$.

In both $(\mathcal{I}^{\ast})^{k}_{a},a^{\prime\prime}$ and $(\mathcal{J}^{\ast})^{k}_{b},b^{\prime\prime}$, the reachable states form a tree of depth at most $k$. This implies that, after $i$ rounds of the game, the two states on either side of the current configuration are nodes at distance $i$ from the root of their respective tree. Thus, whenever $k$ rounds have been played in the game, $S$ does not have a legal move in the next round, because at that point, both nodes in the configuration are necessarily leaves and thus blocking. This in turn means that if $D$ can win the $k$-round game, she also wins the unbounded game, so, by bisimulation invariance of $\phi$, $|\phi^{(\mathcal{I}^{\ast})^{k}_{a}}(a^{\prime\prime})-\phi^{(\mathcal{J}^{\ast})^{k}_{b}}(b^{\prime\prime})|\leq\epsilon$.

By locality and bisimulation invariance of $\phi$, and again Lemma 6.2, we have $\phi^{(\mathcal{I}^{\ast})^{k}_{a}}(a^{\prime\prime})=\phi^{\mathcal{I}^{\ast}}(a^{\prime})=\phi^{\mathcal{I}}(a)$ as well as $\phi^{(\mathcal{J}^{\ast})^{k}_{b}}(b^{\prime\prime})=\phi^{\mathcal{J}^{\ast}}(b^{\prime})=\phi^{\mathcal{J}}(b)$. Thus $|\phi^{\mathcal{I}}(a)-\phi^{\mathcal{J}}(b)|\leq\epsilon$, as claimed.