plain 30

11institutetext:  East China Normal University 22institutetext: Shanghai
Normal University 33institutetext: VU University Amsterdam

# Modal Characterisations of Behavioral Pseudometrics

Yuxin Deng 11 Wenjie Du 22 Daniel Gebler 33

###### Abstract

For the model of probabilistic labelled transition systems that allow for the
co-existence of nondeterminism and probabilities, we present two notions of
bisimulation metrics: one is state-based and the other is distribution-based.
We provide a sound and complete modal characterisation for each of them, using
real-valued modal logics based on the Hennessy-Milner logic. The logic for
characterising the state-based metric is much simpler than an earlier logic by
Desharnais et al. as it uses only two non-expansive operators rather than the
general class of non-expansive operators.

###### Keywords:

P

robabilistic labelled transition systems, behavioral pseudometrics, real-
valued modal logics

##  1 Introduction

Bisimulation is an important proof technique for establishing behavioural
equivalences of concurrent systems. In probabilistic concurrency theory, there
are roughly two kinds of bisimulations: one is state-based because it is
directly defined over states and then lifted to distributions, and the other
is distribution-based as it is a relation between distributions. The former is
originally defined in [LS91] to represent a branching time semantics; the
latter, as defined in [HKK14, FZ14, DFD15], is strictly coarser and represents
a linear time semantics.

In correspondence with those bisimulations, there are two notions of
behavioural pseudometrics (simply called metrics). They are more robust ways
of formalising behavioural similarity between formal systems than
bisimulations because, particularly in the probabilistic setting,
bisimulations are too sensitive to probabilities (a very small perturbation of
the probabilities would render two systems non-bisimilar). A metric gives a
quantitative measure of the distance between two systems and distance $0$
usually means that the two systems are bisimilar. A logical characterisation
of the state-based bisimulation metric for labelled Markov processes is given
in [DGJP04]. For a more general model of labelled concurrent Markov chains
(LCMCs) that allow for the co-existence of nondeterminism and probabilities, a
weak bisimulation metric is proposed in [DJGP02]. Its logical characterisation
uses formulae like $h\circ f$, where $f$ is a formula and $h$ can be any non-
expansive operator on $[0,1]$, i.e. $|h(x)-h(y)|\leq|x-y|$ for any
$x,y\in[0,1]$. A natural question then arises: instead of the general class of
non-expansive operators, is it possible to use only a few simple non-expansive
operators without losing the capability of characterising the bisimulation
metric?

In the current work, we give a positive answer to the above question. We work
in the framework of probabilistic labelled transition systems (pLTSs) that are
essentially the same as LCMCs, so the interplay of nondeterminism and
probabilities is allowed. We provide a modal characterisation of the state-
based bisimulation metric closely in line with the classical Hennessy-Milner
logic (HML) [HM85]. Our variant of the HML makes use of state formulae and
distribution formulae, which are formulae evaluated at states and
distributions, respectively, and yield success probabilities. We use merely
two non-expansive operators: negation ($\neg\phi$) and testing ($\phi\ominus
p$). Negation is self-explanatory and the testing operator checks if a state
satisfies a property with certain threshold probability. More precisely, if
state $s$ satisfies formula $\phi$ with probability $q$, then it satisfies
$\neg\phi$ with probability $1-q$, and satisfies $\phi\ominus p$ with
probability $q-p$ if $q>p$ and $0$ otherwise. In other words, we do not need
the general classs of non-expansive operators because negation and testing,
together with other modalities in the classical HML, are expressive enough to
characterise bisimulation metrics. As regards to the characterisation of
distribution-based bisimulation metric, we drop state formulae and use
distribution formulae only.

The rest of this paper is organised as follows. Section 2 provides some basic
concepts on pLTSs. Section 3 defines a two-sorted modal logic that leads to a
sound and complete characterisation of the state-based bisimulation metric.
Section 4 gives a similar characterisation for the distribution-based
bisimulation metric. In Section 5 we review some related work. Finally, we
conclude in Section 6.

##  2 Preliminaries

Let $S$ be a countable set. A _(discrete) probability subdistribution_ over
$S$ is a function $\Delta:S\rightarrow[0,1]$ with $\sum_{s\in S}\Delta(s)\leq
1$. It is a _(full) distribution_ if $\sum_{s\in S}\Delta(s)=1$. Let
$\mathop{\mbox{$\mathcal{D}$}}({S})$ denote the set of all distributions over
$S$. A matching $\omega\in\mathop{\mbox{$\mathcal{D}$}}({S\times S})$ for
$(\Delta,\Theta)\in\mathop{\mbox{$\mathcal{D}$}}({S})\times\mathop{\mbox{$\mathcal{D}$}}({S})$
is given if $\sum_{t\in S}\omega(s,t)=\Delta(s)$ and $\sum_{s\in
S}\omega(s,t)=\Theta(t)$ for all $s,t\in S$. We denote the set of all
matchings for $(\Delta,\Theta)$ by $\Omega(\Delta,\Theta)$.

A _metric_ $d$ over space $S$ is a distance function $d:S\times
S\rightarrow\mathbb{R}_{\geq 0}$ satisfying: (i) $d(s,t)=0$ iff $s=t$
(isolation), (ii) $d(s,t)=d(t,s)$ (symmetry), (iii) $d(s,t)\leq d(s,u)+d(u,t)$
(triangle inequality), for any $s,t,u\in S$. If we replace (i) with $d(s,s)=0$
for all $s\in S$, we obtain a _pseudometric_. In this paper we are interested
in pseudometrics because two distinct states can still be at distance zero if
their behaviour is similar. But for simplicity, we often use metrics for
pseudometrics. A metric $d$ over $S$ is $c$-bounded if $d(s,t)\leq c$ for any
$s,t\in S$, where $c\in\mathbb{R}_{\geq 0}$ is a positive real number.

Let $d\colon S\times S\to[0,1]$ be a metric over $S$. We lift it to be a
metric over $\mathop{\mbox{$\mathcal{D}$}}({S})$ by using the _Kantorowich
metric_ [KR58]
$\operatorname{\mathit{K}}(d)\colon\mathop{\mbox{$\mathcal{D}$}}({S})\times\mathop{\mbox{$\mathcal{D}$}}({S})\to[0,1]$
defined via a linear programming problem as follows:

$\operatorname{\mathit{K}}(d)(\Delta,\Theta)=\min_{\omega\in\Omega(\Delta,\Theta)}\sum_{s,t\in
S}d(s,t)\cdot\omega(s,t)$

for $\Delta,\Theta\in\mathop{\mbox{$\mathcal{D}$}}({S})$. The dual of the
above linear programming problem is the following

$\begin{array}[]{rl}\max\ \sum_{s\in S}(\Delta(s)-\Theta(s))x_{s},\text{
subject to }&0\leq x_{s}\leq 1\\\ &\forall s,t\in S\colon\ x_{s}-x_{t}\leq
d(s,t)\;.\end{array}$

The duality theorem in linear programming guarantees that both problems have
the same optimal value.

Let
$\hat{d}\colon\mathop{\mbox{$\mathcal{D}$}}({S})\times\mathop{\mbox{$\mathcal{D}$}}({S})\to[0,1]$
be a metric over $\mathop{\mbox{$\mathcal{D}$}}({S})$. We lift it to be a
metric over the powerset of $\mathop{\mbox{$\mathcal{D}$}}({S})$, written
$\mathop{\mbox{$\mathcal{P}$}}({\mathop{\mbox{$\mathcal{D}$}}({S})})$, by
using the _Hausdorff metric_
$\operatorname{\mathit{H}}(\hat{d})\colon\mathop{\mbox{$\mathcal{P}$}}({\mathop{\mbox{$\mathcal{D}$}}({S})})\times\mathop{\mbox{$\mathcal{P}$}}({\mathop{\mbox{$\mathcal{D}$}}({S})})\to[0,1]$
given as follows

$\operatorname{\mathit{H}}(\hat{d})(\Pi_{1},\Pi_{2})=\max\\{\adjustlimits{\sup}_{\Delta\in\Pi_{1}}{\inf}_{\Theta\in\Pi_{2}}\hat{d}(\Delta,\Theta),\
\
\adjustlimits{\sup}_{\Theta\in\Pi_{2}}{\inf}_{\Delta\in\Pi_{1}}\hat{d}(\Theta,\Delta)\\}$

for all $\Pi_{1},\Pi_{2}\subseteq\mathop{\mbox{$\mathcal{D}$}}({S})$, whereby
$\inf\emptyset=1$ and $\sup\emptyset=0$.

Probabilistic labelled transition systems (pLTSs) generalize labelled
transition systems (LTSs) by allowing for probabilistic choices in the
transitions. We consider pLTSs (or essentially _simple probabilistic automata_
[Seg95]) with countable state spaces.

######  Definition 1.

A _probabilistic labelled transition system_ is a triple
$(S,A,{\xrightarrow{\,{}\,}})$, where $S$ is a countable set of states, $A$ is
a countable set of actions, and the relation ${\xrightarrow{\,{}\,}}\subseteq
S\times A\times\mathop{\mbox{$\mathcal{D}$}}({S})$ is a transition relation.

We write $s\xrightarrow{\,{a}\,}\Delta$ for
${(s,a,\Delta)}\in{\xrightarrow{\,{}\,}}$ and define
$\operatorname{\mathit{der}}(s,a)=\\{\Delta\mid
s\xrightarrow{\,{a}\,}\Delta\\}$ as the set of all $a$-successor distributions
of $s$. A pLTS is _image-finite_ if for any state $s$ and action $a$ the set
$\operatorname{\mathit{der}}(s,a)$ is finite. In the current work, we focus on
image-finite pLTSs.

##  3 State-Based Bisimulation Metrics

We consider the complete lattice $([0,1]^{S\times S},\sqsubseteq)$ defined by
$d\sqsubseteq d^{\prime}$ iff $d(s,t)\leq d^{\prime}(s,t)$, for all $s,t\in
S$. For some $D\subseteq[0,1]^{S\times S}$ the least upper bound is given by
$(\bigsqcup D)(s,t)=\sup_{d\in D}d(s,t)$, and the greatest lower bound is
given by $(\bigsqcap D)(s,t)=\inf_{d\in D}d(s,t)$ for all $s,t\in S$. The
bottom element $\operatorname{\mathbf{0}}$ is the constant zero function
$\operatorname{\mathbf{0}}(s,t)=0$ and the top element
$\operatorname{\mathbf{1}}$ is the constant one function
$\operatorname{\mathbf{1}}(s,t)=1$ for all $s,t\in S$.

######  Definition 2.

A $1$-bounded metric $d$ on $S$ is a _state-based bisimulation metric_ if for
all $s,t\in S$ and $\epsilon\in[0,1)$ with $d(s,t)\leq\epsilon$, if
$s\xrightarrow{\,{a}\,}\Delta$ then there exists some
$t\xrightarrow{\,{a}\,}\Delta^{\prime}$ with
$\operatorname{\mathit{K}}(d)(\Delta,\Delta^{\prime})\leq\epsilon$.

The smallest (wrt. $\sqsubseteq$) state-based bisimulation metric, denoted by
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$, is called _state-
based bisimilarity metric_. Its kernel is the state-based bisimilarity as
defined in [LS91, Seg95].

$s$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$t$$t_{1}$$t_{2}$$t_{3}$$t_{4}$$t_{5}$$a$$b$$\frac{1}{2}$$\frac{1}{2}$$c$$d$$a$$\frac{1}{2}$$\frac{1}{2}$$b$$b$$c$$d$

Figure 1:
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)=\frac{1}{2}$

######  Example 1.

In this example, we calculate the distance between states $s$ and $t$ in
Figure 1. Firstly, observe that
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{2},t_{3})=0$
because $s_{2}$ is bisimilar to $t_{3}$ while
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{3},t_{3})=1$
because the two states $s_{3}$ and $t_{3}$ perform completely different
actions. Secondly, let
$\Delta=\frac{1}{2}\overline{s_{2}}+\frac{1}{2}\overline{s_{3}}$ and
$\Theta=\overline{t_{3}}$. We see that

$\begin{array}[]{rcl}\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta,\Theta)&=&\min_{\omega\in\Omega(\Delta,\Theta)}\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{2},t_{3})\cdot\omega(s_{2},t_{3})+\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{3},t_{3})\cdot\omega(s_{3},t_{3})\\\
&=&\min_{\omega\in\Omega(\Delta,\Theta)}1\cdot\omega(s_{2},t_{3})+0\cdot\omega(s_{3},t_{3})\\\
&=&\min_{\omega\in\Omega(\Delta,\Theta)}1\cdot\frac{1}{2}+0\cdot\frac{1}{2}\\\
&=&\frac{1}{2}\end{array}$

It follows that
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{1},t_{1})=\frac{1}{2}$.
Similarly, we get
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{1},t_{2})=\frac{1}{2}$.
Then it not difficult to see that

$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\overline{s_{1}},\frac{1}{2}\overline{t_{1}}+\frac{1}{2}\overline{t_{2}})~{}=~{}\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{1},t_{1})\cdot\frac{1}{2}+\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s_{1},t_{2})\cdot\frac{1}{2}~{}=~{}\frac{1}{2}$

from which we finally obtain
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)=\frac{1}{2}$.

The above coinductively defined bisimilarity metric can be reformulated as a
fixed point of a monotone functor. Let us define the functor
$\operatorname{\operatorname{\mathit{F}}}\colon[0,1]^{S\times
S}\to[0,1]^{S\times S}$ for $d\colon S\times S\to[0,1]$ and $s,t\in S$ by

$\operatorname{\operatorname{\mathit{F}}}(d)(s,t)=\sup_{a\in
A}\\{\operatorname{\mathit{H}}(\operatorname{\mathit{K}}(d))(\operatorname{\mathit{der}}(s,a),\operatorname{\mathit{der}}(t,a))\\}\,.$

It can be shown that $\operatorname{\operatorname{\mathit{F}}}$ is monotone
and its least fixed point is defined by $\bigsqcap d_{i}$, where
$d_{0}=\operatorname{\mathbf{0}}$ and
$d_{i+1}=\operatorname{\operatorname{\mathit{F}}}(d_{i})$ for all
$i\in\mathbb{N}$.

######  Proposition 1.

For image-finite pLTSs, the strong bisimilarity metric is the least fixed
point of $\operatorname{\operatorname{\mathit{F}}}$.

Now we proceed by defining a real-valued modal logic based on the Hennessy-
Milner logic [HM85], called metric HML, to characterize the bisimilarity
metric. Our logic is motivated by [DJGP02, Def. 4.1], [DGJP04, Def. 4.1] and
[DTW10, Sec. 4]. In the remainder of this section we confine ourselves to
pLTSs with finitely many states.

######  Definition 3.

Our metric HML is two-sorted and has the following syntax:

$\begin{array}[]{rl}\varphi::=&\top\ |\ \lnot\varphi\ |\ \varphi\ominus p\ |\
\varphi_{1}\land\varphi_{2}\ |\ \langle a\rangle\psi\\\\[2.15277pt]
\psi::=&\psi\ominus p\ |\ \psi_{1}\land\psi_{2}\ |\ [\varphi]\end{array}$

with $a\in A$ and $p\in[0,1]$.

Let $\operatorname{\mathcal{L}}$ denote the set of all metric HML formulae,
$\varphi$ range over the set of all _state formulae_
$\operatorname{\operatorname{\mathcal{L}}^{S}}$, and $\psi$ range over the set
of all _distribution formulae_
$\operatorname{\operatorname{\mathcal{L}}^{D}}$. The two kinds of formulae are
defined simultaneously. The operator $\phi\ominus p$ tests if a state passes
$\phi$ with probability at least $p$. If $\phi$ is a state formula then it
immediately induces a distribution formula $[\phi]$. Sometimes we abbreviate
$\langle a\rangle[\varphi]$ as $\langle a\rangle\varphi$. All other operators
are standard and have appeared in the classical HML.

######  Definition 4.

A state formula $\varphi\in\operatorname{\operatorname{\mathcal{L}}^{S}}$
evaluates in $s\in S$ as follows:

  * $\displaystyle\llbracket{\top}\rrbracket({s})=1$,

  * $\displaystyle\llbracket{\lnot\varphi}\rrbracket({s})=1-\llbracket{\varphi}\rrbracket({s})$,

  * $\displaystyle\llbracket{\varphi\ominus p}\rrbracket({s})=\max(\llbracket{\varphi}\rrbracket({s})-p,~{}0)$,

  * $\displaystyle\llbracket{\varphi_{1}\land\varphi_{2}}\rrbracket({s})=\min(\llbracket{\varphi_{1}}\rrbracket({s}),\llbracket{\varphi_{2}}\rrbracket({s}))$,

  * $\displaystyle\llbracket{\langle a\rangle\psi}\rrbracket({s})=\max_{s\xrightarrow{\,{a}\,}\Delta}\llbracket{\psi}\rrbracket({\Delta})$,

and a distribution formula
$\psi\in\operatorname{\operatorname{\mathcal{L}}^{D}}$ evaluates in
$\Delta\in\mathop{\mbox{$\mathcal{D}$}}({S})$ as follows:

  * $\displaystyle\llbracket{\psi\ominus p}\rrbracket({\Delta})=\max(\llbracket{\psi}\rrbracket({\Delta})-p,0)$,

  * $\displaystyle\llbracket{\psi_{1}\land\psi_{2}}\rrbracket({\Delta})=\min(\llbracket{\psi_{1}}\rrbracket({\Delta}),\llbracket{\psi_{2}}\rrbracket({\Delta}))$,

  * $\displaystyle\llbracket{[\varphi]}\rrbracket({\Delta})=\sum_{s\in S}\Delta(s)\llbracket{\varphi}\rrbracket({s})$.

We often use constant formulae e.g. $\underline{p}$ for any $p\in[0,1]$ with
the semantics $\llbracket{\underline{p}}\rrbracket({s})=p$, which is derivable
in the above logic by letting $\underline{p}=\top\ominus(1-p)$. Moreover, we
write $\varphi\oplus p$ for $\lnot((\lnot\varphi)\ominus p)$ which has the
semantics $\displaystyle\llbracket{\varphi\oplus
p}\rrbracket({s})=\min(\llbracket{\varphi}\rrbracket({s})+p,~{}1)=1-\max(1-\llbracket{\varphi}\rrbracket({s})-p,0)$.
In the presence of negation and conjunction we can derive disjunction by
letting $\varphi_{1}\vee\varphi_{2}$ to be
$\lnot(\lnot\varphi_{1}\wedge\lnot\varphi_{2})$. Semantics of $\langle
a\rangle\varphi$ is a translation of [DJGP02, Def. 4.1] from labelled
concurrent Markov chain semantics to pLTSs. Conjunction of distribution
formulae $\psi_{1}\land\psi_{2}$ could alternatively be replaced by
$\psi_{1}\oplus_{p}\psi_{2}$ or $\psi_{1}\oplus\psi_{2}$ [Hen12, Sec. 4] with
semantics

$\begin{array}[]{rl}\llbracket{\psi_{1}\oplus_{p}\psi_{2}}\rrbracket({\Delta})&=\displaystyle\sup_{\Delta=p\Delta_{1}+(1-p)\Delta_{2}}(p\cdot\llbracket{\psi_{1}}\rrbracket({\Delta_{1}})+(1-p)\llbracket{\psi_{2}}\rrbracket({\Delta_{2}})\\\
\llbracket{\psi_{1}\oplus\psi_{2}}\rrbracket({\Delta})&=\displaystyle\sup_{p\in(0,1)}\llbracket{\psi_{1}\oplus_{p}\psi_{2}}\rrbracket({\Delta})\end{array}$

The above metric HML induces two natural logical metrics
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}$ and
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ld}}$ on states and
distributions respectively, by letting

$\begin{array}[]{rcl}\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)&=&\sup_{\varphi\in\operatorname{\operatorname{\mathcal{L}}^{S}}}|\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})|\\\
\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ld}}(\Delta,\Theta)&=&\sup_{\psi\in\operatorname{\operatorname{\mathcal{L}}^{D}}}|\llbracket{\psi}\rrbracket({\Delta})-\llbracket{\psi}\rrbracket({\Theta})|\end{array}$

######  Example 2.

Consider the two probabilistic systems depicted in Figure 2. We have the
formula $\varphi=\langle a\rangle\psi$ where $\psi=[\langle
a\rangle\top]\land[\langle b\rangle\top])$ and would like to know the
difference $s$ and $t$ given by $\varphi$. Let

$\begin{array}[]{rcl}\Delta_{1}&=&0.2\cdot\overline{s_{1}}+0.8\cdot\overline{s_{2}}\\\
\Delta_{2}&=&0.8\cdot\overline{s_{5}}+0.2\cdot\overline{s_{6}}\\\
\Delta_{3}&=&0.5\cdot\overline{s_{3}}+0.5\cdot\overline{s_{4}}\end{array}$

Note that $\llbracket{\langle a\rangle\top}\rrbracket({s_{1}})=1$ and
$\llbracket{\langle a\rangle\top}\rrbracket({s_{2}})=0$. Then
$\llbracket{[\langle
a\rangle\top]}\rrbracket({\Delta_{1}})=0.2\cdot\llbracket{\langle
a\rangle\top}\rrbracket({s_{1}})+0.8\cdot\llbracket{\langle
a\rangle\top}\rrbracket({s_{2}})=0.2$. Similarly, $\llbracket{[\langle
b\rangle\top]}\rrbracket({\Delta_{1}})=0.8$. It follows that
$\llbracket{\psi}\rrbracket({\Delta_{1}})=\min(\llbracket{[\langle
a\rangle\top]}\rrbracket({\Delta_{1}}),~{}\llbracket{[\langle
b\rangle\top]}\rrbracket({\Delta_{1}}))=0.2$. With similar arguments, we see
that $\llbracket{\psi}\rrbracket({\Delta_{2}})=0.2$ and
$\llbracket{\psi}\rrbracket({\Delta_{3}})=0.5$. Therefore, we can calculate
that

$\begin{array}[]{l}\llbracket{\varphi}\rrbracket({s})=\max(\llbracket{\psi}\rrbracket({\Delta_{1}}),\llbracket{\psi}\rrbracket({\Delta_{2}}))=0.2\\\
\llbracket{\varphi}\rrbracket({t})=\max(\llbracket{\psi}\rrbracket({\Delta_{1}}),\llbracket{\psi}\rrbracket({\Delta_{2}}),\llbracket{\psi}\rrbracket({\Delta_{3}}))=0.5.\end{array}$

So the difference between $s$ and $t$ with respect to $\varphi$ is
$|\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})|=0.3$.
In fact we also have
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)=0.3$.

$s$$s_{1}$$s_{2}$$s_{5}$$s_{6}$$a$$a$$0.2$$0.8$$0.8$$0.2$$a$$b$$a$$b$$1.0$$1.0$$1.0$$1.0$

$t$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$s_{5}$$s_{6}$$a$$a$$a$$0.2$$0.8$$0.5$$0.5$$0.8$$0.2$$a$$b$$a$$b$$a$$b$$1.0$$1.0$$1.0$$1.0$$1.0$$1.0$

Figure 2:
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)=0.3$

######  Example 3.

At first sight the following two equations seem to be sound.

$\llbracket{[\varphi]\ominus p}\rrbracket({\Delta})=\llbracket{[\varphi\ominus
p]}\rrbracket({\Delta})\qquad\mbox{and}\qquad\llbracket{\psi}\rrbracket({\sum_{i}p_{i}\Delta_{i}})=\sum_{i}p_{i}(\llbracket{\psi}\rrbracket({\Delta_{i}}))$

However, in general they do not hold, as witnessed by the counterexamples
below. Let $\varphi=\langle b\rangle\top$, $\psi=[\varphi]\ominus 0.5$ and the
distribution $\Delta_{1}$ be the same as in Example 2. Then we have

$\begin{array}[]{rcl}\llbracket{[\varphi]\ominus
0.5}\rrbracket({\Delta_{1}})&=&\max(\llbracket{[\varphi]}\rrbracket({\Delta_{1}})-0.5,\;0)\\\
&=&\max(0.2\llbracket{[\langle
b\rangle\top]}\rrbracket({\overline{s_{1}}})+0.8\llbracket{[\langle
b\rangle\top]}\rrbracket({\overline{s_{2}}})-0.5,\;0)\\\ &=&\max(0.2\cdot
0+0.8\cdot 1-0.5,\;0)\\\ &=&0.3\\\ \\\ \llbracket{[\varphi\ominus
0.5]}\rrbracket({\Delta_{1}})&=&0.2\llbracket{\varphi\ominus
0.5}\rrbracket({s_{1}})+0.8\llbracket{\varphi\ominus
0.5}\rrbracket({s_{2}})\\\
&=&0.2\max(\llbracket{\varphi}\rrbracket({s_{1}})-0.5,\;0)+0.8\max(\llbracket{\varphi}\rrbracket({s_{2}})-0.5,\;0)\\\
&=&0.2\max(0-0.5,\;0)+0.8\max(1-0.5,\;0)\\\ &=&0.4\\\ \\\
0.2\llbracket{\psi}\rrbracket({\overline{s_{1}}})+0.8\llbracket{\psi}\rrbracket({\overline{s_{2}}})&=&0.2\llbracket{[\varphi]\ominus
0.5}\rrbracket({\overline{s_{1}}})+0.8\llbracket{[\varphi]\ominus
0.5}\rrbracket({\overline{s_{2}}})\\\
&=&0.2\max(\llbracket{[\varphi]}\rrbracket({\overline{s_{1}}})-0.5,\;0)+0.8\max(\llbracket{[\varphi]}\rrbracket({\overline{s_{2}}})-0.5,\;0)\\\
&=&0.2\max(0-0.5,\;0)+0.8\max(1-0.5,\;0)\\\ &=&0.4\end{array}$

So we see that $\llbracket{[\varphi]\ominus
0.5}\rrbracket({\Delta_{1}})\not=\llbracket{[\varphi\ominus
0.5]}\rrbracket({\Delta_{1}})$ and
$\llbracket{\psi}\rrbracket({\Delta_{1}})\not=0.2\llbracket{\psi}\rrbracket({\overline{s_{1}}})+0.8\llbracket{\psi}\rrbracket({\overline{s_{2}}})$

In what follows we will show that the logic $\operatorname{\mathcal{L}}$
precisely captures the bisimilarity metric
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$: the metric
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}$ defined by state
formulae coincides with
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$ and the metric
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ld}}$ defined by
distribution formulae coincides with
$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})$,
the lifted form of $\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$.
The two properties are entangled because state formulae and distribution
formulae are not independent.

######  Lemma 1.

  1. 1.

$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}\sqsubseteq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$

  2. 2.

$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ld}}\sqsubseteq\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})$

###### Proof.

We show the two statements simultaneously by structural induction on formulae.
For any two states $s,t\in S$ and distributions
$\Delta_{1},\Delta_{2}\in\mathop{\mbox{$\mathcal{D}$}}({S})$, we prove that

  1. (1)

$|\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})|\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)$
for all $\varphi\in\operatorname{\operatorname{\mathcal{L}}^{S}}$;

  2. (2)

$|\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})|\leq\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta_{1},\Delta_{2})$
for all $\psi\in\operatorname{\operatorname{\mathcal{L}}^{D}}$.

We first analyze the structure of $\varphi$ in (1).

  * •

$\varphi\equiv\top$. Then it is trivial to see that
$|\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})|=|1-1|=0\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)$.

  * •

$\varphi\equiv\lnot\varphi^{\prime}$. Then
$|\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})|=|\llbracket{\varphi^{\prime}}\rrbracket({t})-\llbracket{\varphi^{\prime}}\rrbracket({s})|\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)$
where the inequality holds by induction.

  * •

$\varphi\equiv\varphi^{\prime}\ominus p$. There are four subcases and we
consider one of them. Suppose $\llbracket{\varphi^{\prime}}\rrbracket({s})>p$
and $\llbracket{\varphi^{\prime}}\rrbracket({t})\leq p$, then
$|\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})|=|\llbracket{\varphi^{\prime}}\rrbracket({s})-p|\leq|\llbracket{\varphi^{\prime}}\rrbracket({s})-\llbracket{\varphi^{\prime}}\rrbracket({t})|\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)$
by induction.

  * •

$\varphi\equiv\varphi_{1}\land\varphi_{2}$. Without loss of generality we
assume that
$\llbracket{\varphi}\rrbracket({s})\geq\llbracket{\varphi}\rrbracket({t})$.
There are two possibilities:

    * –

If
$\llbracket{\varphi_{1}}\rrbracket({t})\leq\llbracket{\varphi_{2}}\rrbracket({t})$,
then
$\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})\leq\llbracket{\varphi_{1}}\rrbracket({s})-\llbracket{\varphi_{1}}\rrbracket({t})\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)$,
where the last inequality holds by induction.

    * –

Symmetrically, if
$\llbracket{\varphi_{2}}\rrbracket({t})\leq\llbracket{\varphi_{1}}\rrbracket({t})$,
then
$\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})\leq\llbracket{\varphi_{2}}\rrbracket({s})-\llbracket{\varphi_{2}}\rrbracket({t})\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)$.

  * •

$\varphi\equiv\langle a\rangle\psi$. We consider the non-trivial case that
both $s$ and $t$ can perform action $a$. (If either of the two states cannot
perform action $a$, the expected result is straightforward.) Let $\Delta_{1}$
be the distribution such that $s\xrightarrow{\,{a}\,}\Delta_{1}$ and
$\llbracket{\langle
a\rangle\psi}\rrbracket({s})=\llbracket{\psi}\rrbracket({\Delta_{1}})$. Since
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$ is a state-based
bisimulation metric, by definition there exists some $\Delta_{2}$ such that
$t\xrightarrow{\,{a}\,}\Delta_{2}$ and
$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta_{1},\Delta_{2})\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)$.
Without loss of generality we assume that
$\llbracket{\varphi}\rrbracket({s})\geq\llbracket{\varphi}\rrbracket({t})$. It
follows that

$\begin{array}[]{rl}&\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})\\\
=&\llbracket{\psi}\rrbracket({\Delta_{1}})-\max_{s\xrightarrow{\,{a}\,}{\Delta^{\prime}}}\llbracket{\psi}\rrbracket({\Delta^{\prime}})\\\
\leq&\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})\\\
\leq&\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta_{1},\Delta_{2})\qquad\mbox{by
induction on $\psi$}\\\
\leq&\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)\end{array}$

Then we analyze the structure of $\psi$ in (2).

  * •

$\psi=\psi_{1}\land\psi_{2}$. Without loss of generality we assume that
$\llbracket{\psi}\rrbracket({\Delta_{1}})\geq\llbracket{\psi}\rrbracket({\Delta_{2}})$.
There are two possibilities:

    * –

If
$\llbracket{\psi_{1}}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{2}}\rrbracket({\Delta_{2}})$,
then
$\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{1}}\rrbracket({\Delta_{1}})-\llbracket{\psi_{1}}\rrbracket({\Delta_{2}})\leq\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta_{1},\Delta_{2})$,
where the last inequality holds by induction.

    * –

Symmetrically, if
$\llbracket{\psi_{2}}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{1}}\rrbracket({\Delta_{2}})$,
then
$\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{2}}\rrbracket({\Delta_{1}})-\llbracket{\psi_{2}}\rrbracket({\Delta_{2}})\leq\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta_{1},\Delta_{2})$.

  * •

$\psi=\psi^{\prime}\ominus p$ for some $p$ in $[0,1]$. There are four subcases
and we consider one of them. Suppose
$\llbracket{\psi^{\prime}}\rrbracket({\Delta_{1}})>p$ and
$\llbracket{\psi^{\prime}}\rrbracket({\Delta_{2}})\leq p$, then
$|\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})|=|\llbracket{\psi^{\prime}}\rrbracket({\Delta_{1}})-p|\leq|\llbracket{\psi^{\prime}}\rrbracket({\Delta_{1}})-\llbracket{\psi^{\prime}}\rrbracket({\Delta_{2}})|\leq\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta_{1},\Delta_{2})$
by induction.

  * •

$\psi=[\varphi]$ for some
$\varphi\in\operatorname{\operatorname{\mathcal{L}}^{S}}$. Without loss of
generality we assume that
$\llbracket{\varphi}\rrbracket({s})\geq\llbracket{\varphi}\rrbracket({t})$. We
infer that

$\begin{array}[]{ll}&\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})\\\
=&\llbracket{[\varphi]}\rrbracket({\Delta_{1}})-\llbracket{[\varphi]}\rrbracket({\Delta_{2}})\\\
=&\sum_{u\in
S}(\Delta_{1}(u)-\Delta_{2}(u))\llbracket{\varphi}\rrbracket({u})\\\
\leq&\max\\{\sum_{u\in S}(\Delta_{1}(u)-\Delta_{2}(u))x_{u}\mid
x_{u},x_{u^{\prime}}\in[0,1]\land
x_{u}-x_{u^{\prime}}\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(u,u^{\prime})\\}\\\
=&\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})(\Delta_{1},\Delta_{2})\end{array}$

where the last equality holds because of the Kantorovich-Rubinstein duality
theorem [KR58, vBW01a] and the last inequality holds because for any states
$u,u^{\prime}\in S$ we have
$\llbracket{\varphi}\rrbracket({u}),\llbracket{\varphi}\rrbracket({u^{\prime}})\in[0,1]$
and
$|\llbracket{\varphi}\rrbracket({u})-\llbracket{\varphi}\rrbracket({u^{\prime}})|\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(u,u^{\prime})$
by induction on $\varphi$.

######  Lemma 2.

$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}})\sqsubseteq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ld}}$

###### Proof.

Let $\Delta_{1},\Delta_{2}$ be any two distributions in
$\operatorname{\operatorname{\mathcal{L}}^{D}}$. We show that

$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}})(\Delta_{1},\Delta_{2})~{}\leq~{}\sup_{\psi\in\operatorname{\operatorname{\mathcal{L}}^{D}}}|\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})|,$

using an idea inspired by [DJGP02]. Let $L(\Delta_{1},\Delta_{2})$ be the
optimal value of the following linear program

$\begin{array}[]{rl}\max\sum_{s\in S}(\Delta_{1}(s)-\Delta_{2}(s))x_{s},\text{
subject to }&0\leq x_{s}\leq 1\\\ &\forall s,t\in S\colon\
x_{s}-x_{t}\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)\end{array}$

Suppose $\\{k_{s}\\}_{s\in S}$ be a set of real numbers that maximizes the
above linear program to reach $L(\Delta_{1},\Delta_{2})$. Let
$e=\min\\{1-k_{t}\mid k_{t}<1\mbox{ and }t\in S\\}$ and $\epsilon>0$ be any
positive real number smaller than $e$. Hence, if $t\in S$ and $k_{t}<1$ then

$k_{t}+\epsilon<1.$ (1)

We construct some formula $\psi$ such that

$L(\Delta_{1},\Delta_{2})-\epsilon~{}<~{}\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}}).$
(2)

For any $s,t\in S$, we distinguish two cases:

  1. 1.

If $k_{s}>k_{t}$, then
$0<k_{s}-k_{t}\leq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)$.
It is easy to see that there exists some formula $\varphi_{st}$ such that

$k_{s}-k_{t}<\llbracket{\varphi_{st}}\rrbracket({s})-\llbracket{\varphi_{st}}\rrbracket({t})+\epsilon.$
(3)

or equivalently
$\llbracket{\varphi_{st}}\rrbracket({t})-\llbracket{\varphi_{st}}\rrbracket({s})+k_{s}<k_{t}+\epsilon$.
We define a new formula

$\varphi^{\prime}_{st}\;=\;\left\\{\begin{array}[]{ll}\varphi_{st}\ominus(\llbracket{\varphi_{st}}\rrbracket({s})-k_{s})&\mbox{if
$\llbracket{\varphi_{st}}\rrbracket({s})>k_{s}$}\\\
\varphi_{st}\oplus(k_{s}-\llbracket{\varphi_{st}}\rrbracket({s}))&\mbox{otherwise.}\end{array}\right.$

Let us compare $\varphi^{\prime}_{st}$ with $k_{t}$.

    1. (a)

If $\llbracket{\varphi_{st}}\rrbracket({s})>k_{s}$, then

$\begin{array}[]{rcl}\llbracket{\varphi^{\prime}_{st}}\rrbracket({t})&=&\max(\llbracket{\varphi_{st}}\rrbracket({t})-\llbracket{\varphi_{st}}\rrbracket({s})+k_{s},0)\\\
&<&\max(k_{t}+\epsilon,0)\qquad\mbox{by (\ref{eq:ks})}\\\
&=&k_{t}+\epsilon\end{array}$

    2. (b)

Otherwise,
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({t})=\min(\llbracket{\varphi_{st}}\rrbracket({t})+k_{s}-\llbracket{\varphi_{st}}\rrbracket({s}),1)$.
By (3) we infer that
$\llbracket{\varphi_{st}}\rrbracket({t})+k_{s}-\llbracket{\varphi_{st}}\rrbracket({s})<k_{t}+\epsilon$.
Since $k_{t}<k_{s}\leq 1$ we infer by (1) that $k_{t}+\epsilon<1$ and thus
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({t})<k_{t}+\epsilon$.

In both (a) and (b) we have
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({t})<k_{t}+\epsilon$, and it is
also easy to see that
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({s})=k_{s}$.

  2. 2.

If $k_{s}\leq k_{t}$, then we simply set $\varphi^{\prime}_{st}$ to be the
formula $\underline{k_{s}}$. As in the last case, we have
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({s})=k_{s}$ and
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({t})=k_{s}\leq
k_{t}<k_{t}+\epsilon$.

In summary, the above reasoning says that for any $s,t\in S$ we can construct
a formula $\varphi^{\prime}_{st}$ such that
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({s})=k_{s}$ and
$\llbracket{\varphi^{\prime}_{st}}\rrbracket({t})<k_{t}+\epsilon$. Now let us
define $\varphi^{\prime}_{s}=\bigwedge_{t\in S}\varphi^{\prime}_{st}$. It is
easy to see that $\llbracket{\varphi^{\prime}_{s}}\rrbracket({s})=k_{s}$ and
$\llbracket{\varphi^{\prime}_{s}}\rrbracket({t})<k_{t}+\epsilon$ for all $t\in
S$. The latter implies
$\max\\{\llbracket{\varphi^{\prime}_{s}}\rrbracket({t})\mid s,t\in
S\\}<k_{t}+\epsilon$. Then define $\varphi=\bigvee_{s\in
S}\varphi^{\prime}_{s}$. For all $t\in S$, we have

$k_{t}~{}=~{}\llbracket{\varphi^{\prime}_{t}}\rrbracket({t})~{}\leq~{}\llbracket{\varphi}\rrbracket({t})~{}=~{}\max\\{\llbracket{\varphi^{\prime}_{s}}\rrbracket({t})\mid
s,t\in S\\}~{}<~{}k_{t}+\epsilon.$

Finally, we define $\psi=[\varphi]$. It follows that

$\begin{array}[]{rcl}\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})&=&\llbracket{[\varphi]}\rrbracket({\Delta_{1}})-\llbracket{[\varphi]}\rrbracket({\Delta_{2}})\\\
&=&\sum_{t\in
S}\Delta_{1}(t)\cdot\llbracket{\varphi}\rrbracket({t})-\sum_{t\in
S}\Delta_{2}(t))\cdot\llbracket{\varphi}\rrbracket({t})\\\ &\geq&\sum_{t\in
S}\Delta_{1}(t)\cdot k_{t}-\sum_{t\in
S}\Delta_{2}(t))\cdot\llbracket{\varphi}\rrbracket({t})\\\ &>&\sum_{t\in
S}\Delta_{1}(t)\cdot k_{t}-\sum_{t\in S}\Delta_{2}(t))\cdot(k_{t}+\epsilon)\\\
&=&\sum_{t\in S}(\Delta_{1}(t)-\Delta_{2}(t))\cdot k_{t}-\sum_{t\in
S}\Delta_{2}(t)\cdot\epsilon\\\
&=&L(\Delta_{1},\Delta_{2})-\epsilon\end{array}$

as required.

The above property will be used to prove the following lemma.

######  Lemma 3.

$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}\sqsubseteq\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}$

###### Proof.

We show that $\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}$ is
a state-based bisimulation metric. Let $s,t$ be any two states in $S$ and
$\epsilon$ be any real number in the interval $[0,1)$ with
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)\leq\epsilon$.
Assume that $s\xrightarrow{\,{a}\,}\Delta_{1}$ is an arbitrarily chosen
transition from $s$. Then state $t$ must be able to perform action $a$ too.
Otherwise it is easy to see that
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)=1>\epsilon$,
which contradicts our assumption above. We need to show that there exists some
transition $t\xrightarrow{\,{a}\,}\Delta_{2}$ with
$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}})(\Delta_{1},\Delta_{2})\leq\epsilon$.
Suppose for a contradiction that no $a$-transition from $t$ satisfies this
condition. In other words, for each $\Delta^{i}_{2}$ with
$t\xrightarrow{\,{a}\,}\Delta^{i}_{2}$ we have
$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}})(\Delta_{1},\Delta^{i}_{2})>\epsilon$.
By Lemma 2, this means
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ld}}(\Delta_{1},\Delta^{i}_{2})>\epsilon$.
Then there must exist some formula
$\psi^{i}_{2}\in\operatorname{\operatorname{\mathcal{L}}^{D}}$ such that
$|\llbracket{\psi^{i}_{2}}\rrbracket({\Delta_{1}})-\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})|>\epsilon$.
Furthermore, we can strengthen this condition to the following one

$\llbracket{\psi^{i}_{2}}\rrbracket({\Delta_{1}})-\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})>\epsilon$
(4)

because we can take the formula $\lnot\psi^{i}_{2}$ in place of $\psi^{i}_{2}$
in the case that
$\llbracket{\psi^{i}_{2}}\rrbracket({\Delta_{1}})<\llbracket{\psi^{i}_{2}}\rrbracket({\Delta_{2}})$.
Let $\varphi=\langle
a\rangle\bigwedge_{i}(\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}}))$.
We infer that

$\begin{array}[]{rcl}\llbracket{\varphi}\rrbracket({s})&=&\max_{s\xrightarrow{\,{a}\,}\Delta}\llbracket{\bigwedge_{i}\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})}\rrbracket({\Delta})\\\
&\geq&\llbracket{\bigwedge_{i}(\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}}))}\rrbracket({\Delta_{1}})\\\
&=&\min_{i}\llbracket{\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})}\rrbracket({\Delta_{1}})\\\
&=&\llbracket{\psi^{k}_{2}\ominus\llbracket{\psi^{k}_{2}}\rrbracket({\Delta^{k}_{2}})}\rrbracket({\Delta_{1}})\qquad\text{for
some $k$}\\\
&=&\max(\llbracket{\psi^{k}_{2}}\rrbracket({\Delta_{1}})-\llbracket{\psi^{k}_{2}}\rrbracket({\Delta^{k}_{2}}),~{}0)\\\
&>&\epsilon\qquad\mbox{by (\ref{eq:psii})}\end{array}$

On the other hand, we have

$\begin{array}[]{rcl}\llbracket{\varphi}\rrbracket({t})&=&\max_{t\xrightarrow{\,{a}\,}\Delta^{i}_{2}}\llbracket{\bigwedge_{j}(\psi^{j}_{2}\ominus\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{j}_{2}}))}\rrbracket({\Delta^{i}_{2}})\\\
&=&\max_{t\xrightarrow{\,{a}\,}\Delta^{i}_{2}}\min_{j}\llbracket{\psi^{j}_{2}\ominus\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{j}_{2}})}\rrbracket({\Delta^{i}_{2}})\\\
&=&\max_{t\xrightarrow{\,{a}\,}\Delta^{i}_{2}}\min_{j}\max((\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{i}_{2}})-\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{j}_{2}})),~{}0)\\\
&=&0\end{array}$

It follows that
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}(s,t)\geq\llbracket{\varphi}\rrbracket({s})-\llbracket{\varphi}\rrbracket({t})>\epsilon$,
which gives rise to a contradiction.

By combining the above three technical lemmas we obtain the following logical
characterisation of the state-based bisimilairty metric.

######  Theorem 3.1.

$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}=\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ls}}$
and
$\operatorname{\mathit{K}}(\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}})=\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}^{ld}}$

######  Remark 1.

In the proof of Lemma 3 we have constructed the formula

$\varphi=\langle
a\rangle\bigwedge_{i}(\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}}))$
(5)

by making use of conjunction and minus connectives for distribution formulae.
This happens because in the presence of non-determinism state $t$ may perform
action $a$ and then evolves into one of successor distributions
$\Delta^{i}_{2}$. If we confine ourselves to deterministic pLTSs, then state
$t$ will have a unique successor distribution $\Delta^{i}_{2}$ and therefore
(5) can be simplified as $\varphi=\langle a\rangle\psi^{i}_{2}$. In this case,
there is no need of conjunction and minus connectives for distribution
formulae. Furthermore, if we fold $[\varphi]$ into state formulae in
Definition 3, distribution formulae can be completely dropped. In other words,
for deterministic pLTSs, the state-based bisimilarity metric can be
characterised by the following metric logic

$\varphi::=\top\ |\ \lnot\varphi\ |\ \varphi\ominus p\ |\
\varphi_{1}\land\varphi_{2}\ |\ \langle a\rangle\varphi$ (6)

Therefore, for deterministic pLTSs, the two-sorted logic in Definition 3
degenerates into the logic considered in [DGJP04, vBW05], as expected.

In [DAMRS08, CDAMR10] a bisimulation metric for game structures is
characterised by a quantitative $\mu$-calculus where formulae are valuated
also on states and no distribution formula is needed. This is not surprising
because games are deterministic: at any state $s$, if two players have chosen
their moves, say $a_{1}$ and $a_{2}$, then there is a unique distribution
$\delta(s,a_{1},a_{2})$ to determine the probabilities of arriving at a set of
destination states.

##  4 Distribution-Based Bisimulation Metric

The bisimilarity metric given in Definition 2 measures the distance between
two states. Alternatively, it is possible to directly define a metric that
measures subdistributions. In order to do so, we first define a transition
relation between subdistributions.

######  Definition 5.

We write $\Delta\xrightarrow{\,{a}\,}\Delta^{\prime}$ if
$\Delta^{\prime}=\sum_{s\in\lceil{\Delta}\rceil}\Delta(s)\cdot\Delta_{s}$,
where $\Delta_{s}$ is determined as follows:

  * •

either $s\xrightarrow{\,{a}\,}\Delta_{s}$

  * •

or there is no $\Theta$ with $s\xrightarrow{\,{a}\,}\Theta$, and in this case
we set $\Delta_{s}=\mathop{\varepsilon}$.

Note that if $\Delta\xrightarrow{\,{a}\,}\Delta^{\prime}$ then some (not
necessarily all) states in the support of $\Delta$ can perform action $a$. For
example, consider the two states $s_{2}$ and $s_{3}$ in Figure 1. Since
$s_{2}\xrightarrow{\,{c}\,}\overline{s_{4}}$ and $s_{3}$ cannot perform action
$c$, the distribution
$\Delta=\frac{1}{2}\overline{s_{2}}+\frac{1}{2}\overline{s_{3}}$ can make the
transition $\Delta\xrightarrow{\,{c}\,}\frac{1}{2}\overline{s_{4}}$ to reach
the subdistribution $\frac{1}{2}\overline{s_{4}}$.

######  Definition 6.

A $1$-bounded pseudometric $d$ on $\mathop{\mbox{$\mathcal{D}$}}({S})$ is a
_distribution-based bisimulation metric_ if
$|\;|\Delta_{1}|-|\Delta_{2}|\;|\leq d(\Delta_{1},\Delta_{2})$ and for all
$\Delta_{1},\Delta_{2}\in\mathop{\mbox{$\mathcal{D}$}}({S})$ and
$\epsilon\in[0,1)$ with $d(\Delta_{1},\Delta_{2})\leq\epsilon$, if
$\Delta_{1}\xrightarrow{\,{a}\,}\Delta^{\prime}_{1}$ then there exists an
$\Delta_{2}\xrightarrow{\,{a}\,}\Delta^{\prime}_{2}$ with
$d(\Delta^{\prime}_{1},\Delta^{\prime}_{2})\leq\epsilon$.

The smallest (wrt. $\sqsubseteq$) distribution-based bisimulation metric,
notation $\operatorname{\operatorname{\mathbf{d}}_{\it db}}$, is called
_distribution-based bisimilarity metric_. Distribution-based bisimilarity
[DFD15] is the kernel of the distribution-based bisimilarity metric.

It is not difficult to see that
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$ is different from
$\operatorname{\operatorname{\mathbf{d}}_{\it db}}$, as witnessed by the
following example.

######  Example 4.

Consider the states in Figure 1. We first observe that
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\overline{s_{2}},\overline{t_{3}})=0$ because $s_{2}$ and $t_{3}$ can
match each other’s action exactly. Similarly, we have
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\overline{s_{3}},\overline{t_{4}})=0$. Then it is easy to see that
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\frac{1}{2}\overline{s_{2}}+\frac{1}{2}\overline{s_{3}},\frac{1}{2}\overline{t_{3}}+\frac{1}{2}\overline{t_{4}})=0$.
Since
$s_{1}\xrightarrow{\,{b}\,}\frac{1}{2}\overline{s_{2}}+\frac{1}{2}\overline{s_{3}}$
and $\frac{1}{2}\overline{t_{1}}+\frac{1}{2}\overline{t_{2}}$, we infer that
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\overline{s_{1}},\frac{1}{2}\overline{t_{1}}+\frac{1}{2}\overline{t_{2}})=0$.
It, in turn, implies $\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\overline{s},\overline{t})=0$. We have already seen in Example 1 that
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}(s,t)=\frac{1}{2}$.
Therefore, the two distance functions
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{sb}}}$ and
$\operatorname{\operatorname{\mathbf{d}}_{\it db}}$ are indeed different.

The rest of this section is devoted to a logical characterisation of
$\operatorname{\operatorname{\mathbf{d}}_{\it db}}$. Consider the metric logic
$\operatorname{\mathcal{L}}^{D*}$ whose formulae are defined below

$\psi::=\top\ |\ \lnot\psi\ |\ \psi\ominus p\ |\ \psi_{1}\land\psi_{2}\ |\
\langle a\rangle\psi$ (7)

This logic is the same as that defined in (6) except that now we only have
distribution formulae. We will show that this logic can capture the
distribution-based bisimilarity metric.

######  Definition 7.

A formula $\psi\in\operatorname{\mathcal{L}}^{D*}$ evaluates in
$\Delta\in\mathop{\mbox{$\mathcal{D}$}}({S})$ as follows:

  * $\displaystyle\llbracket{\top}\rrbracket({\Delta})=|\Delta|$,

  * $\displaystyle\llbracket{\lnot\psi}\rrbracket({\Delta})=1-\llbracket{\psi}\rrbracket({\psi})$,

  * $\displaystyle\llbracket{\psi\ominus p}\rrbracket({\Delta})=\max(\llbracket{\psi}\rrbracket({\psi})-p,~{}0)$,

  * $\displaystyle\llbracket{\psi_{1}\land\psi_{2}}\rrbracket({\Delta})=\min(\llbracket{\psi_{1}}\rrbracket({\Delta}),\llbracket{\psi_{2}}\rrbracket({\Delta}))$,

  * $\displaystyle\llbracket{\langle a\rangle\psi}\rrbracket({\Delta})=\max_{\Delta\xrightarrow{\,{a}\,}\Delta^{\prime}}\llbracket{\psi}\rrbracket({\Delta^{\prime}})$,

This induces a natural logical metric
$\operatorname{\operatorname{\mathbf{d}}_{\it db}^{ld}}$ over subdistributions
defined by

$\operatorname{\operatorname{\mathbf{d}}_{\it
db}^{ld}}(\Delta,\Theta)=\sup_{\psi\in\operatorname{\mathcal{L}}^{D}}|[\\![\psi]\\!](\Delta)-[\\![\psi]\\!](\Theta)|$

It turns out that $\operatorname{\operatorname{\mathbf{d}}_{\it db}^{ld}}$
coincides with $\operatorname{\operatorname{\mathbf{d}}_{\it db}}$. We split
the proof of this coincidence result into two parts, to show that one metric
is dominated by the other and vice versa.

######  Lemma 4.

$\operatorname{\operatorname{\mathbf{d}}_{\it
db}^{ld}}\sqsubseteq\operatorname{\operatorname{\mathbf{d}}_{\it db}}$

###### Proof.

Similar to the proof of Lemma 1. We proceed by structural induction on
formulae. For any two subdistributions
$\Delta_{1},\Delta_{2}\in\mathop{\mbox{$\mathcal{D}$}}({S})$, we prove that

$|\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})|\leq\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})$

for all $\psi\in\operatorname{\mathcal{L}}^{D*}$.

We first analyze the structure of $\psi$.

  * •

$\varphi\equiv\top$. Then it is trivial to see that
$|\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})|=|\,|\Delta_{1}|-|\Delta_{2}|\,|\leq\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})$.

  * •

$\psi\equiv\lnot\psi^{\prime}$. Then
$|\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})|=|\llbracket{\psi^{\prime}}\rrbracket({\Delta_{2}})-\llbracket{\psi^{\prime}}\rrbracket({\Delta_{1}})|\leq\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})$ where the inequality holds by induction.

  * •

$\psi\equiv\psi^{\prime}\ominus p$. There are four subcases and we consider
one of them. Suppose $\llbracket{\psi^{\prime}}\rrbracket({\Delta_{1}})>p$ and
$\llbracket{\psi^{\prime}}\rrbracket({\Delta_{2}})\leq p$, then
$|\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})|=|\llbracket{\psi^{\prime}}\rrbracket({\Delta_{1}})-p|\leq|\llbracket{\psi^{\prime}}\rrbracket({\Delta_{1}})-\llbracket{\psi^{\prime}}\rrbracket({\Delta_{2}})|\leq\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})$ by induction.

  * •

$\psi\equiv\psi_{1}\land\psi_{2}$. Without loss of generality we assume that
$\llbracket{\psi}\rrbracket({\Delta_{1}})\geq\llbracket{\psi}\rrbracket({\Delta_{2}})$.
There are two possibilities:

    * –

If
$\llbracket{\psi_{1}}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{2}}\rrbracket({\Delta_{2}})$,
then
$\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{1}}\rrbracket({\Delta_{1}})-\llbracket{\psi_{1}}\rrbracket({\Delta_{2}})\leq\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})$, where the last inequality holds by induction.

    * –

Symmetrically, if
$\llbracket{\psi_{2}}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{1}}\rrbracket({\Delta_{2}})$,
then
$\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})\leq\llbracket{\psi_{2}}\rrbracket({\Delta_{1}})-\llbracket{\psi_{2}}\rrbracket({\Delta_{2}})\leq\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})$.

  * •

$\psi\equiv\langle a\rangle\psi^{\prime}$. Let $\Delta^{\prime}_{1}$ be the
distribution such that $\Delta_{1}\xrightarrow{\,{a}\,}\Delta^{\prime}_{1}$
and $\llbracket{\langle
a\rangle\psi^{\prime}}\rrbracket({\Delta_{1}})=\llbracket{\psi^{\prime}}\rrbracket({\Delta^{\prime}_{1}})$.
Since $\operatorname{\operatorname{\mathbf{d}}_{\it db}}$ is a distribution-
based bisimulation metric, by definition there exists some
$\Delta^{\prime}_{2}$ such that
$\Delta_{2}\xrightarrow{\,{a}\,}\Delta^{\prime}_{2}$ and
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta^{\prime}_{1},\Delta^{\prime}_{2})\leq\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})$. Without loss of generality we assume that
$\llbracket{\psi}\rrbracket({\Delta_{1}})\geq\llbracket{\psi}\rrbracket({\Delta_{2}})$.
It follows that

$\begin{array}[]{rl}&\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})\\\
=&\llbracket{\psi^{\prime}}\rrbracket({\Delta^{\prime}_{1}})-\max_{\Delta_{2}\xrightarrow{\,{a}\,}{\Delta^{\prime\prime}_{2}}}\llbracket{\psi^{\prime}}\rrbracket({\Delta^{\prime\prime}_{2}})\\\
\leq&\llbracket{\psi^{\prime}}\rrbracket({\Delta^{\prime}_{1}})-\llbracket{\psi^{\prime}}\rrbracket({\Delta^{\prime}_{2}})\\\
\leq&\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta^{\prime}_{1},\Delta^{\prime}_{2})\qquad\mbox{by induction on
$\psi^{\prime}$}\\\ \leq&\operatorname{\operatorname{\mathbf{d}}_{\it
db}}(\Delta_{1},\Delta_{2})\end{array}$

######  Lemma 5.

$\operatorname{\operatorname{\mathbf{d}}_{\it
db}}\sqsubseteq\operatorname{\operatorname{\mathbf{d}}_{\it db}^{ld}}$

###### Proof.

Similar to the proof of Lemma 3. We show that
$\operatorname{\operatorname{\mathbf{d}}_{\it db}^{ld}}$ is a distribution-
based bisimulation metric. Let $\Delta_{1},\Delta_{2}$ be any two
subdistributions in $\mathop{\mbox{$\mathcal{D}$}}({S})$ and $\epsilon$ be any
real number in the interval $[0,1)$ with
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}^{ld}}(\Delta_{1},\Delta_{2})\leq\epsilon$. Assume that
$\Delta_{1}\xrightarrow{\,{a}\,}\Delta^{\prime}_{1}$ is an arbitrarily chosen
transition from $\Delta_{1}$. We need to show that there exists some
transition $\Delta_{2}\xrightarrow{\,{a}\,}\Delta^{\prime}_{2}$ with
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}^{ld}}(\Delta^{\prime}_{1},\Delta^{\prime}_{2})\leq\epsilon$. Suppose for a
contradiction that no $a$-transition from $\Delta_{2}$ satisfies this
condition. In other words, for each $\Delta^{i}_{2}$ with
$\Delta_{2}\xrightarrow{\,{a}\,}\Delta^{i}_{2}$ we have
$\operatorname{\operatorname{\mathbf{d}}_{\it
db}^{ld}}(\Delta^{\prime}_{1},\Delta^{i}_{2})>\epsilon$. Then there must exist
some formula $\psi^{i}_{2}\in\operatorname{\operatorname{\mathcal{L}}^{D}}$
such that
$|\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{\prime}_{1}})-\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})|>\epsilon$.
Furthermore, we can strengthen this condition to the following one

$\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{\prime}_{1}})-\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})>\epsilon$
(8)

because we can take the formula $\lnot\psi^{i}_{2}$ in place of $\psi^{i}_{2}$
in the case that
$\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{\prime}_{1}})<\llbracket{\psi^{i}_{2}}\rrbracket({\Delta_{2}})$.
Let $\varphi=\langle
a\rangle\bigwedge_{i}(\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}}))$.
We infer that

$\begin{array}[]{rcl}\llbracket{\varphi}\rrbracket({\Delta_{1}})&=&\max_{\Delta_{1}\xrightarrow{\,{a}\,}\Delta}\llbracket{\bigwedge_{i}\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})}\rrbracket({\Delta})\\\
&\geq&\llbracket{\bigwedge_{i}(\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}}))}\rrbracket({\Delta^{\prime}_{1}})\\\
&=&\min_{i}\llbracket{\psi^{i}_{2}\ominus\llbracket{\psi^{i}_{2}}\rrbracket({\Delta^{i}_{2}})}\rrbracket({\Delta^{\prime}_{1}})\\\
&=&\llbracket{\psi^{k}_{2}\ominus\llbracket{\psi^{k}_{2}}\rrbracket({\Delta^{k}_{2}})}\rrbracket({\Delta^{\prime}_{1}})\qquad\text{for
some $k$}\\\
&=&\max(\llbracket{\psi^{k}_{2}}\rrbracket({\Delta^{\prime}_{1}})-\llbracket{\psi^{k}_{2}}\rrbracket({\Delta^{k}_{2}}),~{}0)\\\
&>&\epsilon\qquad\mbox{by (\ref{eq:psii1})}\end{array}$

On the other hand, we have

$\begin{array}[]{rcl}\llbracket{\psi}\rrbracket({\Delta_{2}})&=&\max_{\Delta_{2}\xrightarrow{\,{a}\,}\Delta^{i}_{2}}\llbracket{\bigwedge_{j}(\psi^{j}_{2}\ominus\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{j}_{2}}))}\rrbracket({\Delta^{i}_{2}})\\\
&=&\max_{\Delta_{2}\xrightarrow{\,{a}\,}\Delta^{i}_{2}}\min_{j}\llbracket{\psi^{j}_{2}\ominus\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{j}_{2}})}\rrbracket({\Delta^{i}_{2}})\\\
&=&\max_{\Delta_{2}\xrightarrow{\,{a}\,}\Delta^{i}_{2}}\min_{j}\max((\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{i}_{2}})-\llbracket{\psi^{j}_{2}}\rrbracket({\Delta^{j}_{2}})),~{}0)\\\
&=&0\end{array}$

It follows that $\operatorname{\operatorname{\mathbf{d}}_{\it
db}^{ld}}(\Delta_{1},\Delta_{2})\geq\llbracket{\psi}\rrbracket({\Delta_{1}})-\llbracket{\psi}\rrbracket({\Delta_{2}})>\epsilon$,
which gives rise to a contradiction.

By combining the previous two lemmas, we arrive at the following logical
characterisation of the distribution-based bisimulation metric.

######  Theorem 4.1.

$\operatorname{\operatorname{\mathbf{d}}_{\it
db}}=\operatorname{\operatorname{\mathbf{d}}_{\it db}^{ld}}$

##  5 Related work

Metrics for probabilistic transition systems are first suggested by Giacalone
et al. to formalize a notion of distance between processes. They are used also
in [KN96, Nor97] to give denotational semantics for reactive models. De Vink
and Rutten [dVR99] show that discrete probabilistic transition systems can be
viewed as coalgebras. They consider the category of complete ultrametric
spaces. Similar ultrametric spaces are considered by den Hartog in [dH02].

Metrics for deterministic systems are extensively studied. Desharnais et al.
[DGJP04] propose a logical pseudometric for labelled Markov chains, which is a
reactive model of probabilistic systems. A similar pseudometric is defined by
van Breugel and Worrell [vBW01b] via the terminal coalgebra of a functor based
on a metric on the space of Borel probability measures. The metric of [DGJP04,
vBW05] works for continuous probabilistic transition systems, while in this
work we concentrate on discrete systems. Interestingly, van Breugel and
Worrell [vBW01a] also present a polynomial-time algorithm to approximate their
coalgebraic distances. Furthermore, van Breugel _et al._ propose an algorithm
to approximate a behavioural pseudometric without discount [vBSW08]. In
[FPP11] a sampling algorithm for calculating bisimulation distances in Markov
decision processes is shown to have good performance. In [DAMRS07, DAMRS08]
the probabilistic bisimulation metric on game structures is characterised by a
quantitative $\mu$-caluclus. Algorithms for game metrics are proposed in
[CDAMR10, Ram10].

Metrics for nondeterministic probabilistic systems are considered in [DJGP02],
where Desharnais et al. deal with labelled concurrent Markov chains (similar
to pLTSs, this model can be captured by the simple probabilistic automata of
[Seg95]). They show that the greatest fixed point of a monotonic function on
pseudometrics corresponds to the weak probabilistic bisimilarity of [PLS00].

In [SDC07] a notion of trace metric is proposed for pLTSs and a tool is
developed to compute the trace metric. In [DCPP06] a notion of bisimulation
metric is proposed that extends the approach of [DJGP02, DGJP04] to a more
general framework called action-labelled quantitative transition systems.

In [DAFS09] de Alfaro _et al._ consider metric transition systems in which the
propositions at each state are interpreted as elements of metric spaces. In
that setting, trace equivalence and bisimulation give rise to linear and
branching distances that can be characterised by quantitative versions of
linear-time temporal logic [MP91] and $\mu$-calculus [Koz83].

In [Yin02] Ying proposes a notion of bisimulation index for the usual labelled
transition systems, by using ultrametrics on actions instead of using
pseudometrics on states. He applies bisimulation indexes on timed CCS and real
time ACP. But the deeper connection between [Yin02] and our work worths some
further studies.

In [GLT15] a notion of uniform continuity is proposed to be an appropriate
property of probabilistic processes for compositional reasoning with respect
to bisimulation metric semantics.

##  6 Concluding remarks

We have considered two behavioural pseudometrics for probabilistic labelled
transition systems where nondeterminism and probabilities co-exist. They
correspond to state-based and distribution-based bisimulations. Our modal
characterisation of the state-based bisimulation metric is much simpler than
an earlier proposal by Desharnais _et al._ since we only use two non-expansive
operators, negation and testing, rather than the general class of non-
expansive operators. Our modal characterisaton of the distribution-based
bisimulation metric is new. The characterisations are shown to be sound and
complete.

In the current work we have not distinguished internal actions from external
ones. But it is not difficult to make the distinction and abstract away
internal actions so as to introduce weak versions of bisimulation metrics. In
a finite-state and finitely branching pLTS, the subdistributions reachable
from a state by weak transitions is infinite but can be represented by the
convex closure of a finite set [Den15]. This entails that the logical
characterisation of weak bisimulation metrics would be similar to those
presented here.

## References

  * [CDAMR10] Krishnendu Chatterjee, Luca De Alfaro, Rupak Majumdar, and Vishwanath Raman.  Algorithms for game metrics.  Logical Methods in Computer Science, 6(3), 2010.
  * [DAFS09] Luca De Alfaro, Marco Faella, and Mariëlle Stoelinga.  Linear and branching system metrics.  IEEE Transactions on Software Engineering, 35(2):258–273, 2009\.
  * [DAMRS07] L. De Alfaro, R. Majumdar, V. Raman, and M. Stoelinga.  Game relations and metrics.  In Proc. LICS’07, pages 99–108. IEEE, 2007.
  * [DAMRS08] Luca De Alfaro, Rupak Majumdar, Vishwanath Raman, and Mariëlle Stoelinga.  Game refinement relations and metrics.  arXiv preprint arXiv:0806.4956, 2008.
  * [DCPP06] Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang.  Metrics for action-labelled quantitative transition systems.  ENTCS, 153(2):79–96, 2006.
  * [Den15] Yuxin Deng.  Semantics of Probabilistic Processes: An Operational Approach.  Springer, 2015.
  * [DFD15] Yuxin Deng, Yuan Feng, and Ugo Dal Lago.  On coinduction and quantum lambda calculi.  In Proceedings of the 26th International Conference on Concurrency Theory, pages 427–440. LIPICS, 2015.
  * [DGJP04] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled markov processes.  Theor. Comput. Sci., 318(3):323–354, 2004.
  * [dH02] J. I. den Hartog.  Probabilistic Extensions of Semantical Models.  PhD thesis, Free University Amsterdam, 2002.
  * [DJGP02] Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden.  The metric analogue of weak bisimulation for probabilistic processes.  In Proc. LICS’02, pages 413–422. IEEE, 2002.
  * [DTW10] Pedro R. D’Argenio, Pedro Sánchez Terraf, and Nicolás Wolovick.  Bisimulations for nondeterministic labeled markov processes.  CoRR, abs/1011.3362, 2010.
  * [dVR99] E. P. de Vink and J. J. M. M. Rutten.  Bisimulation for probabilistic transition systems: A coalgebraic approach.  Theoretical Computer Science, 221(1/2):271–293, 1999.
  * [FPP11] Norm Ferns, Prakash Panangaden, and Doina Precup.  Bisimulation metrics for continuous markov decision processes.  SIAM J. Comput., 40(6):1662–1714, 2011.
  * [FZ14] Yuan Feng and Lijun Zhang.  When equivalence and bisimulation join forces in probabilistic automata.  In Proceedings of the 19th International Symposium on Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 247–262. Springer, 2014.
  * [GLT15] Daniel Gebler, Kim Guldstrand Larsen, and Simone Tini.  Compositional metric reasoning with probabilistic process calculi.  In Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures, volume 9034 of Lecture Notes in Computer Science, pages 230–245. Springer, 2015.
  * [Hen12] Matthew Hennessy.  Exploring probabilistic bisimulations, part i.  Formal Aspects of Computing, 24(4-6):749–768, 2012.
  * [HKK14] Holger Hermanns, Jan Krcál, and Jan Kretínský.  Probabilistic bisimulation: Naturally on distributions.  In Proceedings of the 25th International Conference on Concurrency Theory, volume 8704 of Lecture Notes in Computer Science, pages 249–265. Springer, 2014.
  * [HM85] Matthew Hennessy and Robin Milner.  Algebraic laws for nondeterminism and concurrency.  J. ACM, 32:137–161, 1985.
  * [KN96] M. Z. Kwiatkowska and G. J. Norman.  Probabilistic metric semantics for a simple language with recursion.  In Proceedings of 21st International Symposium on Mathematical Foundations of Computer Science, volume 1113 of Lecture Notes in Computer Science, pages 419–430. Springer-Verlag, 1996.
  * [Koz83] D. Kozen.  Results on the propositional mu-calculus.  Theoretical Computer Science, 27:333–354, 1983.
  * [KR58] L.V. Kantorovich and G.S. Rubinshtein.  On a space of totally additive functions.  Vestn Len. Univ., 13(7):52–59, 1958.
  * [LS91] Kim G. Larsen and Arne Skou.  Bisimulation through probabilistic testing.  Inf. Comput., 94:1–28, 1991.
  * [MP91] Z. Manna and A. Pnueli.  The Temporal Logic of Reactive and Concurrent Systems: Specification.  Springer-Verlang, 1991.
  * [Nor97] G. J. Norman.  Metric Semantics for Reactive Probabilistic Systems.  PhD thesis, University of Birmingham, 1997.
  * [PLS00] Anna Philippou, Insup Lee, and Oleg Sokolsky.  Weak bisimulation for probabilistic systems.  In Proceedings of the 11th International Conference on Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 334–349. Springer-Verlag, 2000.
  * [Ram10] Vishwanath Raman.  Game Relations, Metrics and Refinements.  PhD thesis, University of California, 2010.
  * [SDC07] Lin Song, Yuxin Deng, and Xiaojuan Cai.  Towards automatic measurement of probabilistic processes.  In Proc. QSIC’07, pages 50–59. IEEE, 2007.
  * [Seg95] Roberto Segala.  Modeling and Verification of Randomized Distributed Real-Time Systems.  PhD thesis, MIT, 1995.
  * [vBSW08] Franck van Breugel, Babita Sharma, and James Worrell.  Approximating a behavioural pseudometric without discount for probabilistic systems.  Logical Methods in Computer Science, 4(2), 2008.
  * [vBW01a] Franck van Breugel and James Worrell.  An algorithm for quantitative verification of probabilistic transition systems.  In Proc. CONCUR’01, volume 2154 of LNCS, pages 336–350. Springer, 2001.
  * [vBW01b] Franck van Breugel and James Worrell.  Towards quantitative verification of probabilistic transition systems.  In Fernando Orejas, Paul Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, volume 2076 of LNCS, pages 421–432. Springer, 2001.
  * [vBW05] Franck van Breugel and James Worrell.  A behavioural pseudometric for probabilistic transition systems.  Theor. Comput. Sci., 331(1):115–142, 2005.
  * [Yin02] M. Ying.  Bisimulation indexes and their applications.  Theoretical Computer Science, 275(1/2):1–68, 2002.

##  Appendix 0.A Convex Bisimulation Metric

For $\Pi\subseteq\mathop{\mbox{$\mathcal{D}$}}({S})$ we denote by
$\operatorname{\mathit{cc}}(\Pi)$ the convex closure of $\Pi$. If
$\Delta\in\operatorname{\mathit{cc}}(\operatorname{\mathit{der}}(s,a))$ then
we say $\Delta$ is a combined transition of $s$ labelled by $a$, written as
$s\xrightarrow{\,{a}\,}_{c}\Delta$.

######  Definition 8 (Convex bisimulation metric).

A $1$-bounded metric $d$ on $S$ is a _convex bisimulation metric_ if for all
$s,t\in S$ and $\epsilon\in[0,1)$ with $d(s,t)\leq\epsilon$, if
$s\xrightarrow{\,{a}\,}\Delta$ then there exists a
$\Delta^{\prime}\in\operatorname{\mathit{cc}}(\operatorname{\mathit{der}}(t,a))$
such that $\operatorname{\mathit{K}}(d)(\Delta,\Delta^{\prime})\leq\epsilon$.

The smallest (wrt. $\sqsubseteq$) convex bisimulation metric, denoted by
$\operatorname{\operatorname{\mathbf{d}}_{\mathit{cb}}}$, is called _convex
bisimilarity metric_. Convex bisimilarity equivalence (also called
probablistic bisimilarity) [Seg95] is the kernel of the convex bisimilarity
metric.

Let us define the functor
$\operatorname{\operatorname{\mathit{F}}_{\mathit{cb}}}\colon[0,1]^{S\times
S}\to[0,1]^{S\times S}$ for $d\colon S\times S\to[0,1]$ and $s,t\in S$ by

$\operatorname{\operatorname{\mathit{F}}_{\mathit{cb}}}(d)(s,t)=\sup_{a\in
A}\\{\operatorname{\mathit{H}}(\operatorname{\mathit{K}}(d))(\operatorname{\mathit{cc}}(\operatorname{\mathit{der}}(s,a)),\operatorname{\mathit{cc}}(\operatorname{\mathit{der}}(t,a)))\\}\,.$

It can be shown that $\operatorname{\operatorname{\mathit{F}}_{\mathit{cb}}}$
is monotone and its least fixed point is the convex bisimilarity metric.

Given a pLTS, we can saturate it with all possible combined transitions. In
the saturated pLTS, convex bisimulation metric coincides with state-based
bisimulation metric because of the following lemma.

######  Lemma 6.

$d$ is a convex bisimulation metric if and only if for all $s,t\in S$ and
$\epsilon\in[0,1)$ with $d(s,t)\leq\epsilon$, if
$s\xrightarrow{\,{a}\,}_{c}\Delta$ then there exists some
$t\xrightarrow{\,{a}\,}_{c}\Delta^{\prime}$ such that
$\operatorname{\mathit{K}}(d)(\Delta,\Delta^{\prime})\leq\epsilon$.

###### Proof.

The “if” direction is trivial. The “only if” direction can be shown by making
use of the following inequality:

$\operatorname{\mathit{K}}(d)(\sum_{i\in I}p_{i}\cdot\Delta_{i},\sum_{i\in
I}p_{i}\cdot\Delta^{\prime}_{i})~{}\leq\sum_{i\in
I}p_{i}\cdot\operatorname{\mathit{K}}(d)(\Delta_{i},\Delta^{\prime}_{i})$

for any pseudometric $d$. This holds because

$\begin{array}[]{ll}&\operatorname{\mathit{K}}(d)(\sum_{i\in
I}p_{i}\cdot\Delta_{i},\sum_{i\in I}p_{i}\cdot\Delta^{\prime}_{i})\\\
=&\max\\{\sum_{u\in S}((\sum_{i\in I}p_{i}\cdot\Delta_{i})(u)-(\sum_{i\in
I}p_{i}\cdot\Delta^{\prime}_{i})(u))x_{u}\mid\\\ &\hskip
170.71652ptx_{u},\;x_{u^{\prime}}\in[0,1]\wedge x_{u}-x_{u^{\prime}}\leq
d(u,u^{\prime})\\}\\\ =&\max\\{\sum_{u\in S}\sum_{i\in
I}p_{i}\cdot(\Delta_{i}(u)-\Delta^{\prime}_{i}(u))x_{u}\mid
x_{u},\;x_{u^{\prime}}\in[0,1]\wedge x_{u}-x_{u^{\prime}}\leq
d(u,u^{\prime})\\}\\\ =&\max\\{\sum_{i\in I}p_{i}\sum_{u\in
S}(\Delta_{i}(u)-\Delta^{\prime}_{i}(u))x_{u}\mid
x_{u},\;x_{u^{\prime}}\in[0,1]\wedge x_{u}-x_{u^{\prime}}\leq
d(u,u^{\prime})\\}\\\ \leq&\sum_{i\in I}p_{i}\cdot\max\\{\sum_{u\in
S}(\Delta_{i}(u)-\Delta^{\prime}_{i}(u))x_{u}\mid
x_{u},\;x_{u^{\prime}}\in[0,1]\wedge x_{u}-x_{u^{\prime}}\leq
d(u,u^{\prime})\\}\\\ =&\sum_{i\in
I}p_{i}\cdot\operatorname{\mathit{K}}(d)(\Delta_{i},\Delta^{\prime}_{i})\end{array}$

Consequently, a simple logical characterisation of convex bisimulation metric
can be obtained by extending the logic in Section
LABEL:sec:logic_characterizations with infinitary conjunctions and by
interpreting the diamand modality with combined transitions, i.e.
$\llbracket{\langle
a\rangle\psi}\rrbracket({s})=\max_{s\xrightarrow{\,{a}\,}_{c}\Delta}\llbracket{\psi}\rrbracket({\Delta})$.
Write $\operatorname{\operatorname{\mathbf{d}}_{\mathit{cb}}^{l}}$ for the
metric induced by this extended logic.

######  Theorem 0.A.1.

$\operatorname{\operatorname{\mathbf{d}}_{\mathit{cb}}}=\operatorname{\operatorname{\mathbf{d}}_{\mathit{cb}}^{l}}$

##  Appendix 0.B Trace Metric

In this section we present a notion of trace metric that enjoys a
straightforward logical characterisation.

###  0.B.1 Trace Metric

A trace ${\it tr}$ is a string in the set $A^{*}$. We write $\epsilon$ for the
empty trace, and ${\it tr}_{1}\cdot{\it tr}_{2}$ for the concatenation of two
traces ${\it tr}_{1}$ and ${\it tr}_{2}$. Given a finitely branching pLTS, the
maximum probability that state $s$ can perform trace ${\it tr}$ is defined as
follows.

${\it Pr}(s,{\it tr})~{}=~{}\left\\{\begin{array}[]{ll}1&\mbox{if ${\it
tr}=\epsilon$}\\\ \max_{s\xrightarrow{\,{a}\,}\Delta}\sum_{t\in
S}\Delta(t)\cdot{\it Pr}(t,{\it tr}^{\prime})&\mbox{if ${\it tr}=a\cdot{\it
tr}^{\prime}$}\end{array}\right.$

######  Definition 9.

For any two states $s,t\in S$, the _trace distance_ between them is given as
follows:

$\operatorname{\operatorname{\mathbf{d}}_{\it t}}(s,t)~{}=~{}\sup_{{\it tr}\in
A^{*}}|{\it Pr}(s,{\it tr})-{\it Pr}(t,{\it tr})|$

Intuitively, the trace distance between $s$ and $t$ is the maximal difference
between the maximum probabilities given by $s$ and $t$ to a same trace.

###  0.B.2 Logical Characterizations

Let $\operatorname{\mathcal{L}}^{T}$ be the set of formulae produced by the
following grammar.

$\varphi::=\top\mid\langle a\rangle{\varphi}$

A formula evaluates in a state $s$ as follows:

$\begin{array}[]{l}\llbracket{\top}\rrbracket({s})=1\\\ \llbracket{\langle
a\rangle{\varphi}}\rrbracket({s})=\max_{s\xrightarrow{\,{a}\,}\Delta}\sum_{t\in
S}\Delta(t)\cdot\llbracket{\varphi}\rrbracket({t})\end{array}$

This logic induces a natural metric
$\operatorname{\operatorname{\mathbf{d}}_{\it t}^{l}}$.

$\operatorname{\operatorname{\mathbf{d}}_{\it
t}^{l}}(s,t)~{}=~{}\sup_{\varphi\in\mathbb{O}_{tr}}|\llbracket\varphi\rrbracket(s)-\llbracket\varphi\rrbracket(t)|$

######  Theorem 0.B.1.

$\operatorname{\operatorname{\mathbf{d}}_{\it
t}}=\operatorname{\operatorname{\mathbf{d}}_{\it t}^{l}}$

###### Proof.

It is easy to see that there is a bijection $f$ between $A^{*}$ and
$\operatorname{\mathcal{L}}^{T}$.

$\begin{array}[]{rcl}f(\epsilon)&=&\top\\\ f(a\cdot{\it tr})&=&\langle
a\rangle{f({\it tr})}\end{array}$

For any state $s$ and trace ${\it tr}$, we can show that ${\it Pr}(s,{\it
tr})=\llbracket{f({\it tr})}\rrbracket({s})$ by induction on the length of
${\it tr}$. The required result now easily follows.


11institutetext: E. Taralli 22institutetext: L. Gottardi 33institutetext: K.
Nagayoshi 44institutetext: M. Ridder 55institutetext: S. Visser
66institutetext: P. Khosropanah 77institutetext: H. Akamatsu 88institutetext:
J. van der Kuur 99institutetext: M. Bruijn 1010institutetext: J.R. Gao
SRON Netherlands Institute for Space Research
Sorbonnelaan 2, Utrecht, 3584 CA, The Netherlands
1010email<EMAIL_ADDRESS>

J.-R. Gao
Faculty of Applied Science, Delft University of Technology
Lorentzweg 1, 2628 CJ, Delft, The Netherlands

# Characterization of high aspect ratio TiAu TES X-ray microcalorimeters array
using the X-IFU Frequency Domain Multiplexing readout

E. Taralli  L. Gottardi  K. Nagayoshi  M. Ridder  S. Visser  P. Khosropanah
H. Akamatsu  J. van der Kuur  M. Bruijn  J.-R. Gao

###### Abstract

We are developing X-ray microcalorimeters as a backup option for the baseline
detectors in the X-IFU instrument on board the ATHENA space mission led by ESA
and to be launched in the early 2030s.
5$\times$5 mixed arrays with TiAu transition-edge sensor (TES), which have
different high aspect ratios and thus high resistances, have been designed and
fabricated to meet the energy resolution requirement of the X-IFU instrument.
Such arrays can also be used to optimise the performance of the Frequency
Domain Multiplexing (FDM) readout and lead to the final steps for the
fabrication of a large detector array.
In this work we present the experimental results from tens of the devices with
an aspect ratio (length-to-width) ranging from 1-to-1 up to 6-to-1, measured
in a single-pixel mode with a FDM readout system developed at SRON/VTT. We
observed a nominal energy resolution of about 2.5 eV at 5.9 keV at bias
frequencies ranging from 1 to 5 MHz. These detectors are proving to be the
best TES microcalorimeters ever reported in Europe, being able to meet not
only the requirements of the X-IFU instrument, but also those of other future
challenging X-ray space missions, fundamental physics experiments, plasma
characterization and material analysis.

###### Keywords:

transition-edge sensor, energy resolution, X-IFU, AC bias

††journal: Journal of Low Temperature Physics

##  1 Introduction

ATHENA 1 \- Advanced Telescope for High-ENergy Astrophysics - is the second
large mission of ESA’s Cosmic Vision-programme to study astrophysical
phenomena near black holes and galaxy clusters. The X-ray Integral Field Unit
(X-IFU) 2, one of the two instruments on board, will deliver spatially-
resolved high-resolution X-ray spectroscopy over a limited field of view.
X-IFU requires detectors in an array of nearly 3264 pixels, being sensitive in
the 0.2–12 keV energy range with 2.5 eV FWHM energy resolution below 7 keV.
SRON is currently developing a Frequency Domain Multiplexing (FDM) readout
system as the baseline and X-ray microcalorimeters arrays based on TiAu
transition-edge sensors (TESs) as a backup technology for the US MoAu TES
array, currently being developed at NASA Goddard Space Flight Center3.
In the last few years, a lot of progress has been reported in both the FDM
readout 4 and in our understanding of TES physics under AC bias. The latter
has been moved forward continuously by improving the detector design and
performance. For instance, bare TESs have been found to be preferable to TESs
with normal metal structures. It has also been shown 5 that AC loss is bias-
frequency dependent and depends also on the amount of the normal metal used in
the TES. Moreover, bare TESs have shown smaller weak-link effects and the
behaviour of $\alpha$ and $\beta$ are not affected by kinks 6 7 in the IV
curve. The normal resistance of the TES, together with its saturation power,
plays a crucial role in the reduction of the Josephson effect 8 which can
affect the performance of a TES microcalorimeter under AC bias. The Josephson
effects are non-dissipative so that they do not add noise to the detector, but
they introduce undesired, bias-dependent nonlinearities, which limit the
optimal bias range. To simplify the FDM read-out of a large TES array, these
effects should be minimised. It was recently been shown that the degradation
of performance from the frequency multiplexing scheme can be mitigated by the
use of TESs with high resistance8, 5. It is also important to have a thicker
bilayer to reduce the internal thermal fluctuation noise.
All of this new knowledge has led the design and fabrication of the new SRON
5$\times$5 TES mixed arrays, containing different pixel designs, as well as
the kilo-pixel uniform arrays with a single TES design at SRON. A thicker TiAu
bilayer with respect to the previous SRON devices 9 is introduced to reduce
the internal thermal fluctuation noise. Furthermore, higher aspect ratios
increase the normal resistance of the single pixel and thus increase the
saturation power; the absence of normal metal structures reduces the weak-link
effect; and a thinner membrane is used to lower the thermal conductance.
In this paper we present our experimental results in terms of energy
resolution for tens of TiAu TESs grouped into ten different types of device
with aspect ratio (length-to-width) ranging from 1-to-1 up to 6-to-1. They
were measured in a single-pixel mode with bias frequencies between 1 and 5
MHz,using an 18-channel FDM readout system which is a a prototype of the FDM
readout system for X-IFU.

##  2 TES Detector Arrays and Experimental Setup

(a)

(b)

Figure 1: 5$\times$5 SRON mixed arrays. Array labelled R3b with high-aspect
ratio devices with the following sizes (from left to right): 100$\times$30,
120$\times$40, 100$\times$25, 100$\times$100 and 80$\times$80 $\mu$m2 (Fig.
1a). Array labelled R4a with very high-aspect ration devices with the
following sizes (from left to right): 100$\times$20, 120$\times$20,
140$\times$30, 80$\times$20 and 80$\times$40 $\mu$m2 (Fig. 1b). Each column
has devices with the same aspect ratio. Red squares identify the TESs that
were connected and measured. (Color figure online.) Figure 2: 4-terminal
resistance measurement of pixels with three different aspect ratios:
100$\times$100 (blue dots), 100$\times$30 (purple crosses) and 140$\times$30
$\mu$m2 (green squares) measured with the same excitation current of 3 $\mu$A.
Lines serve no other purpose than to guide the eye. (Color figure online.)

Fig. 1 shows the design of two different 5$\times$5 mixed arrays that are
fabricated on a wafer together with other arrays. We can identify one array,
labelled array R3b, as containing high-aspect ratio devices with the following
dimensions (length$\times$width) (from left to right in Fig. 1a):
100$\times$30, 120$\times$40, 100$\times$25, 100$\times$100 and 80$\times$80
$\mu$m2, while the other array, labelled array R4a, contains very high-aspect
ratio devices with the following sizes (from left to right in Fig. 1b):
100$\times$20, 120$\times$20, 140$\times$30, 80$\times$20 and 80$\times$40
$\mu$m2. Note that every column has the same detector size in order to study
the performance of the TES as a function of the bias frequency and to have
reasonable statistics on pixel with the same design. The red squares point out
the 31 TESs that have been connected and measured. All the TESs have the same
bilayer thickness of Ti (35 nm) and Au (200 nm) and use a 0.5 $\mu$m thick SiN
membrane. We measured a normal squared resistance R = 25 m$\Omega$/sq and a
critical temperature T${}_{c}\sim$115 mK. The thermal conductance G at Tc
ranges from 107 to 172 pW/K and from 61 to 104 pW/K for the different aspect-
ratio arrays R3b and R4a, respectively.
Recently it has been shown10 that, depending on the quality of the Bismuth in
the absorber, a non-Gaussian thermal response can be induced in the energy
spectra. In order to identify the real performance of the pixel design, all
the absorbers consist only of Au 2.3 $\mu$m thick and have the same size
(240$\times$240 $\mu$m2) with a heat capacity C = 1.1 pJ/K at Tc. Each
absorber has, at its corners, four contacting points to the membrane and two
central contacting points directly to the sides of the TES. More details on
fabrication of the SRON TES array will be published in this special issue 11.
Due to the thicker bilayer used in this work, compared to the previous batch
9, we need to tailor the aspect ratio to obtain the required normal resistance
and bias power. Fig. 2 shows the 4-terminal resistance measurements as a
function of bath temperature measured for TESs with different dimensions which
are a squared 100$\times$100, a 100$\times$30 and a 140$\times$30 $\mu$m2 TES.
The characterization of the two arrays was performed in two different
experimental measurement setups, named XFDMLarge for the R3b array and named
XFDMProbe for the R4a array. Both setups were placed in the same dilution
refrigerator that can provide a bath temperature of $\sim$ 40 mK. TESs were
characterised under AC bias using an existing FDM readout system (1–5 MHz) 12
in the single-pixel mode configuration. Each TES is connected in series with
an LC resonator on a LC filter chip with a coil inductance L = 2 $\mu$H and a
1:2 transformer chip for the XFDMLarge and an L = 1 $\mu$H and a direct
connection to the TESs (no transformers) for the XFDMProbe. The TES array
chips and the cryogenic components of FDM readout were mounted in a low
magnetic impurity copper bracket fitted into an Al superconducting shield. The
bracket of each setup also accommodates a heater, a thermometer and a
Helmholtz coil. The heater and thermometer are used to regulate the
temperature locally on the chip. The coil is for applying a uniform magnetic
field perpendicular to the TES array to compensate any remnant magnetic field
trapped in the experiment setup.

##  3 Energy Resolution

(a)

(b)

Figure 3: Overview of the-single pixel energy resolution measured in array R3b
array (Fig. 3a) and in array R4a (Fig. 3b). Consider an error bar of $\pm$0.15
eV for each value. (Color figure online.)

An Fe-55 X-ray source is placed closely above the array in both the setups and
illuminates the entire TES array at a count rate of $\sim$1 cps per pixel for
the given absorber with the Mn-K$\alpha$ 5.9-keV fluorescent X-ray line. We
measured the X-ray energy resolution for each TES connected in the bias range
of 10–20% of RN, where the Noise Equivalent Power (NEP) scan usually predicted
the lowest energy resolution. Fig. 3a and 3b show a graphical impression of
the global energy resolution measured for arrays R3b and R4a, respectively.
About 20 of the pixels show an excellent energy resolution between 2.4 and 2.8
eV, eight of them between 2.8 and 3 eV and only three are worse than 3 eV.
In Fig. 4 we present four typical spectra, as examples. The best energy
resolution obtained for array R3b mounted in the XFDMLarge setup is shown in
Fig. 4b. It is worth noting how the energy resolution in both the setups
remains excellent when devices with the same aspect ratio are biased at
different resonant frequency f0 as shown for instance in Fig. 4c-4d. The best
energy resolution 2.39$\pm$0.14 eV at 5.9 keV was measured in the XFDMProbe
for the high-aspect ratio 140$\times$30 $\mu$m2 biased at a resonant frequency
of 1.6 MHz and between 10-20% of RN. This result is shown in Fig. 4a. At this
stage we are not yet able to identify the best TES design illustrating the
ultimate energy resolution. It is also still unclear, whether there is a
correlation between the energy resolution and the different aspect ratios of
the TES. In the ideal scenario, we would expect to find the identical energy
resolution along the columns of Fig. 3 and possibly a significant variation
between them, according to the pixel design variation. However, we still have
to deal with the different behaviour of the TES at the different bias
frequencies, which is reflected in the spread of the energy resolution along a
single column. If we consider the R3b array (Fig. 3a) and take the mean of the
energy resolution for each column, we get a uniform energy resolution ranging
from 2.7 to 2.84 eV, although the different squared TESs (last two columns)
have worse statistics, i.e. small spread in bias frequencies. In the R4a array
these averages are slightly more scattered, giving an energy resolution
ranging from 2.55 up to 2.86 eV. This could be due to the broader variation in
the pixel design but also to the poorer statistics for the last two columns of
Fig. 3b. Of course, with the upcoming measurements on other high aspect-ratio
mixed arrays and on the uniform kilo-pixel array, we might define the
relationship between the detector energy resolution, the pixel design and the
bias frequency. What is clear is that seven pixels out of 16 in R4a (mounted
in the XFDMProbe setup) show an energy resolution around 2.5 eV, which is a
slightly better than that found for array R3b (3 out of 15). This difference
is likely due to the better temperature stability ($\sim$ 1.9 $\mu$K at 55 mK)
in the XFDMProbe; the XFDMLarge ($\sim$ 3 $\mu$K at 50 mK) is less stable.
Furthermore, we notice that square or close-to-square TESs with a lower normal
resistance are more affected by the weak-link effect, showing an oscillation
in the predicted energy resolution as can be seen in the NEP plotted in Fig.
5a. This means that, although there might be very good energy resolution (Fig.
4b), this happens only for a limited number of bias points through the
transition. On the other hand, high aspect-ratio devices with a higher normal
resistance show a flat NEP over a wide bias range between 5 and 30% of RN as
shown in Fig. 5b.
It is important to highlight that these results have been obtained with a Tc
of 110 mK and for these arrays this could be a limiting factor. Reducing the
Tc down to $\sim$ 90 mK should give an improvement in the energy resolution of
between 15 and 20%, approaching even closer to the X-IFU requirements (2.5 eV
below 7 keV over the whole array).

(a) TES14-140$\times$30 $\mu$m2, f0=1.6 MHz

(b) TES24-80$\times$80 $\mu$m2, f0=2.9 MHz

(c) TES12-100$\times$25 $\mu$m2, f0=3.8 MHz

(d) TES13-100$\times$25 $\mu$m2, f0=4.6 MHz

Figure 4: Small selection of the best spectra at 5.9 keV for TESs mounted in
the XFDMLarge setup (from Fig. 4b to 4d) and in the XFDMProbe (Fig. 4a) with
bias points between 15-20% of RN. The red solid line is the best fit to the
data, and the blue points are the measured Mn-K$\alpha$ emission lines. The
lower plots show the residuals of the fit normalised by the error bars. (Color
figure online)

(a)

(b)

Figure 5: Noise Equivalent Power (NEP) scan for TES24-80$\times$80 $\mu$m2
(Fig. 5a) and for TES12-100$\times$25 $\mu$m2 (Fig. 5b) as a function of bias
point for three different bias frequencies.

##  4 Conclusion

New 5$\times$5 TiAu TES mixed arrays, containing TESs with a thick bilayer,
but varying aspect-ratios of the TES, were fabricated and experimentally
evaluated with 5.9-keV X-ray photons. Those TESs have a Tc of 110 mK, no
normal metal structures on the top of the bilayer, and make use of a thinner
SiN membrane (0.5 $\mu$m). We measured an energy resolution between 2.4 and
2.8 eV at 5.9 keV on 20 out of the 31 TESs. New TESs with a Tc $\sim$ 90 mK
should improve the energy resolution further and meet the X-IFU requirements
for all the pixels in the array.
Our microcalorimeters represent the best TES microcalorimeters ever reported
in Europe. Not only are our detectors able to meet the detector requirements
of the X-IFU instrument, but they also potentially offer technology for other
future X-ray space missions, fundamental physics experiments, plasma
characterization, and material analysis. We are now ready to test a kilo-pixel
array in combination with the FDM readout in multi-pixel mode.

###### Acknowledgements.

This work is partly funded by European Space Agency (ESA) and coordinated with
other European efforts under ESA CTP contract ITT AO/1-7947/14/NL/BW. It has
also received funding from the European Union’s Horizon 2020 Programme under
the AHEAD (Activities for the High-Energy Astrophysics Domain) project with
grant agreement number 654215.

## References

  * 1 F. Pajot, D. Barret, T. Lam-Trong, J.-W. den Herder et al, J. Low Temp. Phys. 193, 901, (2018).
  * 2 European Space Agency (ESA), ”ATHENA Mission Summary”, Available: http://sci.esa.int/athena/59896-missionsummary.
  * 3 S. J. Smith, J. S. Adams, S. R. Bandler, et. al., Proc. SPIE 99055S, (2016), https://doi.org/10.1117/12.2231749
  * 4 H. Akamatsu, L. Gottardi, J. van der Kuur, C.P. de Vries, M. P. Bruijn, J. A. Chervenak, M. Kiviranta, A. J. van den Linden, B. D. Jackson, A. Miniussi, K. Sakai, S. J. Smith and N. A. Wakeham, Proc. SPIE 106991N, (2018), https://doi.org/10.1117/12.2313284
  * 5 K. Sakai, J. S. Adams, S. R. Bandler, J. A. Chervenak, A. M. Datesman, M. E. Eckart, F. M. Finkbeiner, R. L. Kelley, C. A. Kilbourne, A. R. Miniussi, F. S. Porter, J. S. Sadleir, S. J. Smith, N. A. Wakeham, E. J. Wassell1, W. Yoon, H. Akamatsu, M. P. Bruijn, L. Gottardi, B. D. Jackson, J. van der Kuur, B. J. van Leeuwen, A. J. van der Linden, H. J. van Weers, M. Kiviranta, J. Low Temp. Phys. 193, 356, (2018).
  * 6 N. A. Wakeham, J. S. Adams, S. R. Bandler, J. A. Chervenak, A. M. Datesman, M. E. Eckart, F. M. Finkbeiner, R. L. Kelley, C. A. Kilbourne, A. R. Miniussi, F. S. Porter, J. E. Sadleir, K. Sakai, S. J. Smith, E. J. Wassell and W. Yoon, J. Low Temp. Phys. 193, 231, (2018).
  * 7 E. Taralli, P. Khosropanah, L. Gottardi, K. Nagayoshi, M. L. Ridder, M. P. Bruijn, and J. R. Gao, AIP Advances 9, 045324, (2019), DOI:10.1063/1.5089739.
  * 8 L. Gottardi, S. J. Smith, A. Kozorezov, H. Akamatsu, J. van der Kuur, S. R. Bandler, M. P. Bruijn, J. A. Chervenak, J. R. Gao, R. H. den Hartog, B. D. Jackson, P. Khosropanah, A. Miniussi, K. Nagayoshi, M. Ridder, J. Sadleir, K. Sakai and N. Wakeham, J. Low Temp. Phys. 193, 209, (2018).
  * 9 P. Khosropanah, E. Taralli, L. Gottardi, C. P. de Vries, K. Nagayoshi, M. L. Ridder, H. Akamatsu, M. P. Bruijn and J.-R. Gao, Proc. SPIE 106991M, (2018), https://doi.org/10.1117/12.2313439
  * 10 D. Yan, R. Divan, L. M. Gades, P. Kenesei, T. J. Madden, A. Miceli, J.-S. Park, U. M. Patel, O. Quaranta, H. Sharma, D. A. Bennett, W. B. Doriese, J. W. Fowler, J. D. Gard, J. P. Hays-Wehle, K. M. Morgan, D. R. Schmidt, D. S. Swetz, and Joel N. Ullom, Appl. Phys. Lett. 111, 192602, (2017); https://doi.org/10.1063/1.5001198
  * 11 K. Nagayoshi, M.L. Ridder, M.P. Bruijn, L. Gottardi, E. Taralli, P. Khosropanah, S. Visser and J. R. Gao, J. Low Temp. Phys.. This Special Issue (2019).
  * 12 H. Akamatsu, L. Gottardi, J. van der Kuur, C. P. de Vries, K. Ravensberg, J. S. Adams, S. R. Bandler, M. P. Bruijn, J. A. Chervenak, C. A. Kilbourne, M. Kiviranta, A. J. van der Linden, B. D. Jackson, S. J. Smith, Proc. SPIE 99055S, (2016), https://doi.org/10.1117/12.2232805