on the powerset of the state space has been established. There is also a
fixpoint characterization given in [fl:quantitative-spectrum-journal] although
on an auxiliary lattice which serves as a
memory.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue][7, Theorem 18]
also seems to show a fixpoint function for trace metrics in a sense. Yours is
still new in that it does not involve an auxiliary lattice and that it is
based on determinization. I think you need to say these differences
explicitly.

Let $d\in\mathit{DPMet}(\mathcal{P}(X))$ such that $d$ is join preserving in
its first argument and $d(X_{1},\emptyset)=1$ for every non-empty set
$X_{1}\subseteq X$. Then the behaviour function $\operatorname{beh_{T}}$ can
be characterized by the conditional equation:
$\operatorname{beh_{T}}(d)(X_{1},\emptyset)=1$ if $X_{1}\neq\emptyset$ and
otherwise

$\operatorname{beh_{T}}(d)(X_{1},X_{2})=\bigvee_{(a,x^{\prime})\in\delta[X_{1}]}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\bigwedge_{b\in\operatorname{lab}(\Delta)}d_{A}(a,b)\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta))\Big{)}.$

Moreover $\operatorname{beh_{T}}$ is continuous, independent of the branching
type of the transition system.

######  Proof 5.18.

Given $d$, a join-preserving directed pseudo-metric on $\mathcal{P}(X)$ that
satisfies $d_{\emptyset}\leq d$, we want to characterize

$\displaystyle\operatorname{\alpha_{T}}(\operatorname{\log_{T}}(\operatorname{\gamma_{T}}(d)))$
$\displaystyle=\operatorname{\alpha_{T}}(\bigcup_{c\in
A}\operatorname{\bigcirc}_{c}[\operatorname{\mathrm{cl}}^{\mathrm{sh}}(\operatorname{\gamma_{T}}(d))]\cup\\{1\\})=\bigvee_{c\in
A}\alpha_{T}(\operatorname{\bigcirc}_{c}[\operatorname{\gamma_{T}}(d)])\lor\operatorname{\alpha_{T}}(\\{1\\})$
$\displaystyle=\bigvee_{c\in
A}\alpha_{T}(\operatorname{\bigcirc}_{c}[\operatorname{\gamma_{T}}(d)])\lor
d_{\emptyset}$

In particular we use that
$\operatorname{\mathrm{cl}}^{\mathrm{sh}}(\operatorname{\gamma_{T}}(d))=\operatorname{\gamma_{T}}(d)$,
since the shift of function $f$ such that $\tilde{f}$ is non-expansive wrt.
$d$ is still non-expansive. This requires the fact that $d_{\emptyset}\leq d$,
since otherwise $f\oplus r$ might induce a larger distance than $f$ if the
second set is empty.

The join with $d_{\emptyset}$ ensures that
$\operatorname{beh_{T}}(d)(X_{1},\emptyset)=1$ if $X_{1}\neq\emptyset$.

It remains to characterize
$\alpha_{T}(\operatorname{\bigcirc}_{c}[\operatorname{\gamma_{T}}(d)])$:

$\displaystyle\alpha_{T}(\operatorname{\bigcirc}_{c}[\operatorname{\gamma_{T}}(d)])(X_{1},X_{2})$
$\displaystyle=\bigvee_{f\in\operatorname{\gamma_{T}}(d)}\big{(}\widetilde{\operatorname{\bigcirc}_{c}f}(X_{1})\ominus\widetilde{\operatorname{\bigcirc}_{c}f}(X_{2})\big{)}$
$\displaystyle=\bigvee_{f\in\operatorname{\gamma_{T}}(d)}\big{(}\bigvee_{x\in
X_{1}}\operatorname{\bigcirc}_{c}f(x)\ominus\widetilde{\operatorname{\bigcirc}_{c}f}(X_{2})\big{)}$
$\displaystyle=\bigvee_{x\in
X_{1}}\bigvee_{f\in\operatorname{\gamma_{T}}(d)}\big{(}\operatorname{\bigcirc}_{c}f(x)\ominus\widetilde{\operatorname{\bigcirc}_{c}f}(X_{2})\big{)}$

We fix $x\in X_{1}$, $f\in\operatorname{\gamma_{T}}(d)$ and continue to
transform, using the definition of $\operatorname{\bigcirc}_{c}$ and Lem.
5.15:

$\displaystyle\operatorname{\bigcirc}_{c}f(x)\ominus\widetilde{\operatorname{\bigcirc}_{c}f}(X_{2})$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\big{(}\overline{D_{c}}(a)\land
f(x^{\prime})\big{)}\ominus\bigwedge_{\Delta\subseteq\delta[X_{2}]}\big{(}\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\lor\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\big{(}\overline{D_{c}}(a)\land
f(x^{\prime})\big{)}\ominus\big{(}\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\lor\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}\Big{)}$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta(x)}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle\qquad\qquad\qquad\qquad\land\big{(}f(x^{\prime})\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}\overline{D_{c}}(a)\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}\Big{)}$
$\displaystyle\leq\bigvee_{(a,x^{\prime})\in\delta(x)}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\Big{)},$

due to non-expansiveness of $\tilde{f}$.

We show that we can choose $f$ such that the terms below the suprema in the
last inequality are in fact equal. For this we fix
$(a,x^{\prime})\in\delta(x)$ and $\Delta\subseteq\delta[X_{2}]$. We can assume
that
$\overline{D_{c}}(a)\geq\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))$
and
$f(x^{\prime})\geq\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))$,
since otherwise both sides of the inequality are $0$ anyway.

We define $g(x)=d(\\{x\\},\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))$
and add or subtract a constant from $g$ to obtain a function $f$ with
$f(x^{\prime})=\overline{D_{c}}(a)$. The function $g$ is always non-expansive
(see proof of Prop. 5.13) and $f$ is non-expansive wrt. $d$ due to the
condition $d_{\emptyset}\leq d$. Furthermore,

$\displaystyle\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle=\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}g(x^{\prime})\ominus\tilde{g}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle=\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\backslash\Delta)),$

because shifting can only decrease the value of
$f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))$
wrt. the value for $g$ if we subtract a constant from $g$, but in this case
$\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))$
is the smaller term and will stay smaller or equal.

More concretely, in this case $e=g(x^{\prime})-\overline{D_{c}}(a)$ will be
subtracted and
$\tilde{g}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\leq e$, such
that
$\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))=\tilde{g}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\ominus
e=0$. But this means that
$\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\leq\overline{D_{c}}(a)=f(x^{\prime})=f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\leq
g(x^{\prime})\ominus\tilde{g}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))$.

Hence, since $f(x^{\prime})=\overline{D_{c}}(a)$:

$\displaystyle\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle\qquad\land\big{(}f(x^{\prime})\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}\overline{D_{c}}(a)\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle=\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle\qquad\land\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land\big{(}f(x^{\prime})\ominus\tilde{f}(\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\big{)}$
$\displaystyle=\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))$

Everything combined, we obtain:

$\displaystyle\alpha_{T}(\operatorname{\bigcirc}_{c}[\operatorname{\gamma_{T}}(d)])(X_{1},X_{2})$
$\displaystyle=\bigvee_{x\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x)}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\Big{)}$
$\displaystyle=\bigvee_{(a,x^{\prime})\in\delta[X_{1}]}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\big{(}\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))\big{)}\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\Big{)}$

As in the proof of Prop. 5.3 we observe that
$\overline{D_{c}}(a)\ominus\widetilde{\overline{D_{c}}}(\operatorname{lab}(\Delta))$
is maximal if $c=a$ and then has the value
$\bigwedge_{b\in\operatorname{lab}(\Delta)}d_{A}(a,b)$. So, finally:

$\displaystyle\operatorname{\alpha_{T}}(\operatorname{\log_{T}}(\operatorname{\gamma_{T}}(d)))(X_{1},X_{2})$
$\displaystyle=\bigvee_{c\in
A}\alpha_{T}(\operatorname{\bigcirc}_{c}[\operatorname{\gamma_{T}}(d)])(X_{1},X_{2})\lor
d_{\emptyset}(X_{1},X_{2})$
$\displaystyle=d_{\emptyset}(X_{1},X_{2})\lor\bigvee_{(a,x^{\prime})\in\delta[X_{1}]}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\bigwedge_{b\in\operatorname{lab}(\Delta)}d_{A}(a,b)\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\backslash\Delta))\Big{)}.$

Continuity of $\operatorname{beh_{T}}$ follows from Lemma 5.21.

The special case of $X_{1}\neq\emptyset$, $X_{2}=\emptyset$ is an effect of
the term $\\{1\\}$ in the logic function $\operatorname{\log_{T}}$.

Note that to our knowledge there is no straightforward way to compute the
bisimilarity distance on the determinization (see Theorem 17 in [afs:linear-
branching-metrics]). Next, we explain the above fixpoint equation as a two-
player game.

######  Remark 5.19.

Given two sets $X_{1},X_{2}\subseteq X$ and a threshold $\varepsilon\in[0,1]$,
we want to check, whether $d_{\mathrm{T}}(X_{1},X_{2})\leq\varepsilon$ with a
game played by two players: Death D and Maiden M. First, D chooses a
transition $(a,x^{\prime})$ of $\delta[X_{1}]$ and also stipulates a set
$\Delta\subseteq\delta[X_{2}]$ of allowed transitions for M. Now M has two
possibilities: she can either accept the set $\Delta$ presented by D, or she
can reject it. If she rejects it, she can only reach states in
$Y^{\prime}:=\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)$ and whatever
way D chooses to continue his trace from the state $x^{\prime}$, M must
continue her trace from one of the states in $Y^{\prime}$. The game therefore
continues with the sets $\\{x^{\prime}\\}$ and $Y^{\prime}$. If, on the other
hand, M chooses to accept the set presented by D, then, in trying to duplicate
the trace begun by D with one of the transitions in $\Delta$, she makes an
error of at least $\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)$. It is clear
that M should only make this decision, if she thinks, that D can otherwise
force a larger error in a later stage of the game. The game therefore ends and
M wins iff $\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)\leq\varepsilon$.

######  Example 5.20.

We compute the directed trace distance of the state $x$ to the state $y$ in
the metric transition system over $A=[0,1]$ depicted in Figure 2 with
$\operatorname{Tr}(x)=\\{(0,0),(0,1)\\},\operatorname{Tr}(y)=\\{(\nicefrac{{1}}{{2}},0),(0,1)\\}$.
There is only one outgoing transition from $x$ and there are four possible
choices for $\Delta\subseteq\delta(y)$. The corresponding terms are calculated
in Figure 2, where we used that we already computed
$d_{\mathrm{T}}(\\{x^{\prime}\\},\\{y_{1}\\})=d_{\mathrm{T}}(\\{x^{\prime}\\},\\{y_{2}\\})=d_{\mathrm{T}}(\\{x^{\prime}\\},\emptyset)=1$
and $d_{\mathrm{T}}(\\{x^{\prime}\\},\\{y_{1},y_{2}\\})=0$. Taking the maximum
of the minima we see that
$d_{\mathrm{T}}(\\{x\\},\\{y\\})=\nicefrac{{1}}{{2}}$, which is indeed the
Hausdorff distance between the two trace sets.

$y$$y_{1}$$y_{2}$$\nicefrac{{1}}{{2}}$$0$$0$$1$$x$$x^{\prime}$$0$$0$$1$ $\Delta$ | $\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)$ | $d_{\mathrm{T}}(\\{x^{\prime}\\},\operatorname{tgt}(\delta(y)\setminus\Delta))$
---|---|---
$\emptyset$ | $1$ | $0$
$\\{(\nicefrac{{1}}{{2}},y_{1})\\}$ | $\nicefrac{{1}}{{2}}$ | 1
$\\{(0,y_{2})\\}$ | 0 | 1
$\delta(y)$ | 0 | 1
Figure 2: Computation of trace distance

######  Lemma 5.21.

The restriction of the behaviour function
$\operatorname{beh_{T}}\colon\mathit{DPMet}(\mathcal{P}(X))\to\mathit{DPMet}(\mathcal{P}(X))$
to the set of metrics that are join-preserving in the first argument is
continuous for every transition system, independent of its branching type.

######  Proof 5.22.

Let $(d_{\beta})_{\beta<\kappa}$ be an ascending sequence in
$\mathit{DPMet}(\mathcal{P}(X))$. From the monotonicity of
$\operatorname{beh_{T}}$ we get

$\operatorname{beh_{T}}(\bigvee_{\beta<\kappa}d_{\beta})\geq\bigvee_{\beta<\kappa}\operatorname{beh_{T}}(d_{\beta})$

For the other direction fix sets $X_{1},X_{2}\subseteq X$ (without loss of
generality we can assume that $X_{2}\neq\emptyset$) and let $\varepsilon>0$.
We can assume that

$\operatorname{beh_{T}}(\bigvee_{\beta<\kappa}d_{\beta})(X_{1},X_{2})=\bigvee_{x\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x)}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)\land(\bigvee_{n\in\mathbb{N}}d_{\beta})(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)\Big{)}$

and choose $x\in X_{1}$, $(a,x^{\prime})\in\delta(x)$ and
$\Delta\subseteq\delta[X_{2}]$, such that

$\displaystyle\operatorname{beh_{T}}(\bigvee_{\beta<\kappa}d_{\beta})(X_{1},X_{2})$
$\displaystyle\leq\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)\land(\bigvee_{\beta<\kappa}d_{\beta})(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)+\varepsilon$
$\displaystyle=\bigvee_{\beta<\kappa}\Big{(}\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)\land
d_{\beta}(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)\Big{)}+\varepsilon$
$\displaystyle\leq\bigvee_{\beta<\kappa}\operatorname{beh_{T}}(d_{\beta})(X_{1},X_{2})+\varepsilon$

Since $\varepsilon>0$ is arbitrary we can conclude that

$\operatorname{beh_{T}}(\bigvee_{\beta<\kappa}d_{\beta})(X_{1},X_{2})\leq\bigvee_{\beta<\kappa}\operatorname{beh_{T}}(d_{\beta})(X_{1},X_{2})$

In the case of the trace metric we can eliminate constant shifts from the
logic without losing expressiveness. This is a consequence of Cor. 5.3, which
we will prove later.

#### Decorated Trace Distances

Now we consider the quantitative generalization of decorated trace preorders.
We follow a presentation similar to Thm. 4.3, wherein we characterize the
least fixpoint of a behaviour function parameterized by a distance
$d_{0}\in\mathit{DPMet}(X)$, which is in turn induced by a set
$\mathcal{G}\subseteq[0,1]^{X}$, corresponding to completed/failure/readiness
traces.

Let $d_{0}\in\mathit{DPMet}(X)$ and consider the map
$\operatorname{beh}_{d_{0}}\colon\mathit{DPMet}(\mathcal{P}(X))\to\mathit{DPMet}(\mathcal{P}(X))$
defined as
$\operatorname{beh}_{d_{0}}(d)=\operatorname{beh_{T}}(d)\vee(d_{0})_{\overrightarrow{H}}$,
for any $d\in\mathit{DPMet}(\mathcal{P}(X))$. Then
$\mu\operatorname{beh}_{d_{0}}(X_{1},X_{2})$ is characterized as the infimum
of those $\varepsilon\in[0,1]$ that satisfy:

$\forall{x_{1}\in X_{1},x^{\prime}_{1},\sigma}\colon
x_{1}\xrightarrow{\sigma}x^{\prime}_{1}\ \implies\ \exists{x_{2}\in
X_{2},x^{\prime}_{2},\tau}\colon x_{2}\xrightarrow{\tau}x^{\prime}_{2}\land
d_{\mathrm{Tr}}(\sigma,\tau)\leq\varepsilon\land
d_{0}(x^{\prime}_{1},x^{\prime}_{2})\leq\varepsilon.$

######  Proof 5.23.

Let $d=\mu\operatorname{beh}_{d_{0}}$. We first show that the left-hand side
is greater or equal to the right-hand side.

$d(X_{1},X_{2})=\bigvee_{x\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x)}\Big{[}\bigwedge_{y\in
X_{2}}d_{0}(x,y)\\\
\lor\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)\land
d\big{(}\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)\big{)}\Big{)}\Big{]}.$

Fix two sets $X_{1},X_{2}\subseteq X$ and define $r:=d(X_{1},X_{2})$. We can
assume that $r<1$, otherwise there is nothing to show. Now let $\varepsilon>r$
and consider $\sigma\in\operatorname{Tr}(x)$ for some $x\in X_{1}$ as well as
a state $x^{\prime}$ with $x\xrightarrow{\sigma}x^{\prime}$. We will construct
a trace $\tau\in\operatorname{Tr}(y)$ with
$d_{\operatorname{Tr}}(\sigma,\tau)\leq\varepsilon$, such that
$y\xrightarrow{\tau}y^{\prime}$ for some state $y^{\prime}$ with
$d_{0}(x^{\prime},y^{\prime})\leq\varepsilon$. Let $\sigma=a_{0}\dots
a_{\ell-1}$ and $(x_{i})$ be a sequence of states with $x_{0}=x$,
$x_{\ell}=x^{\prime}$ and $x_{i+1}\in\delta_{a_{i}}(x_{i})$ for all
$i=1,\dots,\ell-1$.

Define $\Delta_{+}=\\{(b,y^{\prime})\in\delta[X_{2}]\mid
d_{A}(a_{0},b)>\varepsilon\\}$ and
$\Delta_{-}=\delta[X_{2}]\setminus\Delta_{+}$, then

$r=d(X_{1},X_{2})=\operatorname{beh}_{d_{0}}(d)(X_{1},X_{2})\geq\bigwedge_{(b,y^{\prime})\in\Delta_{+}}d_{A}(a_{0},b)\land
d\big{(}\\{x_{1}\\},\operatorname{tgt}(\Delta_{-})\big{)}$

and therefore $d\big{(}\\{x_{1}\\},\operatorname{tgt}(\Delta_{-})\big{)}\leq
r$, in particular $\operatorname{tgt}(\Delta_{-})\neq\emptyset$. We now
inductively define non-empty sets $\Delta_{0},\dots,\Delta_{\ell-1}$ with
$\Delta_{0}=\Delta_{-}$, such that the following properties hold:

  1. 1.

$\Delta_{n+1}\subseteq\delta[\operatorname{tgt}(\Delta_{n})]$ for all
$n<\ell-1$

  2. 2.

$d(\\{x_{n+1}\\},\operatorname{tgt}(\Delta_{n}))\leq r$ for all $n<\ell$

  3. 3.

For all $n<\ell$ and all $(b,y^{\prime})\in\Delta_{n}$ we have
$d_{A}(a_{n},b)\leq\varepsilon$

If $\Delta_{n}$ has already been defined, we again consider the sets
$\Delta^{(n)}_{+}=\\{(b,y^{\prime})\in\delta[\operatorname{tgt}(\Delta_{n})]\mid
d_{A}(a_{n+1},b)>\varepsilon\\}$ and
$\Delta^{(n)}_{-}=\delta[\operatorname{tgt}(\Delta_{n})]\setminus\Delta^{(n)}_{+}$.
Then by the inductive hypothesis we get

$\displaystyle r$ $\displaystyle\geq
d\big{(}\\{x_{n+1}\\},\operatorname{tgt}(\Delta_{n})\big{)}=\operatorname{beh}_{d_{0}}(d)\big{(}\\{x_{n+1}\\},\operatorname{tgt}(\Delta_{n})\big{)}$
$\displaystyle\geq\bigwedge_{(b,y^{\prime})\in\Delta^{(n)}_{+}}d_{A}(a_{n+1},b)\land
d\big{(}\\{x_{n+2}\\},\operatorname{tgt}(\Delta^{(n)}_{-})\big{)}$

and therefore
$d\big{(}\\{x_{n+2}\\},\operatorname{tgt}(\Delta^{(n)}_{-})\big{)}\leq r$,
since $\bigwedge_{(b,y^{\prime})\in\Delta^{(n)}_{+}}\geq\varepsilon$. In
particular $\operatorname{tgt}(\Delta^{(n)}_{-})\neq\emptyset$. We can thus
put $\Delta_{n+1}=\Delta^{(n)}_{-}$. This finishes the induction.

Now note that

$\bigwedge_{y\in\operatorname{tgt}(\Delta_{\ell-1})}d_{0}(x_{\ell},y)\leq\operatorname{beh}_{d_{0}}(d)(\\{x_{\ell}\\},\operatorname{tgt}(\Delta_{\ell-1})\big{)}=d(\\{x_{\ell}\\},\operatorname{tgt}(\Delta_{\ell-1})\big{)}\leq
r$

In particular there is some $y_{\ell}\in\operatorname{tgt}(\Delta_{\ell-1})$,
such that $d_{0}(x_{\ell},y_{\ell})\leq\varepsilon$. We can choose a
transition $(b_{\ell-1},y_{\ell})\in\Delta_{\ell-1}$ and since
$\Delta_{\ell-1}\subseteq\delta[\operatorname{tgt}(\Delta_{\ell-2})]$, there
is some $y_{\ell-1}\in\operatorname{tgt}(\Delta_{\ell-2})$ such that
$(b,y_{\ell})\in\delta(y_{\ell-1})$. Continuing in this way, we can now
construct a sequence $(y_{1},\dots,y_{\ell})$ by backwards induction with
$y_{n}\in\operatorname{tgt}(\Delta_{n-1})$ for all $n=1,\dots,\ell$.

For the other direction we show by induction on $i$, that
$\operatorname{beh}_{d_{0}}^{i}(\bot)(X_{1},X_{2})\leq r$ for all pairs
$(X_{1},X_{2})$ in the set

$\displaystyle\Omega=\\{(X_{1},X_{2})\mid\ $ For all $x\in X_{1}$, all
$\sigma\in\operatorname{Tr}(x)$ and every $x^{\prime}$ with
$x\xrightarrow{\sigma}x^{\prime}$ there is $y\in X_{2}$,
$\tau\in\operatorname{Tr}(y)$ and $y^{\prime}$ with
$y\xrightarrow{\tau}y^{\prime}$, $\displaystyle\text{such that
$d_{\mathrm{Tr}}(\sigma,\tau)\leq r$ and $d_{0}(x^{\prime},y^{\prime})\leq
r$}\\}$

For $i=0$ there is nothing to show, in the successor case we have

$\displaystyle\operatorname{beh}_{d_{0}}^{i+1}(\bot)(X_{1},X_{2})=$
$\displaystyle\bigvee_{x\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x)}\Big{[}\bigwedge_{y\in
X_{2}}d_{0}(x,y)$
$\displaystyle\quad\lor\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)\land\operatorname{beh}_{d_{0}}^{i}(\bot)\big{(}\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)\big{)}\Big{)}\Big{]}$

By considering the empty trace $\sigma=\varepsilon$ in the definition of
$\Omega$, it is clear that

$\bigvee_{x\in X_{1}}\bigwedge_{y\in X_{2}}d_{0}(x,y)\leq\varepsilon$

It thus suffices to show that

$\bigvee_{x\in
X_{1}}\bigvee_{(a,x^{\prime})\in\delta(x)}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)\land\operatorname{beh}_{d_{0}}^{i}(\bot)\big{(}\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)\big{)}\Big{)}\leq
r$

Fix $x\in X_{1}$ and a transition $(a,x^{\prime})\in\delta(x)$. Consider a
subset $\Delta\subseteq\delta[X_{2}]$ and assume that
$r_{1}:=\bigwedge_{(b,y^{\prime})\in\Delta}d_{A}(a,b)>r$. By the inductive
hypothesis, it suffices to show that

$(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta))\in\Omega$

Let $\sigma$ be a trace of $x^{\prime}$ and
$x^{\prime}\xrightarrow{\sigma}x^{\prime\prime}$. Then $a\sigma$ is a trace of
$x$ and therefore there is some $y\in X_{2}$, a trace of the form
$b\tau\in\operatorname{Tr}(y)$ and states $y^{\prime},y^{\prime\prime}$ with
$y\xrightarrow{b}y^{\prime}\xrightarrow{\tau}y^{\prime\prime}$ with
$d_{\operatorname{Tr}}(a\sigma,b\tau)\leq r$ and
$d_{0}(x^{\prime\prime},y^{\prime\prime})\leq r$. But this implies in
particular that $d_{A}(a,b)\leq r$ and therefore
$y^{\prime}\in\operatorname{tgt}(\delta[X_{2}]\setminus\Delta))$, as desired.

When $d_{0}$ is the constant $0$-metric, this results in the behaviour
function $\operatorname{beh_{T}}$ that characterizes trace distance. Next, we
reformulate the result in terms of a set $\mathcal{G}\subseteq[0,1]^{X}$; this
in turn helps in deriving the characterization of various decorated trace
distances. We start by imposing a condition on such a set $\mathcal{G}$ that
guarantees that $\operatorname{\alpha_{T}}(\mathcal{G})$ is the directed
Hausdorff lifting of $d_{0}=\operatorname{\alpha_{S}}(\mathcal{G})$ (cf. Sct.
5.2), which ensures that by Prop. 3 the enriched logic function induces a
behaviour function as in the previous theorem.color=green!20]Removed the
reference to the figure, since it is not yet relevant in my opinion.

Let $\mathcal{G}\subseteq[0,1]^{X}$ such that
$d_{0}=\operatorname{\alpha_{S}}(\mathcal{G})$. Then
$\operatorname{\alpha_{T}}(\mathcal{G})=(d_{0})_{\overrightarrow{H}}$ whenever

$\forall\varepsilon>0,x\in X\ \exists g\in\mathcal{G}:\ g(x)=1\land\forall
x^{\prime}:\ g(x)\ominus g(x^{\prime})\geq d_{0}(x,x^{\prime})-\varepsilon.$

######  Proof 5.24.

We show both inequalities:

“$\geq$”

By substituting the definition of $\operatorname{\alpha_{S}}$ we get

$\displaystyle(d_{0})_{\overrightarrow{H}}(X_{1},X_{2})$
$\displaystyle=\bigvee_{x_{1}\in X_{1}}\bigwedge_{x_{2}\in
X_{2}}d_{0}(x_{1},x_{2})$ $\displaystyle=\bigvee_{x_{1}\in
X_{1}}\bigwedge_{x_{2}\in X_{2}}\bigvee_{f\in\mathcal{G}}(f(x_{1})\ominus
f(x_{2}))$ $\displaystyle\geq\bigvee_{f\in\mathcal{G}}\bigvee_{x_{1}\in
X_{1}}\bigwedge_{x_{2}\in X_{2}}(f(x_{1})\ominus f(x_{2}))$
$\displaystyle=\bigvee_{f\in\mathcal{G}}\Big{(}\bigvee_{x_{1}\in
X_{1}}f(x_{1})\ominus\bigvee_{x_{2}\in X_{2}}f(x_{2})\Big{)}$
$\displaystyle=\bigvee_{f\in\mathcal{G}}\big{(}\tilde{f}(X_{1})\ominus\tilde{f}(X_{2})\big{)}=\operatorname{\alpha_{T}}(\mathcal{G})(X_{1},X_{2}),$

where the inequality follows from the monotonicity of conjunction and we use
Lem. 2.1 for the third-last step.

“$\leq$”

Given $x,\varepsilon$, let $g_{x}^{\varepsilon}\in\mathcal{G}$ be a function
which satisfies $g_{x}^{\varepsilon}(x)\ominus
g_{x}^{\varepsilon}(x^{\prime})\geq d_{0}(x,x^{\prime})-\varepsilon$ for all
$x^{\prime}\in X$. Then we have for each $\varepsilon>0$:

$\displaystyle\bigvee_{x_{1}\in X_{1}}\bigwedge_{x_{2}\in
X_{2}}d_{0}(x_{1},x_{2})$ $\displaystyle\leq\bigvee_{x_{1}\in
X_{1}}\bigwedge_{x_{2}\in X_{2}}(g_{x_{1}}^{\varepsilon}(x_{1})\ominus
g_{x_{1}}^{\varepsilon}(x_{2}))+\varepsilon$ $\displaystyle=\bigvee_{x_{1}\in
X_{1}}\Big{(}g_{x_{1}}^{\varepsilon}(x_{1})\ominus\bigvee_{x_{2}\in
X_{2}}g_{x_{1}}^{\varepsilon}(x_{2})\Big{)}+\varepsilon$
$\displaystyle=\bigvee_{x_{1}\in
X_{1}}\Big{(}\widetilde{g_{x_{1}}^{\varepsilon}}(\\{x_{1}\\})\ominus\widetilde{g_{x_{1}}^{\varepsilon}}(X_{2})\Big{)}+\varepsilon$
$\displaystyle\leq\bigvee_{x_{1}\in
X_{1}}\bigvee_{f\in\mathcal{G}}\Big{(}\tilde{f}(\\{x_{1}\\})\ominus\tilde{f}(X_{2})\Big{)}+\varepsilon$
$\displaystyle=\bigvee_{f\in\mathcal{G}}\Big{(}\bigvee_{x_{1}\in
X_{1}}\tilde{f}(\\{x_{1}\\})\ominus\tilde{f}(X_{2})\Big{)}+\varepsilon$
$\displaystyle=\bigvee_{f\in\mathcal{G}}\Big{(}\tilde{f}(X_{1})\ominus\tilde{f}(X_{2})\Big{)}+\varepsilon$
$\displaystyle=\operatorname{\alpha_{T}}(\mathcal{G})(X_{1},X_{2})+\varepsilon$
$\displaystyle=(d_{0})_{\overrightarrow{H}}(X_{1},X_{2})+\epsilon$

We again use Lem. 2.1 for the calculations. Since this holds for all
$\varepsilon$, we obtain the desired inequality.

Assume that $\mathcal{G}\subseteq[0,1]^{X}$ satisfies the requirements of Lem.
5.3. Then
$\operatorname{\alpha_{T}}(\mu(\operatorname{\log_{T}}\cup\mathcal{G}))=(d_{\mathrm{Tr}}\otimes
d_{0})_{\overrightarrow{H}}\circ(\hat{\delta}\times\hat{\delta})$. The same
holds if the logic function $\operatorname{\log_{T}}$ is replaced by
$\operatorname{log}^{\prime}$ with
$\operatorname{log}^{\prime}(\mathcal{F})=\bigcup_{a\in
A}\bigcirc_{a}[\mathcal{F}]\cup\\{1\\}$ (without shifts).

######  Proof 5.25.

Let
$\operatorname{beh}_{\mathcal{G}}:=\alpha\circ(\operatorname{\log_{T}}\cup\mathcal{G})\circ\gamma$,
then by compositionality (Prop. 3) and Lem. 5.3:

$\operatorname{beh}_{\mathcal{G}}=\operatorname{beh_{T}}\lor\operatorname{\alpha_{T}}(\mathcal{G})=\operatorname{beh_{T}}\lor(d_{0})_{\overrightarrow{H}}.$

With Thm. 5.3 we conclude that

$\displaystyle\operatorname{\alpha_{T}}(\mu(\operatorname{log}T\cup\mathcal{G}))(X_{1},X_{2})$
$\displaystyle=\mu(\operatorname{beh_{T}}\lor(d_{0})_{\overrightarrow{H}})(X_{1},X_{2})$
$\displaystyle=\bigvee_{(\sigma_{1},x^{\prime}_{1})\in\hat{\delta}[X_{1}]}\bigwedge_{(\sigma_{2},x^{\prime}_{2})\in\hat{\delta}[X_{2}]}\big{(}d_{\mathrm{Tr}}(\sigma_{1},\sigma_{2})\lor
d_{0}(x^{\prime}_{1},x^{\prime}_{2})\big{)}$
$\displaystyle=(d_{\mathrm{Tr}}\otimes
d_{0})_{\overrightarrow{H}}(\hat{\delta}[X_{1}]\times\hat{\delta}[X_{2}])$
$\displaystyle=(d_{\mathrm{Tr}}\otimes
d_{0})_{\overrightarrow{H}}\circ(\hat{\delta}\times\hat{\delta})(X_{1},X_{2})$

It remains to show that the weaker logic function is strong enough to witness
all distances. To this end, let $X_{1},X_{2}$, we fix
$(\sigma_{1},x^{\prime}_{1})\in\hat{\delta}[X_{1}]$. Let $\varepsilon>0$ and
choose a function $g\in\mathcal{G}$, such that $g(x_{1}^{\prime})=1$ and
$g(x_{1}^{\prime})-g(x_{2}^{\prime})\geq
d_{0}(x_{1}^{\prime},x_{2}^{\prime})-\varepsilon$ for all $x_{2}^{\prime}$, in
particular those which are reachable from $X_{2}$ in exactly $|\sigma_{1}|$
steps. Let $\sigma_{1}=c_{1}\dots c_{n}$, then the function
$f=\operatorname{\bigcirc}_{c_{1}}\dots\operatorname{\bigcirc}_{c_{n}}g\in\mu(\operatorname{\log_{T}}\cup\mathcal{G})$
satisfies $\tilde{f}(X_{1})=1$ and, by induction on $n$,

$\displaystyle\tilde{f}(X_{2})=$ $\displaystyle\bigvee_{(\sigma_{2}=d_{1}\dots
d_{n},x^{\prime}_{2})\in\hat{\delta}[X_{2}]}\big{(}(1-d_{A}(c_{1},d_{1}))\land\dots\land(1-d_{A}(c_{n},d_{n}))\land
g(x_{2}^{\prime})\big{)}$
$\displaystyle=1-\bigwedge_{(\sigma_{2},x^{\prime}_{2})\in\hat{\delta}[X_{2}]}\big{(}d_{\mathrm{Tr}}(\sigma_{1},\sigma_{2})\lor(1-g)(x_{2}^{\prime})\big{)}.$

Hence this formula witnesses that

$\displaystyle\tilde{f}(X_{1})\ominus\tilde{f}(X_{2})$ $\displaystyle\geq
1-\Big{(}1-\bigwedge_{(\sigma_{2},x^{\prime}_{2})\in\hat{\delta}[X_{2}]}\big{(}d_{\mathrm{Tr}}(\sigma,\tau)\lor(1-g)(x_{2}^{\prime})\big{)}\Big{)}$
$\displaystyle\geq\bigwedge_{(\sigma_{2},x^{\prime}_{2})\in\hat{\delta}[X_{2}]}\big{(}d_{\mathrm{Tr}}(\sigma,\tau)\lor
d_{0}(x_{1}^{\prime},x_{2}^{\prime})\big{)}-\varepsilon$

Since $\varepsilon>0$ is arbitrary, the result follows.

$\mathcal{G}$ | $d_{0}(x,y)$ | Behavioural distance
---|---|---
$\\{f^{\mathrm{Ref}}_{A}\\}$ | $f^{\mathrm{Ref}}_{A}(x)\ominus f^{\mathrm{Ref}}_{A}(y)$ | completed trace
$\\{f^{\mathrm{Ref}}_{B},\mid B\subseteq A\\}$ | $(d_{\text{disc}})_{\overrightarrow{H}}(\operatorname{lab}(\delta(y)),\operatorname{lab}(\delta(x))$ | (discrete) failures
$\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}(\\{g_{a}\mid a\in A\\})$ | $(d_{A})_{\overrightarrow{H}}(\operatorname{lab}(\delta(y)),\operatorname{lab}(\delta(x)))$ | (Hausdorff) failures
$\\{f^{\mathrm{Ready}}_{B}\mid B\subseteq A\\}$ | $d_{\text{disc}}(\operatorname{lab}(\delta(x)),\operatorname{lab}(\delta(y)))$ | (discrete) readiness
$\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}(\\{g_{a},1-g_{a}\mid a\in A\\})$ | $(d_{A})_{H}(\operatorname{lab}(\delta(x)),\operatorname{lab}(\delta(y)))$ | (Hausdorff) readiness
$\operatorname{\mathrm{cl}}^{\land,\mathrm{sh}}(\mu\,\operatorname{\log_{T}}\cup\neg(\mu\,\operatorname{\log_{T}}))$ | $\overline{d_{\mathrm{T}}}(\\{x\\},\\{y\\})$ | possible futures
Figure 3: Behavioural distances obtained from a logic of the form
$\operatorname{log}_{0}(\mathcal{F})=\operatorname{\log_{T}}(\mathcal{F})\cup\mathcal{G}$,
respectively a behaviour function of the form
$\operatorname{beh}_{0}=\operatorname{beh_{T}}\lor(d_{0})_{\overrightarrow{H}}$,
where $d_{0}=\operatorname{\alpha_{S}}(\mathcal{G})$.

These results supply fixpoint characterizations of many meaningful behavioural
distances. In Figure 3 we summarize which primitive set of functions
$\mathcal{G}\subseteq[0,1]^{X}$ has to be added to the trace logic in order to
get (directed) metric versions of some decorated trace semantics considered in
[g:linear-branching-time]: completed/failure/ready trace semantics.

Consider the following functions
$f^{\mathrm{Ref}}_{B},f^{\mathrm{Ready}}_{B},g_{a}\in[0,1]^{X}$:

$f^{\mathrm{Ref}}_{B}(x)=\begin{cases}1&\text{$x\in\operatorname{\mathrm{Ref}}(B)$}\\\
0&\text{otherwise}\end{cases}\quad
f^{\mathrm{Ready}}_{B}(x)=\begin{cases}1&\text{$x\in\operatorname{\mathrm{Ready}}(B)$}\\\
0&\text{otherwise}\end{cases}\quad
g_{a}(x)=\bigwedge_{b\in\operatorname{lab}(\delta(x))}d_{A}(a,b).$

Then by adding $\mathcal{G}$ to $\operatorname{\log_{T}}$ results in the
behaviour functions and distances as given in Figure 3.

######  Proof 5.26.

It is easy to see that in each case, $\mathcal{G}\cup\\{1\\}$ satisfies the
requirements of Cor. 5.3. In the case of completed trace, (discrete) failues
and readiness semantics this is true for analogous reasons as explained in the
proof of Cor. 4.3. In the other three cases we close under arbitrary meets and
shifts.

Note that the different versions of failures and readiness metrics correspond
to different ways to measure the distance between the refuse/ready sets of two
states. In the first version we take the discrete metric on $\mathcal{P}(A)$,
and in the second version we take the Hausdorff lifting of $d_{A}$. In the
qualitative setting, the two notions collapse. The Hausdorff versions are the
ones to use if we want to recover the hierarchy of [g:linear-branching-time].

TraceCompleted TraceHausdorff Failurepseudo-Hausdorff FailureHausdorff
Readydiscrete FailurePossible Futuresdiscrete ReadyBisimulation

Consider also the pseudo-Hausdorff failure semantics arising from choosing a
set $\mathcal{G}$ of predicates with
$\alpha_{S}(\mathcal{G})(x,y)=d_{0}(x,y)=(d_{A})_{\overrightarrow{H}}(A\backslash\operatorname{lab}(\delta(x)),A\backslash\operatorname{lab}(\delta(y)))$.
In the qualitative setting this notion collapses with Hausdorff failure and
discrete failure semantics, but in the metric setting the pseudo-Hausdorff
failure distance is not even bounded by the bisimulation distance. The shown
relations are obvious from comparing the corresponding metrics $d_{0}$ in
Figure 3.

Again we conclude by comparing the qualitative and quantitative case.

Consider the map
$\alpha\colon\mathit{DPMet}(\mathcal{P}(X))\to\operatorname{Pre}(\mathcal{P}(X))$
given by $\alpha(d)=\\{(X_{1},X_{2})\mid d(X_{1},X_{2})=0\\}$. If the set $A$
of actions is finite, then
$\mu\,\operatorname{beh_{t}}=\alpha(\overline{\mu\,\operatorname{beh_{T}}})$.

######  Proof 5.27.

Let
$\gamma\colon\operatorname{Pre}(\mathcal{P}(X))\to\mathit{DPMet}(\mathcal{P}(X))$
be given by $\gamma(R)=1-\chi_{R}$ and note that $\alpha\dashv\gamma$ is a
Galois connection. Also consider the directed version
$\operatorname{beh}_{\overrightarrow{t}}\colon\operatorname{Pre}(X)\to\operatorname{Pre}(X)$
given by

$\operatorname{beh}_{\overrightarrow{t}}(R)=\\{(X_{1},X_{2})\mid(X_{2}=\emptyset\implies
X_{1}=\emptyset)\land\forall a\in
A\colon\delta_{a}[X_{1}]\mathrel{R}\delta_{a}[X_{2}]\\}$

It is easy to see, that analogous to the reasoning in the undirected case, the
least fixpoint of $\operatorname{beh}_{\overrightarrow{t}}$ characterizes
trace inclusion. It now suffices to show that
$\operatorname{beh}_{\overrightarrow{t}}\circ\alpha(d)=\alpha\circ\operatorname{beh_{T}}(d)$
for all $d$ that are join-preserving in the first argument. Since join-
preservation is preserved throughout the fixpoint iteration, this will allow
us to conclude that
$\mu\,\operatorname{beh}_{\overrightarrow{t}}=\alpha(\mu\,\operatorname{beh_{T}})$,
so in particular
$\mu\,\operatorname{beh_{t}}=\mu\,\operatorname{beh}_{\overrightarrow{t}}\cap(\mu\,\operatorname{beh}_{\overrightarrow{t}})^{-1}=\alpha(\overline{\mu\,\operatorname{beh_{T}}})$.

Let $d\in\mathit{DPMet}(\mathcal{P}(X))$ be join-preserving in the first
argument. First consider
$(X_{1},X_{2})\in\operatorname{beh}_{\overrightarrow{t}}\circ\alpha(d)$, then
$X_{2}=\emptyset$ implies $X_{1}=\emptyset$ and
$\delta_{a}[X_{1}]\mathrel{\alpha(d)}\delta_{a}[X_{2}]$ for all $a\in A$. We
need to show that $(X_{1},X_{2})\in\alpha\circ\operatorname{beh_{T}}(d)$, that
means $\operatorname{beh_{T}}(d)(X_{1},X_{2})=0$.

We can assume that $X_{2}\neq\emptyset$. Fix $x\in X$, a transition
$(a,x^{\prime})\in\delta(x)$ and $\Delta\subseteq\delta[X_{2}]$ If $\Delta$
contains an $a$-transition, then
$\bigwedge_{b\in\operatorname{lab}(\Delta)}d_{A}(a,b)=0$, otherwise
$\operatorname{tgt}(\delta[X_{2}]\setminus\Delta)\supseteq\delta_{a}[X_{2}]$
and therefore, due to (anti-)monotonicity in the arguments,

$d(\\{x^{\prime}\\},\operatorname{tgt}(\delta_{a}[X_{2}]\setminus\Delta))\leq
d(\delta_{a}[X_{1}],\delta_{a}[X_{2}])=0$

Consequently

$\operatorname{beh_{T}}(d)(X_{1},X_{2})=\bigvee_{(a,x^{\prime})\in\delta[X_{1}]}\bigvee_{\Delta\subseteq\delta[X_{2}]}\Big{(}\bigwedge_{b\in\operatorname{lab}(\Delta)}d_{A}(a,b)\land
d(\\{x^{\prime}\\},\operatorname{tgt}(\delta[X_{2}]\setminus\Delta))\Big{)}=0$

For the other direction consider
$(X_{1},X_{2})\in\alpha\circ\operatorname{beh_{T}}(d)$, that means
$\operatorname{beh_{T}}(d)(X_{1},X_{2})=0$. We need to show that
$X_{2}=\emptyset$ implies $X_{1}=\emptyset$ and that
$\delta_{a}[X_{1}]\mathrel{\alpha(d)}\delta_{a}[X_{2}]$ for all $a\in A$. The
first point is clear, for the other point we fix $a\in A$ and a state
$x^{\prime}\in\delta_{a}[X_{1}]$. Now note that

$0=\operatorname{beh_{T}}(d)(X_{1},X_{2})\geq\bigwedge_{b\in
A\setminus\\{a\\}}d_{A}(a,b)\land d(\\{x^{\prime}\\},\delta_{a}[X_{2}])$

Since $A$ is assumed to be finite and $d_{A}$ is a proper metric, this yields
$d(\\{x^{\prime}\\},\delta_{a}[X_{2}])=0$. Using that $d$ is join-preserving
in the first argument, we finally get
$d(\delta_{a}[X_{1}],\delta_{a}[X_{2}])=0$.

The necessity of requiring finiteness of $A$ is illustrated by Ex. 5.28.

######  Example 5.28.

Consider the transition system: $X=\\{x,y_{i+1}\mid i\in\mathbb{N}\\}$ with
transitions $x\xrightarrow{0}x$ and
$y_{i}\xrightarrow{\nicefrac{{1}}{{i}}}y_{i}$ for $i\geq 1$. The trace
distance of $X_{1}=\\{y_{i+1}\mid i\in\mathbb{N}\\}$ and
$X_{2}=X_{1}\cup\\{x\\}$ is
$\overline{\mu\,\operatorname{beh_{T}}}(X_{1},X_{2})=0$. However we do not
have full trace inclusion, hence
$(X_{1},X_{2})\notin\mu\,\operatorname{beh_{t}}$.

##  6 Concluding Remarks, Related and Future Work

We presented a recipe to construct (bi)simulation equivalence/distance and
trace equivalence/distance (together with various forms of their decorated
trace counterparts) as the least fixpoint of behaviour functions on the
underlying lattice $\mathbb{B}$ of equivalences/distances. Furthermore, upon
realising the relevant Galois connection $\alpha\dashv\gamma$ between the
lattices $\mathbb{L}$ (modelling sets of predicates) and $\mathbb{B}$, we
showed in each case that these behaviour functions arise naturally (i.e.,
$\operatorname{beh}=\alpha\circ\operatorname{log}\circ\gamma$) when the logic
function $\operatorname{log}$ is compatible with the closure
$\gamma\circ\alpha$. By doing so, we not only recover the fixpoint
characterizations of the branching-time spectrum, but we also gave novel ones
in the linear-time spectrum (like the trace distances and their variations:
completed trace/failure/ready/possible futures).

Related work. Our work is related to [afs:linear-branching-metrics,
fl:quantitative-spectrum-journal], where the former establishes a logical
characterization (using the syntax of LTL and $\mu$-calculus) of bisimulation
and trace distances, while the latter recasts a part of the classical linear-
branching time spectrum to a quantitative one involving metrics, based on
gamescolor=green!20]B: mentioned games, since this is important for Fahrenberg
et al.. The fixpoint and logical characterizations of (decorated) trace
distances were not present in both [afs:linear-branching-metrics,
fl:quantitative-spectrum-journal]. In [fl:quantitative-spectrum-journal] the
authors parameterize over trace distances, which we are notcolor=green!20]B: I
clarified that we do not do this parameterization., and by restricting to
pointwise trace distance with discount one, we obtain corresponding notions
for bisimilarity, trace, (Hausdorff) readiness and 2-nested simulation
distance. Note that [fl:quantitative-spectrum-journal] does not treat
failures. linecolor=blue,backgroundcolor=blue!25,bordercolor=blue][7, Figure
1] seems to claim that their framework includes possible futures as “2-nested
trace inclusion/equivalence”. Also, our game in Remark 5.19 is different from
the games played in [fl:quantitative-spectrum-journal], since it is played
locally on the powerset domain.

Coalgebraists familiar with fibrations/indexed category [jacobs-fibrations]
will recognize the Galois connection between the fibres of two indexed
categories: one modelling the logical universe, the other behavioural universe
on the state space of a coalgebra. Indeed, Klin in his PhD thesis [k:coalg-
process-equivalence] has explored this adjoint situation
$\operatorname{\alpha_{b}}\dashv\operatorname{\gamma_{b}}$ (cf. Section 4.1);
note behavioural metrics were not treated in [k:coalg-process-equivalence].
The two approaches diverge in the treatment of closures especially in the
context of decorated traces. In this paper, closures are always induced as
monad from the adjoint situation and to handle (decorated) trace equivalences
we consider the adjoint situation
$\operatorname{\alpha_{t}}\dashv\operatorname{\gamma_{t}}$ since the closure
$\operatorname{c_{b}}$ is not sound w.r.t. (decorated) trace equivalence. In
Klin’s approach, on the contrary, the adjunction
$\operatorname{\alpha_{b}}\dashv\operatorname{\gamma_{b}}$ used to
characterize bisimilarity is fixed (even for decorated trace equivalences),
but the notion of closure is left parametric [k:coalg-process-equivalence,
Definition 3.31]. Our new insight in the qualitative case is that the closure
is naturally induced by the Galois connection and the characterization of
fixpoint preservation is a fundamental ingredient. color=green!20]B: Here
there was a sentence on how we could handle 2-nested simulation equivalence
more easily. But since we deleted this, I removed the sentence.

We also point out the differences to the dual adjunction approach
[k:coalgebraic-logic-beyond-sets, kp:coalgebraic-modal-logics-overview,
kr:logics-coinductive-predicates, Pavlovic2006:DualAdj] to coalgebraic modal
logic. There the functor on the “logic universe” characterizes the _syntax_ of
the logics, while the semantics is given by a natural transformation. In
[kr:logics-coinductive-predicates] the approach is lifted to fibrations (in
which the equivalence lives). Generalizing our approach however would lead to
situation where we obtain a fibred adjunction between two fibrations (for
logic and behaviour) on the same category. In [kkkrh:expressivity-
quantitative-modal-logics] the approach of [kr:logics-coinductive-predicates]
is instantiated to a quantitative setting, without treating trace metrics. A
central notion there is that of an approximating family, which, translated
into our language, says that $\mathcal{F}\subseteq[0,1]^{X}$ is an
approximating family iff $\forall
f\in[0,1]^{X}\colon\alpha(\mathcal{F})\geq\alpha(\\{f\\})$ implies
$\alpha(\operatorname{log}(\mathcal{F}))\geq\alpha(\operatorname{log}(\\{f\\}))$,
with $\operatorname{log}$ being restricted to applying modalities. If
$\operatorname{log}$ is join-preserving, this is equivalent to
$\operatorname{log}(c(\mathcal{F}))\subseteq
c(\operatorname{log}(\mathcal{F}))$, i.e., it is strongly related to
compatibility (see Lemma 6.1 in the appendix).

######  Lemma 6.1.

Let $\alpha\dashv\gamma$ be a Galois connection between lattices $\mathbb{L}$,
$\mathbb{B}$ (with $c=\gamma\circ\alpha$) and let
$\operatorname{log}\colon\mathbb{L}\to\mathbb{L}$ be a monotone function.
Furthermore let $\ell\in\mathbb{L}$. Then
$\operatorname{log}(c(\ell))\sqsubseteq c(\operatorname{log}(\ell))$ iff

$\forall\ell^{\prime}\in\mathbb{L}\colon\big{(}\alpha(\ell^{\prime})\sqsubseteq\alpha(\ell)\implies\alpha(\operatorname{log}(\ell^{\prime}))\sqsubseteq\alpha(\operatorname{log}(\ell))\big{)}$

If, more concretely, $\mathbb{L}=\mathcal{P}([0,1]^{X})$, $\operatorname{log}$
is join-preserving (union-preserving) and $\mathcal{F}\in\mathbb{L}$, then
$\alpha(\operatorname{log}(\mathcal{F}))=\alpha(\operatorname{log}(c(\mathcal{F}))=\operatorname{beh}(\alpha(\mathcal{F}))$
iff

$\forall
f\in[0,1]^{X}\colon\big{(}\alpha(\\{f\\}))\leq\alpha(\mathcal{F})\implies\alpha(\operatorname{log}(\\{f\\}))\leq\alpha(\operatorname{log}(\mathcal{F}))\big{)}.$

######  Proof 6.2.

We first assume that $\operatorname{log}(c(\ell))\sqsubseteq
c(\operatorname{log}(\ell))$. Let $\ell^{\prime}\in\mathbb{L}$ and assume that
$\alpha(\ell^{\prime})\sqsubseteq\alpha(\ell)$, which is equivalent to
$\ell^{\prime}\sqsubseteq\gamma(\alpha(\ell))=c(\ell)$ due to the properties
of Galois connections. Hence, due to compatibility:

$\operatorname{log}(\ell^{\prime})\sqsubseteq\operatorname{log}(c(\ell))\sqsubseteq
c(\operatorname{log}(\ell))=\gamma(\alpha(\operatorname{log}(\ell)),$

which implies
$\alpha(\operatorname{log}(\ell^{\prime}))\sqsubseteq\alpha(\operatorname{log}(\ell))$.

If, on the other hand, assume that for all $\ell^{\prime}\in\mathbb{L}$,
$\alpha(\ell^{\prime})\sqsubseteq\alpha(\ell)$ implies
$\alpha(\operatorname{log}(\ell^{\prime}))\sqsubseteq\alpha(\operatorname{log}(\ell))$.
We know that
$\alpha(c(\ell))=\alpha(\gamma(\alpha(\ell)))\sqsubseteq\alpha(\ell)$ due to
the properties of a Galois connection (we even have equality). Setting
$\ell^{\prime}=c(\ell)$ this implies that:

$\alpha(\operatorname{log}(c(\ell)))\sqsubseteq\alpha(\operatorname{log}(\ell))$

Again, we can use the adjoint property and obtain

$\operatorname{log}(c(\ell))\sqsubseteq\gamma(\alpha(\operatorname{log}(\ell)))=c(\operatorname{log}(\ell)).$

To conclude, we have to show that

$\forall
f\in[0,1]^{X}\colon\big{(}\alpha(\\{f\\}))\leq\alpha(\mathcal{F})\implies\alpha(\operatorname{log}(\\{f\\})\leq\alpha(\operatorname{log}(\mathcal{F}))\big{)}$

is equivalent to

$\forall\mathcal{G}\subseteq[0,1]^{X}\colon\big{(}\alpha(\mathcal{G}))\leq\alpha(\mathcal{F})\implies\alpha(\operatorname{log}(\mathcal{G}))\leq\alpha(\operatorname{log}(\mathcal{F}))\big{)}.$

Clearly, one direction is obvious. For the other assume that the first
property holds and let $\mathcal{G}\subseteq[0,1]^{X}$ with
$\alpha(\mathcal{G})\leq\mathcal{\alpha}(\mathcal{F})$. Then, since $\alpha$
preserves joins,

$\bigvee_{g\in\mathcal{G}}\alpha(\\{g\\})=\alpha(\bigcup_{g\in\mathcal{G}}\\{g\\})=\alpha(\mathcal{G})\leq\mathcal{\alpha}(\mathcal{F}),$

which implies $\alpha(\\{g\\})\leq\mathcal{\alpha}(\mathcal{F})$, for all
$g\in\mathcal{G}$, from which we can conclude
$\alpha(\operatorname{log}(\\{g\\}))\leq\mathcal{\alpha}(\operatorname{log}(\mathcal{F}))$.
And finally, due to the fact that $\alpha$ _and_ $\operatorname{log}$ are
join-preserving:

$\alpha(\operatorname{log}(\mathcal{G}))=\bigvee_{g\in\mathcal{G}}\alpha(\operatorname{log}(\\{g\\}))\leq\bigvee_{g\in\mathcal{G}}\alpha(\operatorname{log}(\mathcal{F}))=\alpha(\operatorname{log}(\mathcal{F})).$

Future work. Taking inspiration from the above, we want to generalize our work
to the level of coalgebras with an approach based on fibrations, enabling us
to treat other branching types, such as probabilistic branching. Note that the
coalgebraic treatment of establishing Hennessy-Milner theorems in
[Klin:LeastFibredLifting2005, k:coalg-process-equivalence] does not subsume
the behavioural distances covered in this paper, while the qualitative
spectrum has been generalized using graded monads [mps:trace-semantics-graded-
monads]. We plan to develop fixpoint and logical characterizations of
coalgebraic behavioural metrics [bbkk:coalgebraic-behavioral-metrics,
km:bisim-games-logics-metric]color=green!20]B: Added CONCUR paper with
Christina, which are generalizations of both bisimulation pseudo-metric and
trace distance.

Another direction is to consider behavioural equivalences (like failure
trace/ready trace equivalences and variations) that cannot be captured by our
modular approach (i.e., by extending the logic functions
$\operatorname{\log_{t}}$/$\operatorname{\log_{T}}$ with a _constant_
function). We also want to characterize undirected trace distance directly
without the symmetrization of directed trace distance.

Another line of research is to determine under which circumstances we can
restrict to finitary operations, from which we deviate occasionally by closing
under arbitrary meets or intersections. This should be feasible by restricting
to finitely branching transition systems. Also, in the metric case, we plan to
optimize the syntax by restricting shifts and modalities to rational numbers.
Last, but not least, it will be interesting to work out the compatibility of
$\operatorname{\log_{B}}$ for a weaker class of metric transition systems than
those which are finitely branching.color=green!20]B: I removed the reference
to compact branching since, as far as I understand, Sebastian’s proposal does
not need this.

## References

  * [1] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Coalgebraic behavioral metrics.  Logical Methods in Computer Science, 14(3), 2018.  Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015).
  * [2] Paolo Baldan, Barbara König, and Tommaso Padoan.  Abstraction, up-to techniques and games for systems of fixpoint equations.  In Proc. of CONCUR ’20, volume 171 of LIPIcs, pages 25:1–25:20. Schloss Dagstuhl – Leibniz Center for Informatics, 2020.
  * [3] Patrick Cousot and Radhia Cousot.  Systematic design of program analysis frameworks.  In Proc. of POPL ’79 (San Antonio, Texas), pages 269–282. ACM Press, 1979.
  * [4] Patrick Cousot and Radhia Cousot.  Temporal abstract interpretation.  In Mark N. Wegman and Thomas W. Reps, editors, Proc. of POPL ’00, pages 12–25. ACM, 2000.
  * [5] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga.  Linear and branching system metrics.  IEEE Transactions on Software Engineering, 35(2):258–273, 2009\.
  * [6] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled Markov processes.  Theoretical Computer Science, 318:323–354, 2004.
  * [7] Uli Fahrenberg and Axel Legay.  The quantitative linear-time-branching-time spectrum.  Theoretical Computer Science, 538:54–69, 2014.
  * [8] Matthew Hennessy and Robin Milner.  Algebraic laws for nondeterminism and concurrency.  Journal of the ACM, 32:137–161, 1985.
  * [9] Bart Jacobs.  Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics.  Elsevier, 1st edition, Jan 1999.
  * [10] Bartek Klin.  The least fibred lifting and the expressivity of coalgebraic modal logic.  In Proc. of CALCO ’05, pages 247–262. Springer, 2005.  LNCS 3629.
  * [11] Bartek Klin.  Coalgebraic modal logic beyond sets.  In Proc. of MFPS ’07, volume 173 of ENTCS, pages 177–201, 2007.
  * [12] Bartosz Klin.  An Abstract Coalgebraic Approach to Process Equivalence for Well-Behaved Operational Semantics.  PhD thesis, University of Aarhus, 2004.
  * [13] Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo.  Expressivity of quantitative modal logics: Categorical foundations via codensity and approximation.  In Proc. LICS ’21, pages 1–14. IEEE, 2021.
  * [14] Barbara König and Christina Mika-Michalski.  (Metric) bisimulation games and real-valued modal logics for coalgebras.  In Proc. of CONCUR ’18, volume 118 of LIPIcs, pages 37:1–37:17. Schloss Dagstuhl – Leibniz Center for Informatics, 2018.
  * [15] Clemens Kupke and Dirk Pattinson.  Coalgebraic semantics of modal logics: An overview.  Theoretical Computer Science, 412:5070–5094, 2011.
  * [16] Clemens Kupke and Jurriaan Rot.  Expressive logics for coinductive predicates.  In Prof. of CSL ’20, volume 152 of LIPIcs, pages 26:1–26:18. Schloss Dagstuhl – Leibniz Center for Informatics, 2020.
  * [17] George Markowsky.  Chain-complete posets and directed sets with applications.  Algebra Universalis, 6(1):53–68, 1976.
  * [18] E. J. McShane.  Extension of range of functions.  Bull. Amer. Math. Soc., 40(12):837–842, 1934.
  * [19] Stefan Milius, Dirk Pattinson, and Lutz Schröder.  Generic trace semantics and graded monads.  In Proc. of CALCO ’15, volume 35 of LIPIcs, pages 253–269. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2015.
  * [20] Dusko Pavlovic, Michael Mislove, and James Worrell.  Testing semantics: Connecting processes and process logics.  In Proc. of AMAST ’06, pages 308–322. Springer, 2006.  LNCS 4019.
  * [21] Damien Pous.  Complete lattices and up-to techniques.  In Proc. of APLAS ’07, pages 351–366. Springer, 2007.  LNCS 4807.
  * [22] Franck van Breugel and James Worrell.  A behavioural pseudometric for probabilistic transition systems.  Theoretical Computer Science, 331:115–142, 2005.
  * [23] Rob van Glabbeek.  The linear time – branching time spectrum I.  In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, chapter 1, pages 3–99. Elsevier, 2001.
  * [24] Hassler Whitney.  Analytic extensions of differentiable functions defined in closed sets.  Transactions of the American Mathematical Society, 36(1):63–89, 1934.