$\displaystyle(\min\nolimits_{u})_{\\#}^{\max_{\in}(d)}((\max\nolimits_{\in})_{\\#}^{d}(R))$

where

$\displaystyle(\max\nolimits_{\in})_{\\#}^{d}\colon\mathbf{2}^{[{X\times
X}]^{d}}\to\mathbf{2}^{[{\mathbf{2}^{X\times X}}]^{\max_{\in}(d)}}$
$\displaystyle(\min\nolimits_{u})_{\\#}^{\max_{\in}(d)}\colon\mathbf{2}^{[{\mathbf{2}^{X\times
X}}]^{\max_{\in}(d)}}\to\mathbf{2}^{[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(d)}}$

We are using the approximations associated to non-expansive functions, given
in 5.4, and obtain:

$\displaystyle\mathcal{H}_{\\#}^{d}(R)$ $\displaystyle=$
$\displaystyle\\{(X_{1},X_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(d)}\mid\mathit{Min}_{\max_{\in}(d)|_{u^{-1}(X_{1},X_{1})}}\cap(\max\nolimits_{\in})_{\\#}^{d}(R)\neq\emptyset\\}$
$\displaystyle=$
$\displaystyle\\{(X_{1},X_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(d)}\mid\exists
C\subseteq X\times X,u(C)=(X_{1},X_{2}),$ $\displaystyle\qquad
C\in(\max\nolimits_{\in})_{\\#}^{d}(R),\mathrm{max}_{\in}(d)(C)=\min_{u(C^{\prime})=(X_{1},X_{2})}\mathrm{max}_{\in}(d)(C^{\prime})\\}$
$\displaystyle=$
$\displaystyle\\{(X_{1},X_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(d)}\mid\exists
C\subseteq X\times X,u(C)=(X_{1},X_{2}),$ $\displaystyle\qquad
C\in(\max\nolimits_{\in})_{\\#}^{d}(R),\max
d[C]=\min_{u(C^{\prime})=(X_{1},X_{2})}\max d[C^{\prime}]\\}$ $\displaystyle=$
$\displaystyle\\{(X_{1},X_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(d)}\mid\exists
C\subseteq X\times X,u(C)=(X_{1},X_{2}),$
$\displaystyle\qquad\mathit{Max}_{d|_{C}}\subseteq R,\max
d[C]=\mathcal{H}(d)(X_{1},X_{2})\\}$

We show that this is equivalent to the characterisation in the statement of
the lemma.

  * •

Assume that for all $x_{1}\in X_{1}$ such that $\min_{x_{2}^{\prime}\in
X_{2}}d(x_{1},x_{2}^{\prime})=\mathcal{H}(d)(X_{1},X_{2})$, there exists
$x_{2}\in X_{2}$ such that $(x_{1},x_{2})\in R$ and
$d(x_{1},x_{2})=\mathcal{H}(d)(X_{1},X_{2})$ (and vice versa).

We define a set $C_{m}$ that contains all such pairs $(x_{1},x_{2})$, obtained
from this guarantee. Now let $x_{1}\not\in\pi_{1}[C_{m}]$. Then necessarily
$\min_{x_{2}^{\prime}\in
X_{2}}d(x_{1},x_{2}^{\prime})<\mathcal{H}(d)(X_{1},X_{2})$ (because the
minimal distance to an element of $X_{2}$ cannot exceed the Hausdorff distance
of the two sets). Construct another set $C^{\prime}$ that contains all such
$(x_{1},x_{2})$ where $x_{2}$ is an argument where the minimum is obtained.
Also add elements $x_{2}\not\in\pi_{2}[C_{m}]$ and their corresponding
partners to $C^{\prime}$.

The $C=C_{m}\cup C^{\prime}$ is a coupling for $X_{1},X_{2}$, i.e.,
$u(C)=(X_{1},X_{2})$. Furthermore $\mathit{Max}_{d|_{C}}=C_{m}\subseteq R$ and
$\max d[C]=\max d[C_{m}]=\mathcal{H}(d)(X_{1},X_{2})$.

  * •

Assume that there exists $C\subseteq X\times X$, $u(C)=(X_{1},X_{2})$,
$\mathit{Max}_{d|_{C}}\subseteq R$, $\max d[C]=\mathcal{H}(d)(X_{1},X_{2})$.

Now let $x_{1}\in X_{1}$ such that $\min_{x_{2}^{\prime}\in
X_{2}}d(x_{1},x_{2}^{\prime})=\mathcal{H}(d)(X_{1},X_{2})$. Since $C$ is a
coupling of $X_{1},X_{2}$, there exists $x_{2}\in X_{2}$ such that
$(x_{1},x_{2})\in C\subseteq R$. It is left to show that
$d(x_{1},x_{2})=\mathcal{H}(d)(X_{1},X_{2})$, which can be done as follows:

$\mathcal{H}(d)(X_{1},X_{2})=\min_{x_{2}^{\prime}\in
X_{2}}d(x_{1},x_{2}^{\prime})\leq d(x_{1},x_{2})\leq\max
d[C]=\mathcal{H}(d)(X_{1},X_{2}).$

For an $x_{2}\in X_{2}$ such that $\min_{x_{1}^{\prime}\in
X_{1}}d(x_{1}^{\prime},x_{2})=\mathcal{H}(d)(X_{1},X_{2})$ the proof is
analogous.

#### Metric transition systems.

A _metric transition system_ is a triple $(X,w,\eta)$ where $X$ is a finite
set of states, and $w:X\to[0,1]$ and $\eta:X\to\mathbf{2}^{X}$ are functions
that assign a weight $w(x)$ and a set of successors $\eta(x)$ to each $x\in
X$. The _MTS pseudo-metric_ 222Different from a metric, for a pseudo-metric
$d$ the fact that $d(x,y)=0$ does not necessarily imply $x=y$. is the least
fixpoint of the function $\mathcal{J}\colon[0,1]^{X\times X}\to[0,1]^{X\times
X}$ defined, for $d\colon X\times X\to[0,1]$ and $x_{1},x_{2}\in X$, as:

$\mathcal{J}(d)(x_{1},x_{2})=\max\\{\mathcal{H}(d)(\eta(x_{1}),\eta(x_{2})),|w(x_{1})-w(x_{2})|\\}$

where $\mathcal{H}$ is the Hausdorff lifting (for $\mathbb{M}=[0,1]$) defined
earlier. Now, let $\bar{w}\colon X\times X\to[0,1]$ be the weight distance
function defined for $x_{1},x_{2}\in X$ via

$\bar{w}(x_{1},x_{2})=|w(x_{1})-w(x_{2})|.$

The function $\mathcal{J}$ can be written as

$\mathcal{J}=\max\nolimits_{p}\circ\left((\eta\times\eta)^{*}\circ\mathcal{H}\uplus
c_{\bar{w}}\right)$

where $p\colon(X\times X)\uplus(X\times X)\to(X\times X)$ with
$p((x_{1},x_{2}),i)=(x_{1},x_{2})$. (We use $i\in\\{0,1\\}$ to distinguish the
elements in the disjoint union.)

######  Proof 6.6.

Let $d\colon X\times X$ and $x_{1},x_{2}\in X$, then we have

$\displaystyle\mathcal{J}(d)(x_{1},x_{2})$
$\displaystyle=\max\nolimits_{p}\left(((\eta\times\eta)^{*}\circ\mathcal{H}\uplus
c_{\bar{w}})(d)\right)(x_{1},x_{2})$
$\displaystyle=\max\\{((\eta\times\eta)^{*}\circ\mathcal{H}(d))(x_{1},x_{2}),\bar{w}(x_{1},x_{2})\\}$
$\displaystyle=\max\\{\mathcal{H}(d)(\eta(x_{1}),\eta(x_{2})),\bar{w}(x_{1},x_{2})\\}$
$\displaystyle=\max\\{\mathcal{H}(d)(\eta(x_{1}),\eta(x_{2}),|w(x_{1})-w(x_{2})|\\}.$

From this representation and section 5 it follows that $\mathcal{J}$ is non-
expansive.

Let $d\colon X\times X\to[0,1]$. The approximation for $\mathcal{J}$ in the
dual sense is $\mathcal{J}_{\\#}^{d}\colon\mathbf{2}^{[{X\times
X}]^{d}}\to\mathbf{2}^{[{X\times X}]^{\mathcal{J}(d)}}$ with

$\mathcal{J}_{\\#}^{d}(Z)=\\{(x_{1},x_{2})\in[{X\times
X}]^{\mathcal{J}(d)}\mid\bar{w}(x_{1},x_{2})<\mathcal{H}(d)(\eta(x_{1}),\eta(x_{2}))\land(\eta(x_{1}),\eta(x_{2}))\in\mathcal{H}^{d}_{\\#}(Z)\\}$

######  Proof 6.7.

Let $d\colon X\times X\to[0,1]$ and $X^{\prime}\subseteq\mathbf{2}^{[{X\times
X}]^{d}}$. We abbreviate
$g=(\eta\times\eta)^{*}\circ\mathcal{H}\colon[0,1]^{X\times
X}\to[0,1]^{X\times X}$ and hence $\mathcal{J}=\max_{p}(g\uplus\bar{w})$. Thus
we obtain

$\mathcal{J}_{\\#}^{d}(X^{\prime})=(\max\nolimits_{p})_{\\#}^{g(d)\uplus\bar{w}}\left(g_{\\#}^{d}(X^{\prime})\uplus(c_{\bar{w}})_{\\#}^{d}(X^{\prime})\right).$

Since $c_{\bar{w}}\colon[0,1]^{\emptyset}\to[0,1]^{X\times X}$ is a constant
function, we conclude

$(c_{\bar{w}})_{\\#}^{d}(X^{\prime})=\emptyset.$

Now

$g_{\\#}^{d}=((\eta\times\eta)^{*})_{\\#}^{\mathcal{H}(d)}\circ\mathcal{H}_{\\#}^{d}$

where

$\displaystyle\mathcal{H}_{\\#}^{d}$ $\displaystyle\colon\mathbf{2}^{[{X\times
X}]^{d}}\to\mathbf{2}^{[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(d)}}$
$\displaystyle((\eta\times\eta)^{*})_{\\#}^{\mathcal{H}(d)}$
$\displaystyle\colon\mathbf{2}^{[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(d)}}\to\mathbf{2}^{[{X\times
X}]^{g(d)}}.$

It holds that
$((\eta\times\eta)^{*})_{\\#}^{\mathcal{H}(d)}=(\eta\times\eta)^{-1}$ and
hence

$(x_{1},x_{2})\in
g_{\\#}^{d}(X^{\prime})\Leftrightarrow(\eta(x_{1}),\eta(x_{2}))\in\mathcal{H}_{\\#}^{d}(X^{\prime}).$

Lastly, we obtain

$\displaystyle\mathcal{J}_{\\#}^{d}(X^{\prime})$
$\displaystyle=(\max\nolimits_{p})_{\\#}^{g(d)\uplus\bar{w}}((g\uplus\bar{w})^{d}_{\\#}(X^{\prime})\times\\{0\\})$
$\displaystyle=\\{(x_{1},x_{2})\in\mathbf{2}^{[{X\times
X}]^{\mathcal{J}(d)}}\mid\mathit{Max}_{(g(d)\uplus\bar{w})\mid_{p^{-1}(\\{(x_{1},x_{2})\\})}}\subseteq
g_{\\#}^{d}(X^{\prime})\times\\{0\\}\\}.$

We have that
$p^{-1}(\\{(x_{1},x_{2})\\})=\\{((x_{1},x_{2}),0),((x_{1},x_{2}),1)\\}$. The
inclusion

$\mathit{Max}_{(g(d)\uplus\bar{w})\mid_{p^{-1}(\\{(x_{1},x_{2})\\})}}\subseteq
g_{\\#}^{d}(X^{\prime})\times\\{0\\}$

can only hold if $g(d)(x_{1},x_{2})>\bar{w}(x_{1},x_{2})$ (and hence the
maximum is achieved by $g(d)$ instead of $\bar{w}$) and additionally
$((x_{1},x_{2}),0)\in g_{\\#}^{d}(X^{\prime})\times\\{0\\}$. Hence

$\displaystyle\mathcal{J}_{\\#}^{d}(Z)$
$\displaystyle=\\{(x_{1},x_{2})\in[{X\times
X}]^{\mathcal{J}(d)}\mid\bar{w}(x_{1},x_{2})<g(d)(x_{1},x_{2})\land(x_{1},x_{2})\in
g^{d}_{\\#}(Z)\\}$ $\displaystyle=\\{(x_{1},x_{2})\in\mathbf{2}^{[{X\times
X}]^{\mathcal{J}(d)}}\mid\bar{w}(x_{1},x_{2})<\mathcal{H}(d)(\eta(x_{1}),\eta(x_{2}))\land(\eta(x_{1}),\eta(x_{2}))\in\mathcal{H}^{d}_{\\#}(Z)\\}.$

######  Example 6.8.

We consider the MTS depicted below.

$x:0.1$
---
$y:0.6$
---
$z:0.3$
---

Here, $\eta(x)=\\{x,z\\}$, $\eta(y)=\\{x,y,z\\}$ and $\eta(z)=\\{x\\}$.
Additionally we have $w(x)=0.1$, $w(y)=0.6$ and $w(z)=0.3$ resulting in
$\bar{w}(x,y)=0.5$, $\bar{w}(x,z)=0.2$ and $\bar{w}(y,z)=0.3$. The least
fixpoint of $\mathcal{J}$ is a pseudo-metric $\mu\mathcal{J}$ given by
$\mu\mathcal{J}(x,y)=\mu\mathcal{J}(y,z)=0.5$ and $\mu\mathcal{J}(x,z)=0.3$.
(Since $\mu\mathcal{J}$ is a pseudo-metric, the remaining entries are fixed:
$\mu\mathcal{J}(u,u)=0$ and $\mu\mathcal{J}(u,v)=\mu\mathcal{J}(v,u)$ for all
$u,v\in\\{x,y,z\\}$.)

Now consider the pseudo-metric $d$ with $d(x,y)=d(x,z)=d(y,z)=0.5$. This is
also a fixpoint of $\mathcal{J}$. Note that
$\mathcal{H}(d)(\eta(x),\eta(y))=\mathcal{H}(d)(\eta(x),\eta(z))=\mathcal{H}(d)(\eta(y),\eta(z))=0.5$.
Let us use our technique in order to verify that $d$ is not the least fixpoint
of $\mathcal{J}$, by showing that $\nu\mathcal{J}_{\\#}^{d}\neq\emptyset$.

We start fixpoint iteration with the approximation $\mathcal{J}_{\\#}^{d}$
from the top element $[{X\times X}]^{d}$, which is given by the symmetric
closure333We denote the symmetric closure of a relation $R$ by $S(R)$. of
$\\{(x,y),(x,z),(y,z)\\}$ (since reflexive pairs do not contain slack).

We first observe that
$(x,y),(y,x)\notin\mathcal{J}_{\\#}^{d}(S(\\{(x,y),(x,z),(y,z)\\}))$ since
$\bar{w}(x,y)=0.5\not<\mathcal{H}(d)(\eta(x),\eta(y))=0.5$. Next,
$(y,z),(z,y)\notin\mathcal{J}_{\\#}^{d}(S(\\{(x,z),(y,z)\\}))$ since
$(\eta(y),\eta(z))\not\in\mathcal{H}_{\\#}^{d}(S(\\{(x,z),(y,z)\\}))$. In
order to see this, consider the approximation of the Hausdorff lifting in
Lemma 6.2 and note that for $y\in\eta(y)$ we have
$\min_{u\in\eta(z)}d(y,u)=0.5=\mathcal{H}(d)(\eta(y),\eta(z))$, but
$(y,x)\notin S(\\{(x,z),(y,z)\\})$ (where $x$ is the only element in
$\eta(z)$).

The pairs $(x,z),(z,x)$ on the other hand satisfy all conditions and hence

$\nu\mathcal{J}_{\\#}^{d}=S(\\{(x,z)\\})=\mathcal{J}_{\\#}^{d}(S(\\{(x,z)\\}))\neq\emptyset$

Thus we conclude that $d$ is not the least fixpoint, but, according to
Proposition 4.5, we can decrease the value of $d$ in the positions
$(x,z),(z,x)$ and obtain a pre-fixpoint from which we can continue fixpoint
iteration.

###  6.3. Bisimilarity

In order to define standard bisimilarity we use a variant $\mathcal{G}$ of the
Hausdorff lifting $\mathcal{H}$ defined before, where $\max$ and $\min$ are
swapped. More precisely, $\mathcal{G}:\mathbb{M}^{X\times
X}\to\mathbb{M}^{\mathbf{2}^{X}\times\mathbf{2}^{X}}$ is defined, for
$d\in\mathbb{M}^{X\times X}$, by

$\mathcal{G}(d)(X_{1},X_{2})=\max\\{\min_{(x_{1},x_{2})\in
C}d(x_{1},x_{2})\mid C\subseteq X\times X\ \land\ u(C)=(X_{1},X_{2})\\}$.

######  Lemma 6.9.

The approximation for the adapted Hausdorff lifting $\mathcal{G}$ in the
primal sense is as follows. Let $a\colon X\times X\to\\{0,1\\}$, then
$\mathcal{G}^{\\#}_{a}\colon\mathbf{2}^{[{X\times
X}]_{a}}\to\mathbf{2}^{[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]_{a}}$ with

$\displaystyle\mathcal{G}_{a}^{\\#}(R)$ $\displaystyle=$
$\displaystyle\\{(X_{1},X_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]_{\mathcal{H}(a)}\mid$
$\displaystyle\qquad\qquad\quad\forall x_{1}\in X_{1}\exists x_{2}\in
X_{2}\colon\big{(}(x_{1},x_{2})\not\in[{X\times X}]_{a}\lor(x_{1},x_{2})\in
R\big{)}$ $\displaystyle\qquad\qquad\mathop{\land}\forall x_{2}\in
X_{2}\exists x_{1}\in X_{1}\colon\big{(}(x_{1},x_{2})\not\in[{X\times
X}]_{a}\lor(x_{1},x_{2})\in R\big{)}\\}$

######  Proof 6.10.

We rely on the characterisation of $\mathcal{H}_{\\#}^{a}$ (dual case) of
subsection 6.2 and we examine the case where $\mathbb{M}=\\{0,1\\}$. In this
case, whenever we have
$(X_{1},X_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]^{\mathcal{H}(a)}$ it
must necessarily hold that $\mathcal{H}(a)(X_{1},X_{2})=1$. Hence, the first
part of the conjunction simplifies to:

$\forall x_{1}\in X_{1}\big{(}\min_{x_{2}^{\prime}\in
X_{2}}a(x_{1},x_{2}^{\prime})=1\,\Rightarrow\,\exists x_{2}\in
X_{2}\colon(x_{1},x_{2})\in R\land a(x_{1},x_{2})=1\big{)},$

from which we can omit $a(x_{1},x_{2})=1$ from the conclusion, since this
holds automatically. Furthermore $\min_{x^{\prime}_{2}\in
X_{2}}a(x_{1},x^{\prime}_{2})=1$ can be rewritten to $\forall x_{2}\in
X_{2}\colon a(x_{1},x_{2})=1$. This gives us:

$\displaystyle\forall x_{1}\in X_{1}\big{(}\lnot\forall x_{2}\in X_{2}\colon
a(x_{1},x_{2})=1\mathop{\lor}\exists x_{2}\in X_{2}\colon(x_{1},x_{2})\in
R\big{)}$ $\displaystyle\equiv$ $\displaystyle\forall x_{1}\in
X_{1}\big{(}\exists x_{2}\in X_{2}\colon a(x_{1},x_{2})=0\mathop{\lor}\exists
x_{2}\in X_{2}\colon(x_{1},x_{2})\in R\big{)}$ $\displaystyle\equiv$
$\displaystyle\forall x_{1}\in X_{1}\exists x_{2}\in
X_{2}\big{(}(x_{1},x_{2})\not\in[{X\times X}]^{a}\mathop{\lor}(x_{1},x_{2})\in
R\big{)}.$

Since this characterisation is independent of the order, we can replace
$[{X\times X}]^{a}$ by $[{X\times X}]_{a}$ and obtain a characterizing
condition for $\mathcal{G}_{a}^{\\#}$ (primal case).

Now we can define the fixpoint function for bisimilarity and its corresponding
approximation. For simplicity we consider unlabelled transition systems, but
it would be straightforward to handle labelled transitions.

Let $X$ be a finite set of states and $\eta:X\to\mathbf{2}^{X}$ a function
that assigns a set of successors $\eta(x)$ to a state $x\in X$. The fixpoint
function for bisimilarity $\mathcal{B}:\\{0,1\\}^{X\times
X}\to\\{0,1\\}^{X\times X}$ can be expressed by using the Hausdorff lifting
$\mathcal{G}$ with $\mathbb{M}=\\{0,1\\}$.

Bisimilarity on $\eta$ is the greatest fixpoint of
$\mathcal{B}=(\eta\times\eta)^{*}\circ\mathcal{G}$.

######  Proof 6.11.

Let for $a:X\times X\to\\{0,1\\}$, $x,y\in X$. Then we have

$\displaystyle(\eta\times\eta)^{*}\circ\mathcal{G}(a)(x,y)$ $\displaystyle=$
$\displaystyle\mathcal{G}(a)(\eta(x),\eta(y))$ $\displaystyle=$
$\displaystyle\max\nolimits_{u}(\min\nolimits_{\in}(a))(\eta(x),\eta(y))$
$\displaystyle=$
$\displaystyle\max_{u(C)=(\eta(x),\eta(y))}(\min\nolimits_{\in}^{X\times
X}(a))(C)$ $\displaystyle=$
$\displaystyle\max_{u(C)=(\eta(x),\eta(y))}\min_{(x^{\prime},y^{\prime})\in
C}a(x^{\prime},y^{\prime})$

Now we prove that this, indeed, corresponds with the standard bisimulation
function, i.e. $\max_{u(C)=(\eta(x),\eta(y))}\min_{(x^{\prime},y^{\prime})\in
C}a(x^{\prime},y^{\prime})=1$ if and only if for all $x^{\prime}\in\eta(x)$
there exists $y^{\prime}\in\eta(y)$ such that $a(x^{\prime},y^{\prime})=1$ and
vice versa. For the first implication, assume that
$\max_{u(C)=(\eta(x),\eta(y))}\min_{(x^{\prime},y^{\prime})\in
C}a(x^{\prime},y^{\prime})=1$. This means that there exists $C\subseteq
X\times X$ such that $u(C)=(\pi_{1}(C),\pi_{2}(C))=(\eta(x),\eta(y))$ and
$\min_{(x^{\prime},y^{\prime})\in C}a(x^{\prime},y^{\prime})=1$. Then we have
two cases. Either $C=\emptyset$, which means that $\eta(x)=\eta(y)=\emptyset$,
that is, $x$ and $y$ have no successors, and so the bisimulation property
vacuously holds. Otherwise, $C\neq\emptyset$, and we must have
$a(x^{\prime},y^{\prime})=1$ for all $(x^{\prime},y^{\prime})\in C$. Then,
since $(\pi_{1}(C),\pi_{2}(C))=(\eta(x),\eta(y))$, for all
$x^{\prime}\in\eta(x)$ there must exists $y^{\prime}\in\eta(y)$ such that
$(x^{\prime},y^{\prime})\in C$, and thus $a(x^{\prime},y^{\prime})=1$. Vice
versa, for all $y^{\prime}\in\eta(y)$ there must exists $x^{\prime}\in\eta(x)$
such that $(x^{\prime},y^{\prime})\in C$, and thus
$a(x^{\prime},y^{\prime})=1$. So the bisimulation property holds.

For the other implication, assume that for all $x^{\prime}\in\eta(x)$ there
exists $y^{\prime}\in\eta(y)$ such that $a(x^{\prime},y^{\prime})=1$ and call
$c_{1}(x^{\prime})$ such a $y^{\prime}$. Vice versa, assume also that for all
$y^{\prime}\in\eta(y)$ there exists $x^{\prime}\in\eta(x)$ such that
$a(x^{\prime},y^{\prime})=1$ and call $c_{2}(y^{\prime})$ such a $x^{\prime}$.
This means that for all $x^{\prime}\in\eta(x)$ and $y^{\prime}\in\eta(y)$, we
have $a(x^{\prime},c_{1}(x^{\prime}))=a(c_{2}(y^{\prime}),y^{\prime})=1$. Now
let $C^{\prime}=\\{(x^{\prime},y^{\prime})\in\eta(x)\times\eta(y)\mid
c_{1}(x^{\prime})=y^{\prime}\lor x^{\prime}=c_{2}(y^{\prime})\\}$. Since we
assumed that for all $x^{\prime}\in\eta(x)$ there exists
$y^{\prime}\in\eta(y)$ such that $c_{1}(x^{\prime})=y^{\prime}$, we must have
that $\pi_{1}(C^{\prime})=\eta(x)$. The same holds for all
$y^{\prime}\in\eta(y)$, thus $\pi_{2}(C^{\prime})=\eta(y)$. Therefore, we know
that $u(C^{\prime})=(\eta(x),\eta(y))$, and we can conclude by showing that
$a(x^{\prime},y^{\prime})=1$ for all $(x^{\prime},y^{\prime})\in C^{\prime}$,
in which case also
$\max_{u(C)=(\eta(x),\eta(y))}\min_{(x^{\prime},y^{\prime})\in
C}a(x^{\prime},y^{\prime})=1$. By definition of $C^{\prime}$ either
$c_{1}(x^{\prime})=y^{\prime}$ or $x^{\prime}=c_{2}(y^{\prime})$, or both,
must hold. Assume the first one holds, the other case is similar. Then, we can
immediately conclude since by hypothesis we know that
$a(x^{\prime},c_{1}(x^{\prime}))=1$.

Since we proved that the function $\mathcal{B}$ is the same of the standard
bisimulation function, then its greatest fixpoint $\nu\mathcal{B}$ is the
bisimilarity on $\eta$.

Since we are interested in the greatest fixpoint, we are working in the primal
sense. Bisimulation relations are represented by their characteristic
functions $a\colon X\times X\to\\{0,1\\}$, in fact the corresponding relation
can be obtained by taking the complement of $[{X\times
X}]_{a}=\\{(x_{1},x_{2})\in X_{1}\times X_{2}\mid a(x_{1},x_{2})=0\\}$.

Let $a\colon X\times X\to\\{0,1\\}$. The approximation for the bisimilarity
function $\mathcal{B}$ in the primal sense is
$\mathcal{B}_{a}^{\\#}\colon\mathbf{2}^{[{X\times
X}]_{a}}\to\mathbf{2}^{[{X\times X}]_{\mathcal{B}(a)}}$ with

$\displaystyle\mathcal{B}_{a}^{\\#}(R)$ $\displaystyle=$
$\displaystyle\\{(x_{1},x_{2})\in[{X\times X}]_{\mathcal{B}(a)}\mid$
$\displaystyle\quad\forall y_{1}\in\eta(x_{1})\exists
y_{2}\in\eta(x_{2})\big{(}(y_{1},y_{2})\not\in[{X\times
X}]_{a}\lor(y_{1},y_{2})\in R)\big{)}$ $\displaystyle\ \land\forall
y_{2}\in\eta(x_{2})\exists
y_{1}\in\eta(x_{1})\big{(}(y_{1},y_{2})\not\in[{X\times
X}]_{a}\lor(y_{1},y_{2})\in R)\big{\\}}$

######  Proof 6.12.

From subsection 6.2 we know that

$\displaystyle\mathcal{G}_{a}^{\\#}\colon[{X\times X}]_{a}$ $\displaystyle\to$
$\displaystyle[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]_{\mathcal{G}(a)}$
$\displaystyle\mathcal{G}_{a}^{\\#}(R)$ $\displaystyle=$
$\displaystyle\\{(X_{1},X_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]_{\mathcal{G}(a)}\mid$
$\displaystyle\quad\forall x_{1}\in X_{1}\exists x_{2}\in
X_{2}\colon\big{(}(x_{1},x_{2})\not\in[{X\times X}]_{a}\lor(x_{1},x_{2})\in
R\big{)}$ $\displaystyle\mathop{\land}\forall x_{2}\in X_{2}\exists x_{1}\in
X_{1}\colon\big{(}(x_{1},x_{2})\not\in[{X\times X}]_{a}\lor(x_{1},x_{2})\in
R\big{)}\\}.$

Furthermore

$\displaystyle((\eta\times\eta)^{*})_{\mathcal{G}(a)}^{\\#}\colon[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]_{\mathcal{G}(a)}$
$\displaystyle\to$ $\displaystyle[{X\times X}]_{\mathcal{B}(a)}$
$\displaystyle((\eta\times\eta)^{*})_{\mathcal{G}(a)}^{\\#}(R)$
$\displaystyle=$ $\displaystyle(\eta\times\eta)^{-1}(R)$

Composing these functions we obtain:

$\displaystyle\mathcal{B}_{a}^{\\#}\colon[{X\times X}]_{a}$ $\displaystyle\to$
$\displaystyle[{X\times X}]_{\mathcal{B}(a)}$
$\displaystyle\mathcal{B}_{a}^{\\#}(R)$ $\displaystyle=$
$\displaystyle(\eta\times\eta)^{-1}(\\{(Y_{1},Y_{2})\in[{\mathbf{2}^{X}\times\mathbf{2}^{X}}]_{\mathcal{G}(a)}\mid$
$\displaystyle\qquad\forall y_{1}\in Y_{1}\exists y_{2}\in
Y_{2}\colon\big{(}(y_{1},y_{2})\not\in[{X\times X}]_{a}\lor(y_{1},y_{2})\in
R\big{)}$ $\displaystyle\quad\,\mathop{\land}\forall y_{2}\in Y_{2}\exists
y_{1}\in Y_{1}\colon\big{(}(y_{1},y_{2})\not\in[{X\times
X}]_{a}\lor(y_{1},y_{2})\in R\big{)}\\})$ $\displaystyle=$
$\displaystyle\\{(x_{1},x_{2})\in[{X\times X}]_{\mathcal{B}(a)}\mid$
$\displaystyle\quad\forall y_{1}\in\eta(x_{1})\exists
y_{2}\in\eta(x_{2})\colon\big{(}(y_{1},y_{2})\not\in[{X\times
X}]_{a}\lor(y_{1},y_{2})\in R\big{)}$ $\displaystyle\mathop{\land}\forall
y_{2}\in\eta(x_{2})\exists
y_{1}\in\eta(x_{1})\colon\big{(}(y_{1},y_{2})\not\in[{X\times
X}]_{a}\lor(y_{1},y_{2})\in R\big{)}\\}.$

We conclude this section by discussing how this view on bisimilarity can be
useful: first, it again opens up the possibility to compute bisimilarity – a
greatest fixpoint – by iterating from below, through smaller fixpoints. This
could potentially be useful if it is easy to compute the least fixpoint of
$\mathcal{B}$ inductively and continue from there.

Furthermore, we obtain a technique for witnessing non-bisimilarity of states.
While this can also be done by exhibiting a distinguishing modal formula
[hm:hm-logic, c:automatically-explaining-bisim] or by a winning strategy for
the spoiler in the bisimulation game [s:bisim-mc-other-games], to our
knowledge there is no known method that does this directly, based on the
definition of bisimilarity.

With our technique we can witness non-bisimilarity of two states
$x_{1},x_{2}\in X$ by presenting a pre-fixpoint $a$ (i.e., $\mathcal{B}(a)\leq
a$) such that $a(x_{1},x_{2})=0$ (equivalent to $(x_{1},x_{2})\in[{X\times
X}]_{a}$) and $\nu\mathcal{B}_{a}^{\\#}=\emptyset$, since this implies
$\nu\mathcal{B}(x_{1},x_{2})\leq a(x_{1},x_{2})=0$ by our proof rule.

There are two issues to discuss: first, how can we characterise a pre-fixpoint
of $\mathcal{B}$ (which is quite unusual, since bisimulations are post-
fixpoints)? In fact, the condition $\mathcal{B}(a)\leq a$ can be rewritten to:
for all $(x_{1},x_{2})\in[{X\times X}]_{a}$ there exists $y_{1}\in\eta(x_{1})$
such that for all $y_{2}\in\eta(x_{2})$ we have $(y_{1},y_{2})\in[{X\times
X}]_{a}$ (_or_ vice versa). Second, at first sight it does not seem as if we
gained anything since we still have to do a fixpoint computation on relations.
However, the carrier set is $[{X\times X}]_{a}$, i.e., a set of non-
bisimilarity witnesses and this set can be small even though $X$ might be
large.

######  Example 6.13.

We consider the transition system depicted below.

$x$$y$$u$

Our aim is to construct a witness showing that $x,u$ are not bisimilar. This
witness is a function $a\colon X\times X\to\\{0,1\\}$ with $a(x,u)=0=a(y,u)$
and for all other pairs the value is $1$. Hence $[{X\times
X}]_{a=\mathcal{B}(a)}=[{X\times X}]_{a}=\\{(x,u),(y,u)\\}$ and it is easy to
check that $a$ is a pre-fixpoint of $\mathcal{B}$ and that
$\nu\mathcal{B}_{a}^{*}=\emptyset$: we iterate over $\\{(x,u),(y,u)\\}$ and
first remove $(y,u)$ (since $y$ has no successors) and then $(x,u)$. This
implies that $\nu\mathcal{B}\leq a$ and hence $\nu\mathcal{B}(x,u)=0$, which
means that $x,u$ are not bisimilar.

######  Example 6.14.

We modify 6.13 and consider a function $a$ where $a(x,u)=0$ and all other
values are $1$. Again $a$ is a pre-fixpoint of $\mathcal{B}$ and
$\nu\mathcal{B}\leq a$ (since only reflexive pairs are in the bisimilarity).
However $\nu\mathcal{B}_{a}^{*}\neq\emptyset$, since $\\{(x,u)\\}$ is a post-
fixpoint. This is a counterexample to completeness discussed after subsection
4.2.

Intuitively speaking, the states $y,u$ over-approximate and claim that they
are bisimilar, although they are not. (This is permissible for a pre-
fixpoint.) This tricks $x,u$ into thinking that there is some wiggle room and
that one can increase the value of $(x,u)$. This is true, but only because of
the limited, local view, since the “true” value of $(y,u)$ is $0$.

###  6.4. Behavioural metrics for probabilistic automata

We now consider behavioural metrics for probabilistic automata, which involve
both non-deterministic branching (as in Section 6.2) as well as probabilistic
branching. Before we start, we first consider the Kantorovich lifting and the
corresponding approximation.

#### Kantorovich lifting.

The Kantorovich (also known as Wasserstein) lifting converts a metric on $X$
to a metric on probability distributions over $X$. As for the Hausdorff
lifting, we lift distance functions that are not necessarily metrics.

Furthermore, in order to ensure finiteness of all the sets involved, we
restrict to $D\subseteq\mathcal{D}(X)$, some finite set of probability
distributions over $X$. A _coupling_ of $p,q\in D$ is a probability
distribution $c\in\mathcal{D}(X\times X)$ whose left and right marginals are
$p,q$, i.e., $p(x_{1})=m_{c}^{L}(x_{1}):=\sum_{x_{2}\in X}c(x_{1},x_{2})$ and
$q(x_{2})=m_{c}^{R}(x_{2}):=\sum_{x_{1}\in X}c(x_{1},x_{2})$. The set of all
couplings of $p,q$, denoted by $\Omega(p,q)$, forms a polytope with finitely
many vertices [pc:computational-ot]. The set of all polytope vertices that are
obtained by coupling any $p,q\in D$ is also finite and is denoted by
$\mathit{VP}_{D}\subseteq\mathcal{D}(X\times X)$.

The Kantorovich lifting is given by $\mathcal{K}:[0,1]^{X\times
X}\to[0,1]^{D\times D}$ where

$\mathcal{K}(d)(p,q)=\min_{c\in\Omega(p,q)}\sum_{(x_{1},x_{2})\in X\times
X}c(x_{1},x_{2})\cdot d(x_{1},x_{2}).$

The coupling $c$ can be interpreted as the optimal transport plan to move
goods from suppliers to customers [v:optimal-transport]. Again we provide an
alternative characterisation, which shows non-expansiveness of $\mathcal{K}$
and allows one to derive its approximations.

Let $u:\mathit{VP}_{D}\to D\times D$, $u(c)=(m_{c}^{L},m_{c}^{R})$. Then

$\mathcal{K}=\min\nolimits_{u}\circ\mathrm{av}_{\mathit{VP}_{D}}$

where $\mathrm{av}_{\mathit{VP}_{D}}\colon[0,1]^{X\times
X}\to[0,1]^{\mathit{VP}_{D}}$,
$\min_{u}\colon[0,1]^{\mathit{VP}_{D}}\to[0,1]^{D\times D}$.

######  Proof 6.15.

It holds that $u^{-1}(p,q)=\Omega(p,q)\cap\textit{VP}_{D}$ for $p,q\in D$.
Furthermore note it is sufficient to consider as couplings the vertices, i.e.,
the elements of $\mathit{VP}_{D}$, since the minimum is always attained there
[pc:computational-ot].

Hence we obtain for $d\colon X\times X\to[0,1]$, $p,q\in D$:

$\displaystyle\min\nolimits_{u}(\mathrm{av}_{\mathit{VP}_{D}}(d))(p,q)$
$\displaystyle=$
$\displaystyle\min_{c\in\Omega(p,q)\cap\mathit{VP}_{D}}\mathrm{av}_{\mathit{VP}_{D}}(d)(c)$
$\displaystyle=$
$\displaystyle\min_{c\in\Omega(p,q)\cap\mathit{VP}_{D}}\sum_{x_{1},x_{2}\in
X\times X}c(x_{1},x_{2})\cdot d(x_{1},x_{2})$ $\displaystyle=$
$\displaystyle\min_{c\in\Omega(p,q)}\sum_{x_{1},x_{2}\in X\times
X}c(x_{1},x_{2})\cdot d(x_{1},x_{2})$ $\displaystyle=$
$\displaystyle\mathcal{K}(d)(p,q)$

We now present the approximation of the Kantorovich lifting in the dual sense.
Intuitively, given a distance function $d$ and a relation $M$ on $X$ it
characterises those pairs $(p,q)$ of distributions whose distance in the
Kantorovich metric decreases by a constant when we decrease the distance $d$
for all pairs in $M$ by the same constant.

######  Lemma 6.16.

Let $d\colon X\times X\to[0,1]$. The approximation for the Kantorovich lifting
$\mathcal{K}$ in the dual sense is
$\mathcal{K}_{\\#}^{d}\colon\mathbf{2}^{[{X\times
X}]^{d}}\to\mathbf{2}^{[{D\times D}]^{\mathcal{K}(d)}}$ with

$\displaystyle\mathcal{K}_{\\#}^{d}(M)$ $\displaystyle=$
$\displaystyle\\{(p,q)\in[{D\times D}]^{\mathcal{K}(d)}\mid\exists
c\in\Omega(p,q),\mathit{supp}(c)\subseteq M,$ $\displaystyle\qquad\sum_{u,v\in
S}d(u,v)\cdot c(u,v)=\mathcal{K}(d)(p,q)\\}.$

######  Proof 6.17.

Let $d\colon X\times X\to[0,1]$ and $M\subseteq[{X\times X}]^{d}$. Then we
have:

$\displaystyle\mathcal{K}_{\\#}^{d}(M)$ $\displaystyle=$
$\displaystyle(\min\nolimits_{u})_{\\#}^{\mathrm{av}_{\mathit{VP}_{D}}(d)}((\mathrm{av}_{\mathit{VP}_{D}})_{\\#}^{d}(M))$

where

$\displaystyle(\mathrm{av}_{\mathit{VP}_{D}})_{\\#}^{d}\colon\mathbf{2}^{[{X\times
X}]^{d}}\to\mathbf{2}^{[{\mathit{VP}_{D}}]^{\mathrm{av}_{\mathit{VP}_{D}}(d)}}$
$\displaystyle(\min\nolimits_{u})_{\\#}^{\mathrm{av}_{\mathit{VP}_{D}}^{X\times
X}(d)}\colon\mathbf{2}^{[{\mathit{VP}_{D}}]^{\mathrm{av}_{\mathit{VP}_{D}}(d)}}\to\mathbf{2}^{[{D\times
D}]^{\mathcal{K}(d)}}$

We are using the approximations associated to non-expansive functions, given
in 5.4, and obtain:

$\displaystyle\mathcal{K}_{\\#}^{d}(M)$ $\displaystyle=$
$\displaystyle\\{(p,q)\in[{D\times
D}]^{\mathcal{K}(d)}\mid\mathit{Min}_{\mathrm{av}_{\mathit{VP}_{D}}^{X\times
X}(d)|_{u^{-1}(p,q)}}\cap(\mathrm{av}_{\mathit{VP}_{D}}^{X\times
X})_{\\#}^{d}(M)\neq\emptyset\\}$ $\displaystyle=$
$\displaystyle\\{(p,q)\in[{D\times D}]^{\mathcal{K}(d)}\mid\exists
c\in\Omega(p,q),c\in(\mathrm{av}_{\mathit{VP}_{D}})_{\\#}^{d}(M),$
$\displaystyle\qquad\mathrm{av}_{\mathit{VP}_{D}}(d)(c)=\min_{c^{\prime}\in\Omega(p,q)}\mathrm{av}_{\mathit{VP}_{D}}^{X\times
X}(d)(c^{\prime})\\}$ $\displaystyle=$ $\displaystyle\\{(p,q)\in[{D\times
D}]^{\mathcal{K}(d)}\mid\exists
c\in\Omega(p,q),c\in(\mathrm{av}_{\mathit{VP}_{D}})_{\\#}^{d}(M),$
$\displaystyle\qquad\mathrm{av}_{\mathit{VP}_{D}}(d)(c)=\mathcal{K}(d)(p,q)\\}$
$\displaystyle=$ $\displaystyle\\{(p,q)\in[{D\times
D}]^{\mathcal{K}(d)}\mid\exists c\in\Omega(p,q),\mathit{supp}(c)\subseteq M,$
$\displaystyle\qquad\sum_{u,v\in S}d(u,v)\cdot c(u,v)=\mathcal{K}(d)(p,q)\\}$

#### Probabilistic automata.

We now compare our approach with [bblmtv:prob-bisim-distance-automata], which
describes the first method for computing behavioural distances for
probabilistic automata. Although the behavioural distance arises as a least
fixpoint, it is in fact better, even the only known method, to iterate from
above, in order to reach this least fixpoint. This is done by guessing and
improving couplings, similarly to what happens for strategy iteration
discussed later in Section 7. A major complication, faced in [bblmtv:prob-
bisim-distance-automata], is that the procedure can get stuck at a fixpoint
which is not the least and one has to determine that this is the case and
decrease the current candidate. In fact this paper was our inspiration to
generalise this technique to a more general setting.

A _probabilistic automaton_ is a tuple $\mathcal{A}=(S,L,\eta,\ell)$, where
$S$ is a non-empty finite set of states, $L$ is a finite set of labels,
$\eta\colon S\to\mathbf{2}^{\mathcal{D}(S)}$ assigns finite sets of
probability distributions to states and $\ell\colon S\to L$ is a labelling
function. (In the following we again replace $\mathcal{D}(S)$ by a finite
subset $D$.)

The _probabilistic bisimilarity pseudo-metrics_ is the least fixpoint of the
function $\mathcal{M}\colon$ $[0,1]^{S\times S}\to[0,1]^{S\times S}$ where for
$d\colon S\times S\to[0,1]$, $s,t\in S$:

$\mathcal{M}(d)(s,t)=\begin{cases}1&\mbox{if $\ell(s)\neq\ell(t)$}\\\
\mathcal{H}(\mathcal{K}(d))(\eta(s),\eta(t))&\mbox{otherwise}\end{cases}$

where $\mathcal{H}$ is the Hausdorff lifting (for $\mathbb{M}=[0,1]$) and
$\mathcal{K}$ is the Kantorovich lifting defined earlier. Now assume that $d$
is a fixpoint of $\mathcal{M}$, i.e., $d=\mathcal{M}(d)$. In order to check
whether $d=\mu f$, [bblmtv:prob-bisim-distance-automata] adapts the notion of
a self-closed relation from [f:game-metrics-markov-decision].

######  Definition 6.18 ([bblmtv:prob-bisim-distance-automata]).

A relation $M\subseteq S\times S$ is _self-closed_ with respect to
$d=\mathcal{M}(d)$ if, whenever $s\,M\,t$, then

  * •

$\ell(s)=\ell(t)$ and $d(s,t)>0$,

  * •

if $p\in\eta(s)$ and
$d(s,t)=\min_{q^{\prime}\in\eta(t)}\mathcal{K}(d)(p,q^{\prime})$, then there
exists $q\in\eta(t)$ and $c\in\Omega(p,q)$ such that $d(s,t)=\sum_{u,v\in
S}d(u,v)\cdot c(u,v)$ and $\mathit{supp}(c)\subseteq M$,

  * •

if $q\in\eta(t)$ and
$d(s,t)=\min_{p^{\prime}\in\eta(s)}\mathcal{K}(d)(p^{\prime},q)$, then there
exists $p\in\eta(s)$ and $c\in\Omega(p,q)$ such that $d(s,t)=\sum_{u,v\in
S}d(u,v)\cdot c(u,v)$ and $\mathit{supp}(c)\subseteq M$.

The largest self-closed relation, denoted by $\approx_{d}$ is empty if and
only if $d=\mu f$ [bblmtv:prob-bisim-distance-automata]. We now investigate
the relation between self-closed relations and post-fixpoints of
approximations. For this we will first show that $\mathcal{M}$ can be obtained
as the composition of non-expansive functions, which proves that it is indeed
non-expansive. Furthermore, this decomposition will help in the comparison.

The fixpoint function $\mathcal{M}$ characterizing probabilistic bisimilarity
pseudo-metrics can be written as:

$\mathcal{M}=\max\nolimits_{\rho}\circ(((\eta\times\eta)^{*}\circ\mathcal{H}\circ\mathcal{K})\uplus
c_{l})$

where $\rho\colon(S\times S)\uplus(S\times S)\to(S\times S)$ with
$\rho((s,t),i)=(s,t)$. Furthermore $l\colon S\times S\to[0,1]$ is defined as
$l(s,t)=0$ if $\ell(s)=\ell(t)$ and $l(s,t)=1$ if $\ell(s)\neq\ell(t)$.

######  Proof 6.19.

In fact, given $d\colon S\times S\to[0,1]$, we have

$\displaystyle\max\nolimits_{\rho}((((\eta\times\eta)^{*}\circ\mathcal{H}\circ\mathcal{K})\uplus
c_{l})(d))(s,t)$ $\displaystyle=$
$\displaystyle\max\\{(\eta\times\eta)^{*}\circ\mathcal{H}\circ\mathcal{K})(d)(s,t),c_{l}(s,t)\\}$
$\displaystyle=$
$\displaystyle\max\\{\mathcal{H}(\mathcal{K}(d)(\eta(s),\eta(t)),c_{l}(s,t)\\}$
$\displaystyle=$ $\displaystyle\mathcal{M}(d)(s,t)$

Hence $\mathcal{M}$ is a composition of non-expansive functions and thus non-
expansive itself. We do not spell out $\mathcal{M}_{\\#}^{d}$ explicitly, but
instead show how it is related to self-closed relations.

Let $d\colon S\times S\to[0,1]$ where $d=\mathcal{M}(d)$. Then
$\mathcal{M}_{\\#}^{d}\colon\mathbf{2}^{[{S\times
S}]^{d}}\to\mathbf{2}^{[{S\times S}]^{d}}$, where $[{S\times
S}]^{d}=\\{(s,t)\in S\times S\mid d(s,t)>0\\}$.

Then $M$ is a self-closed relation with respect to $d$ if and only if
$M\subseteq[{S\times S}]^{d}$ and $M$ is a post-fixpoint of
$\mathcal{M}_{\\#}^{d}$.

######  Proof 6.20.

First note that whenever $M$ is self-closed, it holds that $d(s,t)>0$ for all
$(s,t)\in M$ and hence $M\subseteq[{S\times S}]^{d}$.

We abbreviate
$g=(\eta\times\eta)^{*}\circ\mathcal{H}\circ\mathcal{K}\colon[0,1]^{S\times
S}\to[0,1]^{S\times S}$ and hence $\mathcal{M}=\max_{\rho}\circ(g\uplus
c_{l})$.

The approximation $g_{\\#}^{d}$ (yet to be determined) is of type
$g_{\\#}^{d}\colon\mathbf{2}^{[{S\times S}]^{d}}\to\mathbf{2}^{[{S\times
S}]^{g(d)}}$. In the following, we are using the approximations associated to
non-expansive functions, given in 5.4.

Since $c_{l}\colon[0,1]^{S\times S}\to[0,1]^{S\times S}$ is a constant
function, we have

$(c_{l})_{\\#}^{d}\colon\mathbf{2}^{[{S\times S}]^{d}}\to\mathbf{2}^{[{S\times
S}]^{l}},\quad(c_{l})_{\\#}^{d}(M)=\emptyset.$

Hence

$\displaystyle(g\uplus c_{l})_{\\#}^{d}\colon\mathbf{2}^{[{S\times S}]^{d}}$
$\displaystyle\to$ $\displaystyle\mathbf{2}^{[{S\times
S}]^{g(d)}\uplus[{S\times S}]^{l}}$ $\displaystyle(g\uplus
c_{l})_{\\#}^{d}(M)$ $\displaystyle=$ $\displaystyle
g_{\\#}^{d}(M)\times\\{0\\}\cup\emptyset\times\\{1\\}=g_{\\#}^{d}(M)\times\\{0\\}$

for $M\subseteq[{S\times S}]^{d}$.

Furthermore we obtain

$\displaystyle\mathcal{M}_{\\#}^{d}(M)$ $\displaystyle=$
$\displaystyle(\max\nolimits_{\rho})_{\\#}^{g(d)\uplus l}((g\uplus
c_{l})_{\\#}^{d}(M))$ $\displaystyle=$
$\displaystyle(\max\nolimits_{\rho})_{\\#}^{g(d)\uplus
l}(g_{\\#}^{d}(M)\times\\{0\\})$ $\displaystyle=$
$\displaystyle\\{(s,t)\in[{S\times
S}]^{\mathcal{M}(d)}\mid\mathit{Max}_{(g(d)\uplus
c_{l})|_{\rho^{-1}(\\{(s,t)\\})}}\subseteq g_{\\#}^{d}(M)\times\\{0\\}\\}$

In order to proceed, we examine
$\rho^{-1}(\\{(s,t)\\}=\\{((s,t),0),((s,t),1)\\}$. Whenever
$\ell(s)\neq\ell(t)$, we have $c_{l}(s,t)=1\geq g(d)(s,t)$, hence
$\mathit{Max}_{(g(d)\uplus l)|_{\rho^{-1}(\\{(s,t)\\})}}$ contains at least
$((s,t),1)$, which is not contained in $g_{\\#}^{d}(M)\times\\{0\\}$, which
means that the condition is not satisfied.

Whenever $\ell(s)=\ell(t)$, we have $c_{l}(s,t)=0<g(d)(s,t)$ (note that
$(s,t)\in[{S\times S}]^{\mathcal{M}(d)}$, hence $g(d)(s,t)>0$), so
$\mathit{Max}_{(g(d)\uplus l)|_{\rho^{-1}(\\{(s,t)\\})}}$ contains only
$((s,t),0)$, which is contained in $g_{\\#}^{d}(M)\times\\{0\\}$ iff $(s,t)\in
g_{\\#}^{d}(M)$.

Summarizing, we obtain

$\displaystyle\mathcal{M}_{\\#}^{d}(M)$ $\displaystyle=$
$\displaystyle\\{(s,t)\in[{S\times
S}]^{\mathcal{M}(d)}\mid\ell(s)=\ell(t),(s,t)\in g_{\\#}^{d}(M)\\}$
$\displaystyle=$ $\displaystyle\\{(s,t)\in S\times S\mid
d(s,t)>0,\ell(s)=\ell(t),(s,t)\in g_{\\#}^{d}(M)\\}$

For the last step observe that $d=\mathcal{M}(d)$.

It is left to characterise $g_{\\#}^{d}$, where
$g=(\eta\times\eta)^{*}\circ\mathcal{H}\circ\mathcal{K}$. We have

$g_{\\#}^{d}=((\eta\times\eta)^{*})_{\\#}^{\mathcal{H}(\mathcal{K}(d))}\circ\mathcal{H}_{\\#}^{\mathcal{K}(d)}\circ\mathcal{K}_{\\#}^{d}$

where

$\displaystyle\mathcal{K}_{\\#}^{d}\colon\mathbf{2}^{[{S\times S}]^{d}}$
$\displaystyle\to$ $\displaystyle\mathbf{2}^{[{D\times D}]^{\mathcal{K}(d)}}$
$\displaystyle\mathcal{H}_{\\#}^{\mathcal{K}(d)}\colon\mathbf{2}^{[{D\times
D}]^{\mathcal{K}(d)}}$ $\displaystyle\to$
$\displaystyle\mathbf{2}^{[{\mathbf{2}^{D}\times\mathbf{2}^{D}}]^{\mathcal{H}(\mathcal{K}(d))}}$
$\displaystyle((\eta\times\eta)^{*})_{\\#}^{\mathcal{H}(\mathcal{K}(d))}\colon\mathbf{2}^{[{\mathbf{2}^{D}\times\mathbf{2}^{D}}]^{\mathcal{H}(\mathcal{K}(d))}}$
$\displaystyle\to$ $\displaystyle\mathbf{2}^{[{S\times S}]^{g(d)}}.$

It holds that
$((\eta\times\eta)^{*})_{\\#}^{\mathcal{H}(\mathcal{K}(d))}=(\eta\times\eta)^{-1}$
and hence

$(s,t)\in
g_{\\#}^{d}(M)\iff(\eta(s),\eta(t))\in\mathcal{H}_{\\#}^{\mathcal{K}(d)}(\mathcal{K}_{\\#}^{d}(M)).$

Using the characterisation of the associated approximation of the Hausdorff
lifting in subsection 6.2, we obtain that this is equivalent to

for all $p\in\eta(s)$, whenever
$\min_{q^{\prime}\in\eta(t)}\mathcal{K}(d)(p,q^{\prime})=\mathcal{H}(\mathcal{K}(d))(\eta(s),\eta(t))$,
then there exists $q\in\eta(t)$ such that $(p,q)\in\mathcal{K}_{\\#}^{d}(M)$
and $\mathcal{K}(d)(p,q)=\mathcal{H}(\mathcal{K}(d))(\eta(s),\eta(t))$ (and
vice versa),

assuming that $\ell(s)=\ell(t)$ (this is a requirement in the definition of
$\mathcal{M}_{\\#}^{d}(M)$), since then we have
$\mathcal{H}(\mathcal{K}(d))(\eta(s),\eta(t))=d(s,t)>0$ and hence
$(\eta(s),\eta(t))\in[{\mathbf{2}^{D}\times\mathbf{2}^{D}}]^{\mathcal{H}(\mathcal{K}(d))}$.

Since also $d=\mathcal{M}(d)$, the condition above can be rewritten to

for all $p\in\eta(s)$, whenever
$\min_{q^{\prime}\in\eta(t)}\mathcal{K}(d)(p,q^{\prime})=d(s,t)$, then there
exists $q\in\eta(t)$ such that $(p,q)\in\mathcal{K}_{\\#}^{d}(M)$ and
$\mathcal{K}(d)(p,q)=d(s,t)$ (and vice versa).

From 6.16 we know that $(p,q)\in\mathcal{K}_{\\#}^{d}(M)$ iff
$\mathcal{K}(d)(p,q)>0$ and there exists $c\in\Omega(p,q)$ such that
$\mathit{supp}(c)\subseteq M$ and $\sum_{u,v\in S}c(u,v)\cdot
d(u,v)=\mathcal{K}(d)(p,q)$. We instantiate the condition above accordingly
and obtain

for all $p\in\eta(s)$, whenever
$d(s,t)=\min_{q^{\prime}\in\eta(t)}\mathcal{K}(d)(p,q^{\prime})$, then there
exists $q\in\eta(t)$ such that there exists $c\in\Omega(p,q)$ with
$\mathit{supp}(c)\subseteq M$, $\mathcal{K}(d)(p,q)=\sum_{u,v\in S}c(u,v)\cdot
d(u,v)$ and $\mathcal{K}(d)(p,q)=d(s,t)$ (and vice versa).

The two last equalities can be simplified to $d(s,t)=\sum_{u,v\in
S}c(u,v)\cdot d(u,v)$, since

$\mathcal{K}(d)(p,q)\leq\sum_{u,v\in S}c(u,v)\cdot
d(u,v)=d(s,t)=\min_{q^{\prime}\in\eta(t)}\mathcal{K}(d)(p,q^{\prime})\leq\mathcal{K}(d)(p,q)$

and hence $\mathcal{K}(d)(p,q)=d(s,t)$ can be inferred from the remaining
conditions.

We finally obtain the following equivalent characterisation:

for all $p\in\eta(s)$, whenever
$d(s,t)=\min_{q^{\prime}\in\eta(t)}\mathcal{K}(d)(p,q^{\prime})$, then there
exists $q\in\eta(t)$ such that there exists $c\in\Omega(p,q)$ with
$\mathit{supp}(c)\subseteq M$, $d(s,t)=\sum_{u,v\in S}c(u,v)\cdot d(u,v)$ (and
vice versa).

Hence we obtain that $(s,t)\in g_{\\#}^{d}(M)$ is equivalent to the the second
and third item of Def. 6.18 (under the assumption that $\ell(s)=\ell(t)$),
while the first item is covered by the other conditions ($d(s,t)>0$ and
$\ell(s)=\ell(t)$) in the characterisation of $\mathcal{M}_{\\#}^{d}(M)$.

##  7\. Simple stochastic games

In this section we show how our techniques can be applied to simple stochastic
games [condon92, c:algorithms-ssg]. In particular, we present two novel
algorithms based on strategy iteration and discuss some runtime results.

###  7.1. Introduction to simple stochastic games.

A simple stochastic game is a state-based two-player game where the two
players, Min and Max, each own a subset of states they control, for which they
can choose the successor. The system also contains sink states with an
assigned payoff and averaging states which randomly choose their successor
based on a given probability distribution. The goal of Min is to minimise and
the goal of Max to maximise the payoff.

Simple stochastic games are an important type of games that subsume parity
games and the computation of behavioural distances for probabilistic automata
(cf. Section 6.4, [bblmtv:prob-bisim-distance-automata]). The associated
decision problem (if both players use their best strategies, is the expected
payoff of Max greater than $\frac{1}{2}$?) is known to lie in
$\mathsf{NP}\cap\mathsf{coNP}$, but it is an open question whether it is
contained in $\mathsf{P}$. There are known randomised subexponential
algorithms [bv:randomized-algorithms-games].

It has been shown that it is sufficient to consider positional strategies,
i.e., strategies where the choice of the player is only dependent on the
current state. The expected payoffs for each state form a so-called value
vector and can be obtained as the least solution of a fixpoint equation (see
below).

A _simple stochastic game_ is given by a finite set $V$ of nodes, partitioned
into $\mathit{MIN}$, $\mathit{MAX}$, $\mathit{AV}$ (average) and
$\mathit{SINK}$, and the following data:
$\eta_{\min}:\mathit{MIN}\to\mathbf{2}^{V}$,
$\eta_{\max}:\mathit{MAX}\to\mathbf{2}^{V}$ (successor functions for Min and
Max nodes), $\eta_{\mathrm{av}}:\mathit{AV}\to D$ (probability distributions,
where $D\subseteq\mathcal{D}(V)$ finite) and $w:\mathit{SINK}\to[0,1]$
(weights of sink nodes).

The fixpoint function $\mathcal{V}\colon[0,1]^{V}\to[0,1]^{V}$ is defined
below for $a\colon V\to[0,1]$ and $v\in V$:

$\displaystyle\mathcal{V}(a)(v)=\begin{cases}\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})&v\in\mathit{MIN}\\\
\max_{v^{\prime}\in\eta_{\max}(v)}a(v^{\prime})&v\in\mathit{MAX}\\\
\sum_{v^{\prime}\in V}\eta_{\mathrm{av}}(v)(v^{\prime})\cdot
a(v^{\prime})&v\in\mathit{AV}\\\ w(v)&v\in\mathit{SINK}\end{cases}$

The _least_ fixpoint of $\mathcal{V}$ specifies the average payoff for all
nodes when Min and Max play optimally. In an infinite game the payoff is $0$.
In order to avoid infinite games and guarantee uniqueness of the fixpoint,
many authors [hk:nonterminating-stochastic-games, c:algorithms-ssg,
tvk:strategy-improvement-ssg] restrict to stopping games, which are guaranteed
to terminate for every pair of Min/Max-strategies. Here we deal with general
games where more than one fixpoint may exist. Such a scenario has been studied
in [kkkw:value-iteration-ssg], which considers value iteration to under- and
over-approximate the value vector. The over-approximation faces challenges
with cyclic dependencies, similar to the vicious cycles described earlier.
Here we focus on strategy iteration, which is usually less efficient than
value iteration, but yields a precise result instead of approximating it.

######  Example 7.1.

We consider the game depicted below. Here $\min$ is a Min node with
$\eta_{\min}(\min)=\\{\textbf{1},\mathrm{av}\\}$, $\max$ is a Max node with
$\eta_{\max}(\max)=\\{\bm{\varepsilon},\mathrm{av}\\}$, 1 is a sink node with
payoff 1, $\bm{\varepsilon}$ is a sink node with some small payoff
$\varepsilon\in(0,1)$ and $\mathrm{av}$ is an average node which transitions
to both $\min$ and $\max$ with probability $\frac{1}{2}$.

Min should choose $\mathrm{av}$ as successor since a payoff of $1$ is bad for
Min. Given this choice of Min, Max should not declare $\mathrm{av}$ as
successor since this would create an infinite play and hence the payoff is
$0$. Therefore Max has to choose $\bm{\varepsilon}$ and be content with a
payoff of $\varepsilon$, which is achieved from all nodes different from
$\bm{1}$.

1
---
$\min$
---
$\mathrm{av}$
---
$\bm{\varepsilon}$
---
$\max$
---
$\frac{1}{2}$$\frac{1}{2}$

In order to be able to determine the approximation of $\mathcal{V}$ and to
apply our techniques, we consider the following equivalent definition.

$\mathcal{V}=(\eta_{\min}^{*}\circ\min\nolimits_{\in})\uplus(\eta_{\max}^{*}\circ\max\nolimits_{\in})\uplus(\eta_{\mathrm{av}}^{*}\circ\mathrm{av}_{D})\uplus
c_{w}$, where $\mathrel{\in}\ \subseteq V\times\mathbf{2}^{V}$ is the “is-
element-of”-relation on $V$.

######  Proof 7.2.

Let $a\colon V\to[0,1]$. For $v\in\mathit{MAX}$ we have

$\mathcal{V}(a)(v)=(\eta^{*}_{\max}\circ\max\nolimits_{\in})(a)(v)=\max\nolimits_{\in}(a)(\eta_{\max}(v))=\max_{v^{\prime}\in\eta_{\max}(v)}a(v^{\prime}).$

For $v\in\mathit{MIN}$ we have

$\mathcal{V}(a)(v)=(\eta^{*}_{\min}\circ\min\nolimits_{\in})(a)(v)=\min\nolimits_{\in}(a)(\eta_{\min}(v))=\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime}).$

For $v\in\mathit{AV}$ we have

$\mathcal{V}(a)(v)=(\eta^{*}_{\mathrm{av}}\circ\mathrm{av}_{D})(a)(v)=\mathrm{av}_{D}(a)(\eta_{\mathrm{av}}(v))=\sum_{v^{\prime}\in
V}\eta_{\mathrm{av}}(v)(v^{\prime})\cdot a(v^{\prime}).$

For $v\in\mathit{SINK}$ we have $\mathcal{V}(a)(v)=c_{w}(a)(v)=w(v)$.

As a composition of non-expansive functions, $\mathcal{V}$ is non-expansive as
well. Since we are interested in the least fixpoint we work in the dual sense
and obtain the following approximation, which intuitively says: we can
decrease a value at node $v$ by a constant only if, in the case of a Min node,
we decrease the value of one successor where the minimum is reached, in the
case of a Max node, we decrease the values of all successors where the maximum
is reached, and in the case of an average node, we decrease the values of all
successors.

Let $a\colon V\to[0,1]$. The approximation for the value iteration function
$\mathcal{V}$ in the dual sense is
$\mathcal{V}_{\\#}^{a}\colon\mathbf{2}^{[{V}]^{a}}\to\mathbf{2}^{[{V}]^{\mathcal{V}(a)}}$
with

$\displaystyle\mathcal{V}_{\\#}^{a}(V^{\prime})$ $\displaystyle=$
$\displaystyle\\{v\in[{V}]^{\mathcal{V}(a)}\mid\big{(}v\in\mathit{MIN}\land\mathit{Min}_{a_{|\eta_{\min}(v)}}\cap
V^{\prime}\not=\emptyset\big{)}\mathop{\lor}$
$\displaystyle\quad\big{(}v\in\mathit{MAX}\land\mathit{Max}_{a_{|\eta_{\max}(v)}}\subseteq
V^{\prime}\big{)}\lor\big{(}v\in\mathit{AV}\land\mathit{supp}(\eta_{\mathrm{av}}(v))\subseteq
V^{\prime}\big{)}\\}$

######  Proof 7.3.

Let $a\colon V\to[0,1]$ and $V^{\prime}\subseteq[{V}]^{a}$. By Proposition
5.10 we have:

$\displaystyle\mathcal{V}_{\\#}^{a}(V^{\prime})=$
$\displaystyle\big{(}\mathit{MIN}\cap(\eta^{*}_{\min}\circ\min\nolimits_{\in})^{a}_{\\#}(V^{\prime})\big{)}\cup\big{(}\mathit{MAX}\cap(\eta^{*}_{\max}\circ\max\nolimits_{\in})^{a}_{\\#}(V^{\prime})\big{)}\cup$
$\displaystyle\big{(}\mathit{AV}\cap(\eta^{*}_{\mathrm{av}}\circ\mathrm{av}_{D})^{a}_{\\#}(V^{\prime})\big{)}\cup\big{(}\mathit{SINK}\cap(c_{w})_{\\#}^{a}(V^{\prime})\big{)}$

It holds that
$({\eta^{*}_{\min}})_{\\#}^{\min\nolimits_{\in}(v)}=\eta^{-1}_{\min}$,
$({\eta^{*}_{\max}})_{\\#}^{\max\nolimits_{\in}(v)}=\eta^{-1}_{\max}$ and
$({\eta^{*}_{\mathrm{av}}})_{\\#}^{\mathrm{av}_{D}(v)}=\eta^{-1}_{\mathrm{av}}$.
Using previous results (5.4) we deduce

$\displaystyle
v\in(\eta^{*}_{\min}\circ\min\nolimits_{\in})^{a}_{\\#}(V^{\prime})\Leftrightarrow\eta_{\min}(v)\in(\min\nolimits_{\in})^{a}_{\\#}(V^{\prime})\Leftrightarrow\mathit{Min}_{a_{|\eta_{\min}(v)}}\cap
V^{\prime}\not=\emptyset$ $\displaystyle
v\in(\eta^{*}_{\max}\circ\max\nolimits_{\in})^{a}_{\\#}(V^{\prime})\Leftrightarrow\eta_{\max}(v)\in(\max\nolimits_{\in})^{a}_{\\#}(V^{\prime})\Leftrightarrow\mathit{Max}_{a_{|\eta_{\max}(v)}}\subseteq
V^{\prime}$ $\displaystyle
v\in(\eta^{*}_{\mathrm{av}}\circ{\mathrm{av}^{V}_{D}})_{\\#}^{a}(V^{\prime})\Leftrightarrow\eta_{\mathrm{av}}(v)\in(\mathrm{av}^{V}_{D})^{a}_{\\#}(V^{\prime})\Leftrightarrow\mathit{supp}(\eta_{\mathrm{av}}(v))\subseteq
V^{\prime}$

Lastly $(c_{w})^{a}_{\\#}(V^{\prime})=\emptyset$ for any $V^{\prime}\subseteq
V$ since $c_{w}$ is a constant function which concludes the proof.

###  7.2. Strategy iteration from above and below.

We describe two algorithms based on the idea of strategy iteration, first
introduced by Hoffman and Karp in [hk:nonterminating-stochastic-games], that
are novel, as far as we know. The first iterates to the least fixpoint from
above and uses the techniques described in Section 4 in order not to get stuck
at a larger fixpoint. The second iterates from below: the role of our results
is not directly visible in the code of the algorithm, but its non-trivial
correctness proof is based on the proof rule introduced earlier.

We first recap the underlying notions. A Min-strategy is a mapping
$\tau\colon\mathit{MIN}\to V$ such that $\tau(v)\in\eta_{\mathrm{min}}(v)$ for
every $v\in\mathit{MIN}$. Following such a strategy, Min decides to always
leave a node $v$ via $\tau(v)$. Analogously, a Max-strategy is a function
$\sigma\colon\mathit{MAX}\to V$. Fixing a strategy for either player induces a
modified value function. If $\tau$ is a Min-strategy, we obtain
$\mathcal{V}_{\tau}$ which is defined exactly as $\mathcal{V}$ but for
$v\in\mathit{MIN}$ where we set $\mathcal{V}_{\tau}(a)(v)=a(\tau(v))$.
Analogously, for $\sigma$ a Max-strategy, $\mathcal{V}_{\sigma}$ is obtained
by setting $\mathcal{V}_{\sigma}(a)(v)=a(\sigma(v))$ when $v\in\mathit{MAX}$.
If both players fix their strategies, the game reduces to a Markov chain.

######  Lemma 7.4.

For any pair of strategies $\sigma,\tau$ we have
$\mathcal{V}_{\sigma}\leq\mathcal{V}\leq\mathcal{V}_{\tau}$.

######  Proof 7.5.

Given any $a\colon V\to[0,1]$ and $v\in V$, we have

$\displaystyle\mathcal{V}_{\sigma}(a)(v)$
$\displaystyle=\begin{cases}\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})&v\in\mathit{MIN}\\\
a(\sigma(v^{\prime}))&v\in\mathit{MAX}\\\ \sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV}\\\
c_{w}(v)&v\in\mathit{SINK}\end{cases}$
$\displaystyle\leq\begin{cases}\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})&v\in\mathit{MIN}\\\
\max_{v^{\prime}\in\eta_{\max}(v)}a(v^{\prime})&v\in\mathit{MAX}\\\
\sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV}\\\
c_{w}(v)&v\in\mathit{SINK}\end{cases}$ $\displaystyle=\mathcal{V}(a)(v)$

The same proof idea can be applied to show
$\mathcal{V}\leq\mathcal{V}_{\tau}$.

In order to describe our algorithms we also need the notion of a _switch_.
Assume that $\tau$ is a Min-strategy and let $a$ be a (pre-)fixpoint of
$\mathcal{V}_{\tau}$. Min can now potentially improve her strategy for nodes
$v\in\mathit{MIN}$ where
$\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})<a(\tau(v))$, called _switch
nodes_. This results in a Min-strategy
$\tau^{\prime}=\mathit{sw}_{\min}(\tau,a)$, where444If the minimum is achieved
in several nodes, Min simply chooses one of them. However, she will only
switch if this strictly improves the value.
$\tau^{\prime}(v)=\text{arg}\min_{v^{\prime}\in\eta_{\min}(v)}a^{(i)}(v^{\prime})$
for a switch node $v$ and $\tau^{\prime}$, $\tau$ agree otherwise. Also,
$\mathit{sw}_{\max}(\sigma,a)$ is defined analogously for Max strategies.

Determine $\mu\mathcal{V}$ (from above)

(1) Guess a Min-strategy $\tau^{(0)}$, $i:=0$ (2)
$a^{(i)}:=\mu\mathcal{V}_{\tau^{(i)}}$ (3)
$\tau^{(i+1)}:=\mathit{sw}_{\min}(\tau^{(i)},a^{(i)})$ (4) If
$\tau^{(i+1)}\neq\tau^{(i)}$ $i:=i+1$ then goto 2. (5) Compute
$V^{\prime}=\nu\mathcal{V}_{\\#}^{a}$, where $a=a^{(i)}$. (6) If
$V^{\prime}=\emptyset$ then stop and return $a^{(i)}$.
Otherwise set
$a^{(i+1)}:=a-(\iota_{\mathcal{V}}^{a}(V^{\prime}))_{V^{\prime}}$,
$\tau^{(i+2)}:=\mathit{sw}_{\min}(\tau^{(i)},a^{(i+1)})$, $i:=i+2$, goto 2 (a)
Strategy iteration from above

Determine $\mu\mathcal{V}$ (from below)

(1) Guess a Max-strategy $\sigma^{(0)}$, $i:=0$ (2)
$a^{(i)}:=\mu\mathcal{V}_{\sigma^{(i)}}$ (3)
$\sigma^{(i+1)}:=\mathit{sw}_{\max}(\sigma^{(i)},a^{(i)})$ (4) If
$\sigma^{(i+1)}\neq\sigma^{(i)}$ then
set $i:=i+1$ and goto 2
Otherwise stop and return $a^{(i)}$. (b) Strategy iteration from below

Figure 3. Strategy iteration from above and below

Now strategy iteration from above works as described in Fig. 3(a). The
computation of $\mu\mathcal{V}_{\tau^{(i)}}$ in the second step intuitively
means that Max chooses his best answering strategy and we compute the least
fixpoint based on this answering strategy. At some point no further switches
are possible and we have reached a fixpoint $a$, which need not yet be the
least fixpoint. Hence we use the techniques from Section 4 to decrease $a$ and
obtain a new pre-fixpoint $a^{(i+1)}$, from which we can continue. The
correctness of this procedure partially follows from 4.2 and 4.5, however we
also need to show the following: first, we can compute
$a^{(i)}=\mu\mathcal{V}_{\tau^{(i)}}$ efficiently by solving a linear program
(cf. subsection 7.2) by adapting [condon92]. Second, the chain of the
$a^{(i)}$ decreases, which means that the algorithm will eventually terminate
(cf. subsection 7.2).

Strategy iteration from below is given in Fig. 3(b). At first sight, the
algorithm looks simpler than strategy iteration from above, since we do not
have to check whether we have already reached $\nu\mathcal{V}$, reduce and
continue from there. However, in this case the computation of
$\mu\mathcal{V}_{\sigma^{(i)}}$ via a linear program is more involved (cf.
subsection 7.2), since we have to pre-compute (via greatest fixpoint iteration
over $\mathbf{2}^{V}$) the nodes where Min can force a cycle based on the
current strategy of Max, thus obtaining payoff $0$.

This algorithm does not directly use our technique but we can use our proof
rules to prove the correctness of the algorithm (subsection 7.2). In
particular, the proof that the sequence $a^{(i)}$ increases is quite involved:
we have to show that
$a^{(i)}=\mu\mathcal{V}_{\sigma^{(i)}}\leq\mu\mathcal{V}_{\sigma^{(i+1)}}=a^{(i+1)}$.
This could be done by showing that $\mu\mathcal{V}_{\sigma^{(i+1)}}$ is a pre-
fixpoint of $\mathcal{V}_{\sigma^{(i)}}$, but there is no straightforward way
to do this. Instead, we prove this fact using our proof rules, by showing that
$a^{(i)}$ is below the least fixpoint of $\mathcal{V}_{\sigma^{(i+1)}}$.

The algorithm generalises strategy iteration by Hoffman and Karp
[hk:nonterminating-stochastic-games]. Note that we cannot simply adapt their
proof, since we do not assume that the game is stopping, which is a crucial
ingredient. In the case where the game is stopping, the two algorithms
coincide, meaning that we also provide an alternative correctness proof in
this situation, while other correctness proofs [condon92] are based on linear
algebra and inverse matrices.

The least fixpoints of $\mathcal{V}_{\tau}$ and $\mathcal{V}_{\sigma}$ can be
determined by solving linear programs.

######  Proof 7.6.

We adapt the linear programs found in the literature on simple stochastic
games (see e.g. [condon92]).

The least fixpoint $a=\mu\mathcal{V}_{\tau}$ can be determined by solving the
following linear program:

$\displaystyle\min$ $\displaystyle\sum_{v\in V}a(v)$ $\displaystyle
a(v)=a(\tau(v))$ $\displaystyle v\in\mathit{MIN}$ $\displaystyle a(v)\geq
a(v^{\prime})$ $\displaystyle\forall
v^{\prime}\in\eta_{\max}(v),v\in\mathit{MAX}$ $\displaystyle
a(v)=\sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})$ $\displaystyle
v\in\mathit{AV}$ $\displaystyle a(v)=w(v)$ $\displaystyle v\in\mathit{SINK}$

By having $a(v)\geq a(v^{\prime})$ for all $v^{\prime}\in\eta_{\max}(v)$ and
$v\in\mathit{MAX}$ we guarantee $a(v)=\max_{v^{\prime}\in\eta_{\max}(v)}$
$a^{(i)}(v^{\prime})$ since we minimise. The minimisation also guarantees
computation of the least fixpoint (in particular, nodes that lie on a cycle
will get a value of $0$). Hence, the linear program correctly characterises
$\mu\mathcal{V}_{\tau}$.

Given a strategy $\sigma$ for Max, we can determine
$a=\mu\mathcal{V}_{\sigma}$ by solving the following linear program:

$\displaystyle\max$ $\displaystyle\sum_{v\in V}a(v)$ $\displaystyle a(v)=0$
$\displaystyle v\in C_{\sigma}$ $\displaystyle a(v)\leq a(v^{\prime})$
$\displaystyle\forall v^{\prime}\in\eta_{\min}(v),v\in\mathit{MIN},v\not\in
C_{\sigma}$ $\displaystyle a(v)=a(\sigma(v))$ $\displaystyle
v\in\mathit{MAX},v\not\in C_{\sigma}$ $\displaystyle a(v)=\sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})$ $\displaystyle
v\in\mathit{AV},v\not\in C_{\sigma}$ $\displaystyle a(v)=w(v)$ $\displaystyle
v\in\mathit{SINK}$

The set $C_{\sigma}$ contains those nodes which will guarantee a non-
terminating play if Min plays optimally, given the fixed Max-strategy
$\sigma$.

The set $C_{\sigma}$ can again be computed via fixpoint-iteration by computing
the greatest fixpoint of $c_{\sigma}$ via Kleene iteration on $\mathbf{2}^{V}$
from above:

$\displaystyle c_{\sigma}\colon\mathbf{2}^{V}$ $\displaystyle\to$
$\displaystyle\mathbf{2}^{V}$ $\displaystyle c_{\sigma}(V^{\prime})$
$\displaystyle=$ $\displaystyle\\{v\in
V\mid(v\in\mathit{MIN}\land\eta_{\min}(v)\cap
V^{\prime}\neq\emptyset)\lor(v\in\mathit{MAX}\land\sigma(v)\in V^{\prime})$
$\displaystyle\qquad\mathop{\lor}(v\in\mathit{AV}\land\mathit{supp}(\eta_{\mathrm{av}}(v))\subseteq
V^{\prime})\\}$

It is easy to see that $C_{\sigma}=\nu c_{\sigma}$ contains all those nodes
from which Min can force a non-terminating play and hence achieve payoff $0$.
(Note that there are further nodes that guarantee payoff $0$ – namely sinks
with that payoff and nodes which can reach such sinks – but those will obtain
value $0$ in any case.)

We now show that this linear program computes $\mu\mathcal{V}_{\sigma}$:
first, by requiring $a(v)\leq a(v^{\prime})$ for all $v\in\mathit{MIN}$,
$v^{\prime}\in\eta_{\min}(v)$, we guarantee
$a(v)=\min_{v^{\prime}\in\eta_{\min}}a(v^{\prime})$ since we maximise. Hence
we obtain the greatest fixpoint of the following function
$\mathcal{V}^{\prime}_{\sigma}\colon[0,1]^{V}\to[0,1]^{V}$:

$\displaystyle\mathcal{V}^{\prime}_{\sigma}(a)(v)$
$\displaystyle=\begin{cases}0&v\in C_{\sigma}\\\ \sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV},v\not\in
C_{\sigma}\\\ a(\sigma(v))&v\in\mathit{MAX},v\not\in C_{\sigma}\\\
\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})&v\in\mathit{MIN},v\not\in
C_{\sigma}\\\ w(v)&v\in\mathit{SINK}\\\ \end{cases}$

It is easy to show that the least fixpoints of $\mathcal{V}^{\prime}_{\sigma}$
and $\mathcal{V}_{\sigma}$ agree, i.e., $\mu\mathcal{V}^{\prime}_{\sigma}$ and
$\mu\mathcal{V}_{\sigma}$:

  * •

$\mu\mathcal{V}^{\prime}_{\sigma}\leq\mu\mathcal{V}_{\sigma}$ can be shown by
observing that $\mathcal{V}^{\prime}_{\sigma}\leq\mathcal{V}_{\sigma}$.

  * •

$\mu\mathcal{V}_{\sigma}\leq\mu\mathcal{V}^{\prime}_{\sigma}$ can be shown by
proving that $\mu\mathcal{V}^{\prime}_{\sigma}$ is a pre-fixpoint of
$\mathcal{V}_{\sigma}$, which can be done via a straightforward case analysis.

We have to show
$\mathcal{V}_{\sigma}(\mu\mathcal{V}^{\prime}_{\sigma})(v)\leq\mu\mathcal{V}^{\prime}_{\sigma}(v)$
for all $v\in V$. We only spell out the case where $v\in\mathit{AV}$, the
other cases are similar. In this case either $v\not\in C_{\sigma}$, which
means that

$\mathcal{V}_{\sigma}(\mu\mathcal{V}^{\prime}_{\sigma})(v)=\mathcal{V}^{\prime}_{\sigma}(\mu\mathcal{V}^{\prime}_{\sigma})(v)=\mu\mathcal{V}^{\prime}_{\sigma}(v).$

If instead $v\in C_{\sigma}$, we have that
$\mathit{supp}(\eta_{\mathrm{av}}(v))\subseteq C_{\sigma}$ and so
$\mu\mathcal{V}^{\prime}_{\sigma}(v^{\prime})=0$ for all
$v^{\prime}\in\mathit{supp}(\eta_{\mathrm{av}}(v))$. Hence

$\mathcal{V}_{\sigma}(\mu\mathcal{V}^{\prime}_{\sigma})(v)=\sum_{v^{\prime}\in
V}\eta_{\mathrm{av}}(v)(v^{\prime})\cdot\mu\mathcal{V}^{\prime}_{\sigma}(v^{\prime})=0=\mu\mathcal{V}^{\prime}_{\sigma}(v)$

If we can now show that $\mathcal{V}^{\prime}_{\sigma}$ has a unique fixpoint,
we are done. The argument for this goes as follows: assume that this function
has another fixpoint $a^{\prime}$ different from
$\mu\mathcal{V}^{\prime}_{\sigma}$. Clearly $[{V}]^{a^{\prime}}\cap
C_{\sigma}=\emptyset$, where $[{V}]^{a^{\prime}}=\\{v\in V\mid
a^{\prime}(v)\neq 0\\}$. Hence, if we compare
$(\mathcal{V}^{\prime}_{\sigma})_{\\#}^{a}\colon\mathbf{2}^{[{V}]^{a}}\to\mathbf{2}^{[{V}]^{\mathcal{V}^{\prime}_{\sigma}(a)}}$
(defined analogously to subsection 7.1) and $c_{\sigma}$ above, we observe
that $(\mathcal{V}^{\prime}_{\sigma})_{\\#}^{a^{\prime}}\subseteq
c_{\sigma}|_{\mathbf{2}^{[{V}]^{a^{\prime}}}}$. (Both functions coincide,
apart from their treatment of nodes $v\in\mathit{MIN}$, where
$c_{\sigma}(V^{\prime})$ contains $v$ whenever one of its successors is
contained in $V^{\prime}$, whereas
$(\mathcal{V}^{\prime}_{\sigma})_{\\#}^{a^{\prime}}(V^{\prime})$ additionally
requires that the value of this successor is minimal.) Since $a^{\prime}$ is
not the least fixpoint we have by 4.2 that

$\emptyset\neq\nu(\mathcal{V}^{\prime}_{\sigma})_{\\#}^{a^{\prime}}\subseteq\nu(c_{\sigma}|_{\mathbf{2}^{[{V}]^{a^{\prime}}}})\subseteq\nu
c_{\sigma}=C_{\sigma}.$

This is a contradiction, since $[{V}]^{a^{\prime}}\cap C_{\sigma}=\emptyset$
as observed above.

This shows that $\mathcal{V}^{\prime}_{\sigma}$ has a unique fixpoint and
completes the proof. Note that if we do not explicitly require that the values
of all nodes in $C_{\sigma}$ are $0$, $\mathcal{V}^{\prime}_{\sigma}$ will
potentially have several fixpoints and the linear program would not
characterise the least fixpoint.

Strategy iteration from above and below both terminate and compute the least
fixpoint of $\mathcal{V}$.

######  Proof 7.7.

_Strategy iteration from above:_

We start by showing the following: Given any $a^{(i)}$ and a new switched Min-
strategy $\tau^{(i+1)}$, i.e.,
$\tau^{(i+1)}=\mathit{sw}_{\min}(\tau^{(i)},a^{(i)})$, then $a^{(i)}$ is a
pre-fixpoint of $\mathcal{V}_{\tau^{(i+1)}}$. By choice of $\tau^{(i+1)}$ we
have

$\displaystyle\mathcal{V}_{\tau^{(i+1)}}(a^{(i)})(v)$
$\displaystyle=\begin{cases}a^{(i)}(\tau^{(i+1)}(v))&v\in\mathit{MIN}\\\
\max_{v^{\prime}\in\eta_{\max}(v)}a^{(i)}(v^{\prime})&v\in\mathit{MAX}\\\
\sum_{v^{\prime}\in
V}a^{(i)}(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV}\\\
w(v)&v\in\mathit{SINK}\end{cases}$
$\displaystyle=\begin{cases}\min_{v^{\prime}\in\eta_{\min}(v)}a^{(i)}(v^{\prime})&v\in\mathit{MIN}\\\
\max_{v^{\prime}\in\eta_{\max}(v)}a^{(i)}(v^{\prime})&v\in\mathit{MAX}\\\
\sum_{v^{\prime}\in
V}a^{(i)}(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV}\\\
w(v)&v\in\mathit{SINK}\end{cases}$ $\displaystyle=\mathcal{V}(a^{(i)})(v)$

By 7.4 $\mathcal{V}\leq\mathcal{V}_{\tau^{(i)}}$ holds and since $a^{(i)}$ is
a fixpoint of $\mathcal{V}_{\tau^{(i)}}$ we conclude

$\displaystyle\mathcal{V}_{\tau^{(i+1)}}(a^{(i)})(v)=\mathcal{V}(a^{(i)})(v)\leq\mathcal{V}_{\tau^{(i)}}(a^{(i)})(v)=a^{(i)}(v)$

Thus we have $a^{(i+1)}\leq a^{(i)}$ (by Knaster-Tarski, since $a^{(i)}$ is a
pre-fixpoint of $\mathcal{V}_{\tau^{(i+1)}}$ and $a^{(i+1)}$ is its least
fixpoint). Furthermore we know that $a^{(i)}$ is not a fixpoint of
$\mathcal{V}_{\tau^{(i+1)}}$ (otherwise we could not have performed a switch)
and hence $a^{(i+1)}$ is strictly smaller than $a^{(i)}$ for at least one
input. Since there are only finitely many strategies we will eventually stop
switching and reach a fixpoint $a=a^{(j)}$ for an index $j$.

Then, if $V^{\prime}=\nu\mathcal{V}_{\\#}^{a}=\emptyset$ then $a$ is the least
fixpoint and we conclude.

Otherwise, we determine
$a^{(j+1)}=a-(\iota_{\mathcal{V}}^{a}(V^{\prime}))_{V^{\prime}}$. By 4.5 (dual
version), $a^{(j+1)}$ is a pre-fixpoint of $\mathcal{V}$. Now Min will choose
her best strategy $\tau=\tau^{(j+2)}=\mathit{sw}_{\min}(\tau^{(i)},a^{(i+1)})$
and we continue computing $a^{(j+2)}=\mu\mathcal{V}_{\tau^{(j+2)}}$. First,
observe that since $a^{(j+1)}$ is a pre-fixpoint of $\mathcal{V}$, it is also
a pre-fixpoint of $\mathcal{V}_{\tau^{(j+2)}}$. In fact, $\mathcal{V}$ and
$\mathcal{V}_{\tau^{(j+1)}}$ coincide on all nodes $v\not\in\mathit{MIN}$. If
$v\in\mathit{MIN}$, we have

$\displaystyle\mathcal{V}_{\tau^{(j+2)}}(a^{(j+1)})(v)$ $\displaystyle=$
$\displaystyle a^{(j+1)}(\tau^{(j+2)}(v))$ $\displaystyle=$
$\displaystyle\min_{v^{\prime}\in\eta_{\min}(v)}a^{(j+1)}(v^{\prime})=\mathcal{V}(a^{(j+1)})(v)\leq
a^{(j+1)}(v).$

Hence it follows by Knaster-Tarski that
$a^{(j+2)}=\mu\mathcal{V}_{\tau^{(j+2)}}\leq a^{(j+1)}$. In turn,
$a^{(j+1)}<a^{(j)}$ since $V^{\prime}$ is non-empty and hence also
$a^{(j+2)}<a^{(j)}$ (where $<$ on tuples means means $\leq$ in all components
and $<$ in at least one component.)

This means that the chain $a^{(i)}$ is strictly descending. Hence, at each
iteration we obtain a new strategy and, since the number of strategies is
finite, the iteration will eventually stop.

Hence the algorithm terminates and stops at the least fixpoint of
$\mathcal{V}$.

_Strategy iteration from below:_

We start as follows: Assume $a$ is the least fixpoint of
$\mathcal{V}_{\sigma}$, i.e. $a=\mu\mathcal{V}_{\sigma}$ and $\sigma^{\prime}$
the new best strategy for Max obtained by switching with respect to $a$, i.e.,
$\sigma^{\prime}=\mathit{sw}_{\max}(\sigma,a)$. We have to show that
$a^{\prime}=\mu\mathcal{V}_{\sigma^{\prime}}$ lies above $a$ ($a^{\prime}\geq
a$). Here we use our proof rules (see subsection 4.2) and show the following:

  * •

First, observe that $a$ is a post-fixpoint of $\mathcal{V}_{\sigma^{\prime}}$.
For any $v\in V$ we have

$\displaystyle a(v)=\mathcal{V}_{\sigma}(a)(v)$
$\displaystyle=\begin{cases}\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})&v\in\mathit{MIN}\\\
a(\sigma(v))&v\in\mathit{MAX}\\\ \sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV}\\\
w(v)&v\in\mathit{SINK}\end{cases}$
$\displaystyle\leq\begin{cases}\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})&v\in\mathit{MIN}\\\
\max_{v^{\prime}\in\eta_{\max}(v)}a(v^{\prime})&v\in\mathit{MAX}\\\
\sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV}\\\
w(v)&v\in\mathit{SINK}\end{cases}$
$\displaystyle=\begin{cases}\min_{v^{\prime}\in\eta_{\min}(v)}a(v^{\prime})&v\in\mathit{MIN}\\\
a(\sigma^{\prime}(v))&v\in\mathit{MAX}\\\ \sum_{v^{\prime}\in
V}a(v^{\prime})\cdot\eta_{\mathrm{av}}(v)(v^{\prime})&v\in\mathit{AV}\\\
w(v)&v\in\mathit{SINK}\end{cases}$
$\displaystyle=\mathcal{V}_{\sigma^{\prime}_{\max}}(a)(v)$

  * •

Next we show that $\nu(\mathcal{V}_{\sigma^{\prime}})_{*}^{a}=\emptyset$, thus
proving that $a\leq\mu\mathcal{V}_{\sigma^{\prime}}=a^{\prime}$ by subsection
4.2. Note that
$(\mathcal{V}_{\sigma^{\prime}})_{*}^{a}\colon[{V}]^{a=\mathcal{V}_{\sigma^{\prime}}(a)}\to[{V}]^{a=\mathcal{V}_{\sigma^{\prime}}(a)}$,
i.e., it restricts to those elements of $a$ where $a$ and
$\mathcal{V}_{\sigma^{\prime}}(a)$ coincide.

Whenever $v\in\mathit{MAX}$ is a node where the strategy has been “switched”
with respect to $a$, we have

$\mathcal{V}_{\sigma^{\prime}}(a)(v)=a(\sigma^{\prime}(v))>a(\sigma(v))=a(v).$

The first equality above is true by the definition of
$\mathcal{V}_{\sigma^{\prime}}$ and the last equality holds since $a$ is a
fixpoint of $\mathcal{V}_{\sigma}$. So if $v$ is a switch node, it holds that
$v\not\in[{V}]^{a=\mathcal{V}_{\sigma}(a)}$. By contraposition if
$v\in[{V}]^{a=\mathcal{V}_{\sigma}(a)}$, $v$ cannot be a switch node.

We next show that $(\mathcal{V}_{\sigma})_{*}^{a}$,
$(\mathcal{V}_{\sigma^{\prime}})_{*}^{a}$ agree on
$[{V}]^{a=\mathcal{V}_{\sigma^{\prime}}(a)}\subseteq[{V}]^{a}=[{V}]^{a=\mathcal{V}_{\sigma}(a)}$
(remember that $a$ is a fixpoint of $\mathcal{V}_{\sigma}$). It holds that

$\displaystyle(\mathcal{V}_{\sigma})_{*}^{a}(V^{\prime})$ $\displaystyle=$
$\displaystyle\gamma_{\mathcal{V}_{\sigma}(a),\iota}(\mathcal{V}_{\sigma}(\alpha_{a,\iota}(V^{\prime})))$
$\displaystyle(\mathcal{V}_{\sigma^{\prime}})_{*}^{a}(V^{\prime})$
$\displaystyle=$
$\displaystyle\gamma_{\mathcal{V}_{\sigma^{\prime}}(a),\iota}(\mathcal{V}_{\sigma^{\prime}}(\alpha_{a,\iota}(V^{\prime})))\cap[{V}]^{a=\mathcal{V}_{\sigma^{\prime}}(a)}$

for a suitable constant $\iota$ and if we choose $\iota$ small enough we can
use the same constant in both cases. Now let
$v\in[{V}]^{a=\mathcal{V}_{\sigma^{\prime}}(a)}$: by definition it holds that
$v\in(\mathcal{V}_{\sigma})_{*}^{a}(V^{\prime})=\gamma_{\mathcal{V}_{\sigma}(a),\iota}(\mathcal{V}_{\sigma}(\alpha_{a,\iota}(V^{\prime})))$
if and only if
$\mathcal{V}_{\sigma}(\alpha_{a,\iota}(V^{\prime}))(v)\ominus\mathcal{V}_{\sigma}(a)(v)\geq\iota$.
Since, by the considerations above, $v$ is not a switch node,
$\mathcal{V}_{\sigma}(b)(v)=\mathcal{V}_{\sigma^{\prime}}(b)(v)$ for all $b$
and we can replace $\mathcal{V}_{\sigma}$ by $\mathcal{V}_{\sigma^{\prime}}$,
resulting in the equivalent statement
$v\in\gamma_{\mathcal{V}_{\sigma^{\prime}}(a),\iota}(\mathcal{V}_{\sigma^{\prime}}(\alpha_{a,\iota}(V^{\prime})))$,
also equivalent to $v\in(\mathcal{V}_{\sigma^{\prime}})_{*}^{a}(V^{\prime})$.

Thus
$\nu(\mathcal{V}_{\sigma^{\prime}})_{*}^{a}\subseteq\nu(\mathcal{V}_{\sigma})_{*}^{a}=\emptyset$.

Hence we obtain an ascending sequence $a^{(i)}$. Furthermore, whenever we
perform a switch, we know that $a^{(i)}$ is not a fixpoint of
$\mathcal{V}_{\sigma^{(i+1)}}$ (otherwise we could not have performed a
switch) and hence $a^{(i+1)}$ is strictly larger than $a^{(i)}$ for at least
one input. Since there are only finitely many strategies we will eventually
stop switching and reach the least fixpoint.

######  Example 7.8.

Ex. 7.1 is well suited to explain our two algorithms.

Starting with strategy iteration from above, we may guess
$\tau^{(0)}(\min)=\textbf{1}$. In this case, Max would choose $\mathrm{av}$ as
successor and we would reach a fixpoint, where each node except for
$\bm{\varepsilon}$ is associated with a payoff of $1$. Next, our algorithm
would detect the vicious cycle formed by $\min$, $\mathrm{av}$ and $\max$. We
can reduce the values in this vicious cycle and reach the correct payoff
values for each node.

For strategy iteration from below assume that
$\sigma^{(0)}(\max)=\mathrm{av}$. Given this strategy of Max, Min can force
the play to stay in a cycle formed by $\min$, $\mathrm{av}$ and $\max$. Thus,
the payoff achieved by the Max strategy $\sigma^{(0)}$ and an optimal play by
Min would be $0$ for each of these nodes. In the next iteration Max switches
and chooses $\bm{\varepsilon}$ as successor, i.e.
$\sigma^{(1)}(\max)=\bm{\varepsilon}$, which results in the correct values.

###  7.3. Runtime results

We implemented strategy iteration from above and from below – in the following
abbreviated by SIA and SIB – and classical Kleene iteration (KI) in MATLAB. In
Kleene iteration we terminate with a tolerance of $10^{-14}$, i.e., we stop if
the change from one iteration to the next is below this value.

In order to test the algorithms we created random stochastic games with $n$
nodes, where each Max, Min respectively average node has a maximal number of
$m$ successors. For each node we choose randomly one of the four types of
nodes. Sink nodes are given a random weight uniformly in $[0,1]$. Max and Min
nodes are randomly assigned to successors and for an average nodes we assign a
random number to each of its successors, followed by normalisation to obtain a
probability distribution.

We performed 1000 runs with different randomly created systems for each value
of $n$ and $m=\frac{n}{2}$. The table below shows the runtimes in seconds and
the number of iterations. Also, for SIB, we display the number of nodes with a
payoff of $0$ (for an optimal play of Min) and the number of times SIA got
stuck at any other fixpoint which is not $\mu\mathcal{V}$ (all numbers –
runtime, iterations, etc. – are summed up over all $1000$ runs).

| runtime (seconds) | number of iterations | number nodes | number of
---|---|---|---|---
$~{}~{}~{}n~{}~{}~{}$ |  KI |  SIA |  SIB |  KI |  SIA |  SIB |  payoff 0 |  other fp
10 | 0.59 | 20.28 | 18.49 | 47302 | 2259 | 2152 | 2439 | 508
20 | 1.05 | 31.71 | 25.96 | 30275 | 3620 | 3018 | 4714 | 743
30 | 2.03 | 35.98 | 29.77 | 27361 | 3881 | 3275 | 7268 | 771
40 | 3.77 | 38.84 | 32.67 | 26999 | 3850 | 3296 | 9806 | 756
50 | 5.31 | 38.09 | 31.85 | 26604 | 3799 | 3215 | 12573 | 734
60 | 7.63 | 40.33 | 34.37 | 26467 | 3737 | 3218 | 15151 | 727
70 | 10.77 | 45.00 | 37.50 | 26569 | 3751 | 3154 | 17473 | 751
80 | 15.38 | 54.89 | 46.72 | 26179 | 3713 | 3105 | 20031 | 752
90 | 16.07 | 52.21 | 43.52 | 26401 | 3695 | 3083 | 22390 | 777
100 | 19.46 | 60.29 | 50.88 | 26464 | 3654 | 3062 | 25163 | 751

Note that SIB always performs slightly better than SIA. Moreover KI neatly
beats both of them. Here we need to remember that KI only converges to the
solution and it is known that the rate of convergence can be exponentially
slow [c:algorithms-ssg].

Note that the linear optimisation problems are quite costly to solve,
especially for large systems. Thus additional iterations are substantially
more costly compared to KI. Observe also that SIA has to perform more
iterations than SIB, which explains the slightly higher runtime.

The number of nodes with a payoff of 0 seems to grow linearly with the number
of nodes in the system. The number of times SIA gets stuck at a fixpoint
different from $\mu\mathcal{V}$ however seems to be independent of the system
size and comparatively small.

We performed a second comparison, where we assigned to sink nodes a value in
$\\{0,1\\}$, which is often done for simple stochastic games.

| runtime | number of iterations | number nodes | number of
---|---|---|---|---
$~{}~{}~{}n~{}~{}~{}$ |  KI |  SIA |  SIB |  KI |  SIB |  SIA |  payoff 0 |  other fp
10 | 0.36 | 14.51 | 14.58 | 42547 | 1703 | 1702 | 5484 | 219
20 | 1.00 | 19.85 | 19.98 | 29515 | 2385 | 2478 | 8168 | 137
30 | 1.97 | 20.45 | 20.77 | 27643 | 2367 | 2469 | 11502 | 33
40 | 3.30 | 20.13 | 20.94 | 26761 | 2306 | 2383 | 14989 | 12
50 | 4.96 | 20.24 | 20.94 | 26562 | 2253 | 2306 | 18821 | 2
60 | 6.87 | 20.57 | 21.19 | 26560 | 2176 | 2227 | 22573 | 0
70 | 9.14 | 21.95 | 22.35 | 26146 | 2142 | 2186 | 26260 | 0
80 | 11.73 | 24.69 | 24.94 | 26235 | 2084 | 2131 | 30136 | 0
90 | 14.73 | 28.90 | 28.71 | 26330 | 2066 | 2091 | 33930 | 0
100 | 18.22 | 34.75 | 34.84 | 26227 | 2051 | 2068 | 37496 | 0

Here, SIA performs very similar to SIB. The SIA approach seems to suffer,
since Max can easily find himself in a situation where he can never reach a
1-sink, since only half of the sink nodes are of this kind. Additionally for
these systems a significantly larger number of nodes have a payoff of 0 and
SIA is less likely to get stuck at a fixpoint different from $\mu\mathcal{V}$.
These factors seem to be correlated since it is now “harder” for Min to choose
a bad successor (with a value greater than 0).

##  8\. Conclusion

It is well-known that several computations in the context of system
verification can be performed by various forms of fixpoint iteration and it is
worthwhile to study such methods at a high level of abstraction, typically in
the setting of complete lattices and monotone functions. Going beyond the
classical results by Tarski [t:lattice-fixed-point], combination of fixpoint
iteration with approximations [CC:TLA, bkp:abstraction-up-to-games-fixpoint]
and with up-to techniques [p:complete-lattices-up-to] has proven to be
successful. Here we treated a more specific setting, where the carrier set
consists of functions from a finite set into an MV-chain and the fixpoint
functions are non-expansive (and hence monotone), and introduced a novel
technique to obtain upper bounds for greatest and lower bounds for least
fixpoints, also providing associated algorithms. Such techniques are
applicable to a wide range of examples and so far they have been studied only
in quite specific scenarios, such as in [bblmtv:prob-bisim-distance-automata,
f:game-metrics-markov-decision, kkkw:value-iteration-ssg].

In the future we plan to lift some of the restrictions of our approach. First,
an extension to an infinite domain $Y$ would of course be desirable, but since
several of our results currently depend on finiteness, such a generalisation
does not seem to be easy. The restriction to total orders, instead, seems
easier to lift: in particular, if the partially ordered MV-algebra
$\bar{\mathbb{M}}$ is of the form $\mathbb{M}^{I}$ where $I$ is a finite index
set and $\mathbb{M}$ an MV-chain. (E.g., finite Boolean algebras are of this
type.) In this case, our function space is
$\bar{\mathbb{M}}^{Y}=\big{(}\mathbb{M}^{I}\big{)}^{\raisebox{-2.0pt}{\scriptsize$Y$}}\cong\mathbb{M}^{Y\times
I}$ and we have reduced to the setting presented in this paper. This will
allow us to handle featured transition systems [ccpshl:simulation-product-
line-mc] where transitions are equipped with boolean formulas.

There are several other application examples that did not fit into this paper,
but that can also be handled by our approach, for instance coalgebraic
behavioural metrics [bbkk:coalgebraic-behavioral-metrics]. We also plan to
investigate other types of games, such as energy games [bcdgr:algorithms-mean-
payoff-games]. While here we introduced strategy iteration techniques for
simple stochastic games, we also want to check whether we can provide an
improvement to value iteration techniques, combining our approach with
[kkkw:value-iteration-ssg].

We also plan to study whether some examples can be handled with other types of
Galois connections: here we used an additive variant, but looking at
multiplicative variants (multiplication by a constant factor) might also be
fruitful.

_Acknowledgements:_ We are grateful to Ichiro Hasuo for making us aware of
stochastic games as an application domain. Furthermore we would like to thank
Matthias Kuntz and Timo Matt for their help with experiments and
implementation.

## References

  * [BBKK18] 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).
  * [BBL+19] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel.  Computing probabilistic bisimilarity distances for probabilistic automata.  In Proc. of CONCUR ’19, volume 140 of LIPIcs, pages 9:1–9:17. Schloss Dagstuhl – Leibniz Center for Informatics, 2019.
  * [BBLM17] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.  On-the-fly exact computation of bisimilarity distances.  Logical Methods in Computer Science, 13(2:13):1–25, 2017.
  * [BCD+11] Lubos Brim, Jakub Chaloupka, Laurent Doyen, Raffaella Gentilini, and Jean-Fran cois Raskin.  Faster algorithms for mean-payoff games.  Formal Methods in System Design, 38(2):97–118, 2011.
  * [BK08] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  MIT Press, 2008.
  * [BKP20] 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.
  * [BV05] Henrik Björklund and Sergei Vorobyov.  Combinatorial structure and randomized subexponential algorithms for infinite games.  Theoretical Computer Science, 349(3):347–360, 2005.
  * [CC77] Patrick Cousot and Radhia Cousot.  Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.  In Proc. of POPL ’77 (Los Angeles, California), pages 238–252. ACM, 1977.
  * [CC00] 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.
  * [CCP+12] Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, and Axel Legay.  Simulation-based abstractions for software product-line model checking.  In Proc. of ICSE ’12 (International Conference on Software Engineering), pages 672–682. IEEE, 2012.
  * [Cle90] Rance Cleaveland.  On automatically explaining bisimulation inequivalence.  In Proc. of CAV ’90, pages 364–372. Springer, 1990.  LNCS 531.
  * [Con90] Anne Condon.  On algorithms for simple stochastic games.  In Advances In Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 51–71, 1990.
  * [Con92] Anne Condon.  The complexity of stochastic games.  Information and Computation, 96(2):203–224, 1992.
  * [dFS09] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga.  Linear and branching system metrics.  IEEE Transactions on Software Engineering, 35(2):258–273, 2009\.
  * [Fu12] Hongfei Fu.  Computing game metrics on Markov decision processes.  In Proc. of ICALP ’12, Part II, pages 227–238. Springer, 2012.  LNCS 7392.
  * [GRS00] Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari.  Making abstract interpretations complete.  Journal of the ACM, 47(2):361–416, 2000.
  * [HM85] Matthew Hennessy and Robin Milner.  Algebraic laws for nondeterminism and concurrency.  Journal of the ACM, 32:137–161, 1985.
  * [KH66] Richard M. Karp and Alan J. Hoffman.  On nonterminating stochastic games.  Management Science, 12(5):359–370, 1966.
  * [KKKW18] Edon Kelmendi, Julia Krämer, Jan Křetínský, and Maximilian Weininger.  Value iteration for simple stochastic games: Stopping criterion and learning algorithm.  In Proc. of CAV ’18, pages 623–642. Springer, 2018.  LNCS 10981.
  * [M1́1] Facundo Mémoli.  Gromov-Wasserstein distances and the metric approach to object matching.  Foundations of Computational Mathematics, 11(4):417–487, 2011.
  * [Mun] Daniele Mundici.  MV-algebras. A short tutorial.  Available at http://www.matematica.uns.edu.ar/IXCongresoMonteiro/Comunicaciones/Mundici_tutorial.pdf.
  * [Mun11] Daniele Mundici.  Advanced Łukasiewicz calculus and MV-algebras, volume 35 of Trends in Logic.  Springer, 2011.
  * [NNH10] Flemming Nielson, Hanne R. Nielson, and Chris Hankin.  Principles of Program Analysis.  Springer, 2010.
  * [PC20] Gabriel Peyré and Marco Cuturi.  Computational optimal transport, 2020.  arXiv:1803.00567.
  * [Pou07] Damien Pous.  Complete lattices and up-to techniques.  In Proc. of APLAS ’07, pages 351–366. Springer, 2007.  LNCS 4807.
  * [RVAK11] Tripathi Rahul, Elena Valkanova, and V.S. Anil Kumar.  On strategy improvement algorithms for simple stochastic games.  Journal of Discrete Algorithms, 9:263–278, 2011.
  * [San11] Davide Sangiorgi.  Introduction to Bisimulation and Coinduction.  Cambridge University Press, 2011.
  * [Sti97] Colin Stirling.  Bisimulation, model checking and other games.  Notes for Mathfit instructional meeting on games and computation, Edinburgh, June 1997.
  * [Tar55] Alfred Tarski.  A lattice-theoretical theorem and its applications.  Pacific Journal of Mathematics, 5:285–309, 1955.
  * [Vil09] Cédric Villani.  Optimal Transport – Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics.  Springer, 2009.