11institutetext: University of Oxford, United Kingdom

# Trace Refinement in
Labelled Markov Decision Processes

Nathanaël Fijalkow  Stefan Kiefer  Mahsa Shirmohammadi

###### Abstract

Given two labelled Markov decision processes (MDPs), the trace-refinement
problem asks whether for all strategies of the first MDP there exists a
strategy of the second MDP such that the induced labelled Markov chains are
trace-equivalent. We show that this problem is decidable in polynomial time if
the second MDP is a Markov chain. The algorithm is based on new results on a
particular notion of bisimulation between distributions over the states.
However, we show that the general trace-refinement problem is undecidable,
even if the first MDP is a Markov chain. Decidability of those problems was
stated as open in 2008. We further study the decidability and complexity of
the trace-refinement problem provided that the strategies are restricted to be
memoryless.

##  1 Introduction

We consider labelled Markov chains (MCs) whose transitions are labelled with
symbols from an alphabet ${\sf L}$. Upon taking a transition, the MC emits the
associated label. In this way, an MC defines a _trace-probability_ function
$\mathit{Tr}:{\sf L}^{*}\to[0,1]$ which assigns to each finite trace $w\in{\sf
L}^{*}$ the probability that the MC emits $w$ during its first $|w|$
transitions. Consider the MC depicted in Figure 2 with initial state $p_{0}$.
For example, see that if in state $p_{0}$, with probability $\frac{1}{4}$, a
transition to state $p_{c}$ is taken and $c$ is emitted. We have, e.g.,
$\mathit{Tr}(abc)=\frac{1}{4}\cdot\frac{1}{4}\cdot\frac{1}{4}$. Two MCs over
the same alphabet ${\sf L}$ are called _equivalent_ if their trace-probability
functions are equal.

$p_{0}$$p_{c}$$p_{d}$$\frac{1}{4},c$$\frac{1}{4},d$$\frac{1}{4},a$$\frac{1}{4},b$$1,c$$1,d$ trace $w$ | $\mathit{Tr}(w)$
---|---
$w\in(a+b)^{n}$ | $\frac{1}{4^{n}}$
$w\in(a+b)^{n}c^{+}$ | $\frac{1}{4^{n+1}}$
$w\in(a+b)^{n}d^{+}$ | $\frac{1}{4^{n+1}}$
otherwise | 0
Figure 1: An MC with its trace-probability function. This MC, denoted by
${\cal C}({\cal A})$, is also used in the reduction from universality of
probabilistic automata to ${\sf MC\sqsubseteq MDP}$.

$q_{0}$$q_{1}$$\frac{1}{4},c$$\frac{1}{4},d$$\frac{1}{4},a$$\frac{1}{4},b$$1,c$${\sf
m}_{1}$${\sf m}_{2}$$1,d$ Figure 2: An MDP where the choice of controller is
relevant only in $q_{1}$. Two available moves ${\sf m}_{1},{\sf m}_{2}$ are
shown with small black circles.

The study of such MCs and their equivalence has a long history, going back to
Schützenberger [18] and Paz [15]. Schützenberger and Paz studied _weighted_
and _probabilistic_ automata, respectively. Those models generalize labelled
MCs, but the respective equivalence problems are essentially the same. It can
be extracted from [18] that equivalence is decidable in polynomial time, using
a technique based on linear algebra. Variants of this technique were
developed, see e.g. [19, 7]. Tzeng [20] considered the path-equivalence
problem for nondeterministic automata which asks, given nondeterministic
automata $A$ and $B$, whether each word has the same number of accepting paths
in $A$ as in $B$. He gives an NC algorithm111The complexity class NC is the
subclass of P containing those problems that can be solved in polylogarithmic
parallel time (see e.g. [9]). for deciding path equivalence which can be
straightforwardly adapted to yield an NC algorithm for equivalence of MCs.

More recently, the efficient decidability of the equivalence problem was
exploited, both theoretically and practically, for the verification of
probabilistic systems, see e.g. [11, 12, 16, 14, 13]. In those works,
equivalence naturally expresses properties such as obliviousness and
anonymity, which are difficult to formalize in temporal logic. The _inclusion
problem_ for two probabilistic automata asks whether for each word the
acceptance probability in the first automaton is less than or equal to the
acceptance probability in the second automaton. Despite its semblance to the
equivalence problem, the inclusion problem is undecidable [5], even for
automata of fixed dimension [2]. This is unfortunate, especially because
deciding language inclusion is often at the heart of verification algorithms.

We study another “inclusion-like” generalization of the equivalence problem:
trace refinement in labelled Markov decision processes (MDPs). MDPs extend MCs
by nondeterminism; in each state, a controller chooses, possibly randomly and
possibly depending on the history, one out of finitely many _moves_ 222As in
[7] we speak of moves rather than of actions, to avoid possible confusion with
the label alphabet ${\sf L}$.. A move determines a probability distribution
over the emitted label and the successor state. In this way, an MDP and a
strategy of the controller induce an MC.

The _trace-refinement problem_ asks, given two MDPs ${\cal D}$ and ${\cal E}$,
whether for all strategies for ${\cal D}$ there is a strategy for ${\cal E}$
such that the induced MCs are equivalent. Consider the MDP depicted in Figure
2 where in state $q_{1}$ there are two available moves; one move generates the
label $c$ with probability 1, the other move generates $d$ with probability 1.
A strategy of the controller that chooses the last generated label in the
state $q_{1}$, either $c$ or $d$, with probability $1$, induces the same
trace-probability function as the MC shown in Figure 2; the MDP thus refines
that MC. The described strategy needs one bit of memory to keep track of the
last generated label. It was shown in [7] that the strategy for ${\cal E}$ may
require _infinite memory_ , even if ${\cal D}$ is an MC. The decidability of
trace refinement was posed as an open problem, both in the introduction and in
the conclusion of [7]. The authors of [7] also ask about the decidability of
subcases, where ${\cal D}$ or ${\cal E}$ are restricted to be MCs. In this
paper we answer all those questions. We show that trace refinement is
undecidable, even if ${\cal D}$ is an MC. In contrast, we show that trace
refinement is decidable efficiently (in NC, hence in P), if ${\cal E}$ is an
MC. Moreover, we prove that the trace-refinement problem becomes decidable if
one imposes suitable _restrictions on the strategies_ for ${\cal D}$ and
${\cal E}$, respectively. More specifically, we consider _memoryless_ (i.e.,
no dependence on the history) and _pure memoryless_ (i.e., no randomization
and no dependence on the history) strategies, establishing various complexity
results between NP and PSPACE.

To obtain the aforementioned NC result, we demonstrate a link between trace
refinement and a particular notion of _bisimulation_ between two MDPs that was
studied in [10]. This variant of bisimulation is not defined between two
states as in the usual notion, but between two _distributions_ on states. An
exponential-time algorithm that decides (this notion of) bisimulation was
provided in [10]. We sharpen this result by exhibiting a coNP algorithm that
decides bisimulation between two MDPs, and an NC algorithm for the case where
one of the MDPs is an MC. For that we refine the arguments devised in [10].
The model considered in [10] is more general than ours in that they also
consider continuous state spaces, but more restricted than ours in that the
label is determined by the move.

##  2 Preliminaries

A trace over a finite set ${\sf L}$ of labels is a finite sequence
$w=a_{1}\cdots a_{n}$ of labels where the length of the trace is $\lvert
w\rvert=n$. The empty trace $\epsilon$ has length zero. For $n\geq 0$, let
${\sf L}^{n}$ be the set of all traces with length $n$; we denote by ${\sf
L}^{*}$ the set of all (finite) traces over ${\sf L}$.

For a function $d:S\to[0,1]$ over a finite set $S$, define the _norm_ $\lVert
d\rVert:=\sum_{s\in S}d(s)$. The _support_ of $d$ is the set ${\sf
Supp}(d)=\\{s\in S\mid d(s)>0\\}$. The function $d$ is a _probability
subdistribution_ over $S$ if $\lVert d\rVert\leq 1$; it is a _probability
distribution_ if $\lVert d\rVert=1$. We denote by ${\sf subDist}(S)$ (resp.
${\sf Dist}(S)$) the set of all probability subdistributions (resp.
distributions) over $S$. Given $s\in S$, the _Dirac distribution_ on $s$
assigns probability $1$ to $s$; we denote it by $d_{s}$. For a non-empty
subset $T\subseteq S$, the _uniform distribution_ over $T$ assigns probability
$\frac{1}{\lvert T\rvert}$ to every element in $T$.

###  2.1 Labelled Markov Decision Processes

A _labelled Markov decision process_ (MDP) ${\cal D}=\langle Q,\mu_{0},{\sf
L},\delta\rangle$ consists of a finite set $Q$ of states, an initial
distribution $\mu_{0}\in{\sf Dist}(Q)$, a finite set ${\sf L}$ of labels, and
a finite probabilistic transition relation $\delta\subseteq Q\times{\sf
Dist}({\sf L}\times Q)$ where states are in relation with distributions over
pairs of labels and successors. We assume that for each state $q\in Q$ there
exists some distribution $d\in{\sf Dist}({\sf L}\times Q)$ where $\langle
q,d\rangle\in\delta$. The set of _moves_ in $q$ is ${\sf moves}(q)=\\{d\in{\sf
Dist}({\sf L}\times Q)\mid\langle q,d\rangle\in\delta\\}$; denote by ${\sf
moves}=\bigcup_{q\in Q}{\sf moves}(q)$ the set of all moves.

For the complexity results, we assume that probabilities of transitions are
rational and given as fractions of integers represented in binary.

We describe the behaviour of an MDP as a trace generator running in steps. The
MDP starts in the first step in state $q$ with probability $\mu_{0}(q)$. In
each step, if the MDP is in state $q$ the controller chooses ${\sf m}\in{\sf
moves}(q)$; then, with probability ${\sf m}(a,q^{\prime})$, the label $a$ is
generated and the next step starts in the successor state $q^{\prime}$.

Given $q\in Q$, denote by ${\sf post}(q)$ the set $\\{(a,q^{\prime})\in{\sf
Supp}({\sf m})\mid{\sf m}\in{\sf moves}(q)\\}$. A _path_ in ${\cal D}$ is a
sequence $\rho=q_{0}a_{1}q_{1}\dots a_{n}q_{n}$ such that
$(a_{i+1},q_{i+1})\in{\sf post}(q_{i})$ for all $0\leq i<n$. The path $\rho$
has the last state ${\sf last}(\rho)=q_{n}$; and the generated trace after
$\rho$ is $a_{1}a_{2}\cdots a_{n}$, denoted by ${\sf trace}(\rho)$. We denote
by ${\sf Paths}({\cal D})$ the set of all paths in ${\cal D}$, and by ${\sf
Paths}(w)=\\{\rho\in{\sf Paths}({\cal D})\mid{\sf trace}(\rho)=w\\}$ the set
of all path generating $w$.

#### Strategies.

A randomized strategy (or simply a strategy) for an MDP ${\cal D}$ is a
function $\alpha:{\sf Paths}({\cal D})\to{\sf Dist}({\sf moves})$ that, given
a finite path $\rho$, returns a probability distribution $\alpha(\rho)\in{\sf
Dist}({\sf moves}({\sf last}(\rho)))$ over the set of moves in ${\sf
last}(\rho)$, used to generate a label $a$ and select a successor state
$q^{\prime}$ with probability $\sum_{{\sf m}\in{\sf
moves}(q)}\alpha(\rho)({\sf m})\cdot{\sf m}(a,q^{\prime})$ where $q={\sf
last}(\rho)$.

A strategy $\alpha$ is _pure_ if for all $\rho\in{\sf Paths}({\cal D})$, we
have $\alpha(\rho)({\sf m})=1$ for some ${\sf m}\in{\sf moves}$; we thus view
pure strategies as functions $\alpha:{\sf Paths}({\cal D})\to{\sf moves}$. A
strategy $\alpha$ is _memoryless_ if $\alpha(\rho)=\alpha(\rho^{\prime})$ for
all paths $\rho,\rho^{\prime}$ with ${\sf last}(\rho)={\sf
last}(\rho^{\prime})$; we thus view memoryless strategies as functions
$\alpha:Q\to{\sf Dist}({\sf moves})$. A strategy $\alpha$ is _trace-based_ if
$\alpha(\rho)=\alpha(\rho^{\prime})$ for all $\rho,\rho^{\prime}$ where ${\sf
trace}(\rho)={\sf trace}(\rho^{\prime})$ and ${\sf last}(\rho)={\sf
last}(\rho^{\prime})$; we view trace-based strategies as functions
$\alpha:{\sf L}^{*}\times Q\to{\sf Dist}({\sf moves})$.

#### Trace-probability function.

For an MDP ${\cal D}$ and a strategy $\alpha$, the probability of a single
path is inductively defined by ${\sf Pr}_{{\cal D},\alpha}(q)=\mu_{0}(q)$ and

${\sf Pr}_{{\cal D},\alpha}(\rho aq)={\sf Pr}_{{\cal
D},\alpha}(\rho)\cdot\sum_{{\sf m}\in{\sf moves}({\sf
last}(\rho))}\alpha(\rho)({\sf m})\cdot{\sf m}(a,q).$

The _trace-probability_ function $\mathit{Tr}_{{\cal D},\alpha}:{\sf
L}^{*}\to[0,1]$ is, given a trace $w$, defined by

$\mathit{Tr}_{{\cal D},\alpha}(w)=\sum_{\rho\in{\sf Paths}(w)}{\sf Pr}_{{\cal
D},\alpha}(\rho).$

We may drop the subscript ${\cal D}$ or $\alpha$ from $\mathit{Tr}_{{\cal
D},\alpha}$ if it is understood. We denote by $\mathit{subDis}_{{\cal
D},\alpha}(w)\in{\sf subDist}(Q)$, the subdistribution after generating a
traces $w$, that is

$\mathit{subDis}_{{\cal D},\alpha}(w)(q)=\sum_{\rho\in{\sf Paths}(w):{\sf
last}(\rho)=q}{\sf Pr}_{{\cal D},\alpha}(\rho).$

We have:

$\mathit{Tr}_{{\cal D},\alpha}(w)=\lVert\mathit{subDis}_{{\cal
D},\alpha}(w)\rVert$ (1)

A version of the following lemma was proved in [7, Lemma 1]:

###### Lemma 1

Let ${\cal D}$ be an MDP and $\alpha$ be a strategy. There exists a trace-
based strategy $\beta$ such that $\mathit{Tr}_{\alpha}=\mathit{Tr}_{\beta}$.

Here, by $\mathit{Tr}_{\alpha}=\mathit{Tr}_{\beta}$ we mean
$\mathit{Tr}_{\alpha}(w)=\mathit{Tr}_{\beta}(w)$ for all traces $w\in{\sf
L}^{*}$.

#### Labeled Markov Chains.

A finite-state labeled Markov chain (MC for short) is an MDP where only a
single move is available in each state, and thus controller’s choice plays no
role. An MC ${\cal C}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ is an MDP where
$\delta:Q\to{\sf Dist}({\sf L}\times Q)$ is a probabilistic transition
function. Since MCs are MDPs, we analogously define paths, and the probability
of a single path inductively as follows: ${\sf Pr}_{{\cal C}}(q)=\mu_{0}(q)$
and ${\sf Pr}_{{\cal C}}(\rho aq)={\sf Pr}_{{\cal
C}}(\rho)\cdot\delta(q^{\prime})(a,q)$ where $q^{\prime}={\sf last}(\rho)$.
The notations $\mathit{subDis}_{{\cal C}}(w)$ and $\mathit{Tr}_{{\cal C}}$ are
defined analogously.

###  2.2 Trace Refinement

Given two MDPs ${\cal D}$ and ${\cal E}$ with the same set ${\sf L}$ of
labels, we say that _${\cal E}$ refines ${\cal D}$_, denoted by ${\cal
D}\sqsubseteq{\cal E}$, if for all strategies $\alpha$ for ${\cal D}$ there
exists some strategy $\beta$ for ${\cal E}$ such that $\mathit{Tr}_{{\cal
D}}=\mathit{Tr}_{{\cal E}}$. We are interested in the problem ${\sf
MDP\sqsubseteq MDP}$, which asks, for two given MDPs ${\cal D}$ and ${\cal
E}$, whether ${\cal D}\sqsubseteq{\cal E}$. The decidability of this problem
was posed as an open question in [7]. We show in Theorem 3.1 that the problem
${\sf MDP\sqsubseteq MDP}$ is undecidable.

We consider various subproblems of ${\sf MDP\sqsubseteq MDP}$, which asks
whether ${\cal D}\sqsubseteq{\cal E}$ holds. Specifically, we speak of the
problem

  * •

${\sf MDP\sqsubseteq MC}$ when ${\cal E}$ is restricted to be an MC;

  * •

${\sf MC\sqsubseteq MDP}$ when ${\cal D}$ is restricted to be an MC;

  * •

${\sf MC\sqsubseteq MC}$ when both ${\cal D}$ and ${\cal E}$ are restricted to
be MCs.

We show in Theorem 3.1 that even the problem ${\sf MC\sqsubseteq MDP}$ is
undecidable. Hence we consider further subproblems. Specifically, we denote by
${\sf MC\sqsubseteq MDP_{m}}$ the problem where the MDP is restricted to use
only memoryless strategies, and by ${\sf MC\sqsubseteq MDP_{pm}}$ the problem
where the MDP is restricted to use only pure memoryless strategies. When both
MDPs ${\cal D}$ and ${\cal E}$ are restricted to use only pure memoryless
strategies, the trace-refinement problem is denoted by ${\sf
MDP_{pm}\sqsubseteq MDP_{pm}}$. The problem ${\sf MC\sqsubseteq MC}$ equals
the _trace-equivalence problem_ for MCs: given two MCs ${\cal C}_{1},{\cal
C}_{2}$ we have ${\cal C}_{1}\sqsubseteq C_{2}$ if and only if
$\mathit{Tr}_{{\cal C}_{1}}=\mathit{Tr}_{{\cal C}_{2}}$ if and only if ${\cal
C}_{2}\sqsubseteq{\cal C}_{1}$. This problem is known to be in NC [20], hence
in P.

##  3 Undecidability Results

In this section we show:

###### Theorem 3.1

The problem ${\sf MC\sqsubseteq MDP}$ is undecidable. Hence a fortiori, ${\sf
MDP\sqsubseteq MDP}$ is undecidable.

###### Proof

To show that the problem ${\sf MC\sqsubseteq MDP}$ is undecidable, we
establish a reduction from the universality problem for probabilistic
automata. A _probabilistic automaton_ is a tuple ${\cal A}=\langle
Q,\mu_{0},{\sf L},\delta,F\rangle$ consisting of a finite set $Q$ of states,
an initial distribution $\mu_{0}\in{\sf Dist}(Q)$, a finite set ${\sf L}$ of
letters, a transition function $\delta:Q\times{\sf L}\to{\sf Dist}(Q)$
assigning to every state and letter a distribution over states, and a set $F$
of final states. For a word $w\in{\sf L}^{*}$ we write $\mathit{dis}_{\cal
A}(w)\in{\sf Dist}(Q)$ for the distribution such that, for all $q\in Q$, we
have that $\mathit{dis}_{\cal A}(w)(q)$ is the probability that, after
inputting $w$, the automaton ${\cal A}$ is in state $q$. We write ${\sf
Pr}_{\cal A}(w)=\sum_{q\in F}\mathit{dis}_{\cal A}(w)(q)$ to denote the
probability that ${\cal A}$ accepts $w$. The _universality problem_ asks,
given a probabilistic automaton ${\cal A}$, whether ${\sf Pr}_{\cal
A}(w)\geq\frac{1}{2}$ holds for all words $w$. This problem is known to be
undecidable [15].

Let ${\cal A}=\langle Q,\mu_{0},{\sf L},\delta,F\rangle$ be a probabilistic
automaton; without loss of generality we assume that ${\sf L}=\\{a,b\\}$. We
construct an MDP ${\cal D}$ such that ${\cal A}$ is universal if and only if
${\cal C}\sqsubseteq{\cal D}$ where ${\cal C}$ is the MC shown in Figure 2.
The MDP ${\cal D}$ is constructed from ${\cal A}$ as follows; see Figure 3.

the automaton ${\cal
A}$$q$$q_{1}$$q_{2}$$x^{\prime},a$$y^{\prime},b$$p$$p_{1}$$p_{2}$$x,a$$y,b$$\Rightarrow$the
MDP ${\cal D}$$q_{c}$$q_{d}$$1,c$$1,d$$q$${\sf
m}$$q_{1}$$q_{2}$$\frac{x^{\prime}}{4},a$$\frac{y^{\prime}}{4},b$$\frac{1}{2},c$$p$${\sf
m}_{d}$$p_{1}$$p_{2}$$~{}\frac{x}{4},a$$\frac{1}{2},d$${\sf
m}_{c}$$~{}\frac{y}{4},b$$\frac{1}{2},c$ Figure 3:  Sketch of the construction
of the MDP ${\cal D}$ from the probabilistic automaton ${\cal A}$, for the
undecidability result of ${\sf MC\sqsubseteq MDP}$. Here, $p$ is an accepting
state whereas $q$ is not. To read the picture, note that in $p$ there is a
transition to the state $p_{1}$ with probability $x$ and label $a$:
$\delta(p,a)(p_{1})=x$.

Its set of states is $Q\cup\\{q_{c},q_{d}\\}$, and its initial distribution is
$\mu_{0}$. (Here and in the following we identify subdistributions $\mu\in{\sf
subDist}(Q)$ and $\mu\in{\sf subDist}(Q\cup\\{q_{c},q_{d}\\})$ if
$\mu(q_{c})=\mu(q_{d})=0$.) We describe the transitions of ${\cal D}$ using
the transition function $\delta$ of ${\cal A}$. Consider a state $q\in Q$:

  * •

If $q\in F$, there are two available moves ${\sf m}_{c},{\sf m}_{d}$; both
emit $a$ with probability $\frac{1}{4}$ and simulate the probabilistic
automaton ${\cal A}$ reading the letter $a$, or emit $b$ with probability
$\frac{1}{4}$ and simulate the probabilistic automaton ${\cal A}$ reading the
letter $b$. With the remaining probability of $\frac{1}{2}$, ${\sf m}_{c}$
emits $c$ and leads to $q_{c}$ and ${\sf m}_{d}$ emits $d$ and leads to
$q_{d}$. Formally, ${\sf m}_{c}(c,q_{c})=\frac{1}{2}$, ${\sf
m}_{d}(d,q_{d})=\frac{1}{2}$ and ${\sf m}_{c}(e,q^{\prime})={\sf
m}_{d}(e,q^{\prime})=\frac{1}{4}\delta(q,e)(q^{\prime})$ where $q^{\prime}\in
Q$ and $e\in\\{a,b\\}$.

  * •

If $q\notin F$, there is a single available move ${\sf m}$ such that ${\sf
m}(d,q_{d})=\frac{1}{2}$ and ${\sf
m}(e,q^{\prime})=\frac{1}{4}\delta(q,e)(q^{\prime})$ where $q^{\prime}\in Q$
and $e\in\\{a,b\\}$.

  * •

The only move from $q_{c}$ is the Dirac distribution on $(c,q_{c})$; likewise
the only move from $q_{d}$ is the Dirac distribution on $(d,q_{d})$.

This MDP ${\cal D}$ “is almost” an MC, in the sense that a strategy $\alpha$
does not influence its behaviour until eventually a transition to $q_{c}$ or
$q_{d}$ is taken. Indeed, for all $\alpha$ and for all $w\in\\{a,b\\}^{*}$ we
have $\mathit{subDis}_{{\cal D},\alpha}(w)=\frac{1}{4^{|w|}}\mathit{dis}_{\cal
A}(w)$. In particular, it follows $\mathit{Tr}_{{\cal
D},\alpha}(w)=\lVert\mathit{subDis}_{{\cal
D},\alpha}(w)\rVert=\frac{1}{4^{|w|}}\lVert\mathit{dis}_{\cal
A}(w)\rVert=\frac{1}{4^{|w|}}$. Further, if $\alpha$ is trace-based we have:

$\displaystyle\mathit{Tr}_{{\cal D},\alpha}(wc)$
$\displaystyle=\lVert\mathit{subDis}_{{\cal D},\alpha}(wc)\rVert$ by (1) (2)
$\displaystyle=\mathit{subDis}_{{\cal D},\alpha}(wc)(q_{c})$ structure of
${\cal D}$ $\displaystyle=\sum_{q\in F}\mathit{subDis}_{{\cal
D},\alpha}(w)(q)\cdot\alpha(w,q)({\sf m}_{c})\cdot\frac{1}{2}$ structure of
${\cal D}$ $\displaystyle=\frac{1}{4^{|w|}}\sum_{q\in F}\mathit{dis}_{\cal
A}(w)(q)\cdot\alpha(w,q)({\sf m}_{c})\cdot\frac{1}{2}$ as argued above

We show that ${\cal A}$ is universal if and only if ${\cal C}\sqsubseteq{\cal
D}$. Let ${\cal A}$ be universal. Define a trace-based strategy $\alpha$ with
$\alpha(w,q)({\sf m}_{c})=\frac{1}{2{\sf Pr}_{\cal A}(w)}$ for all
$w\in\\{a,b\\}^{*}$ and $q\in F$. Note that $\alpha(w,q)({\sf m}_{c})$ is a
probability as ${\sf Pr}_{\cal A}(w)\geq\frac{1}{2}$. Let $w\in\\{a,b\\}^{*}$.
We have:

$\displaystyle\mathit{Tr}_{{\cal D},\alpha}(w)$
$\displaystyle=\frac{1}{4^{|w|}}$ as argued above
$\displaystyle=\mathit{Tr}_{{\cal C}}(w)$ Figure 2

Further we have:

$\displaystyle\mathit{Tr}_{{\cal D},\alpha}(wc)$
$\displaystyle=\frac{1}{4^{|w|}}\sum_{q\in F}\mathit{dis}_{\cal
A}(w)(q)\cdot\alpha(w,q)({\sf m}_{c})\cdot\frac{1}{2}$ by (2)
$\displaystyle=\frac{1}{4^{|w|}}\sum_{q\in F}\mathit{dis}_{\cal
A}(w)(q)\cdot\frac{1}{{\sf Pr}_{\cal A}(w)}\cdot\frac{1}{4}$ definition of
$\alpha$ $\displaystyle=\frac{1}{4^{|w|+1}}$ $\displaystyle{\sf Pr}_{\cal
A}(w)=\sum_{q\in F}\mathit{dis}_{\cal A}(w)(q)$
$\displaystyle=\mathit{Tr}_{{\cal C}}(wc)$ Figure 2

It follows from the definitions of ${\cal D}$ and ${\cal C}$ that for all
$k\geq 1$, we have $\mathit{Tr}_{{\cal D},\alpha}(wc^{k})=\mathit{Tr}_{{\cal
D},\alpha}(wc)=\mathit{Tr}_{{\cal C}}(wc)=\mathit{Tr}_{{\cal C}}(wc^{k})$. We
have $\sum_{e\in\\{a,b,c,d\\}}\mathit{Tr}_{{\cal
D},\alpha}(we)=\mathit{Tr}_{{\cal D},\alpha}(w)=\mathit{Tr}_{{\cal
C}}(w)=\sum_{e\in\\{a,b,c,d\\}}\mathit{Tr}_{{\cal C}}(we)$. Since for
$e\in\\{a,b,c\\}$ we also proved that $\mathit{Tr}_{{\cal
D},\alpha}(we)=\mathit{Tr}_{{\cal C}}(we)$ it follows that $\mathit{Tr}_{{\cal
D},\alpha}(wd)=\mathit{Tr}_{{\cal C}}(wd)$. Hence, as above,
$\mathit{Tr}_{{\cal D},\alpha}(wd^{k})=\mathit{Tr}_{{\cal C}}(wd^{k})$ for all
$k\geq 1$. Finally, if $w\notin(a+b)^{*}\cdot(c^{*}+d^{*})$ then
$\mathit{Tr}_{{\cal D},\alpha}(w)=0=\mathit{Tr}_{{\cal C}}(w)$.

For the converse, assume that ${\cal A}$ is not universal. Then there is
$w\in\\{a,b\\}^{*}$ with ${\sf Pr}_{\cal A}(w)<\frac{1}{2}$. Let $\alpha$ be a
trace-based strategy. Then we have:

$\displaystyle\mathit{Tr}_{{\cal D},\alpha}(wc)$
$\displaystyle=\frac{1}{4^{|w|}}\sum_{q\in F}\mathit{dis}_{\cal
A}(w)(q)\cdot\alpha(w,q)({\sf m}_{c})\cdot\frac{1}{2}$ by (2)
$\displaystyle\leq\frac{1}{4^{|w|}}\cdot\frac{1}{2}\cdot\sum_{q\in
F}\mathit{dis}_{\cal A}(w)(q)$ $\displaystyle\alpha(w,q)({\sf m}_{c})\leq 1$
$\displaystyle=\frac{1}{4^{|w|}}\cdot\frac{1}{2}\cdot{\sf Pr}_{\cal A}(w)$
$\displaystyle{\sf Pr}_{\cal A}(w)=\sum_{q\in F}\mathit{dis}_{\cal A}(w)(q)$
$\displaystyle<\frac{1}{4^{|w|}}\cdot\frac{1}{2}\cdot\frac{1}{2}$ definition
of $w$ $\displaystyle=\mathit{Tr}_{\cal C}(wc)$ Figure 2

We conclude that there is no trace-based strategy $\alpha$ with
$\mathit{Tr}_{{\cal D},\alpha}=\mathit{Tr}_{\cal C}$. By Lemma 1 there is _no_
strategy $\alpha$ with $\mathit{Tr}_{{\cal D},\alpha}=\mathit{Tr}_{\cal C}$.
Hence ${\cal C}\not\sqsubseteq{\cal D}$. ∎

A straightforward reduction from ${\sf MDP\sqsubseteq MDP}$ now establishes:

###### Theorem 3.2

The problem that, given two MDPs ${\cal D}$ and ${\cal E}$, asks whether
${\cal D}\sqsubseteq{\cal E}$ and ${\cal E}\sqsubseteq{\cal D}$ is
undecidable.

##  4 Decidability for Memoryless Strategies

Given two MCs ${\cal C}_{1}$ and ${\cal C}_{2}$, the (symmetric) trace-
equivalence relation ${\cal C}_{1}\sqsubseteq{\cal C}_{2}$ is polynomial-time
decidable [20]. An MDP ${\cal D}$ under a memoryless strategy $\alpha$ induces
a finite MC ${\cal D}(\alpha)$, and thus once a memoryless strategy is fixed
for the MDP, its relation to another given MC in the trace-equivalence
relation $\sqsubseteq$ can be decided in P. Theorems 4.1 and 4.2 provide tight
complexity bounds of the trace-refinement problems for MDPs that are
restricted to use only pure memoryless strategies. In Theorems 4.3 and 4.4 we
establish bounds on the complexity of the problem when randomization is
allowed for memoryless strategies.

###  4.1 Pure Memoryless Strategies

In this subsection, we show that the two problems ${\sf MC\sqsubseteq
MDP_{pm}}$ and ${\sf MDP_{pm}\sqsubseteq MDP_{pm}}$ are NP-complete and
$\Pi^{p}_{2}$-complete.

Membership of ${\sf MC\sqsubseteq MDP_{pm}}$ in NP and ${\sf
MDP_{pm}\sqsubseteq MDP_{pm}}$ in $\Pi^{p}_{2}$ are obtained as follows. Given
an MC ${\cal C}$ and an MDP ${\cal D}$, the polynomial witness of ${\cal
C}\sqsubseteq{\cal D}$ is a pure memoryless strategy $\alpha$ for ${\cal D}$.
Once $\alpha$ is fixed, then ${\cal C}\sqsubseteq{\cal D}(\alpha)$ can be
decided in P. Given another MDP ${\cal E}$, for all pure memoryless strategies
$\beta$ of ${\cal E}$ whether there exists a polynomial witness $\alpha$ for
${\cal E}\sqsubseteq{\cal D}$ such that ${\cal E}(\beta)\sqsubseteq{\cal
D}(\alpha)$ can be decided in P.

The hardness results are by reductions from the _subset-sum problem_ and a
variant of the _quantified subset-sum_ problem. Given a set
$\\{s_{1},s_{2},\cdots,s_{n}\\}$ of natural numbers and $N\in\mathbb{N}$, the
subset-sum problem asks whether there exists a subset
$S\subseteq\\{s_{1},\cdots,s_{n}\\}$ such that $\sum_{s\in S}s=N$. The subset-
sum problem is known to be NP-complete [6]. The quantified version of subset
sum is a game between a _universal player_ and an _existential player_. Given
$k,N\in\mathbb{N}$, the game is played turn-based for $k$ rounds. For each
round $1\leq i\leq k$, two sets $\\{s_{1},s_{2},\cdots,s_{n}\\}$ and
$\\{t_{1},t_{2},\cdots,t_{m}\\}$ of natural numbers are given. In each round
$i$, the universal player first chooses
$S_{i}\subseteq\\{s_{1},\cdots,s_{n}\\}$ and then the existential player
chooses $T_{i}\subseteq\\{t_{1},\cdots,t_{m}\\}$. The existential player wins
if and only if

$\sum_{s\in S_{1}}s+\sum_{t\in T_{1}}t+\cdots+\sum_{s\in S_{k}}s+\sum_{t\in
T_{k}}t=N.$

The quantified subset sum is known to be PSPACE-complete [8]. The proof
therein implies that the variant of the problem with a fixed number $k$ of
rounds is $\Pi^{p}_{2k}$-complete.

To establish the NP-hardness of ${\sf MC\sqsubseteq MDP_{pm}}$, consider an
instance of subset sum, i.e., a set $\\{s_{1},\cdots,s_{n}\\}$ and
$N\in\mathbb{N}$. We construct an MC ${\cal C}$ and an MDP ${\cal D}$ such
that there exists $S\subseteq\\{s_{1},\cdots,s_{n}\\}$ with $\sum_{s\in S}s=N$
if and only if ${\cal C}\sqsubseteq{\cal D}$ when ${\cal D}$ uses only pure
memoryless strategies.

$q_{0}$$q_{b}$$q_{c}$$\frac{N}{P},a$$1-\frac{N}{P},a$$1,c$$1,b$ Figure 4: The
MC ${\cal C}$ in the reduction for NP-hardness of ${\sf MC\sqsubseteq
MDP_{m}}$.

$u_{1}$$\cdots$$u_{k}$${\sf m}_{1,b}$${\sf m}_{1,c}$${\sf m}_{k,b}$${\sf
m}_{k,c}$$u_{b}$$u_{c}$$1,c$$1,b$$b$$c$$b$$c$ Figure 5: The gadget $G_{u}$ for
the set $\\{u_{1},\cdots,u_{k}\\}$.

The MC ${\cal C}$ is shown in Figure 5. it generates traces in $ab^{+}$ with
probability $\frac{N}{P}$ and traces in $ac^{+}$ with probability
$1-\frac{N}{P}$ where $P=s_{1}+\cdots+s_{n}$.

For a set $\\{u_{1},\cdots,u_{k}\\}$, we define a gadget $G_{u}$ that is an
MDP with $k+2$ states: $u_{1},\cdots,u_{k}$ and $u_{b},u_{c}$; see Figure 5.
For all states $u_{i}$, two moves ${\sf m}_{i,b}$ and ${\sf m}_{i,c}$ are
available, the Dirac distributions on $(a,u_{b})$ and $(a,u_{c})$. The states
$u_{b},u_{c}$ emit only the single labels $b$ and $c$. The MDP ${\cal D}$ is
exactly the gadget $G_{s}$ for $\\{s_{1},\cdots,s_{n}\\}$ equipped with the
initial distribution $\mu_{0}$ where $\mu_{0}(s_{i})=\frac{s_{i}}{P}$ for all
$1\leq i\leq n$. Choosing $b$ in $s_{i}$ simulates the membership of $s_{i}$
in $S$ by adding $\frac{s_{i}}{P}$ to the probability of generating $ab^{+}$.

###### Theorem 4.1

The problem ${\sf MC\sqsubseteq MDP_{pm}}$ is NP-complete.

To establish the $\Pi^{p}_{2}$-hardness of ${\sf MDP_{pm}\sqsubseteq
MDP_{pm}}$, consider an instance of quantified subset sum, i.e.,
$N\in\mathbb{N}$ and two sets $\\{s_{1},\cdots,s_{n}\\}$ and
$\\{t_{1},\cdots,t_{m}\\}$. We construct MDPs ${\cal E}_{univ},{\cal
E}_{exist}$ such that the existential player wins in one round if and only if
${\cal E}_{univ}\sqsubseteq{\cal E}_{exist}$ restricted to use pure memoryless
strategies.

Let $P=s_{1}+\cdots+s_{n}$ and $R=t_{1}+\cdots+t_{m}$. Pick a small real
number $0<x<1$ so that $0<xP,xR,xN<1$. Pick real numbers $0\leq
y_{1},y_{2}\leq 1$ such that $y_{1}+xN=y_{2}+xR$.

The MDPs ${\cal E}_{univ}$ and ${\cal E}_{exist}$ have symmetric
constructions. To simulate the choice of the universal player, the MDP ${\cal
E}_{univ}$ is the gadget $G_{s}$ for the set $\\{s_{1},\cdots,s_{n}\\}$ where
two new states $s_{r},s_{y}$ are added. The transitions in $s_{r}$ and $s_{y}$
are the Dirac distributions on $(a,s_{b})$ and $(a,s_{c})$, respectively. The
initial distribution $\mu_{0}$ for ${\cal E}_{univ}$ is such that
$\mu_{0}(s_{y})=\frac{1}{2}y_{1}$ and
$\mu_{0}(s_{r})=1-\frac{1}{2}(xP+y_{1})$, and
$\mu_{0}(s_{i})=\frac{1}{2}xs_{i}$ for all $1\leq i\leq n$. Similarly, to
simulate the counter-attack of the existential player, the MDP ${\cal
E}_{exist}$ is the gadget $G_{t}$ for $\\{t_{1},\cdots,t_{m}\\}$ with two new
states $t_{r},t_{y}$. The transitions in $t_{r}$ and $t_{y}$ are the Dirac
distributions on $(a,t_{b})$ and $(a,t_{c})$, respectively. The initial
distribution $\mu^{\prime}_{0}$ is $\mu^{\prime}_{0}(p_{y})=\frac{1}{2}y_{2}$
and $\mu^{\prime}_{0}(p_{r})=1-\frac{1}{2}(xT+y_{2})$, and
$\mu^{\prime}_{0}(t_{j})=\frac{1}{2}xt_{j}$ for all $1\leq j\leq m$. Choosing
$b$ in a set of states $s_{i}$ by the universal player must be defended by
choosing $c$ in a right set of states $t_{j}$ by existential player such that
the probabilities of emitting $ab^{+}$ in MDPs are equal.

###### Theorem 4.2

The problem ${\sf MDP_{pm}\sqsubseteq MDP_{pm}}$ is $\Pi^{p}_{2}$-complete.

###  4.2 Memoryless Strategies

In this subsection, we provide upper and lower complexity bounds for the
problem ${\sf MC\sqsubseteq MDP_{m}}$: a reduction to the existential theory
of the reals and a reduction from nonnegative factorization of matrices.

A formula of the _existential theory of the reals_ is of the form $\exists
x_{1}\ldots\exists x_{m}~{}R(x_{1},\ldots,x_{n})$, where
$R(x_{1},\ldots,x_{n})$ is a boolean combination of comparisons of the form
$p(x_{1},\ldots,x_{n})\sim 0$, where $p(x_{1},\ldots,x_{n})$ is a multivariate
polynomial and
$\mathord{\sim}\in\\{\mathord{<},\mathord{>},\mathord{\leq},\mathord{\geq},\mathord{=},\mathord{\neq}\\}$.
The validity of closed formulas (i.e., when $m=n$) is decidable in PSPACE [3,
17], and is not known to be PSPACE-hard.

###### Theorem 4.3

The problem ${\sf MC\sqsubseteq MDP_{m}}$ is polynomial-time reducible to the
existential theory of the reals, hence in PSPACE.

$q_{{\mathit{in}}}$$q_{1}$$\vdots$$q_{n}$$q_{{\mathit{fi}}}$$\frac{1}{n},a_{1}$$\frac{1}{n},a_{n}$$b_{1},M[1,1]$$\vdots$$b_{m},M[1,m]$$b_{1},M[n,1]$$\vdots$$b_{m},M[n,m]$$c,1$
Figure 6: The MC ${\cal C}$ of the reduction from NMF to ${\sf MC\sqsubseteq
MDP_{m}}$.

Given a nonnegative matrix $M\in\mathbb{R}^{n\times m}$, a _nonnegative
factorization_ of $M$ is any representation of the form $M=A\cdot W$ where
$A\in\mathbb{R}^{n\times r}$ and $W\in\mathbb{R}^{r\times m}$ are nonnegative
matrices (see [4, 21, 1] for more details). The _NMF problem_ asks, given a
nonnegative matrix $M\in\mathbb{R}^{n\times m}$ and a number $r\in\mathbb{N}$,
whether there exists a factorization $M=A\cdot W$ with nonnegative matrices
$A\in\mathbb{R}^{n\times r}$ and $W\in\mathbb{R}^{r\times m}$. The NMF problem
is known to be NP-hard, but membership in NP is open [21].

Below, we present a reduction from the NMF problem to ${\sf MC\sqsubseteq
MDP_{m}}$. To establish the reduction, consider an instance of the NMF
problem, i.e., a nonnegative matrix $M\in\mathbb{R}^{n\times m}$ and a number
$r\in\mathbb{N}$. We construct an MC ${\cal C}$ and an MDP ${\cal D}$ such
that the NMF instance is a yes-instance if and only if ${\cal
C}\sqsubseteq{\cal D}$ where ${\cal D}$ is restricted to use only memoryless
strategies.

We assume, without loss of generality, that $M$ is a stochastic matrix, that
is $\sum\limits_{j=1}^{m}M[i,j]=1$ for all rows $1\leq i\leq n$. We know, by
[1, Section 5], that there exists a nonnegative factorization of $M$ with rank
$r$ if and only if there exist two stochastic matrices
$A\in\mathbb{R}^{n\times r}$ and $W\in\mathbb{R}^{r\times m}$ such that
$M=A\cdot W$.

The transition probabilities in the MC ${\cal C}$ encode the entries of matrix
$M$. The initial distribution of the MC is the Dirac distribution on
$q_{{\mathit{in}}}$; see Figure 6. There are $n+m+1$ labels
$a_{1},\cdots,a_{n},b_{1},\cdots,b_{m},c$. The transition in
$q_{{\mathit{in}}}$ is the uniform distribution over $\\{(a_{i},q_{i})\mid
1\leq i\leq n\\}$. In each state $q_{i}$, each label $b_{j}$ is emitted with
probability $M[i,j]$, and a transition to $q_{{\mathit{fi}}}$ is taken. In
state $q_{{\mathit{fi}}}$ only $c$ is emitted. Observe that for all $1\leq
i\leq n$ and $1\leq j\leq m$ we have $\mathit{Tr}_{{\cal
C}}(a_{i})=\frac{1}{n}$ and $\mathit{Tr}_{{\cal C}}(a_{i}\cdot b_{j}\cdot
c^{*})=\frac{1}{n}M[i,j]$.

The initial distribution of the MDP ${\cal D}$ is the uniform distribution
over $\\{p_{1},\cdots,p_{n}\\}$; see Figure 7. In each $p_{i}$ (where $1\leq
i\leq n$), there are $r$ moves ${\sf m}_{i,1},{\sf m}_{i,2},\cdots,{\sf
m}_{i,r}$ where ${\sf m}_{i,k}(a_{i},\ell_{k})=1$ and $1\leq k\leq r$. In each
$\ell_{k}$, there are $m$ moves ${\sf m}^{\prime}_{k,1},{\sf
m}^{\prime}_{k,2},\cdots,{\sf m}^{\prime}_{k,m}$ where ${\sf
m}^{\prime}_{k,j}(b_{j},p_{{\mathit{fi}}})=1$ where $1\leq j\leq m$. In state
$p_{{\mathit{fi}}}$, only $c$ is emitted. The probabilities of choosing the
move $m_{i,k}$ in $p_{i}$ and choosing $m^{\prime}_{k,j}$ in $\ell_{k}$
simulate the entries of $A[i,k]$ and $W[k,j]$.

$p_{1}$$\frac{1}{n}$$\vdots$$p_{n}$$\frac{1}{n}$${\sf m}_{1,1}$${\sf
m}_{1,r}$${\sf m}_{n,r}$${\sf m}_{n,1}$$\ell_{1}$$\vdots$$\ell_{r}$${\sf
m}^{\prime}_{1,1}$${\sf m}^{\prime}_{1,r}$${\sf m}^{\prime}_{n,r}$${\sf
m}^{\prime}_{n,1}$$p_{{\mathit{fi}}}$$a_{1}$$a_{1}$$a_{n}$$a_{n}$$b_{1}$$\vdots$$b_{m}$$b_{1}$$\vdots$$b_{m}$$c,1$
Figure 7: The MDP ${\cal D}$ of the reduction from NMF to ${\sf MC\sqsubseteq
MDP_{m}}$.

###### Theorem 4.4

The NMF problem is polynomial-time reducible to ${\sf MC\sqsubseteq MDP_{m}}$,
hence ${\sf MC\sqsubseteq MDP_{m}}$ is NP-hard.

Recall that it is open whether the NMF problem is in NP and whether the
existential theory of the reals is PSPACE-hard. So Theorems 4.3 and 4.4 show
that proving NP-completeness or PSPACE-completeness of ${\sf MC\sqsubseteq
MDP_{m}}$ requires a breakthrough in those areas.

##  5 Bisimulation

In this section we show:

###### Theorem 5.1

The problem ${\sf MDP\sqsubseteq MC}$ is in NC, hence in P.

We prove Theorem 5.1 in two steps: First, in Proposition 1 below, we establish
a link between trace refinement and a notion of bisimulation between
distributions that was studied in [10]. Second, we show that this notion of
bisimulation can be decided efficiently (in NC, hence in P) if one of the MDPs
is an MC. Proposition 1 then implies Theorem 5.1. Along the way, we prove that
bisimulation between two MDPs can be decided in coNP, improving the
exponential-time result from [10]. We rebuild a detailed proof from scratch,
not referring to [10], as the authors were unable to verify some of the
technical claims made in [10].

A _local strategy_ for an MDP ${\cal D}=\langle Q,\mu_{0},{\sf
L},\delta\rangle$ is a function $\alpha:Q\to{\sf Dist}({\sf moves})$ that maps
each state $q$ to a distribution $\alpha(q)\in{\sf Dist}({\sf moves}(q))$ over
moves in $q$. We call $\alpha$ _pure_ if for all states $q$ there is a move
${\sf m}$ such that $\alpha(q)({\sf m})=1$. For a subdistribution $\mu\in{\sf
subDist}(Q)$, a local strategy $\alpha$, and a label $a\in{\sf L}$, define the
_successor_ subdistribution ${\sf Succ}(\mu,\alpha,a)$ with

${\sf Succ}(\mu,\alpha,a)(q^{\prime})=\sum_{q\in Q}\mu(q)\cdot\sum_{{\sf
m}\in{\sf moves}(q)}\alpha(q)({\sf m})\cdot{\sf m}(a,q^{\prime})$

for all $q^{\prime}\in Q$. Let ${\cal D}=\langle Q_{\cal D},\mu^{{\cal
D}}_{0},{\sf L},\delta_{{\cal D}}\rangle$ and ${\cal E}=\langle Q_{\cal
E},\mu^{{\cal E}}_{0},{\sf L},\delta_{{\cal E}}\rangle$ be two MDPs over the
same set ${\sf L}$ of labels. A _bisimulation_ is a relation ${\cal
R}\subseteq{\sf subDist}(Q_{\cal D})\times{\sf subDist}(Q_{\cal E})$ such that
whenever $\mu_{\cal D}\mathrel{{\cal R}}\mu_{\cal E}$ then

  * •

$\lVert\mu_{\cal D}\rVert=\lVert\mu_{\cal E}\rVert$;

  * •

for all local strategies $\alpha_{\cal D}$ there exists a local strategy
$\alpha_{\cal E}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\mathrel{{\cal R}}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$;

  * •

for all local strategies $\alpha_{\cal E}$ there exists a local strategy
$\alpha_{\cal D}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\mathrel{{\cal R}}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$.

As usual, a union of bisimulations is a bisimulation. Denote by
$\mathord{\sim}$ the union of all bisimulations, i.e., $\mathord{\sim}$ is the
largest bisimulation. We write ${\cal D}\sim{\cal E}$ if $\mu^{\cal
D}_{0}\sim\mu^{{\cal E}}_{0}$. In general, the set $\sim$ is uncountably
infinite, so methods for computing state-based bisimulation (e.g., partition
refinement) are not applicable. The following proposition establishes a link
between trace refinement and bisimulation.

###### Proposition 1

Let ${\cal D}$ be an MDP and ${\cal C}$ be an MC. Then ${\cal D}\sim{\cal C}$
if and only if ${\cal D}\sqsubseteq{\cal C}$.

We often view a subdistribution $d\in{\sf subDist}(Q)$ as a row vector
$d\in[0,1]^{Q}$. For a local strategy $\alpha$ and a label $a$, define the
_transition matrix_ $\Delta_{\alpha}(a)\in[0,1]^{Q\times Q}$ with
$\Delta_{\alpha}(a)[q,q^{\prime}]=\sum_{{\sf m}\in{\sf
moves}(q)}\alpha(q)({\sf m})\cdot{\sf m}(a,q^{\prime})$. Viewing
subdistributions $\mu$ as row vectors, we have:

${\sf Succ}(\mu,\alpha,a)=\mu\cdot\Delta_{\alpha}(a)$ (3)

In the following we consider MDPs ${\cal D}=\langle Q,\mu^{{\cal D}}_{0},{\sf
L},\delta\rangle$ and ${\cal E}=\langle Q,\mu^{{\cal E}}_{0},{\sf
L},\delta\rangle$ over the same state space. This is without loss of
generality, since we might take the disjoint union of the state spaces. Since
${\cal D}$ and ${\cal E}$ differ only in the initial distribution, we will
focus on ${\cal D}$.

Let $B\in\mathbb{R}^{Q\times k}$ with $k\geq 1$. Assume the label set is ${\sf
L}=\\{a_{1},\ldots,a_{|{\sf L}|}\\}$. For $\mu\in{\sf subDist}(Q)$ and a local
strategy $\alpha$ we define a point $p(\mu,\alpha)\in\mathbb{R}^{{|{\sf
L}|}\cdot k}$ such that

$p(\mu,\alpha)\ =\
\big{(}\mu\Delta_{\alpha}(a_{1})B\quad\mu\Delta_{\alpha}(a_{2})B\quad\cdots\quad\mu\Delta_{\alpha}(a_{|{\sf
L}|})B\big{)}.$

For the reader’s intuition, we remark that we will choose matrices
$B\in\mathbb{R}^{Q\times k}$ so that if two subdistributions $\mu_{\cal
D},\mu_{\cal E}$ are bisimilar then $\mu_{\cal D}B=\mu_{\cal E}B$. (In fact,
one can compute $B$ so that the converse holds as well, i.e., $\mu_{\cal
D}\sim\mu_{\cal E}$ if and only if $\mu_{\cal D}B=\mu_{\cal E}B$.) It follows
that, for subdistributions $\mu_{\cal D},\mu_{\cal E}$ and local strategies
$\alpha_{\cal D},\alpha_{\cal E}$, if ${\sf Succ}(\mu_{\cal D},\alpha_{\cal
D},a)\sim{\sf Succ}(\mu_{\cal E},\alpha_{\cal E},a)$ holds for all $a\in{\sf
L}$ then $p(\mu_{\cal D},\alpha_{\cal D})=p(\mu_{\cal E},\alpha_{\cal E})$.
Let us also remark that for fixed $\mu\in{\sf subDist}(Q)$, the set
$P_{\mu}=\\{p(\mu,\alpha)\mid\alpha\text{ is a local
strategy}\\}\subseteq\mathbb{R}^{{|{\sf L}|}\cdot k}$ is a (bounded and
convex) polytope. As a consequence, if $\mu_{\cal D}\sim\mu_{\cal E}$ then the
polytopes $P_{\mu_{\cal D}}$ and $P_{\mu_{\cal E}}$ must be equal. In the next
paragraph we define _“extremal”_ strategies $\widehat{\alpha}$, which
intuitively are local strategies such that $p(\mu,\widehat{\alpha})$ is a
vertex of the polytope $P_{\mu}$.

Let $\vec{v}\in\mathbb{R}^{{|{\sf L}|}\cdot k}$ be a _column_ vector; we
denote column vectors in boldface. We view $\vec{v}$ as a “direction”. Recall
that $d_{q}$ is the Dirac distribution on the state $q$. A pure local strategy
$\widehat{\alpha}$ is _extremal in direction $\vec{v}$ with respect to $B$_ if

$\displaystyle p(d_{q},\alpha)\vec{v}\leq p(d_{q},\widehat{\alpha})\vec{v}$
(4) $\displaystyle
p(d_{q},\alpha)\vec{v}=p(d_{q},\widehat{\alpha})\vec{v}\text{\quad implies
\quad}p(d_{q},\alpha)=p(d_{q},\widehat{\alpha})$ (5)

for all states $q\in Q$ and all pure local strategies $\alpha$.

By linearity, if (4) and (5) hold for all pure local strategies $\alpha$ then
(4) and (5) hold for all local strategies $\alpha$. We say a local strategy
$\widehat{\alpha}$ is _extremal with respect to $B$_ if there is a direction
$\vec{v}$ such that $\widehat{\alpha}$ is extremal in direction $\vec{v}$ with
respect to $B$.

###### Proposition 2

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let
$B_{1}\in\mathbb{R}^{Q\times k_{1}}$ and $B_{2}\in\mathbb{R}^{Q\times k_{2}}$
for $k_{1},k_{2}\geq 1$. Denote by
$\mathcal{V}_{1},\mathcal{V}_{2}\subseteq\mathbb{R}^{Q}$ the subspaces spanned
by the columns of $B_{1},B_{2}$, respectively. Assume
$\mathcal{V}_{1}\subseteq\mathcal{V}_{2}$. If a local strategy
$\widehat{\alpha}$ is extremal with respect to $B_{1}$ then $\widehat{\alpha}$
is extremal with respect to $B_{2}$.

In light of this fact, we may define that $\widehat{\alpha}$ be _extremal with
respect to a column-vector space $\mathcal{V}$_ if $\widehat{\alpha}$ is
extremal with respect to a matrix $B$ whose column space equals $\mathcal{V}$.

The following proposition describes a vector space $\mathcal{V}$ so that two
subdistributions are bisimilar if and only if their difference (viewed as a
row vector) is orthogonal to $\mathcal{V}$.

###### Proposition 3

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let
$\mathcal{V}\subseteq\mathbb{R}^{Q}$ be the smallest column-vector space such
that

  * •

$\vec{1}=(1\ 1\cdots 1)^{T}\in\mathcal{V}$ (where $T$ denotes transpose) and

  * •

$\Delta_{\widehat{\alpha}}(a)\vec{u}\in\mathcal{V}$ for all
$\vec{u}\in\mathcal{V}$, all labels $a\in{\sf L}$ and local strategies
$\widehat{\alpha}$ that are extremal with respect to $\mathcal{V}$.

Then for all $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$, we have
$\mu_{\cal D}\sim\mu_{\cal E}$ if and only if $\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}$ for all $\vec{u}\in\mathcal{V}$.

Proposition 3 allows us to prove the following theorem:

###### Theorem 5.2

The problem that, given two MDPs ${\cal D}$ and ${\cal E}$, asks whether
${\cal D}\sim{\cal E}$ is in coNP.

In the following, without loss of generality, we consider an MDP ${\cal
D}=\langle Q,\mu^{{\cal D}}_{0},{\sf L},\delta\rangle$ and an MC ${\cal
C}=\langle Q_{\cal C},\mu^{{\cal C}}_{0},{\sf L},\delta\rangle$ with $Q_{\cal
C}\subseteq Q$. We may view subdistributions $\mu_{\cal C}\in{\sf
subDist}(Q_{\cal C})$ as $\mu_{\cal C}\in{\sf subDist}(Q)$ in the natural way.
The following proposition is analogous to Proposition 3.

###### Proposition 4

Let ${\cal D}=\langle Q,\mu^{{\cal D}}_{0},{\sf L},\delta\rangle$ be an MDP
and ${\cal C}=\langle Q_{\cal C},\mu^{{\cal C}}_{0},{\sf L},\delta\rangle$ be
an MC with $Q_{\cal C}\subseteq Q$. Let $\mathcal{V}\subseteq\mathbb{R}^{Q}$
be the smallest column-vector space such that

  * •

$\vec{1}=(1\ 1\cdots 1)^{T}\in\mathcal{V}$ (where $T$ denotes transpose) and

  * •

$\Delta_{\alpha}(a)\vec{u}\in\mathcal{V}$ for all $\vec{u}\in\mathcal{V}$, all
labels $a\in{\sf L}$ and all local strategies $\alpha$.

Then for all $\mu_{\cal D}\in{\sf subDist}(Q)$ and all $\mu_{\cal C}\in{\sf
subDist}(Q_{\cal C})$, we have $\mu_{\cal D}\sim\mu_{\cal C}$ if and only if
$\mu_{\cal D}\vec{u}=\mu_{\cal C}\vec{u}$ for all $\vec{u}\in\mathcal{V}$.

Notice the differences to Proposition 3: there we considered all extremal
local strategies (potentially exponentially many), here we consider all local
strategies (in general infinitely many). However, we show that one can
efficiently find few local strategies that span all local strategies. This
allows us to reduce (in logarithmic space) the bisimulation problem between an
MDP and an MC to the bisimulation problem between two MCs, which is equivalent
to the trace-equivalence problem in MCs (by Proposition 1). The latter problem
is known to be in NC [20]. Theorem 5.1 then follows with Proposition 1.

## References

  * [1] S. Arora, R. Ge, R. Kannan, and A. Moitra.  Computing a nonnegative matrix factorization - provably.  In STOC, pages 145–162. ACM, 2012.
  * [2] V. D. Blondel and V. Canterini.  Undecidable problems for probabilistic automata of fixed dimension.  Theoretical Computer Science, 36 (3):231–245, 2003.
  * [3] J. Canny.  Some algebraic and geometric computations in PSPACE.  In STOC, pages 460–467, 1988.
  * [4] J. Cohen and U. Rothblum.  Nonnegative ranks, decompositions, and factorizations of nonnegative matrices.  Linear Algebra and its Applications, 190:149–168, 1993.
  * [5] A. Condon and R. Lipton.  On the complexity of space bounded interactive proofs (extended abstract).  In FOCS, pages 462–467, 1989.
  * [6] T. Cormen, C. Stein, R. Rivest, and C. E. Leiserson.  Introduction to algorithms.  McGraw-Hill Higher Education, 2nd edition, 2001.
  * [7] L. Doyen, T.A. Henzinger, and J.-F. Raskin.  Equivalence of labeled Markov chains.  International Journal on Foundations of Computer Science, 19(3):549–563, 2008.
  * [8] J. Fearnley and M. Jurdzinski.  Reachability in two-clock timed automata is pspace-complete.  Information and Computation, 243:26–36, 2015.
  * [9] R. Greenlaw, H.J. Hoover, and W.L. Ruzzo.  Limits to parallel computation: P-completeness theory.  Oxford University Press, 1995.
  * [10] H. Hermanns, J. Krčál, and J. Křetínský.  Probabilistic bisimulation: Naturally on distributions.  In CONCUR, volume 8704 of LNCS, pages 249–265. Springer, 2014\.  Technical report at `http://arxiv.org/abs/1404.5084`.
  * [11] S. Kiefer, A.S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell.  Language equivalence for probabilistic automata.  In CAV, volume 6806 of LNCS, pages 526–540. Springer, 2011\.
  * [12] S. Kiefer, A.S. Murawski, J. Ouaknine, B. Wachter, and J. Worrell.  APEX: An analyzer for open probabilistic programs.  In CAV, volume 7358 of LNCS, pages 693–698. Springer, 2012\.
  * [13] L. Li and Y. Feng.  Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties.  Information and Computation, 244:229–244, 2015.
  * [14] T.M. Ngo, M. Stoelinga, and M. Huisman.  Confidentiality for probabilistic multi-threaded programs and its verification.  In Engineering Secure Software and Systems, volume 7781 of LNCS, pages 107–122. Springer, 2013.
  * [15] A. Paz.  Introduction to Probabilistic Automata.  Academic Press, 1971.
  * [16] S. Peyronnet, M. de Rougemont, and Y. Strozecki.  Approximate verification and enumeration problems.  In ICTAC, volume 7521 of LNCS, pages 228–242. Springer, 2012\.
  * [17] J. Renegar.  On the computational complexity and geometry of the first-order theory of the reals. Parts I–III.  Journal of Symbolic Computation, 13(3):255–352, 1992.
  * [18] M.-P. Schützenberger.  On the definition of a family of automata.  Information and Control, 4:245–270, 1961.
  * [19] W. Tzeng.  A polynomial-time algorithm for the equivalence of probabilistic automata.  SIAM Journal on Computing, 21(2):216–227, 1992.
  * [20] W. Tzeng.  On path equivalence of nondeterministic finite automata.  Information Processing Letters, 58(1):43–46, 1996.
  * [21] S. Vavasis.  On the complexity of nonnegative matrix factorization.  SIAM Journal on Optimization, 20(3):1364–1377, 2009.

##  Appendix 0.A Proofs of Section 2

In this section we prove Lemma 1 from the main text:

Lemma 1. Let ${\cal D}$ be an MDP and $\alpha$ be a strategy. There exists a
trace-based strategy $\beta$ such that
$\mathit{Tr}_{\alpha}=\mathit{Tr}_{\beta}$.

###### Proof

Let $\alpha$ be a strategy of the MDP ${\cal D}=\langle Q,\mu_{0},{\sf
L},\delta\rangle$, and let ${\sf Paths}(w,q)=\\{\rho\in{\sf Paths}({\cal
D})\mid{\sf trace}(\rho)=w\text{ and }{\sf last}(\rho)=q\\}$. We define a
trace-based strategy $\beta:{\sf L}^{*}\times Q\to{\sf Dist}({\sf moves})$,
given a pair of trace $w$ and state $q$, such that

$\beta(w,q)=\sum_{\rho\in{\sf Paths}(w,q)}\frac{{\sf Pr}_{{\cal
D},\alpha}(\rho)}{\mathit{subDis}_{{\cal D},\alpha}(w)(q)}\cdot\alpha(\rho)$

if $q\in S_{w,\alpha}$; and the uniform distribution on ${\sf moves}(q)$
otherwise.

We prove that $\mathit{subDis}_{{\cal D},\alpha}(w)=\mathit{subDis}_{{\cal
D},\beta}(w)$ for all traces $w\in{\sf L}^{*}$. The proof is by induction on
the length of $w$. The induction base holds since for the empty trace
$\epsilon$, we have $\mathit{subDis}_{{\cal
D},\alpha}(\epsilon)=\mathit{subDis}_{{\cal D},\beta}(\epsilon)=\mu_{0}$. For
the induction step, we assume that two subdistributions
$\mathit{subDis}_{{\cal D},\alpha}(v)=\mathit{subDis}_{{\cal D},\beta}(v)$ are
equal for all traces $v$ with length $\lvert v\rvert\leq k$. Let $w=v\cdot a$
be a trace of length $k+1$. By definition, $\mathit{subDis}_{{\cal
D},\alpha}(w)(q)=\sum_{\rho\in{\sf Paths}(w,q)}{\sf Pr}_{{\cal
D},\alpha}(\rho)$ for all states $q$. Since each path $\rho$ with the trace
$w$ is a continuation of a path $\rho^{\prime}$ such that ${\sf
trace}(\rho^{\prime})=v$, and $\rho^{\prime}$ ends in some state
$q^{\prime}\in S_{v,\alpha}$ where the label $a$ is generated under the
strategy $\alpha$. We thus have

$\displaystyle\mathit{subDis}_{{\cal D},\alpha}(w)(q)=$
$\displaystyle\sum_{q^{\prime}\in S_{v,\alpha}}\,\sum_{\rho^{\prime}\in{\sf
Paths}(v,q^{\prime})}{\sf Pr}_{{\cal D},\alpha}(\rho^{\prime})\sum_{m\in{\sf
moves}(q^{\prime})}\alpha(\rho^{\prime})({\sf m})\cdot{\sf m}(a,q)$
$\displaystyle=\sum_{q^{\prime}\in S_{v,\alpha}}\,\sum_{m\in{\sf
moves}(q^{\prime})}\sum_{\rho^{\prime}\in{\sf Paths}(v,q^{\prime})}{\sf
Pr}_{{\cal D},\alpha}(\rho^{\prime})\cdot\alpha(\rho^{\prime})({\sf
m})\cdot{\sf m}(a,q)$ $\displaystyle=\sum_{q^{\prime}\in
S_{v,\alpha}}\,\sum_{m\in{\sf moves}(q^{\prime})}\mathit{subDis}_{{\cal
D},\alpha}(v)(q^{\prime})\cdot$
$\displaystyle\quad\quad\quad\quad\quad\left(\sum_{\rho^{\prime}\in{\sf
Paths}(v,q^{\prime})}\frac{{\sf Pr}_{{\cal
D},\alpha}(\rho^{\prime})}{\mathit{subDis}_{{\cal
D},\alpha}(v)(q^{\prime})}\cdot\alpha(\rho^{\prime})({\sf m})\cdot{\sf
m}(a,q)\right)$ and based on the definition of $\beta$ and the induction
hypothesis, we have $\displaystyle=\sum_{q^{\prime}\in
S_{v,\beta}}\,\sum_{m\in{\sf moves}(q^{\prime})}\mathit{subDis}_{{\cal
D},\beta}(v)(q^{\prime})\cdot\beta(v,q^{\prime})({\sf m})\cdot{\sf m}(a,q)$
and as $\beta$ is traced-based, then $\displaystyle=\sum_{q^{\prime}\in
S_{v,\beta}}\,\mathit{subDis}_{{\cal D},\beta}(v)(q^{\prime})\sum_{m\in{\sf
moves}(q^{\prime})}\beta(v,q^{\prime})({\sf m})\cdot{\sf m}(a,q)$
$\displaystyle=\mathit{subDis}_{{\cal D},\beta}(w)(q).$

The proof of the inductive step is complete; we have proved that
$\mathit{subDis}_{{\cal D},\alpha}(w)=\mathit{subDis}_{{\cal D},\beta}(w)$ for
all traces $w\in{\sf L}^{*}$.

This implies that $\mathit{Tr}_{\alpha}=\mathit{Tr}_{\beta}$, and completes
the proof. ∎

##  Appendix 0.B Proofs of Section 3

Theorem 3.2. The problem that, given two MDPs ${\cal D}$ and ${\cal E}$, asks
whether ${\cal D}\sqsubseteq{\cal E}$ and ${\cal E}\sqsubseteq{\cal D}$ is
undecidable.

###### Proof

We reduce the problem ${\sf MDP\sqsubseteq MDP}$ to the problem that asks,
given two MDPs ${\cal D}_{1}$ and ${\cal D}_{2}$, whether both ${\cal
D}_{1}\sqsubseteq{\cal D}_{2}$ and ${\cal D}_{2}\sqsubseteq{\cal D}_{1}$
holds.

The reduction is as follows; given two MDPs ${\cal D}=\langle Q,\mu_{0},{\sf
L},\delta\rangle$ and ${\cal E}=\langle Q^{\prime},\mu^{\prime}_{0},{\sf
L},\delta^{\prime}\rangle$, construct the MDP ${\cal D}+{\cal E}$ by simply
having a copy of each MDP, adding a new label $\\#$ and a new state $p_{0}$.
The initial distribution of ${\cal D}+{\cal E}$ is the Dirac distribution on
$p_{0}$, where there are two available moves ${\sf m}_{{\cal D}}$ and ${\sf
m}_{{\cal E}}$. Let ${\sf m}_{{\cal D}}(\\#,q)=\mu_{0}(q)$ for all $q\in Q$
and ${\sf m}_{{\cal D}}(\\#,q)=0$ otherwise; and let ${\sf m}_{{\cal
E}}(\\#,q)=\mu^{\prime}_{0}(q)$ for all $q\in Q^{\prime}$ and ${\sf m}_{{\cal
D}}(\\#,q)=0$ otherwise. We see that ${\cal D}+{\cal E}$ always starts by
generating label $\\#$ with probability $1$, and based on the strategic choice
can simulate ${\cal D}$ or ${\cal E}$.

We construct ${\cal E}_{2}$ from ${\cal E}$ as follows. We extend the set of
labels with the new label $\\#$ and set $Q^{\prime}$ of states with a new
state $q_{0}$. The new initial distribution of ${\cal D}$ is the Dirac
distribution on $q_{0}$, where there is only one available move ${\sf m}$ such
that ${\sf m}(\\#,q)=\mu^{\prime}_{0}(q)$. We see that ${\cal E}_{2}$ always
starts by generating label $\\#$ with probability $1$, and then simply behaves
as ${\cal E}$.

We argue that ${\cal D}\sqsubseteq{\cal E}$ if, and only if, ${\cal
E}_{2}\sqsubseteq{\cal D}+{\cal E}$ and ${\cal D}+{\cal E}\sqsubseteq{\cal
E}_{2}$. This follows from three simple observations:

  * •

the relation ${\cal E}_{2}\sqsubseteq{\cal D}+{\cal E}$ always holds.
Strategies of ${\cal D}+{\cal E}$ can choose to simulate ${\cal E}_{2}$ by
playing ${\sf m}_{{\cal E}}$ with probability $1$.

  * •

if ${\cal D}\sqsubseteq{\cal E}$ then ${\cal D}+{\cal E}\sqsubseteq{\cal
E}_{2}$: a strategy $\gamma$ of ${\cal D}+{\cal E}$, at first step, would play
${\sf m}_{{\cal D}}$ and ${\sf m}_{{\cal E}}$ with probabilities
$\gamma(p_{0})({\sf m}_{{\cal D}})$ and $\gamma(p_{0})({\sf m}_{{\cal E}})$.
Next, it follows a strategy $\alpha$ for the copy of ${\cal D}$ and a strategy
$\beta$ for the copy of ${\cal E}$. Since ${\cal D}\sqsubseteq{\cal E}$, then
there exists some strategy $\beta^{\prime}$ of ${\cal E}$ such that
$\mathit{Tr}_{{\cal D},\alpha}=\mathit{Tr}_{{\cal E},\beta^{\prime}}$. Then a
strategy of ${\cal E}_{2}$ that, at all steps, plays $\beta^{\prime}$ with
probability $\gamma(p_{0})({\sf m}_{{\cal D}})$ and plays $\beta$ with
probability $\gamma(p_{0})({\sf m}_{{\cal E}})$ would result in the same
trace-probability function as $\gamma$ of ${\cal D}+{\cal E}$ does. It gives
${\cal D}+{\cal E}\sqsubseteq{\cal E}_{2}$.

  * •

if ${\cal D}+{\cal E}\sqsubseteq{\cal E}_{2}$ then ${\cal D}\sqsubseteq{\cal
E}$: consider a strategy $\alpha$ of ${\cal D}$. Construct strategy
$\alpha^{\prime}$ of ${\cal D}+{\cal E}$ such that
$\alpha^{\prime}(p_{0})({\sf m}_{{\cal D}})=1$ and
$\alpha^{\prime}(p_{0}\\#\rho)=\alpha(\rho)$ for all paths $\rho$. Since
${\cal D}+{\cal E}\sqsubseteq{\cal E}_{2}$, there must be some strategy
$\beta^{\prime}$ such that $\mathit{Tr}_{{\cal D}+{\cal
E},\alpha^{\prime}}=\mathit{Tr}_{{\cal E}_{2},\beta^{\prime}}$. For the
strategy $\beta$ where $\beta(\rho)=\beta^{\prime}(q_{0}\\#\rho)$ for all
paths $\rho$, we have $\mathit{Tr}_{{\cal D},\alpha}=\mathit{Tr}_{{\cal
E},\beta}$, and thus ${\cal D}\sqsubseteq{\cal E}$.

##  Appendix 0.C Proofs of Section 4

###  0.C.1 Proofs of Theorems 4.1 and 4.2

Theorem 4.1. The problem ${\sf MC\sqsubseteq MDP_{pm}}$ is NP-complete.

###### Proof

Given an instance of the subset-sum problem, a set
$\\{s_{1},s_{2},\cdots,s_{n}\\}$ and $N\in\mathbb{N}$, we construct the MC
${\cal C}$ and an MDP ${\cal D}$ as described in subsection 4.1. We prove that
there exists a subset $S\subseteq\\{s_{1},s_{2},\cdots,s_{n}\\}$ where
$\sum_{s\in S}s=N$ if and only if ${\cal C}\sqsubseteq{\cal D}$ when ${\cal
D}$ uses only pure memoryless strategies.

Observe that, in one hand, $\mathit{Tr}_{{\cal C}}(ab^{+})=\frac{N}{P}$ and
$\mathit{Tr}_{{\cal C}}(ac^{+})=1-\frac{N}{P}$ holds for the MC ${\cal C}$. On
the other hand, in the MDP ${\cal D}$, strategies would purely choose between
moves ${\sf m}_{i,b}$ and ${\sf m}_{i,c}$ in states $s_{i}$. For a pure
strategy $\alpha$ for ${\cal D}$, let $S_{\alpha}$ be the set of states
$s_{i}$ where $\alpha(s_{i})=m_{i,b}$. Then,
$\mathit{Tr}_{D}(ab^{+})=\sum_{s\in S_{\alpha}}\frac{s}{P}$ and
$\mathit{Tr}_{D}(ac^{+})=1-Tr_{D}(ab^{+})$. The above arguments provide that
${\cal C}\sqsubseteq{\cal D}$ if and only if there exists a strategy $\alpha$
for ${\cal D}$ such that $\sum_{s\in S_{\alpha}}\frac{s}{P}=\frac{N}{P}$. It
implies that the instance of subset problem is positive, meaning that there
exists a subset $S\subseteq\\{s_{1},s_{2},\cdots,s_{n}\\}$ such that
$\sum_{s\in S}s=N$, if and only if ${\cal C}\sqsubseteq{\cal D}$ when ${\cal
D}$ uses only pure memoryless strategies. The NP-hardness results follows.

Theorem 4.2. The problem ${\sf MDP_{pm}\sqsubseteq MDP_{pm}}$ is
$\Pi^{p}_{2}$-complete.

###### Proof

Given an instance of the quantified subset-sum problem, two sets
$\\{s_{1},s_{2},\cdots,s_{n}\\}$ and $\\{t_{1},t_{2},\cdots,t_{m}\\}$ and
$N\in\mathbb{N}$, we construct the MDPs ${\cal E}_{univ}$ and ${\cal
E}_{exist}$ as described in subsection 4.1. We prove that the existential
player wins in one round if and only if ${\cal E}_{univ}\sqsubseteq{\cal
E}_{exist}$ where the MDPs use only pure memoryless strategies.

We see that the strategic choices in the MDPs are relevant only in states
$s_{i}$ and $t_{j}$. For a pure strategy $\alpha$ of ${\cal E}_{univ}$, let
$S_{\alpha}$ be the set of states $s_{i}$ where $\alpha(s_{i})=m_{i,b}$. We
therefore have $\mathit{Tr}_{{\cal
E}_{univ}}(ab^{+})=\frac{1}{2}y_{1}+\frac{1}{2}\sum_{s\in
S_{\alpha}}\frac{xs}{P}$. For a pure strategy $\beta$ of ${\cal E}_{exist}$,
let $T_{\beta}$ be the set of states $t_{j}$ where $\beta(t_{j})=m_{i,c}$.
Then, $\mathit{Tr}_{{\cal
E}_{exist}}(ab^{+})=\frac{1}{2}y_{2}+\frac{1}{2}R(1-\sum_{t\in
T_{\beta}}\frac{xt}{R})$. Since $y_{1}+xN=y_{2}+xR$, to achieve
$\mathit{Tr}_{{\cal E}_{univ}}=\mathit{Tr}_{{\cal E}_{exist}}$ the equality
$\sum_{s\in S_{\alpha}}s=N-\sum_{t\in T_{\beta}}t$ must be guaranteed. It
shows that the existential player wins in one round, meaning that for all
subsets $S\subseteq\\{s_{1},s_{2},\cdots,s_{n}\\}$ there exists a subset
$T\subseteq\\{t_{1},t_{2},\cdots,t_{n}\\}$ such that $\sum_{s\in
S}s+\sum_{t\in T}t=N$, if and only if for all strategies $\alpha$ of ${\cal
D}$ there exists some strategy $\beta$ for ${\cal E}$ such that $\sum_{s\in
S_{\alpha}}s=N-\sum_{t\in T_{\beta}}t$ implying $\mathit{Tr}_{{\cal
E}_{univ}}=\mathit{Tr}_{{\cal E}_{exist}}$. Note that $\alpha$ and $\beta$ are
chosen pure and memoryless. The $\Pi^{p}_{2}$-hardness result follows.

###  0.C.2 Proof of Theorem 4.3

In this section we prove Theorem 4.3 from the main text:

Theorem 4.3. The problem ${\sf MC\sqsubseteq MDP_{m}}$ is polynomial-time
reducible to the existential theory of the reals, hence in PSPACE.

Given an MC ${\cal C}=\langle Q,\mu_{0},{\sf L},\delta\rangle$, to each label
$a\in{\sf L}$ we associate a _transition matrix_ $\Delta(a)\in[0,1]^{Q\times
Q}$ with $\Delta(a)[q,q^{\prime}]=\delta(q)(a,q^{\prime})$. We view
subdistributions $\mu_{0}$ over states as row vectors $\mu_{0}\in[0,1]^{Q}$.
We denote column vectors in boldface; in particular, $\vec{1}\in\\{1\\}^{Q}$
and $\vec{0}\in\\{0\\}^{Q}$ are column vectors all whose entries are $1$ and
$0$, respectively. We build on [14KW-ICALP, Proposition 10] which
reads—translated to our framework—as follows:

###### Proposition 5

Let ${\cal C}_{1}=\langle Q_{1},\mu_{0},{\sf L},\delta\rangle$ and ${\cal
C}_{2}=\langle Q_{2},\mu^{\prime}_{0},{\sf L},\delta^{\prime}\rangle$ be MCs
with $Q$ as the disjoint union of $Q_{1},Q_{2}$. Then $\mathit{Tr}_{{\cal
C}_{1}}=\mathit{Tr}_{{\cal C}_{2}}$ if and only if there exists a matrix
$F\in\mathbb{R}^{Q\times Q}$ such that

  * •

the first row of $F$ equals $(\mu_{0},-\mu^{\prime}_{0})$,

  * •

$F\vec{1}=\vec{0}$,

and moreover, for all labels $a\in{\sf L}$ there exist matrices
$M(a)\in\mathbb{R}^{Q\times Q}$ such that

$F\begin{pmatrix}\Delta(a)\ &\ 0\\\ 0\ &\
\Delta^{\prime}(a)\end{pmatrix}=M(a)F$

where $\Delta(a),\Delta(a)^{\prime}$ are the transition matrices of $C_{1}$
and ${\cal C}_{2}$ for the label $a$.

With this at hand we prove Theorem 4.3:

######  Proof (of Theorem 4.3)

Let ${\cal C}=\langle Q_{1},\mu_{0},{\sf L},\delta\rangle$ be an MC and ${\cal
D}=\langle Q_{2},\mu^{\prime}_{0},{\sf L},\delta^{\prime}\rangle$ be an MDP
with $Q$ as the disjoint union of $Q_{1},Q_{2}$. A memoryless strategy
$\alpha$ of ${\cal D}$ can be characterized by numbers $x_{q,{\sf m}}\in[0,1]$
where $q\in Q_{2}$ and ${\sf m}\in{\sf moves}(q)$, such that $x_{q,{\sf
m}}=\alpha(q)({\sf m})$. We have $\sum_{{\sf m}\in{\sf moves}(q)}x_{q,{\sf
m}}=1$ for all states $q$. We write $\overline{x}$ for the collection
$(x_{q,{\sf m}})_{q\in Q_{2},\ {\sf m}\in{\sf moves}(q)}$, and
$\alpha(\overline{x})$ for the memoryless strategy characterized by
$\overline{x}$. We have:

$\displaystyle{\cal C}\sqsubseteq{\cal D}\text{ for~{}${\cal D}$ restricted to
memoryless strategies}$
$\displaystyle\Longleftrightarrow\exists\,\text{memoryless strategy
}\alpha:\mathit{Tr}_{{\cal C}}=\mathit{Tr}_{{\cal D},\alpha}$ definition
$\displaystyle\Longleftrightarrow\mathit{Cond}$
$\displaystyle\text{Proposition~{}\ref{prop-Bjoern}},$

where $\mathit{Cond}$ is the following condition:

> There exist
>
>   * •
>
> $x_{q,{\sf m}}\in[0,1]$ for all $q\in Q_{2}$ and all ${\sf m}\in{\sf
> moves}(q)$
>
>   * •
>
> matrices $M(a)\in\mathbb{R}^{Q\times Q}$ for all labels $a\in{\sf L}$,
>
>   * •
>
> a matrix $F\in\mathbb{R}^{Q\times Q}$
>
>

>
> such that
>
>   * •
>
> $\sum_{{\sf m}\in{\sf moves}(q)}x_{q,{\sf m}}=1$ for all $q\in Q_{2}$,
>
>   * •
>
> the first row of $F$ equals $(\mu_{0},-\mu^{\prime}_{0})$,
>
>   * •
>
> $F\vec{1}=\vec{0}$,
>
>   * •
>
> for all labels $a\in{\sf L}$,
>
> $F\begin{pmatrix}\Delta(a)\ &\ 0\\\ 0\ &\
> \Delta^{\prime}(a)\end{pmatrix}=M(a)F$
>
> where $\Delta(a),\Delta^{\prime}(a)$ are the transition matrices of $C$ and
> the finite MC ${\cal D}(\alpha(\overline{x}))$ induced by ${\cal D}$ under
> the strategy $\alpha(\overline{x})$.
>
>

This condition $\mathit{Cond}$ is a closed formula in the existential theory
of the reals. ∎

###  0.C.3 Proof of Theorem 4.4

Theorem 4.4. The NMF problem is polynomial-time reducible to ${\sf
MC\sqsubseteq MDP_{m}}$, hence ${\sf MC\sqsubseteq MDP_{m}}$ is NP-hard.

###### Proof

Given a nonnegative matrix $M\in\mathbb{R}^{n\times m}$ and rank $r$, we
construct the MC ${\cal C}$ and the MDP ${\cal D}$ as described in subsection
4.2. We prove that there is a nonnegative factorization for $M=A\cdot W$ such
that $A\in\mathbb{R}^{n\times r}$ and $W\in\mathbb{R}^{r\times m}$ if and only
if ${\cal C}\sqsubseteq{\cal D}$ where ${\cal D}$ is restricted to use only
memoryless strategies.

We establish the correctness of the reduction as follows. First, assume that
there is a nonnegative factorization for $M$. Thus, there are stochastic
matrices $A\in\mathbb{R}^{n\times r}$ and $W\in\mathbb{R}^{r\times m}$ such
that $M=A\cdot W$. To prove that ${\cal C}\sqsubseteq{\cal D}$, we construct a
memoryless strategy $\alpha$ such that $\mathit{Tr}_{{\cal
C}}=\mathit{Tr}_{{\cal D},\alpha}$. For all states $q$ of ${\cal D}$, strategy
$\alpha$ is defined by

$\alpha(q)=\left\\{\begin{array}[]{ll}d\in{\sf Dist}({\sf
moves}(p_{i}))&\mbox{if }q=p_{i}\text{ and }1\leq i\leq n,\\\ \text{where
}d({\sf m}_{i,k})=A[i,k]\text{ for all }1\leq k\leq r\\\ &\\\ d\in{\sf
Dist}({\sf moves}(\ell_{k}))&\mbox{if }q=p_{i}\text{ and }1\leq k\leq r,\\\
\text{where }d({\sf m}^{\prime}_{k,j})=W[k,j]\text{ for all }1\leq j\leq m\\\
&\\\ \text{ the Dirac distribution on~{}$(c,p_{{\mathit{fi}}})$ }&\mbox{if
}q=p_{{\mathit{fi}}}.\\\ \end{array}\right.$

The trace-probability function for ${\cal D}$ and $\alpha$ is such that for
all $1\leq i\leq n$ and all $1\leq j\leq m$, we have $\mathit{Tr}_{{\cal
D},\alpha}(a_{i})=\frac{1}{n}$, and

$\displaystyle\mathit{Tr}_{{\cal D},\alpha}(a_{i}\cdot b_{j}\cdot c^{*})$
$\displaystyle=\frac{1}{n}\sum\limits_{k=1}^{r}\alpha(p_{i})({\sf
m}_{i,k})\cdot\alpha(\ell_{k})({\sf m}^{\prime}_{k,j})$
$\displaystyle=\frac{1}{n}\sum\limits_{k=1}^{r}A[i,k]\cdot
W[k,j]=\frac{1}{n}M[i,j].$

This gives $\mathit{Tr}_{{\cal D},\alpha}=\mathit{Tr}_{{\cal C}}$, and thus
${\cal C}\sqsubseteq{\cal D}$ where ${\cal D}$ uses a memoryless strategy.

Second, assume that there exists a memoryless strategy $\beta$ for the MDP
${\cal D}$ such that $\mathit{Tr}_{{\cal C}}=\mathit{Tr}_{{\cal D},\beta}$. We
present a factorization $M=A\cdot W$ where $A\in\mathbb{R}^{n\times r}$ and
$W\in\mathbb{R}^{r\times m}$. For all $1\leq i\leq n$, $1\leq k\leq r$ and
$1\leq j\leq m$, let

$A[i,k]=\beta(p_{i})({\sf m}_{i,k})\quad\quad\text{ and }\quad\quad
W[k,j]=\beta(\ell_{k})({\sf m}^{\prime}_{k,j}).$

Since ${\cal D}$ under the strategy $\beta$ refines ${\cal C}$, then for all
$1\leq i\leq n$ and all $1\leq j\leq m$

$\mathit{Tr}_{{\cal D},\beta}(a_{i}\cdot b_{j}\cdot c^{*})=\mathit{Tr}_{{\cal
C}}(a_{i}\cdot b_{j}\cdot c^{*})=\frac{1}{n}M[i,j].$

Since the probability of generating $a_{i}\cdot b_{j}\cdot c^{*}$ is
$\frac{1}{n}\sum\limits_{k=1}^{r}\beta(p_{i})({\sf
m}_{i,k})\cdot\beta(\ell_{k})({\sf m}^{\prime}_{k,j})$ then we have
$\sum\limits_{k=1}^{r}A[i,k]\cdot W[k,j]=M[i,j]$. This completes the proof. ∎

##  Appendix 0.D Proofs of Section 5

###  0.D.1 Proof of Proposition 1

For a trace-based strategy $\alpha:{\sf L}^{*}\times Q\to{\sf Dist}({\sf
moves})$ and a trace $w\in{\sf L}^{*}$, define the local strategy
$\alpha[w]:Q\to{\sf Dist}({\sf moves})$ with $\alpha[w](q)=\alpha(w,q)$ for
all $q\in Q$. We have the following lemma.

###### Lemma 2

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let
$\alpha:{\sf L}^{*}\times Q\to{\sf Dist}({\sf moves})$ be a trace-based
strategy. Let $w\in{\sf L}^{*}$ and $a\in{\sf L}$. Then:

$\mathit{subDis}_{{\cal D},\alpha}(wa)=\mathit{subDis}_{{\cal
D},\alpha}(w)\cdot\Delta_{\alpha[w]}(a)$

###### Proof

Let $q^{\prime}\in Q$. We have:

$\displaystyle\mathit{subDis}_{{\cal D},\alpha}(wa)(q^{\prime})$
$\displaystyle=\sum_{\rho\in{\sf Paths}(w)}{\sf Pr}_{{\cal D},\alpha}(\rho
aq^{\prime})$ definition of $\mathit{subDis}$ $\displaystyle=\sum_{q\in
Q}\mathop{\sum_{\rho\in{\sf Paths}(w)}}_{{\sf last}(\rho)=q}{\sf Pr}_{{\cal
D},\alpha}(\rho)\cdot\sum_{{\sf m}\in{\sf moves}(q)}\alpha(\rho)({\sf
m})\cdot{\sf m}(a,q^{\prime})$ definition of ${\sf Pr}$
$\displaystyle=\sum_{q\in Q}\mathop{\sum_{\rho\in{\sf Paths}(w)}}_{{\sf
last}(\rho)=q}{\sf Pr}_{{\cal D},\alpha}(\rho)\cdot\sum_{{\sf m}\in{\sf
moves}(q)}\alpha(w,q)({\sf m})\cdot{\sf m}(a,q^{\prime})$ $\alpha$ is trace-
based $\displaystyle=\sum_{q\in Q}\mathit{subDis}_{{\cal
D},\alpha}(w)(q)\cdot\sum_{{\sf m}\in{\sf moves}(q)}\alpha(w,q)({\sf
m})\cdot{\sf m}(a,q^{\prime})$ definition of $\mathit{subDis}$
$\displaystyle=\sum_{q\in Q}\mathit{subDis}_{{\cal
D},\alpha}(w)(q)\cdot\sum_{{\sf m}\in{\sf moves}(q)}\alpha[w](q)({\sf
m})\cdot{\sf m}(a,q^{\prime})$ definition of $\alpha[w]$
$\displaystyle=\sum_{q\in Q}\mathit{subDis}_{{\cal
D},\alpha}(w)(q)\cdot\Delta_{\alpha[w]}(a)[q,q^{\prime}]$ definition of
$\Delta_{\alpha[w]}(a)$ $\displaystyle=\left(\mathit{subDis}_{{\cal
D},\alpha}(w)\cdot\Delta_{\alpha[w]}(a)\right)(q^{\prime})$

∎

The following lemma allows us to view strategies as a composition of local
strategies, and conversely.

###### Lemma 3

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let
$w=a_{1}a_{2}\cdots a_{n}\in{\sf L}^{*}$. Let $\mu_{1},\mu_{2},\ldots,\mu_{n}$
be subdistributions over $Q$. Then there is a strategy $\alpha:{\sf
Paths}({\cal D})\to{\sf Dist}({\sf moves})$ with

$\mu_{i}=\mathit{subDis}_{{\cal D},\alpha}(a_{1}a_{2}\cdots
a_{i})\qquad\text{for all $i\in\\{0,1,\ldots,n\\}$}$

if and only if there are local strategies
$\alpha_{0},\alpha_{1},\ldots,\alpha_{n-1}:Q\to{\sf Dist}({\sf moves})$ with

$\mu_{i+1}={\sf Succ}(\mu_{i},\alpha_{i},a_{i+1})\qquad\text{for all
$i\in\\{0,1,\ldots,n-1\\}$}.$

###### Proof

We prove the two implications from the lemma in turn.

  * “$\Longrightarrow$”:

Let $\alpha$ be a strategy with $\mu_{i}=\mathit{subDis}_{{\cal
D},\alpha}(a_{1}a_{2}\cdots a_{i})$ for all $i\in\\{0,1,\ldots,n\\}$. By Lemma
1 we can assume that $\alpha$ is trace-based. For all
$i\in\\{0,1,\ldots,n-1\\}$ define a local strategy $\alpha_{i}$ with
$\alpha_{i}=\alpha[a_{1}a_{2}\cdots a_{i}]$. Then we have for all
$i\in\\{0,1,\ldots,n-1\\}$:

$\displaystyle\mu_{i+1}$ $\displaystyle=\mathit{subDis}_{{\cal
D},\alpha}(a_{1}a_{2}\cdots a_{i+1})$ definition of $\alpha$
$\displaystyle=\mathit{subDis}_{{\cal D},\alpha}(a_{1}a_{2}\cdots
a_{i})\cdot\Delta_{\alpha[a_{1}a_{2}\cdots a_{i}]}(a_{i+1})$ Lemma 2
$\displaystyle=\mu_{i}\cdot\Delta_{\alpha_{i}}(a_{i+1})$ definitions of
$\alpha,\alpha_{i}$ $\displaystyle={\sf Succ}(\mu_{i},\alpha_{i},a_{i+1})$ by
(3)

  * “$\Longleftarrow$”:

Let $\alpha_{0},\alpha_{1},\ldots,\alpha_{n-1}$ be local strategies with
$\mu_{i+1}={\sf Succ}(\mu_{i},\alpha_{i},a_{i+1})$ for all
$i\in\\{0,1,\ldots,n-1\\}$. Define a trace-based strategy $\alpha$ such that
$\alpha[a_{1}a_{2}\cdots a_{i}]=\alpha_{i}$ for all
$i\in\\{0,1,\ldots,n-1\\}$. (This condition need not completely determine
$\alpha$.) We prove by induction on $i$ that $\mu_{i}=\mathit{subDis}_{{\cal
D},\alpha}(a_{1}a_{2}\cdots a_{i})$ for all $i\in\\{0,1,\ldots,n\\}$. For
$i=0$ this is trivial. For the step, we have:

$\displaystyle\mu_{i+1}$ $\displaystyle={\sf
Succ}(\mu_{i},\alpha_{i},a_{i+1})$ definition of $\alpha_{i}$
$\displaystyle=\mu_{i}\cdot\Delta_{\alpha_{i}}(a_{i+1})$ by (3)
$\displaystyle=\mathit{subDis}_{{\cal D},\alpha}(a_{1}a_{2}\cdots
a_{i})\cdot\Delta_{\alpha_{i}}(a_{i+1})$ induction hypothesis
$\displaystyle=\mathit{subDis}_{{\cal D},\alpha}(a_{1}a_{2}\cdots
a_{i})\cdot\Delta_{\alpha[a_{1}a_{2}\cdots a_{i}]}(a_{i+1})$ definition of
$\alpha$ $\displaystyle=\mathit{subDis}_{{\cal D},\alpha}(a_{1}a_{2}\cdots
a_{i+1})$ Lemma 2

∎

Now we can prove Proposition 1 from the main text:

Proposition 1. Let ${\cal D}$ be an MDP and ${\cal C}$ be an MC. Then ${\cal
D}\sim{\cal C}$ if and only if ${\cal D}\sqsubseteq{\cal C}$.

###### Proof

Let ${\cal D}=\langle Q_{\cal D},\mu^{{\cal D}}_{0},{\sf L},\delta^{{\cal
D}}\rangle$ and ${\cal C}=\langle Q_{\cal C},\mu^{{\cal C}}_{0},{\sf
L},\delta^{{\cal C}}\rangle$.

  * “$\Longrightarrow$”:

Let ${\cal D}\sim{\cal C}$. Hence $\mu^{{\cal D}}_{0}\sim\mu^{{\cal C}}_{0}$.
We show that ${\cal D}\sqsubseteq{\cal C}$. Let $\alpha^{{\cal D}}$ be a
strategy for ${\cal D}$. Let $w=a_{1}a_{2}\cdots a_{n}\in{\sf L}^{*}$. Let
$\mu^{{\cal D}}_{0},\mu^{{\cal D}}_{1},\ldots,\mu^{{\cal D}}_{n}$ be the
subdistributions with $\mu^{{\cal D}}_{i}=\mathit{subDis}_{{\cal
D},\alpha^{{\cal D}}}(a_{1}a_{2}\cdots a_{i})$ for all $i$. By Lemma 3 there
exist local strategies $\alpha^{{\cal D}}_{0},\alpha^{{\cal
D}}_{1},\ldots,\alpha^{{\cal D}}_{n-1}$ with $\mu^{{\cal D}}_{i+1}={\sf
Succ}(\mu^{{\cal D}}_{i},\alpha^{{\cal D}}_{i},a_{i+1})$ for all $i$. Since
$\mu^{{\cal D}}_{0}\sim\mu^{{\cal C}}_{0}$, there exist local strategies
$\alpha^{{\cal C}}_{0},\alpha^{{\cal C}}_{1},\ldots,\alpha^{{\cal C}}_{n-1}$
for ${\cal C}$ and subdistributions $\mu^{{\cal C}}_{1},\mu^{{\cal
C}}_{2},\ldots,\mu^{{\cal C}}_{n}$ with $\mu^{{\cal C}}_{i+1}={\sf
Succ}(\mu^{{\cal C}}_{i},\alpha^{{\cal C}}_{i},a_{i+1})$ for all $i$ and
$\mu^{{\cal D}}_{i}\sim\mu^{{\cal C}}_{i}$ for all $i$. Since ${\cal C}$ is an
MC, the local strategies $\alpha^{{\cal C}}_{i}$ are, in fact, irrelevant. By
Lemma 3 we have $\mu^{{\cal C}}_{i}=\mathit{subDis}_{{\cal
C}}(a_{1}a_{2}\cdots a_{i})$ for all $i$. So we have:

$\displaystyle\mathit{Tr}_{{\cal D},\alpha^{{\cal D}}}(w)$
$\displaystyle=\lVert\mathit{subDis}_{{\cal D},\alpha^{{\cal D}}}(w)\rVert$ by
(1) $\displaystyle=\lVert\mu^{{\cal D}}_{n}\rVert$ $\displaystyle\mu^{{\cal
D}}_{n}=\mathit{subDis}_{{\cal D},\alpha^{{\cal D}}}(w)$
$\displaystyle=\lVert\mu^{{\cal C}}_{n}\rVert$ $\displaystyle\mu^{{\cal
D}}_{n}\sim\mu^{{\cal C}}_{n}$ $\displaystyle=\lVert\mathit{subDis}_{{\cal
C}}(w)\rVert$ $\displaystyle\mu^{{\cal C}}_{n}=\mathit{subDis}_{{\cal C}}(w)$
$\displaystyle=\mathit{Tr}_{{\cal C}}(w)$ by (1)

Since $\alpha^{{\cal D}}$ and $w$ were chosen arbitrarily, we conclude that
${\cal D}\sqsubseteq{\cal C}$.

  * “$\Longleftarrow$”:

Let ${\cal D}\sqsubseteq{\cal C}$. We show $\mu^{{\cal D}}_{0}\sim\mu^{{\cal
C}}_{0}$. Define a relation ${\cal R}\subseteq{\sf subDist}(Q_{\cal
D})\times{\sf subDist}(Q_{\cal C})$ such that $\mu^{{\cal D}}\mathrel{{\cal
R}}\mu^{{\cal C}}$ if and only if there exist a strategy $\alpha^{{\cal D}}$
for ${\cal D}$ and a trace $w$ with $\mu^{{\cal D}}=\mathit{subDis}_{{\cal
D},\alpha^{{\cal D}}}(w)$ and $\mu^{{\cal C}}=\mathit{subDis}_{{\cal C}}(w)$.
We claim that ${\cal R}$ is a bisimulation. To prove the claim, consider any
$\mu^{{\cal D}},\mu^{{\cal C}}$ with $\mu^{{\cal D}}\mathrel{{\cal
R}}\mu^{{\cal C}}$. Then there exist a strategy $\alpha^{{\cal D}}$ for ${\cal
D}$ and a trace $w$ with $\mu^{{\cal D}}=\mathit{subDis}_{{\cal
D},\alpha^{{\cal D}}}(w)$ and $\mu^{C}=\mathit{subDis}_{{\cal C}}(w)$. Since
${\cal D}\sqsubseteq{\cal C}$, we have $\mathit{Tr}_{{\cal D},\alpha^{{\cal
D}}}(w)=\mathit{Tr}_{{\cal C}}(w)$. So we have:

$\displaystyle\lVert\mu^{{\cal D}}\rVert$
$\displaystyle=\lVert\mathit{subDis}_{{\cal D},\alpha^{{\cal D}}}(w)\rVert$
$\displaystyle\mu^{{\cal D}}=\mathit{subDis}_{{\cal D},\alpha^{{\cal D}}}(w)$
$\displaystyle=\mathit{Tr}_{{\cal D},\alpha^{{\cal D}}}(w)$ by (1)
$\displaystyle=\mathit{Tr}_{{\cal C}}(w)$ as argued above
$\displaystyle=\lVert\mathit{subDis}_{{\cal C}}(w)\rVert$ by (1)
$\displaystyle=\lVert\mu^{{\cal C}}\rVert$ $\displaystyle\mu^{{\cal
C}}=\mathit{subDis}_{{\cal C}}(w)$

This proves the first condition for ${\cal R}$ being a bisimulation.

For the rest of the proof assume $w=a_{1}a_{2}\cdots a_{n}$. Write $\mu^{{\cal
D}}_{n}=\mu^{{\cal D}}$ and $\mu^{{\cal C}}_{n}=\mu^{{\cal C}}$. Let
$\alpha^{{\cal D}}_{n}$ be a local strategy for ${\cal D}$. Let
$a_{n+1}\in{\sf L}$. Define $\mu^{{\cal D}}_{n+1}={\sf Succ}(\mu^{{\cal
D}}_{n},\alpha^{{\cal D}}_{n},a_{n+1})$, and $\mu^{{\cal C}}_{n+1}={\sf
Succ}(\mu^{{\cal C}}_{n},\alpha^{{\cal C}}_{n},a_{n+1})$ for an arbitrary (and
unimportant) local strategy $\alpha^{{\cal C}}_{n}$ for ${\cal C}$. For the
second and the third condition of ${\cal R}$ being a bisimulation we need to
prove $\mu^{{\cal D}}_{n+1}\mathrel{{\cal R}}\mu^{{\cal C}}_{n+1}$. Define
$\mu^{{\cal D}}_{1},\mu^{{\cal D}}_{2},\ldots,\mu^{{\cal D}}_{n-1}$ such that
$\mu^{{\cal D}}_{i}=\mathit{subDis}_{{\cal D},\alpha^{{\cal
D}}}(a_{1}a_{2}\cdots a_{i})$ for all $i\in\\{0,1,\ldots,n\\}$. By Lemma 3
there are local strategies $\alpha^{{\cal D}}_{0},\alpha^{{\cal
D}}_{1},\ldots,\alpha^{{\cal D}}_{n-1}$ such that $\mu^{{\cal D}}_{i+1}={\sf
Succ}(\mu^{{\cal D}}_{i},\alpha^{{\cal D}}_{i},a_{i+1})$ for all
$i\in\\{0,1,\ldots,n-1\\}$. We also have $\mu^{{\cal D}}_{n+1}={\sf
Succ}(\mu^{{\cal D}}_{n},\alpha^{{\cal D}}_{n},a_{n+1})$, so again by Lemma 3
there is a strategy $\beta^{{\cal D}}$ with $\mu^{{\cal
D}}_{i}=\mathit{subDis}_{{\cal D},\beta^{{\cal D}}}(a_{1}a_{2}\cdots a_{i})$
for all $i\in\\{0,1,\ldots,n+1\\}$. In particular, $\mu^{{\cal
D}}_{n+1}=\mathit{subDis}_{{\cal D},\beta^{{\cal D}}}(wa_{n+1})$. Similarly,
we have $\mu^{{\cal C}}_{n+1}=\mathit{subDis}_{{\cal C}}(wa_{n+1})$. Thus,
$\mu^{{\cal D}}_{n+1}\mathrel{{\cal R}}\mu^{{\cal C}}_{n+1}$. Hence we have
proved that ${\cal R}$ is a bisimulation.

Considering the empty trace, we see that $\mu^{{\cal D}}_{0}\mathrel{{\cal
R}}\mu^{{\cal C}}_{0}$. Since ${\cal R}\subseteq\mathord{\sim}$, we also have
$\mu^{{\cal D}}_{0}\sim\mu^{{\cal C}}_{0}$, as desired.

∎

###  0.D.2 On the Notion of _Extremal with Respect to a Vector Space_

We prove here:

Proposition 2. Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an
MDP. Let $B_{1}\in\mathbb{R}^{Q\times k_{1}}$ and $B_{2}\in\mathbb{R}^{Q\times
k_{2}}$ for $k_{1},k_{2}\geq 1$. Denote by
$\mathcal{V}_{1},\mathcal{V}_{2}\subseteq\mathbb{R}^{Q}$ the subspaces spanned
by the columns of $B_{1},B_{2}$, respectively. Assume
$\mathcal{V}_{1}\subseteq\mathcal{V}_{2}$. If a local strategy
$\widehat{\alpha}$ is extremal with respect to $B_{1}$ then $\widehat{\alpha}$
is extremal with respect to $B_{2}$.

###### Proof

Let $\vec{v}_{1}\in\mathbb{R}^{|{\sf L}|\cdot k_{1}}$ be a direction in which
$\widehat{\alpha}$ is extremal with respect to $B_{1}$. Since
$\mathcal{V}_{1}\subseteq\mathcal{V}_{2}$, there exists a matrix
$T\in\mathbb{R}^{k_{2}\times k_{1}}$ with $B_{1}=B_{2}T$. Define columns
$\vec{v}_{1,1},\vec{v}_{1,2},\ldots,\vec{v}_{1,|{\sf
L}|}\in\mathbb{R}^{k_{1}}$ such that:

$\vec{v}_{1}=\begin{pmatrix}\vec{v}_{1,1}\\\ \vec{v}_{1,2}\\\ \vdots\\\
\vec{v}_{1,|{\sf L}|}\end{pmatrix}$

Define $\vec{v}_{2}\in\mathbb{R}^{|{\sf L}|\cdot k_{2}}$ by:

$\vec{v}_{2}=\begin{pmatrix}T\vec{v}_{1,1}\\\ T\vec{v}_{1,2}\\\ \vdots\\\
T\vec{v}_{1,|{\sf L}|}\end{pmatrix}$

For $\mu\in{\sf subDist}(Q)$ and $\alpha:Q\to{\sf Dist}({\sf moves})$, let us
write $p_{1}(\mu,\alpha)\in\mathbb{R}^{|{\sf L}|\cdot k_{1}}$ (resp.,
$p_{2}(\mu,\alpha)\in\mathbb{R}^{|{\sf L}|\cdot k_{2}}$) for the point
$p(\mu,\alpha)$ defined in terms of $B_{1}$ (resp., $B_{2}$). We have:

$\displaystyle p_{1}(\mu,\alpha)\vec{v}_{1}$ $\displaystyle=\sum_{i=1}^{|{\sf
L}|}\mu\Delta_{\alpha}(a_{i})B_{1}\vec{v}_{1,i}$ definitions of $p_{1}$ and
$\vec{v}_{1,i}$ $\displaystyle=\sum_{i=1}^{|{\sf
L}|}\mu\Delta_{\alpha}(a_{i})B_{2}T\vec{v}_{1,i}$ $\displaystyle B_{1}=B_{2}T$
$\displaystyle=p_{2}(\mu,\alpha)\vec{v}_{2}$ definitions of $p_{2}$ and
$\vec{v}_{2}$

It follows that $\widehat{\alpha}$ is extremal in direction $\vec{v}_{2}$ with
respect to $B_{2}$. ∎

###  0.D.3 Further Geometrical Facts about Extremal Strategies

In this section we prove facts about extremal local strategies that will be
needed later.

###### Lemma 4

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let
$B\in\mathbb{R}^{Q\times k}$ with $k\geq 1$. Let $\mu\in{\sf subDist}(Q)$. Let
$\alpha,\widehat{\alpha}$ be local strategies. Suppose
$\vec{v}\in\mathbb{R}^{{|{\sf L}|}\cdot k}$ is a direction in which
$\widehat{\alpha}$ is extremal and
$p(\mu,\alpha)\vec{v}=p(\mu,\widehat{\alpha})\vec{v}$. Then
$p(\mu,\alpha)=p(\mu,\widehat{\alpha})$.

###### Proof

We have:

$\displaystyle\sum_{q\in Q}\mu(q)\cdot p(d_{q},\alpha)\vec{v}$
$\displaystyle=p(\mu,\alpha)\vec{v}$ definition of $p$
$\displaystyle=p(\mu,\widehat{\alpha})\vec{v}$ assumption on
$\widehat{\alpha}$ $\displaystyle=\sum_{q\in Q}\mu(q)\cdot
p(d_{q},\widehat{\alpha})\vec{v}$ definition of $p$

With (4) it follows that for all $q\in{\sf Supp}(\mu)$ we have
$p(d_{q},\alpha)\vec{v}=p(d_{q},\widehat{\alpha})\vec{v}$. Hence by (5) we
obtain $p(d_{q},\alpha)=p(d_{q},\widehat{\alpha})$ for all $q\in{\sf
Supp}(\mu)$. Thus:

$p(\mu,\alpha)=\sum_{q\in Q}\mu(q)\cdot p(d_{q},\alpha)=\sum_{q\in
Q}\mu(q)\cdot p(d_{q},\widehat{\alpha})=p(\mu,\widehat{\alpha})$

∎

For a subdistribution $\mu$ define the bounded, convex polytope
$P_{\mu}\subseteq\mathbb{R}^{{|{\sf L}|}\cdot k}$ with

$P_{\mu}=\\{p(\mu,\alpha)\mid\alpha:Q\to{\sf Dist}({\sf moves})\\}.$

Comparing two polytopes $P_{\mu_{\cal D}}$ and $P_{\mu_{\cal E}}$ for
subdistributions $\mu_{\cal D},\mu_{\cal E}$ will play a key role for deciding
bisimulation. First we prove the following lemma, which states that any vertex
of the polytope $P_{\mu}$ can be obtained by applying an extremal local
strategy. Although this is intuitive, the proof is not very easy.

###### Lemma 5

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let
$B\in\mathbb{R}^{Q\times k}$ with $k\geq 1$. Let $\mu\in{\sf subDist}(Q)$. If
$x\in P_{\mu}$ is a vertex of $P_{\mu}$ then there is an extremal local
strategy $\widehat{\alpha}$ with $x=p(\mu,\widehat{\alpha})$.

###### Proof

Let $x\in P_{\mu}$ be a vertex of $P_{\mu}$. Let $\alpha_{1}:Q\to{\sf
Dist}({\sf moves})$ be a local strategy so that $x=p(\mu,\alpha_{1})$. Since
$x$ is a vertex, we can assume that $\alpha_{1}$ is pure. Since $x$ is a
vertex of $P_{\mu}$, there is a hyperplane $H\subseteq\mathbb{R}^{{|{\sf
L}|}\cdot k}$ such that $\\{x\\}=P_{\mu}\cap H$. Let
$\vec{v}_{1}\in\mathbb{R}^{{|{\sf L}|}\cdot k}$ be a normal vector of $H$.
Since $\\{x\\}=P_{\mu}\cap H$, we have $x\vec{v}_{1}=\max_{y\in
P_{\mu}}y\vec{v}_{1}$ or $x\vec{v}_{1}=\min_{y\in P_{\mu}}y\vec{v}_{1}$;
without loss of generality, say $x\vec{v}_{1}=\max_{y\in
P_{\mu}}y\vec{v}_{1}$. Since $\\{x\\}=P_{\mu}\cap H$, we have for all
$q\in{\sf Supp}(\mu)$ and all $\alpha$:

$p(d_{q},\alpha)\vec{v}_{1}=p(d_{q},\alpha_{1})\vec{v}_{1}\quad\text{implies}\quad
p(d_{q},\alpha)=p(d_{q},\alpha_{1}).$ (6)

For all $q\in Q\setminus{\sf Supp}(\mu)$, redefine the pure local strategy
$\alpha_{1}(q)$ so that all $q\in Q$ and all local strategies $\alpha$ satisfy
$p(d_{q},\alpha)\vec{v}_{1}\leq p(d_{q},\alpha_{1})\vec{v}_{1}$. Since $Q$ and
${\sf moves}$ are finite, there is $\varepsilon>0$ such that all $q\in Q$ and
all _pure_ local strategies $\alpha$ either satisfy
$p(d_{q},\alpha)\vec{v}_{1}=p(d_{q},\alpha_{1})\vec{v}_{1}$ or
$p(d_{q},\alpha)\vec{v}_{1}\leq p(d_{q},\alpha_{1})\vec{v}_{1}-\varepsilon$.

Define

$\Sigma=\left\\{\alpha:Q\to{\sf Dist}({\sf moves})\mid\forall\,q\in
Q:p(d_{q},\alpha)\vec{v}_{1}=p(d_{q},\alpha_{1})\vec{v}_{1}\right\\}.$

Consider the bounded, convex polytope $P_{2}\subseteq\mathbb{R}^{{|{\sf
L}|}\cdot k}$ defined by

$P_{2}=\left\\{\sum_{q\in
Q}p(d_{q},\alpha)\;\middle|\;\alpha\in\Sigma\right\\}.$

By an argument similar to the one above, there are a pure local strategy
$\widehat{\alpha}\in\Sigma$, a vertex $x_{2}=\sum_{q\in
Q}p(d_{q},\widehat{\alpha})$ of $P_{2}$, and a vector
$\vec{v}_{2}\in\mathbb{R}^{{|{\sf L}|}\cdot k}$ such that for all $q\in Q$ and
all $\alpha\in\Sigma$, we have $p(d_{q},\alpha)\vec{v}_{2}\leq
p(d_{q},\widehat{\alpha})\vec{v}_{2}$, and if
$p(d_{q},\alpha)\vec{v}_{2}=p(d_{q},\widehat{\alpha})\vec{v}_{2}$ then
$p(d_{q},\alpha)=p(d_{q},\widehat{\alpha})$. By scaling down $\vec{v}_{2}$ by
a small positive scalar, we can assume that all $q\in Q$ and all local
strategies $\alpha$ satisfy

$\left\lvert p(d_{q},\alpha)\vec{v}_{2}\right\rvert\leq\frac{\varepsilon}{3}.$
(7)

Since $\widehat{\alpha}\in\Sigma$, all $q\in Q$ satisfy
$p(d_{q},\widehat{\alpha})\vec{v}_{1}=p(d_{q},\alpha_{1})\vec{v}_{1}$. By (6)
all $q\in{\sf Supp}(\mu_{\cal D})$ satisfy
$p(d_{q},\widehat{\alpha})=p(d_{q},\alpha_{1})$. Hence:

$p(\mu_{\cal D},\widehat{\alpha})=\sum_{q\in{\sf Supp}(\mu_{\cal D})}\mu_{\cal
D}(q)p(d_{q},\widehat{\alpha})=\sum_{q\in{\sf Supp}(\mu_{\cal D})}\mu_{\cal
D}(q)p(d_{q},\alpha_{1})=p(\mu_{\cal D},\alpha_{1})=x$

It remains to show that there is a direction $\vec{v}$ in which
$\widehat{\alpha}$ is extremal. Take $\vec{v}=\vec{v}_{1}+\vec{v}_{2}$. Let
$q\in Q$ and let $\alpha$ be a pure local strategy. We consider two cases:

  * •

Assume $p(d_{q},\alpha)\vec{v}_{1}=p(d_{q},\alpha_{1})\vec{v}_{1}$. Then there
is $\beta\in\Sigma$ with $\alpha(q)=\beta(q)$, hence
$p(d_{q},\alpha)=p(d_{q},\beta)$. We have:

$\displaystyle p(d_{q},\alpha)\vec{v}$ $\displaystyle=p(d_{q},\beta)\vec{v}$
$\displaystyle p(d_{q},\alpha)=p(d_{q},\beta)$
$\displaystyle=p(d_{q},\beta)\vec{v}_{1}+p(d_{q},\beta)\vec{v}_{2}$ definition
of $\vec{v}$
$\displaystyle=p(d_{q},\alpha_{1})\vec{v}_{1}+p(d_{q},\beta)\vec{v}_{2}$
$\displaystyle\beta\in\Sigma$
$\displaystyle=p(d_{q},\widehat{\alpha})\vec{v}_{1}+p(d_{q},\beta)\vec{v}_{2}$
$\displaystyle\widehat{\alpha}\in\Sigma$ $\displaystyle\leq
p(d_{q},\widehat{\alpha})\vec{v}_{1}+p(d_{q},\widehat{\alpha})\vec{v}_{2}$
definition of $\widehat{\alpha}$
$\displaystyle=p(d_{q},\widehat{\alpha})\vec{v}$ definition of $\vec{v}$

Hence (4) holds for $\widehat{\alpha}$. To show (5), assume
$p(d_{q},\alpha)\vec{v}=p(d_{q},\widehat{\alpha})\vec{v}$. Then all terms in
the computation above are equal, and
$p(d_{q},\beta)\vec{v}_{2}=p(d_{q},\widehat{\alpha})\vec{v}_{2}$. By the
definition of $\widehat{\alpha}$, this implies
$p(d_{q},\beta)=p(d_{q},\widehat{\alpha})$. Hence
$p(d_{q},\alpha)=p(d_{q},\beta)=p(d_{q},\widehat{\alpha})$. Hence (5) holds
for $\widehat{\alpha}$.

  * •

Assume $p(d_{q},\alpha)\vec{v}_{1}\neq p(d_{q},\alpha_{1})\vec{v}_{1}$. By the
definition of $\varepsilon$ it follows $p(d_{q},\alpha)\vec{v}_{1}\leq
p(d_{q},\alpha_{1})\vec{v}_{1}-\varepsilon$. We have:

$\displaystyle p(d_{q},\alpha)\vec{v}$
$\displaystyle=p(d_{q},\alpha)\vec{v}_{1}+p(d_{q},\alpha)\vec{v}_{2}$
definition of $\vec{v}$ $\displaystyle\leq
p(d_{q},\alpha_{1})\vec{v}_{1}-\varepsilon+p(d_{q},\alpha)\vec{v}_{2}$ as
argued above
$\displaystyle=p(d_{q},\widehat{\alpha})\vec{v}_{1}-\varepsilon+p(d_{q},\alpha)\vec{v}_{2}$
$\displaystyle\widehat{\alpha}\in\Sigma$ $\displaystyle\leq
p(d_{q},\widehat{\alpha})\vec{v}_{1}-\varepsilon+\frac{\varepsilon}{3}$ by (7)
$\displaystyle\leq
p(d_{q},\widehat{\alpha})\vec{v}_{1}+p(d_{q},\widehat{\alpha})\vec{v}_{2}-\varepsilon+\frac{\varepsilon}{3}+\frac{\varepsilon}{3}$
by (7)
$\displaystyle<p(d_{q},\widehat{\alpha})\vec{v}_{1}+p(d_{q},\widehat{\alpha})\vec{v}_{2}$
$\displaystyle\varepsilon>0$ $\displaystyle=p(d_{q},\widehat{\alpha})\vec{v}$
definition of $\vec{v}$

This implies (4) and (5) for $\widehat{\alpha}$.

Hence, $\widehat{\alpha}$ is extremal in direction $\vec{v}$. ∎

The following lemma states the intuitive fact that in order to compare the
polytopes $P_{\mu_{\cal D}}$ and $P_{\mu_{\cal E}}$, it suffices to compare
the vertices obtained by applying extremal local strategies:

###### Lemma 6

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let
$B\in\mathbb{R}^{Q\times k}$ with $k\geq 1$. Then for all $\mu_{\cal
D},\mu_{\cal E}\in{\sf subDist}(Q)$ we have $P_{\mu_{\cal D}}=P_{\mu_{\cal
E}}$ if and only if for all extremal local strategies $\widehat{\alpha}$ we
have $p(\mu_{\cal D},\widehat{\alpha})=p(\mu_{\cal E},\widehat{\alpha})$.

###### Proof

We prove the two implications from the lemma in turn.

  * “$\Longrightarrow$”:

Suppose $P_{\mu_{\cal D}}=P_{\mu_{\cal E}}$. Let $\widehat{\alpha}$ be a local
strategy that is extremal in direction $\vec{v}$. Since $P_{\mu_{\cal
D}}=P_{\mu_{\cal E}}$, there are $\alpha_{{\cal E}}$ and $\alpha_{{\cal D}}$
such that $p(\mu_{\cal D},\widehat{\alpha})=p(\mu_{\cal E},\alpha_{\cal E})$
and $p(\mu_{\cal E},\widehat{\alpha})=p(\mu_{\cal D},\alpha_{\cal D})$. We
have:

$\displaystyle p(\mu_{\cal D},\widehat{\alpha})\vec{v}$
$\displaystyle=p(\mu_{\cal E},\alpha_{\cal E})\vec{v}$ $\displaystyle
p(\mu_{\cal D},\widehat{\alpha})=p(\mu_{\cal E},\alpha_{\cal E})$
$\displaystyle\leq p(\mu_{\cal E},\widehat{\alpha})\vec{v}$ $\widehat{\alpha}$
is extremal in direction $\vec{v}$ $\displaystyle=p(\mu_{\cal D},\alpha_{\cal
D})\vec{v}$ $p(\mu_{\cal E},\widehat{\alpha})=p(\mu_{\cal D},\alpha_{\cal D})$
$\displaystyle\leq p(\mu_{\cal D},\widehat{\alpha})\vec{v}$ $\widehat{\alpha}$
is extremal in direction $\vec{v}$

So all inequalities are in fact equalities. In particular, we have
$p(\mu_{\cal D},\widehat{\alpha})\vec{v}=p(\mu_{\cal D},\alpha_{\cal
D})\vec{v}$. It follows:

$\displaystyle p(\mu_{\cal D},\widehat{\alpha})$ $\displaystyle=p(\mu_{\cal
D},\alpha_{\cal D})$ Lemma 4 $\displaystyle=p(\mu_{\cal E},\widehat{\alpha})$
definition of $\alpha_{\cal D}$

  * “$\Longleftarrow$”:

Let $x$ be a vertex of $P_{\mu_{\cal D}}$. By Lemma 5 there exists an extremal
local strategy $\widehat{\alpha}$ with $x=p(\mu_{\cal D},\widehat{\alpha})$.
By the assumption we have $p(\mu_{\cal D},\widehat{\alpha})=p(\mu_{\cal
E},\widehat{\alpha})$. Hence $x=p(\mu_{\cal D},\widehat{\alpha})=p(\mu_{\cal
E},\widehat{\alpha})\in P_{\mu_{\cal E}}$. Since $x$ is an arbitrary vertex of
$P_{\mu_{\cal D}}$, and $P_{\mu_{\cal D}},P_{\mu_{\cal E}}$ are bounded,
convex polytopes, it follows $P_{\mu_{\cal D}}\subseteq P_{\mu_{\cal E}}$. The
reverse inclusion is shown similarly.

∎

###  0.D.4 Proof of Proposition 3

For $n\geq 0$, define a relation $\mathord{\sim}_{n}\subseteq{\sf
subDist}(Q)\times{\sf subDist}(Q)$ as follows. Let $\mu_{\cal D},\mu_{\cal
E}\in{\sf subDist}(Q)$. Define $\mathord{\sim}_{0}$ such that $\mu_{\cal
D}\sim_{0}\mu_{\cal E}$ if and only if $\lVert\mu_{\cal
D}\rVert=\lVert\mu_{\cal E}\rVert$. For $n\geq 0$, define
$\mathord{\sim}_{n+1}$ such that $\mu_{\cal D}\sim_{n+1}\mu_{\cal E}$ if and
only if

  * •

$\lVert\mu_{\cal D}\rVert=\lVert\mu_{\cal E}\rVert$;

  * •

for all local strategies $\alpha_{\cal D}$ there exists a local strategy
$\alpha_{\cal E}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$;

  * •

for all local strategies $\alpha_{\cal E}$ there exists a local strategy
$\alpha_{\cal D}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$.

###### Lemma 7

We have:

  1. 1.

$\mathord{\sim}_{n}\supseteq\mathord{\sim}_{n+1}\supseteq\mathord{\sim}$ for
all $n\geq 0$.

  2. 2.

If $\mathord{\sim}_{n}=\mathord{\sim}_{n+1}$ then
$\mathord{\sim}_{n}=\mathord{\sim}$.

###### Proof

Item 1. follows from a straightforward induction.

For item 2., let $\mathord{\sim}_{n}=\mathord{\sim}_{n+1}$. By item 1. we have
$\mathord{\sim}_{n}\supseteq\mathord{\sim}$, so it remains to prove
$\mathord{\sim}_{n}\subseteq\mathord{\sim}$. It suffices to prove that
$\mathord{\sim}_{n}$ is a bisimulation.

Suppose $\mu_{\cal D}\sim_{n}\mu_{\cal E}$. Since
$\mathord{\sim}_{n}=\mathord{\sim}_{n+1}$, we have $\mu_{\cal
D}\sim_{n+1}\mu_{\cal E}$. Thus:

  * •

$\lVert\mu_{\cal D}\rVert=\lVert\mu_{\cal E}\rVert$;

  * •

for all local strategies $\alpha_{\cal D}$ there exists a local strategy
$\alpha_{\cal E}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$;

  * •

for all local strategies $\alpha_{\cal E}$ there exists a local strategy
$\alpha_{\cal D}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$.

Hence we have shown that $\mathord{\sim}_{n}$ is a bisimulation. ∎

We will show later that we have $\mathord{\sim}_{n}=\mathord{\sim}$ for
$n=|Q|-1$.

The following lemma reduces the membership problem of $\mathord{\sim}_{n+1}$
to the membership problem of $\mathord{\sim}_{n}$ and a polytope-comparison
problem.

###### Lemma 8

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let $n\geq
0$ and $k\geq 1$. Suppose that a matrix $B\in\mathbb{R}^{Q\times k}$ is such
that for all $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$ we have $\mu_{\cal
D}\sim_{n}\mu_{\cal E}$ if and only if $\mu_{\cal D}B=\mu_{\cal E}B$. Then for
all $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$ we have $\mu_{\cal
D}\sim_{n+1}\mu_{\cal E}$ if and only if $\mu_{\cal D}B=\mu_{\cal E}B$ and
$P_{\mu_{\cal D}}=P_{\mu_{\cal E}}$.

###### Proof

Let $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$. For any local strategies
$\alpha_{\cal D},\alpha_{\cal E}$ we have:

$\displaystyle\forall\,a\in{\sf L}:{\sf Succ}(\mu_{\cal D},\alpha_{\cal
D},a)\sim_{n}{\sf Succ}(\mu_{\cal E},\alpha_{\cal E},a)$ (8)
$\displaystyle\Longleftrightarrow$ $\displaystyle\forall\,a\in{\sf
L}:\mu_{\cal D}\Delta_{\alpha_{\cal D}}(a)\sim_{n}\mu_{\cal
E}\Delta_{\alpha_{\cal E}}(a)$ by (3) $\displaystyle\Longleftrightarrow$
$\displaystyle\forall\,a\in{\sf L}:\mu_{\cal D}\Delta_{\alpha_{\cal
D}}(a)B=\mu_{\cal E}\Delta_{\alpha_{\cal E}}(a)B$ assumption on $B$
$\displaystyle\Longleftrightarrow$ $\displaystyle p(\mu_{\cal D},\alpha_{\cal
D})=p(\mu_{\cal E},\alpha_{\cal E})$ definition of $p$

We prove the two implications from the lemma in turn.

  * “$\Longrightarrow$”:

Let $\mu_{\cal D}\sim_{n+1}\mu_{\cal E}$. Since
$\mathord{\sim}_{n+1}\subseteq\mathord{\sim}_{n}$, we have $\mu_{\cal
D}\sim_{n}\mu_{\cal E}$. By the assumption on $B$ it follows $\mu_{\cal
D}B=\mu_{\cal E}B$.

To show $P_{\mu_{\cal D}}=P_{\mu_{\cal E}}$, choose an arbitrary local
strategy $\alpha_{\cal D}$. Since $\mu_{\cal D}\sim_{n+1}\mu_{\cal E}$, there
is $\alpha_{\cal E}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$. By (8) we have $p(\mu_{\cal D},\alpha_{\cal
D})=p(\mu_{\cal E},\alpha_{\cal E})$. Since $\alpha_{\cal D}$ was chosen
arbitrarily, we have shown $P_{\mu_{\cal D}}\subseteq P_{\mu_{\cal E}}$. The
reverse inclusion is shown similarly.

  * “$\Longleftarrow$”:

Suppose $\mu_{\cal D}B=\mu_{\cal E}B$ and $P_{\mu_{\cal D}}=P_{\mu_{\cal E}}$.
By the assumption on $B$ it follows $\mu_{\cal D}\sim_{n}\mu_{\cal E}$, hence
$\lVert\mu_{\cal D}\rVert=\lVert\mu_{\cal E}\rVert$. It remains to show:

    * –

for all local strategies $\alpha_{\cal D}$ there exists a local strategy
$\alpha_{\cal E}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$;

    * –

for all local strategies $\alpha_{\cal E}$ there exists a local strategy
$\alpha_{\cal D}$ such that for all $a\in{\sf L}$ we have ${\sf
Succ}(\mu_{\cal D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal
E},\alpha_{\cal E},a)$.

Let $\alpha_{\cal D}$ be a local strategy. Since $P_{\mu_{\cal
D}}=P_{\mu_{\cal E}}$, there is a local strategy $\alpha_{\cal E}$ such that
$p(\mu_{\cal D},\alpha_{\cal D})=p(\mu_{\cal E},\alpha_{\cal E})$. By (8) we
obtain that for all $a\in{\sf L}$ we have ${\sf Succ}(\mu_{\cal
D},\alpha_{\cal D},a)\sim_{n}{\sf Succ}(\mu_{\cal E},\alpha_{\cal E},a)$. We
have shown the first condition. The second condition is shown similarly.

∎

The characterization of $\mathord{\sim}_{n+1}$ provided by Lemma 8 depends
strongly on comparing two polytopes $P_{\mu_{\cal D}}$ and $P_{\mu_{\cal E}}$.
Using Lemma 6, we can instead formulate a characterization in terms of
matrices and extremal local strategies:

###### Lemma 9

Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an MDP. Let $n\geq
0$ and $k\geq 1$. Suppose that a matrix $B\in\mathbb{R}^{Q\times k}$ is such
that for all $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$ we have $\mu_{\cal
D}\sim_{n}\mu_{\cal E}$ if and only if $\mu_{\cal D}B=\mu_{\cal E}B$. Then for
all $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$ we have $\mu_{\cal
D}\sim_{n+1}\mu_{\cal E}$ if and only if $\mu_{\cal D}B=\mu_{\cal E}B$ and
$\mu_{\cal D}\Delta_{\widehat{\alpha}}(a)B=\mu_{\cal
E}\Delta_{\widehat{\alpha}}(a)B$ holds for all $a\in{\sf L}$ and for all
extremal local strategies $\widehat{\alpha}$.

###### Proof

By combining Lemmas 8 and 6, and the definitions of $p(\mu_{\cal
D},\widehat{\alpha})$ and $p(\mu_{\cal E},\widehat{\alpha})$. ∎

Now we can prove Proposition 3 from the main text:

Proposition 3. Let ${\cal D}=\langle Q,\mu_{0},{\sf L},\delta\rangle$ be an
MDP. Let $\mathcal{V}\subseteq\mathbb{R}^{Q}$ be the smallest column-vector
space such that

  * •

$\vec{1}=(1\ 1\cdots 1)^{T}\in\mathcal{V}$ (where $T$ denotes transpose) and

  * •

$\Delta_{\widehat{\alpha}}(a)\vec{u}\in\mathcal{V}$ for all
$\vec{u}\in\mathcal{V}$, all labels $a\in{\sf L}$ and local strategies
$\widehat{\alpha}$ that are extremal with respect to $\mathcal{V}$.

Then for all $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$, we have
$\mu_{\cal D}\sim\mu_{\cal E}$ if and only if $\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}$ for all $\vec{u}\in\mathcal{V}$.

###### Proof

Define $\mathcal{V}_{0}=\\{r\vec{1}\mid
r\in\mathbb{R}\\}\subseteq\mathbb{R}^{Q}$. For all $n\geq 0$ define
$\mathcal{V}_{n+1}$ to be the smallest vector space such that

  * •

$\mathcal{V}_{n}\subseteq\mathcal{V}_{n+1}$

  * •

$\Delta_{\widehat{\alpha}}(a)\vec{u}\in\mathcal{V}_{n+1}$, for all
$\vec{u}\in\mathcal{V}_{n}$ and all $a\in{\sf L}$ and all local strategies
$\widehat{\alpha}$ that are extremal with respect to $\mathcal{V}_{n}$.

We have $\mathcal{V}_{n}\subseteq\mathcal{V}$ for all $n\geq 0$. We claim for
all $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$:

$\mu_{\cal D}\sim_{n}\mu_{\cal E}\quad\Longleftrightarrow\quad\mu_{\cal
D}\vec{u}=\mu_{\cal E}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{n}$}$
(9)

We proceed by induction on $n$. For $n=0$, we have:

$\displaystyle\mu_{\cal D}\sim_{0}\mu_{\cal E}$
$\displaystyle\Longleftrightarrow\lVert\mu_{\cal D}\rVert=\lVert\mu_{\cal
E}\rVert$ definition of $\mathord{\sim}_{0}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{1}=\mu_{\cal E}\vec{1}$
definition of $\lVert\cdot\rVert$ $\displaystyle\Longleftrightarrow\mu_{\cal
D}\vec{u}=\mu_{\cal E}\vec{u}\quad\forall\,\vec{u}\in\mathcal{V}_{0}$
definition of $\mathcal{V}_{0}$

For the induction step, let $n\geq 0$. Define $B$ as a matrix whose columns
span $\mathcal{V}_{n}$. We have:

$\displaystyle\mu_{\cal D}\sim_{n}\mu_{\cal E}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}\quad\forall\,\vec{u}\in\mathcal{V}_{n}$ induction hypothesis (10)
$\displaystyle\Longleftrightarrow\mu_{\cal D}B=\mu_{\cal E}B$ definition of
$B$

In the following, let $\widehat{\alpha}$ range over all local strategies that
are extremal with respect to $B$:

$\displaystyle\mu_{\cal D}\sim_{n+1}\mu_{\cal E}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}B=\mu_{\cal E}B\ \text{ and }\
\mu_{\cal D}\Delta_{\widehat{\alpha}}(a)B=\mu_{\cal
E}\Delta_{\widehat{\alpha}}(a)B\qquad\forall\,a\in{\sf
L}\quad\forall\,\widehat{\alpha}$ (10), Lemma 9
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal E}\vec{u}\
\text{ and }\ \mu_{\cal D}\Delta_{\widehat{\alpha}}(a)\vec{u}=\mu_{\cal
E}\Delta_{\widehat{\alpha}}(a)\vec{u}\qquad\forall\,\vec{u}\in\mathcal{V}_{n}\quad\forall\,a\in{\sf
L}\quad\forall\,\widehat{\alpha}$ definition of $B$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}\qquad\forall\,\vec{u}\in\mathcal{V}_{n+1}$ definition of
$\mathcal{V}_{n+1}$

Hence (9) is shown.

Let $s$ be the smallest number with $\mathcal{V}_{s}=\mathcal{V}_{s+1}$. We
have $s\leq|Q|-1$, since $\mathcal{V}_{0},\mathcal{V}_{1},\ldots$ are
increasing subspaces of $\mathbb{R}^{Q}$. By the definition, the subspace
$\mathcal{V}_{n+1}$ depends only on $\mathcal{V}_{n}$, so we have
$\mathcal{V}_{s}=\mathcal{V}_{t}$ for all $t\geq s$. The vector space
$\mathcal{V}_{s}$ has the closure properties required by the definition of
$\mathcal{V}$, hence $\mathcal{V}_{s}\supseteq\mathcal{V}$. Since
$\mathcal{V}_{n}\subseteq\mathcal{V}$ for all $n$, it follows that
$\mathcal{V}_{s}=\mathcal{V}$.

Let $\mu_{\cal D},\mu_{\cal E}\in{\sf subDist}(Q)$. We have:

$\displaystyle\mu_{\cal D}\sim_{s}\mu_{\cal E}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{s}$}$ by (9)
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{s+1}$}$
$\displaystyle\mathcal{V}_{s}=\mathcal{V}_{s+1}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\sim_{s+1}\mu_{\cal E}$ by (9)

By Lemma 7.2. this implies $\mathord{\sim}_{s}=\mathord{\sim}$. We have:

$\displaystyle\mu_{\cal D}\sim\mu_{\cal E}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\sim_{s}\mu_{\cal E}$
$\displaystyle\mathord{\sim}=\mathord{\sim}_{s}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{s}$}$ by (9)
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
E}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}$}$
$\displaystyle\mathcal{V}_{s}=\mathcal{V}$

∎

###  0.D.5 Proof of Theorem 5.2

We prove Theorem 5.2 from the main text. The proof is mainly based on
Proposition 3.

Theorem 5.2. The problem that, given two MDPs ${\cal D}$ and ${\cal E}$, asks
whether ${\cal D}\sim{\cal E}$ is in coNP.

###### Proof

Without loss of generality we assume ${\cal D}=\langle Q,\mu^{{\cal
D}}_{0},{\sf L},\delta\rangle$ and ${\cal E}=\langle Q,\mu^{{\cal E}}_{0},{\sf
L},\delta\rangle$. Hence we wish to decide in NP whether $\mu^{{\cal
D}}_{0}\not\sim\mu^{{\cal E}}_{0}$.

Let $\mathcal{V}\subseteq\mathbb{R}^{Q}$ be the vector space defined in
Proposition 3. We have:

$\displaystyle\mu^{{\cal D}}_{0}\not\sim\mu^{{\cal E}}_{0}$
$\displaystyle\quad\Longleftrightarrow\quad\exists\,\vec{u}\in\mathcal{V}\text{
with }\mu^{{\cal D}}_{0}\vec{u}\neq\mu^{{\cal E}}_{0}\vec{u}$ Proposition 3
$\displaystyle\quad\Longleftrightarrow\quad\mathit{Cond}$
$\displaystyle\text{from the definition of~{}$\mathcal{V}$},$

where $\mathit{Cond}$ is the following condition:

> There are $k\in\\{1,2,\ldots,|Q|\\}$ and
> $\vec{b}_{0}=\vec{1},\vec{b}_{1},\ldots,\vec{b}_{k-1}\in\mathbb{R}^{Q}$ and
> $i_{0},i_{1},\ldots,i_{k-1}\in\\{0,1,\ldots,k-2\\}$ and
> $a_{1},a_{2},\ldots,a_{k-1}\in{\sf L}$ and pure local strategies
> $\widehat{\alpha}_{1},\widehat{\alpha}_{2},\ldots,\widehat{\alpha}_{k-1}$
> such that for all $j\in\\{1,2,\ldots,k-1\\}$
>
>   * •
>
> $\widehat{\alpha}_{j}$ is extremal with respect to the vector space spanned
> by $\vec{b}_{0},\vec{b}_{1},\ldots,\vec{b}_{j-1}$ and
>
>   * •
>
> $i_{j}<j$ and
>
>   * •
>
> $\vec{b}_{j}=\Delta_{\widehat{\alpha}_{j}}(a_{j})\vec{b}_{i}$,
>
>

>
> and $\mu^{{\cal D}}_{0}\vec{b}_{k-1}\neq\mu^{{\cal E}}_{0}\vec{b}_{k-1}$.

It remains to argue that $\mathit{Cond}$ can be checked in NP. We can
nondeterministically guess $k\leq|Q|$ and $i_{0},i_{1},\ldots,i_{k-1}\leq k-2$
and $a_{1},a_{2},\ldots,a_{k-1}\in{\sf L}$ and pure local strategies
$\widehat{\alpha}_{1},\widehat{\alpha}_{2},\ldots,\widehat{\alpha}_{k-1}$.
This determines $\vec{b}_{1},\ldots,\vec{b}_{k-1}$. All conditions in
$\mathit{Cond}$ are straightforward to check in polynomial time, except the
condition that for all $j\in\\{1,2,\ldots,k-1\\}$ we have that
$\widehat{\alpha}_{j}$ is extremal with respect to the vector space spanned by
$\vec{b}_{0},\vec{b}_{1},\ldots,\vec{b}_{j-1}$. In the remainder of the proof,
we argue that this can also be checked in polynomial time.

Let $j\in\\{1,2,\ldots,k-1\\}$. Let $B\in\mathbb{R}^{Q\times j}$ be the matrix
with columns $\vec{b}_{0},\vec{b}_{1},\ldots,\vec{b}_{j-1}$. We want to check
that $\widehat{\alpha}_{j}$ is extremal with respect to $B$. For all $q\in Q$,
compute in polynomial time the set ${\sf eqmoves}(q)\subseteq{\sf moves}(q)$
defined by

${\sf eqmoves}(q)=\\{{\sf m}\in{\sf moves}(q)\mid p(d_{q},\alpha_{q,{\sf
m}})=p(d_{q},\widehat{\alpha}_{j})\\},$

where $\alpha_{q,{\sf m}}$ is a pure local strategy with $\alpha_{q,{\sf
m}}(q)({\sf m})=1$ (it does not matter how $\alpha_{q,{\sf m}}(q^{\prime})$ is
defined for $q^{\prime}\neq q$). We want to verify that (4) and (5) holds for
$\widehat{\alpha}_{j}$. By linearity, it suffices to check (4) and (5) for all
_pure_ local strategies $\alpha$. Hence we need to find
$\vec{v}\in\mathbb{R}^{|{\sf L}|\cdot j}$ so that for all $q\in Q$ and all
${\sf m}\in{\sf moves}(q)\setminus{\sf eqmoves}(q)$ we have
$p(d_{q},\alpha_{q,{\sf m}})\vec{v}<p(d_{q},\widehat{\alpha}_{j})\vec{v}$. If
such a vector $\vec{v}$ exists, it can be scaled up by a large positive scalar
so that we have:

$p(d_{q},\alpha_{q,{\sf m}})\vec{v}+1\leq
p(d_{q},\widehat{\alpha}_{j})\vec{v}\quad\forall\,q\in Q\quad\forall\,{\sf
m}\in{\sf moves}(q)\setminus{\sf eqmoves}(q)$ (11)

Hence it suffices to check if there exists a vector $\vec{v}$ that satisfies
(11). This amounts to a feasibility check of a linear program of polynomial
size. Such a check can be carried out in polynomial time. ∎

###  0.D.6 Proof of Proposition 4

The following Lemma is analogous to Lemma 9.

###### Lemma 10

Let ${\cal D}=\langle Q,\mu^{{\cal D}}_{0},{\sf L},\delta\rangle$ be an MDP
and ${\cal C}=\langle Q_{\cal C},\mu^{{\cal C}}_{0},{\sf L},\delta\rangle$ be
an MC with $Q_{\cal C}\subseteq Q$. Let $n\geq 0$ and $k\geq 1$. Suppose that
a matrix $B\in\mathbb{R}^{Q\times k}$ is such that for all $\mu_{\cal
D}\in{\sf subDist}(Q)$ and all $\mu_{\cal C}\in{\sf subDist}(Q_{\cal C})$ we
have $\mu_{\cal D}\sim_{n}\mu_{\cal C}$ if and only if $\mu_{\cal
D}B=\mu_{\cal C}B$. Then for all $\mu_{\cal D}\in{\sf subDist}(Q)$ and all
$\mu_{\cal C}\in{\sf subDist}(Q_{\cal C})$ we have $\mu_{\cal
D}\sim_{n+1}\mu_{\cal C}$ if and only if $\mu_{\cal D}B=\mu_{\cal C}B$ and
$\mu_{\cal D}\Delta_{\alpha}(a)B=\mu_{\cal C}\Delta_{\alpha}(a)B$ holds for
all $a\in{\sf L}$ and for all local strategies $\alpha$.

###### Proof

By combining Lemma 8 and the definition of $p(\mu,\alpha)$. ∎

Now we can prove Proposition 4 from the main text:

Proposition 4. Let ${\cal D}=\langle Q,\mu^{{\cal D}}_{0},{\sf
L},\delta\rangle$ be an MDP and ${\cal C}=\langle Q_{\cal C},\mu^{{\cal
C}}_{0},{\sf L},\delta\rangle$ be an MC with $Q_{\cal C}\subseteq Q$. Let
$\mathcal{V}\subseteq\mathbb{R}^{Q}$ be the smallest column-vector space such
that

  * •

$\vec{1}=(1\ 1\cdots 1)^{T}\in\mathcal{V}$ (where $T$ denotes transpose) and

  * •

$\Delta_{\alpha}(a)\vec{u}\in\mathcal{V}$ for all $\vec{u}\in\mathcal{V}$, all
labels $a\in{\sf L}$ and all local strategies $\alpha$.

Then for all $\mu_{\cal D}\in{\sf subDist}(Q)$ and all $\mu_{\cal C}\in{\sf
subDist}(Q_{\cal C})$, we have $\mu_{\cal D}\sim\mu_{\cal C}$ if and only if
$\mu_{\cal D}\vec{u}=\mu_{\cal C}\vec{u}$ for all $\vec{u}\in\mathcal{V}$.

###### Proof

The proof is very similar to the one of Proposition 3. We give it explicitly
for completeness.

Define $\mathcal{V}_{0}=\\{r\vec{1}\mid
r\in\mathbb{R}\\}\subseteq\mathbb{R}^{Q}$. For all $n\geq 0$ define
$\mathcal{V}_{n+1}$ to be the smallest vector space such that

  * •

$\mathcal{V}_{n}\subseteq\mathcal{V}_{n+1}$

  * •

$\Delta_{\alpha}(a)\vec{u}\in\mathcal{V}_{n+1}$, for all
$\vec{u}\in\mathcal{V}_{n}$ and all $a\in{\sf L}$ and all local strategies
$\alpha$.

We have $\mathcal{V}_{n}\subseteq\mathcal{V}$ for all $n\geq 0$. We claim for
all $\mu_{\cal D}\in{\sf subDist}(Q)$ and all $\mu_{\cal C}\in{\sf
subDist}(Q_{\cal C})$:

$\mu_{\cal D}\sim_{n}\mu_{\cal C}\quad\Longleftrightarrow\quad\mu_{\cal
D}\vec{u}=\mu_{\cal C}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{n}$}$
(12)

We proceed by induction on $n$. For $n=0$, we have:

$\displaystyle\mu_{\cal D}\sim_{0}\mu_{\cal C}$
$\displaystyle\Longleftrightarrow\lVert\mu_{\cal D}\rVert=\lVert\mu_{\cal
C}\rVert$ definition of $\mathord{\sim}_{0}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{1}=\mu_{\cal C}\vec{1}$
definition of $\lVert\cdot\rVert$ $\displaystyle\Longleftrightarrow\mu_{\cal
D}\vec{u}=\mu_{\cal C}\vec{u}\quad\forall\,\vec{u}\in\mathcal{V}_{0}$
definition of $\mathcal{V}_{0}$

For the induction step, let $n\geq 0$. Define $B$ as a matrix whose columns
span $\mathcal{V}_{n}$. We have:

$\displaystyle\mu_{\cal D}\sim_{n}\mu_{\cal C}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
C}\vec{u}\quad\forall\,\vec{u}\in\mathcal{V}_{n}$ induction hypothesis (13)
$\displaystyle\Longleftrightarrow\mu_{\cal D}B=\mu_{\cal C}B$ definition of
$B$

In the following, let $\alpha$ range over all local strategies:

$\displaystyle\mu_{\cal D}\sim_{n+1}\mu_{\cal C}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}B=\mu_{\cal C}B\text{ and
}\mu_{\cal D}\Delta_{\alpha}(a)B=\mu_{\cal
C}\Delta_{\alpha}(a)B\qquad\forall\,a\in{\sf L}\quad\forall\,\alpha$ (13),
Lemma 10 $\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
C}\vec{u}\text{ and }\mu_{\cal D}\Delta_{\alpha}(a)\vec{u}=\mu_{\cal
C}\Delta_{\alpha}(a)\vec{u}\qquad\forall\,\vec{u}\in\mathcal{V}_{n}\quad\forall\,a\in{\sf
L}\quad\forall\,\alpha$ definition of $B$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
C}\vec{u}\qquad\forall\,\vec{u}\in\mathcal{V}_{n+1}$ definition of
$\mathcal{V}_{n+1}$

Hence (12) is shown.

Let $s$ be the smallest number with $\mathcal{V}_{s}=\mathcal{V}_{s+1}$. We
have $s\leq|Q|-1$, since $\mathcal{V}_{0},\mathcal{V}_{1},\ldots$ are
increasing subspaces of $\mathbb{R}^{Q}$. By the definition, the subspace
$\mathcal{V}_{n+1}$ depends only on $\mathcal{V}_{n}$, so we have
$\mathcal{V}_{s}=\mathcal{V}_{t}$ for all $t\geq s$. The vector space
$\mathcal{V}_{s}$ has the closure properties required by the definition of
$\mathcal{V}$, hence $\mathcal{V}_{s}\supseteq\mathcal{V}$. Since
$\mathcal{V}_{n}\subseteq\mathcal{V}$ for all $n$, it follows that
$\mathcal{V}_{s}=\mathcal{V}$.

Let $\mu_{\cal D}\in{\sf subDist}(Q)$ and $\mu_{\cal C}\in{\sf
subDist}(Q_{\cal C})$. We have:

$\displaystyle\mu_{\cal D}\sim_{s}\mu_{\cal C}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
C}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{s}$}$ by (12)
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
C}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{s+1}$}$
$\displaystyle\mathcal{V}_{s}=\mathcal{V}_{s+1}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\sim_{s+1}\mu_{\cal C}$ by (12)

By Lemma 7.2. this implies $\mathord{\sim}_{s}=\mathord{\sim}$. We have:

$\displaystyle\mu_{\cal D}\sim\mu_{\cal C}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\sim_{s}\mu_{\cal C}$
$\displaystyle\mathord{\sim}=\mathord{\sim}_{s}$
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
C}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}_{s}$}$ by (12)
$\displaystyle\Longleftrightarrow\mu_{\cal D}\vec{u}=\mu_{\cal
C}\vec{u}\text{\quad for all $\vec{u}\in\mathcal{V}$}$
$\displaystyle\mathcal{V}_{s}=\mathcal{V}$

∎

###  0.D.7 Proof of Theorem 5.1

We prove Theorem 5.1 from the main text:

Theorem 5.1. The problem ${\sf MDP\sqsubseteq MC}$ is in NC, hence in P.

###### Proof

Let ${\cal D}=\langle Q,\mu^{{\cal D}}_{0},{\sf L},\delta\rangle$ be an MDP
and ${\cal C}=\langle Q_{\cal C},\mu^{{\cal C}}_{0},{\sf L},\delta\rangle$ be
an MC with $Q_{\cal C}\subseteq Q$.

Let $\alpha_{0}$ denote an arbitrary pure local strategy. For each $q\in Q$
and each ${\sf m}\in{\sf moves}(q)$ denote by $\alpha_{q,{\sf m}}$ the pure
local strategy such that $\alpha_{q,{\sf m}}(q)({\sf m})=1$ and
$\alpha_{q,{\sf m}}(q^{\prime})=\alpha_{0}(q^{\prime})$ for all $q^{\prime}\in
Q\setminus\\{q\\}$. Define

$\displaystyle\Sigma$ $\displaystyle=\\{\alpha_{0}\\}\cup\\{\alpha_{q,{\sf
m}}\mid q\in Q,\ {\sf m}\in{\sf moves}(q)\\}$ and $\displaystyle\mathcal{M}$
$\displaystyle=\\{\Delta_{\alpha}(a)\in\mathbb{R}^{Q\times
Q}\mid\alpha\in\Sigma,\ a\in{\sf L}\\}$ and
$\displaystyle\mathcal{M}_{\infty}$
$\displaystyle=\left\\{\Delta_{\alpha}(a)\in\mathbb{R}^{Q\times
Q}\;\middle|\;\alpha\text{ is a local strategy, $a\in{\sf L}$}\right\\}.$

By the definition of $\mathcal{M}_{\infty}$ the vector space
$\mathcal{V}\subseteq\mathbb{R}^{Q}$ from Proposition 4 is the smallest
column-vector space such that

  * •

$\vec{1}=(1\ 1\cdots 1)^{T}\in\mathcal{V}$ and

  * •

$M\vec{u}\in\mathcal{V}$, for all $\vec{u}\in\mathcal{V}$ and all
$M\in\mathcal{M}_{\infty}$.

We have $\mathcal{M}\subseteq\mathcal{M}_{\infty}$, where $|\mathcal{M}|$ is
finite and $|\mathcal{M}_{\infty}|$ is infinite. Every matrix in
$\mathcal{M}_{\infty}$ can be expressed as a linear combination of matrices
from $\mathcal{M}$: Indeed, let $\alpha$ be a local strategy. Then for all
$a\in{\sf L}$ we have:

$\Delta_{\alpha}(a)=\Delta_{\alpha_{0}}(a)+\sum_{q\in
Q}\left(-\Delta_{\alpha_{0}}(a)+\sum_{{\sf m}\in{\sf moves}(q)}\alpha(q)({\sf
m})\cdot\Delta_{\alpha_{q,{\sf m}(q)}}(a)\right)$

So by linearity, the vector space $\mathcal{V}$ is the smallest column-vector
space such that

  * •

$\vec{1}=(1\ 1\cdots 1)^{T}\in\mathcal{V}$ and

  * •

$M\vec{u}\in\mathcal{V}$, for all $\vec{u}\in\mathcal{V}$ and all
$M\in\mathcal{M}$.

Define a finite set of labels ${\sf
L}^{\prime}=\\{b_{\alpha,a}\mid\alpha\in\Sigma,\ a\in{\sf L}\\}$, and for each
$\alpha\in\Sigma$ and each $a\in{\sf L}$ a matrix

$\Delta^{\prime}(b_{\alpha,a})=\frac{1}{|\Sigma|}\Delta_{\alpha}(a).$

The matrix $\sum_{b\in{\sf L}^{\prime}}\Delta^{\prime}(b)$ is stochastic.
Define the MCs ${\cal D}^{\prime}=\langle Q,\mu^{{\cal D}}_{0},{\sf
L}^{\prime},\delta^{\prime}\rangle$ and ${\cal C}^{\prime}=\langle
Q,\mu^{{\cal C}}_{0},{\sf L}^{\prime},\delta^{\prime}\rangle$ such that
$\delta^{\prime}$ induces the transition matrices $\Delta^{\prime}(b)$ for all
$b\in{\sf L}^{\prime}$. The MCs ${\cal D}^{\prime}$ and ${\cal C}^{\prime}$
are computable in logarithmic space. Let
$\mathcal{V}^{\prime}\subseteq\mathbb{R}^{Q}$ be the smallest column-vector
space such that

  * •

$\vec{1}=(1\ 1\cdots 1)^{T}\in\mathcal{V}$ and

  * •

$\Delta^{\prime}(b)\vec{u}\in\mathcal{V}$, for all $\vec{u}\in\mathcal{V}$ and
all $b\in{\sf L}^{\prime}$.

Since the matrices in $\mathcal{M}$ and the matrices $\Delta^{\prime}(b)$ are
scalar multiples of each other, we have $\mathcal{V}=\mathcal{V}^{\prime}$. It
holds:

$\displaystyle{\cal D}\sqsubseteq{\cal C}$
$\displaystyle\Longleftrightarrow{\cal D}\sim{\cal C}\text{ in~{}${\cal D}$}$
Proposition 1 $\displaystyle\Longleftrightarrow\mu^{\cal D}_{0}\sim\mu^{{\cal
C}}_{0}\text{ in~{}${\cal D}$}$ definition
$\displaystyle\Longleftrightarrow\forall\,\vec{u}\in\mathcal{V}:\mu^{{\cal
D}}_{0}\vec{u}=\mu^{{\cal C}}_{0}\vec{u}$ Proposition 4
$\displaystyle\Longleftrightarrow\forall\,\vec{u}\in\mathcal{V}^{\prime}:\mu^{{\cal
D}}_{0}\vec{u}=\mu^{{\cal C}}_{0}\vec{u}$
$\displaystyle\mathcal{V}=\mathcal{V}^{\prime}$
$\displaystyle\Longleftrightarrow\mu^{\cal D}_{0}\sim\mu^{{\cal C}}_{0}\text{
in~{}${\cal D}^{\prime}$}$ Proposition 4
$\displaystyle\Longleftrightarrow{\cal D}^{\prime}\sim{\cal C}^{\prime}\text{
in~{}${\cal D}^{\prime}$}$ definition $\displaystyle\Longleftrightarrow{\cal
D}^{\prime}\sqsubseteq{\cal C}^{\prime}$ Proposition 1

As mentioned in Section 2.2, deciding whether ${\cal
D}^{\prime}\sqsubseteq{\cal C}^{\prime}$ holds amounts to the trace-
equivalence problem for MCs. It follows from Tzeng [20] that the latter is
decidable in NC, hence in P. ∎