The Complexity of Graph-Based Reductions for
Reachability in Markov Decision Processes

arXiv:1710.07903v4 [cs.LO] 24 Feb 2018

Stéphane Le Roux
Department of Mathematics, Technische Universität Darmstadt
leroux@mathematik.tu-darmstadt.de
Guillermo A. Pérez
Université libre de Bruxelles, Departement d’Informatique
gperezme@ulb.ac.be
February 27, 2018
Abstract
We study the never-worse relation (NWR) for Markov decision processes with an infinite-horizon reachability objective. A state q is never
worse than a state p if the maximal probability of reaching the target
set of states from p is at most the same value from q, regardless of the
probabilities labelling the transitions. Extremal-probability states, end
components, and essential states are all special cases of the equivalence
relation induced by the NWR. Using the NWR, states in the same equivalence class can be collapsed. Then, actions leading to sub-optimal states
can be removed. We show that the natural decision problem associated
to computing the NWR is coNP-complete. Finally, we extend a previously known incomplete polynomial-time iterative algorithm to underapproximate the NWR.

1

Introduction

Markov decision processes (MDPs) are a useful model for decision-making in the
presence of a stochastic environment. They are used in several fields, including
robotics, automated control, economics, manufacturing and in particular planning [21], model-based reinforcement learning [23], and formal verification [1].
We elaborate on the use of MDPs and the need for graph-based reductions
thereof in verification and reinforcement learning applications below.
Several verification problems for MDPs reduce to reachability [1, 5]. For
instance, MDPs can be model checked against linear-time objectives (expressed
in, say, LTL) by constructing an omega-automaton recognizing the set of runs
that satisfy the objective and considering the product of the automaton with
the original MDP [6]. In this product MDP, accepting end components — a
generalization of strongly connected components — are identified and selected
1

...

s

p

q

t

...

Figure 1: An MDP with states depicted as circles and distributions as squares.
The maximal reachability probability values from p and q are the same since,
from both, one can enforce to reach s with probability 1, or t with probability
1, using different strategies.
as target components. The question of maximizing the probability that the
MDP behaviours satisfy the linear-time objective is thus reduced to maximizing
the probability of reaching the target components.
The maximal reachability probability is computable in polynomial time by
reduction to linear programming [6, 1]. In practice, however, most model checkers use value iteration to compute this value [18, 9]. The worst-case time
complexity of value iteration is pseudo-polynomial. Hence, when implementing model checkers it is usual for a graph-based pre-processing step to remove
as many unnecessary states and transitions as possible while preserving the
maximal reachability probability. Well-known reductions include the identification of extremal-probability states and maximal end components [5, 1]. The
intended outcome of this pre-processing step is a reduced amount of transition
probability values that need to be considered when computing the number of
iterations required by value iteration.
The main idea behind MDP reduction heuristics is to identify subsets of
states from which the maximal probability of reaching the target set of states is
the same. Such states are in fact redundant and can be “collapsed”. Figure 1
depicts an MDP with actions and probabilities omitted for clarity. From p and
q there are strategies to ensure that s is reached with probability 1. The same
holds for t. For instance, from p, to get to t almost surely, one plays to go to the
distribution directly below q; from q, to the distribution above q. Since from
the state p, there is no strategy to ensure that q is reached with probability 1,
p and q do not form an end component. In fact, to the best of our knowledge,
no known MDP reduction heuristic captures this example (i.e., recognizes that
p and q have the same maximal reachability probability for all possible values
of the transition probabilities).
In reinforcement learning the actual probabilities labelling the transitions
of an MDP are not assumed to be known in advance. Thus, they have to
be estimated by experimenting with different actions in different states and
collecting statistics about the observed outcomes [15]. In order for the statistics to be good approximations, the number of experiments has to be high
enough. In particular, when the approximations are required to be probably
approximately correct [24], the necessary and sufficient number of experiments
is pseudo-polynomial [13]. Furthermore, the expected number of steps before
reaching a particular state even once may already be exponential (even if all
the probabilities are fixed). The fact that an excessive amount of experiments
is required is a known drawback of reinforcement learning [16, 20].
A natural and key question to ask in this context is whether the maximal
reachability probability does indeed depend on the actual value of the probability labelling a particular transition of the MDP. If this is not the case, then it

2

need not be learnt. One natural way to remove transition probabilities which
do not affect the maximal reachability value is to apply model checking MDP
reduction techniques.
Contributions and structure of the paper. We view the directed graph
underlying an MDP as a directed bipartite graph. Vertices in this graph are
controlled by players Protagonist and Nature. Nature is only allowed to choose
full-support probability distributions for each one of her vertices, thus instantiating an MDP from the graph; Protagonist has strategies just as he would in an
MDP. Hence, we consider infinite families of MDPs with the same support. In
the game played between Protagonist and Nature, and for vertices u and v, we
are interested in knowing whether the maximal reachability probability from u
is never (in any of the MDPs with the game as its underlying directed graph)
worse than the same value from v.
In Section 2 we give the required definitions. We formalize the never-worse
relation in Section 3. We also show that we can “collapse” sets of equivalent
vertices with respect to the NWR (Theorem 1) and remove sub-optimal edges
according to the NWR (Theorem 2). Finally, we also argue that the NWR
generalizes most known heuristics to reduce MDP size before applying linear
programming or value iteration. Then, in Section 4 we give a graph-based characterization of the relation (Theorem 3), which in turn gives us a coNP upper
bound on its complexity. A matching lower bound is presented in Section 5 (Theorem 4). To conclude, we recall and extend an iterative algorithm to efficiently
(in polynomial time) under-approximate the never-worse relation from [2].
Previous and related work. Reductions for MDP model checking were considered in [7] and [5]. From the reductions studied in both papers, extremalprobability states, essential states, and end components are computable using
only graph-based algorithms. In [3], learning-based techniques are proposed to
obtain approximations of the maximal reachability probability in MDPs. Their
algorithms, however, do rely on the actual probability values of the MDP.
This work is also related to the widely studied model of interval MDPs,
where the transition probabilities are given as intervals meant to model the
uncertainty of the numerical values. Numberless MDPs [11] are a particular
case of the latter in which values are only known to be zero or non-zero. In the
context of numberless MDPs, a special case of the question we study can be
simply rephrased as the comparison of the maximal reachability values of two
given states.
In [2] a preliminary version of the iterative algorithm we give in Section 6
was described, implemented, and shown to be efficient in practice. Proposition 1
was first stated therein. In contrast with [2], we focus chiefly on characterizing
the never-worse relation and determining its computational complexity.

2

Preliminaries

We use set-theoretic notation to indicate whether a letter b ∈ Σ occurs in a
word α = a0 . . . ak ∈ Σ∗ , i.e. b ∈ α if and only if b = ai for some 0 ≤ i ≤ k.
Consider a directed graph G = (V, E) and a vertex u ∈ V . We write uE for
the set of successors of u. That is to say, uE := {v ∈ V | (u, v) ∈ E}. We say
3

that a path π = u0 . . . uk ∈ V ∗ in G visits a vertex v if v ∈ π. We also say that
π is a v–T path, for T ⊆ V , if u0 = v and uk ∈ T .

2.1

Stochastic models

Let S be a finite set. We denote by D(S) the set of all (rational) probabilistic
P distributions on S, i.e. the set of all functions f : S → Q≥0 such that
s∈S f (s) = 1. A probabilistic distribution f ∈ D(S) has full support if
f (s) > 0 for all s ∈ S.
Definition 1 (Markov chains). A Markov chain C is a tuple (Q, δ) where Q is
a finite set of states and δ is a probabilistic transition function δ : Q → D(Q).
A run of a Markov chain is a finite non-empty word ̺ = p0 . . . pn over Q.
We
Q say ̺ reaches q if q = pi for some 0 ≤ i ≤ n. The probability of the run is
0≤i<n δ(pi , pi+1 ).
Let T ⊆ Q be a set of states. The probability of (eventually) reaching T in
C from q0 , which will be denoted by PqC0 [♦T ], is the measure of the runs of C
that start at q0 and reach T . For convenience, let us first define the probability
of staying in states from S ⊆ Q until T is reached 1 , written PqC0 [S U T ], as 1 if
q0 ∈ T and otherwise



X Y
δ(qi , qi+1 ) q0 . . . qn ∈ (S \ T )∗ T for n ≥ 1 .


0≤i<n

We then define PqC0 [♦T ] := PqC0 [Q U T ].
When all runs from q0 to T reach some set U ⊆ Q before, the probability of
reaching T can be decomposed into a finite sum as in the lemma below.

Lemma 1. Consider a Markov chain C = (Q, δ), sets of states U, T ⊆ Q, and a
state q0 ∈ Q \ U . If PqC0 [(Q \ U ) U T ] = 0, then
X q
PqC0 [♦T ] =
PC0 [(Q \ U ) U u] PuC [♦T ].
u∈U

Definition 2 (Markov decision processes). A (finite, discrete-time) Markov
decision process M, MDP for short, is a tuple (Q, A, δ, T ) where Q is a finite
set of states, A a finite set of actions, δ : Q × A → D(Q) a probabilistic transition
function, and T ⊆ Q a set of target states.
For convenience, we write δ(q|p, a) instead of δ(p, a)(q).
Definition 3 (Strategies). A (memoryless deterministic) strategy σ in an MDP
M = (Q, A, δ, T ) is a function σ : Q → A.
Note that we have deliberately defined only memoryless deterministic strategies. This is at no loss of generality since, in this work, we focus on maximizing
the probability of reaching a set of states. It is known that for this type of
objective, memoryless deterministic strategies suffice [19].

4

1
2
1
4

b

1
2

a

p

q

a

3
4
1
2

b

1
4

1
4

p

q

3
4

3
4

1
2

1
2

1
2

Figure 2: On the left we have an MDP with actions {a, b}. On the right we have
the Markov chain induced by the left MDP and the strategy {p 7→ a, q 7→ b}.
From MDPs to chains. An MDP M = (Q, A, δ, T ) and a strategy σ induce
the Markov chain Mσ = (Q, µ) where µ(q) = δ(q, σ(q)) for all q ∈ Q.
Example 1. Figure 2 depicts an MDP on the left. Circles represent states;
double-circles, target states; and squares, distributions. The labels on arrows
from states to distributions are actions; those on arrows from distributions to
states, probabilities.
Consider the strategy σ that plays from p the action a and from q the action
b, i.e. σ(p) = a and σ(q) = b. The Markov chain on the right is the chain
induced by σ and the MDP on the left. Note that we no longer have action
labels.
The probability of reaching a target state from q under σ is easily seen to
be 3/4. In other words, if we write M for the MDP and T for the set of target
states then PqMσ [♦T ] = 34 .

2.2

Reachability games against Nature

We will speak about families of MDPs whose probabilistic transition functions
have the same support. To do so, we abstract away the probabilities and focus
on a game played on a graph. That is, given an MDP M = (Q, A, δ, T ) we
consider its underlying directed graph GM = (V, E) where V := Q ∪ (Q × A) and
E := {(q, hq, ai) ∈ Q × (Q × A)} ∪ {(hp, ai, q) | δ(q|p, a) > 0}. In GM , Nature
controls the vertices Q × A. We formalize the game and the arena it is played
on below.
Definition 4 (Target arena). A target arena A is a tuple (V, VP , E, T ) such
that (VP , VN := V \ VP , E) is a bipartite directed graph, T ⊆ VP is a set of
target vertices, and uE 6= ∅ for all u ∈ VN .
Informally, there are two agents in a target arena: Nature, who controls the
vertices in VN , and Protagonist, who controls the vertices in VP .
From arenas to MDPs. A target arena A = (V, VP , E, T ) together with
a family of probability distributions µ = (µu ∈ D(uE))u∈VN induce an MDP.
Formally, let Aµ be the MDP (Q, A, δ, T ) where Q = VP ⊎{⊥}, A = VN , δ(q|p, a)
is µa (q) if (p, a), (a, q) ∈ E and 0 otherwise, for all p ∈ VP ∪ {⊥} and a ∈ A we
have δ(⊥|p, a) = 1 if (p, a) 6∈ E.
1S

U T should be read as “S until T ” and not understood as a set union.

5

p

q

t

fin

p

q

fin

fail

s

t

fail

Figure 3: Two target arenas with T = {fin} are shown. Round vertices are
elements from VP ; square vertices, from VN . In the left target arena we have
that pE{q} and q E{p} since any path from either vertex visits t before T — see
Lemma 1. In the right target arena we have that t E {p} — see Proposition 1.
The value of a vertex. Consider a target arena A = (V, VP , E, T ) and a
vertex v ∈ VP . We define its (maximal reachability probability) value with
respect to a family of full-support probability
distributions µ as Valµ (v) :=
P
µ
maxσ PvAσµ [♦T ]. For u ∈ VN we set Val (u) := {µu (v)Valµ (v) | v ∈ uE}.

3

The never-worse relation

We are now in a position to define the relation that we study in this work. Let
us fix a target arena A = (V, VP , E, T ).
Definition 5 (The never-worse relation (NWR)). A subset W ⊆ V of vertices
is never worse than a vertex v ∈ V , written v E W , if and only if
∀µ = (µu ∈ D(uE))u∈VN , ∃w ∈ W : Valµ (v) ≤ Valµ (w)
where all the µu have full support. We write v ∼ w if v E {w} and w E {v}.
It should be clear from the definition that ∼ is an equivalence relation. For
u ∈ V let us denote by ũ the set of vertices that are ∼-equivalent and belong
to the same owner, i.e. ũ is {v ∈ VP | v ∼ u} if u ∈ VP and {v ∈ VN | v ∼ u}
otherwise.
Example 2. Consider the left target arena depicted in Figure 3. Using Lemma 1,
it is easy to show that neither p nor q is ever worse than the other since t is
visited before fin by all paths starting from p or q.
The literature contains various heuristics which consist in computing sets of
states and “collapsing” them to reduce the size of the MDP without affecting the
maximal reachability probability of the remaining states. We now show that we
can collapse equivalence classes and, further, remove sub-optimal distributions
using the NWR.

3.1

The usefulness of the NWR

We will now formalize the idea of “collapsing” equivalent vertices with respect
to the NWR. For convenience, we will also remove self-loops while doing so.
Consider a target arena A = (V, VP , E, T ). We denote by A/∼ its ∼-quotient.
That is, A/∼ is the target arena (S, SP , R, U ) where SP = {ṽ | ∃v ∈ VP },
S = {ṽ | ∃v ∈ VN } ∪ SP , U = {t̃ | ∃t ∈ T }, and
R ={(ũ, ṽ) | ∃(u, v) ∈ (VP × VN ) ∩ E : vE \ ũ 6= ∅}
∪{(ũ, ṽ) | ∃(u, v) ∈ (VN × VP ) ∩ E}.
6

For a family µ = (µu ∈ D(uE))u∈VN of full-support distributions we denote by
µ/∼ the family ν = (νũ ∈ D(ũR))
ũ∈SN defined as follows. For all ũ ∈ SN and
P
all ṽ ∈ ũR we have νũ (ṽ) = w∈ṽ µu (w), where u is any element of ũ.
The following property of the ∼-quotient follows from the fact that all the
vertices in ṽ have the same maximal probability of reaching the target vertices.
Theorem 1. Consider a target arena A = (V, VP , E, T ). For all families µ =
(µu ∈ D(uE))u∈VN of full-support probability distributions and all v ∈ VP we
have
max PvAσµ [♦T ] = max
PṽBσ′ [♦U ],
′
σ

σ

ν

where B = A/∼ , ν = µ/∼ , and U = {t̃ | ∃t ∈ T }.
We can further remove edges that lead to sub-optimal Nature vertices. When
this is done after ∼-quotienting the maximal reachability probabilities are preserved.
Theorem 2. Consider a target arena A = (V, VP , E, T ) such that A/∼ = A.
For all families µ = (µu ∈ D(uE))u∈VN of full-support probability distributions,
for all (w, x) ∈ E ∩ (VP × VN ) such that x E (wE \ {x}), and all v ∈ VP we have
max PvAσµ [♦T ] = max
PvBσ′ [♦T ],
′
σ

σ

µ

where B = (V, VP , E \ {(w, x)}, T ).

3.2

Known efficiently-computable special cases

We now recall the definitions of the set of extremal-probability states, end components, and essential states. Then, we observe that for all these sets of states
their maximal probability reachability coincide and their definitions are independent of the probabilities labelling the transitions of the MDP. Hence, they
are subsets of the set of the equivalence classes induced by ∼.
3.2.1

Extremal-probability states.

The set of extremal-probability states of an MDP M = (Q, A, δ, T ) consists of
the set of states with maximal probability reachability 0 and 1. Both sets can be
computed in polynomial time [1, 4]. We give below a game-based definition of
both sets inspired by the classical polynomial-time algorithm to compute them
(see, e.g., [1]). Let us fix a target arena A = (V, VP , E, T ) for the sequel.
For a set T ⊆ V , let us write ZT := {v ∈ V | T is not reachable from v}.
(Almost-surely winning) strategies. A strategy for Protagonist in a target
arena is a function σ : VP → VN . We then say that a path v0 . . . vn ∈ V ∗ is consistent with σ if vi ∈ VP =⇒ σ(vi ) = vi+1 for all 0 ≤ i < n. Let Reach(v0 , σ)
denote the set of vertices reachable from v0 under σ, i.e. Reach(v0 , σ) := {vk |
v0 . . . vk is a path consistent with σ}.
We say that a strategy σ for Protagonist is almost-surely winning from u0 ∈
V to T ⊆ VP if, after modifying the arena to make all t ∈ T into sinks, for all
v0 ∈ Reach(u0 , σ) we have Reach(v0 , σ) ∩ T 6= ∅. We denote the set of all
such strategies by WinvT0 .
7

The following properties regarding almost-surely winning strategies in a target arena follow from the correctness of the graph-based algorithm used to
compute extremal-probability states in an MDP [1, Lemma 10.108].
Lemma 2 (From [1]). Consider a target arena A = (V, VP , E, T ). For all
families µ = (µu ∈ D(uE))u∈VN of full-support probability distributions, for all
v ∈ VP the following hold.
(i) maxσ PvAσµ [♦T ] = 0 ⇐⇒ v ∈ ZT
(ii) ∀σ : σ ∈ WinvT ⇐⇒ PvAσµ [♦T ] = 1
3.2.2

End components.

Let us consider an MDP M = (Q, A, δ, T ). A set S ⊆ Q of states is an end
component in M if for all pairs of states p, q ∈ S there exists a strategy σ such
that PpMσ [S U q] = 1.
Example 3. Let us consider the MDP shown on the left in Figure 2. The set
{p, q} is an end component since, by playing a from both states, one can ensure
to reach either state from the other with probability 1.
It follows immediately from the definition of end component that the maximal probability of reaching T from states in the same end component is the
same.
Lemma 3. Let S ⊆ Q be an end component in M. For all p, q ∈ S we have
that maxσ PpMσ [♦T ] = maxσ PqMσ [♦T ].
We say an end component is maximal if it is maximal with respect to set
inclusion. Furthermore, from the definition of end components in MDPs and
Lemma 2 it follows that we can lift the notion of end component to target
arenas. More precisely, a set S ⊆ VP is an end component in A if and only if
for some family of full-support probability distributions µ we have that S is an
end component in Aµ (if and only if for all µ′ the set S is an end component in
Aµ′ ).
The set of all maximal end components of a target arena can be computed
in polynomial time using an algorithm based on the strongly connected components of the graph [8, 1].
3.2.3

Essential states.

Consider a target arena A = (V, VP , E, T ) and let ⊑ be the smallest relation
satisfying the following. For all u ∈ VP we have u ⊑ u. For all u0 , v ∈ VP \ ZT
such that u0 6= v we have u0 ⊑ v if for all paths u0 u1 u2 we have that u2 ⊑ v
and there is at least one such path. Intuitively, u ⊑ v holds whenever all paths
starting from u reach v. In [7], the maximal vertices according to ⊑ are called
essential states 2 .
Lemma 4 (From [7]). Consider a target arena A = (V, VP , E, T ). For all families µ = (µu ∈ D(uE))u∈VN of full-support probability distributions, for all v ∈
VP and all essential states w, if v ⊑ w then maxσ PvAσµ [♦T ] = maxσ′ Pw
[♦T ].
Aσ′
µ

2 This

is not the usual notion of essential states from classical Markov chain theory

8

Note that, in the left arena in Figure 3, p ⊑ t does not hold since there is a
cycle between p and q which does not visit t.
It was also shown in [7] that the ⊑ relation is computable in polynomial
time.

4

Graph-based characterization of the NWR

In this section we give a characterization of the NWR that is reminiscent of the
topological-based value iteration proposed in [5]. The main intuition behind our
characterization is as follows. If v E W does not hold, then for all 0 < ε < 1
there is some family µ of full-support distributions such that Valµ (v) is at least
1 − ε, while Valµ (w) is at most ε for all w ∈ W . In turn, this must mean that
there is a path from v to T which can be assigned a high probability by µ while,
from W , all paths go with high probability to ZT .
We capture the idea of separating a “good” v–T path from all paths starting
from W by using partitioning of V into layers Si ⊆ V . Intuitively, we would
like it to be easy to construct a family µ of probability distributions such that
from all vertices in Si+1 all paths going to vertices outside of Si+1 end up, with
high probability, in lower layers, i.e. some Sk with k < i. A formal definition
follows.
Definition 6 (Drift partition and vertices). Consider a target arena A =
(V, VP , E, T ) and a partition (Si )0≤i≤k of V . For all 0 ≤ i ≤ k, let Si+ := ∪i<j Sj
and Si− := ∪j<i Sj , and let Di := {v ∈ Si ∩ VN | vE ∩ Si− 6= ∅}. We define the
set D := ∪0<i<k Di of drift vertices. The partition is called a drift partition if
the following hold.
• For all i ≤ k and all v ∈ Si ∩ VP we have vE ∩ Si+ = ∅.
• For all i ≤ k and all v ∈ Si ∩ VN we have vE ∩ Si+ 6= ∅ =⇒ v ∈ D.
Using drift partitions, we can now formalize our characterization of the negation of the NWR.
Theorem 3. Consider a target arena A = (V, VP , E, T ), a non-empty set of
vertices W ⊆ V , and a vertex v ∈ V . The following are equivalent
(i) ¬ (v E W )
(ii) There exists a drift partition (Si )0≤i≤k and a simple path π starting in v
and ending in T such that π ⊆ Sk and W ⊆ Sk− .
Before proving Theorem 3 we need an additional definition and two intermediate results.
Definition 7 (Value-monotone paths). Let A = (V, VP , E, T ) be a target
arena and consider a family of full-support probability distributions µ = (µu ∈
D(uE))u∈VN . A path v0 . . . vk is µ-non-increasing if and only if Valµ (vi+1 ) ≤
Valµ (vi ) for all 0 ≤ i < k; it is µ-non-decreasing if and only if Valµ (vi ) ≤
Valµ (vi+1 ) for all 0 ≤ i < k.
It can be shown that from any path in a target arena ending in T one can
obtain a simple non-decreasing one.
9

Lemma 5. Consider a target arena A = (V, VP , E, T ) and a family of fullsupport probability distributions µ = (µu ∈ D(uE))u∈VN . If there is a path
from some v ∈ V to T , there is also a simple µ-non-decreasing one.
Additionally, we will make use of the following properties regarding vertexvalues. They formalize the relation between the value of a vertex, its owner,
and the values of its successors.
Lemma 6. Consider a target arena A = (V, VP , E, T ) and a family of fullsupport probability distributions µ = (µu ∈ D(uE))u∈VN .
(i) For all u ∈ VP , for all successors v ∈ uE it holds that Valµ (v) ≤ Valµ (u).
(ii) For all u ∈ VN it holds that
(∃v ∈ uE : Valµ (u) < Valµ (v)) =⇒ (∃w ∈ uE : Valµ (w) < Valµ (u)).
Proof of Theorem 3. Recall that, by definition, (i) holds if and only if there
exists a family µ = (µu ∈ D(uE))u∈VN of full-support probability distributions
such that ∀w ∈ W : Valµ (w) < Valµ (v).
Let us prove (i) =⇒ (ii). Let x0 < x1 < . . . be the finitely many (i.e. at
most |V |) values that occur in the MDP Aµ , and let k be such that Valµ (v) = xk .
For all 0 ≤ i < k let Si := {u ∈ V | Valµ (u) = xi }, and let Sk := V \ ∪i<k Si .
Let us show below that the Si form a drift partition.
• ∀i ≤ k, ∀u ∈ Si ∩ SP : uE ∩ Si+ = ∅ by Lemma 6.(i) (for i < k) and since
Sk+ = ∅.
• ∀i ≤ k, ∀u ∈ Si ∩ SN : uE ∩ Si+ 6= ∅ =⇒ x ∈ D by Lemma 6.(ii) (for
i < k) and since Sk+ = ∅.
We have that Valµ (w) < Valµ (v) = xk for all w ∈ W , by assumption, so
W ⊆ Sk− by construction. By Lemma 5 there exists a simple µ-non-decreasing
path π from v to T , so all the vertices occurring in π have values at least Valµ (v),
so π ⊆ Sk .
We will prove (ii) =⇒ (i) by defining some full-support distribution family
µ. The definition will be partial only, first on π ∩ VN , and then on the drift
vertices in V \ Sk . Let 0 < ε < 1, which is meant to be small enough. Let us
write π = v0 . . . vn so that v0 = v and vn ∈ T . Let us define µ on π ∩ VN as
follows: for all i < n, if vi ∈ VN let µvi (vi+1 ) := 1 − ε. Let σ be an arbitrary
Protagonist strategy such that for all i < n, if vi ∈ VP then σ(vi ) := vi+1 .
Therefore
(1 − ε)|V | ≤ (1 − ε)n
Y
µvi (vi+1 )
≤

since π is simple
by definition of µ

i<n,vi ∈SN

≤ PvAσµ [♦T ]

≤ max
PvAσ′ [♦T ] = Valµ (v).
′
σ

So, for 0 < ε < 1 −

(1)

µ

1

|V√
|

2

, we have

1
2

< (1 − ε)|V | ≤ Valµ (v). Below we will

further define µ such that Valµ (w) ≤ 1 − (1 − ε)|V | <
10

1
2

for all w ∈ W and all

0 < ε < 1 − |V1√| , which will prove (ii) =⇒ (i). However, the last part of the
2
proof is more difficult.
For all 1 ≤ i ≤ k, for all drift vertices u ∈ Si , let ̺(u) be a successor
of u in Si− . Such a ̺(u) exists by definition of the drift vertices. Then let
µu (̺(u)) := 1 − ε. We then claim that
̺(u)

∀u ∈ D : (1 − ε)(1 − PAσµ [♦T ]) ≤ 1 − PuAσµ [♦T ].

(2)

Indeed, 1 − PuAσµ [♦T ] is the probability that, starting at u and following σ, T is
̺(u)

never reached; and (1 − ε)(1 − PAσµ [♦T ]) is the probability that, starting at u
and following σ, the second vertex is ̺(u) and T is never reached.
Now let σ be an arbitrary strategy, and let us prove the following by induction on j.
∀0 ≤ j < k, ∀w ∈ Sj ∪ Sj− : Pw
[♦T ] ≤ 1 − (1 − ε)j
Aσ
µ
Base case, j = 0: by assumption W is non-empty and included in Sk− ,
so 0 < k. Also by assumption T ⊆ Sk , so T ∩ S0 = ∅. By definition of
a drift partition, there are no edges going out of S0 , regardless of whether
the starting vertex is in VP or VN . So there is no path from w to T , which
implies Valµ (w) = 0 for all w ∈ S0 , and the claim holds for the base case.
Inductive case, let w ∈ Sj , let D′ := D ∩ (Sj ∪ Sj− ) and let us argue that every
path π from w to T must at some point leave Sj ∪ Sj− to reach a vertex with
higher index, i.e. there is some edge (πi , πi+1 ) from πi ∈ Sj ∪ Sj− to some
πi+1 ∈ Sℓ with j < ℓ. By definition of a drift partition, πi must also be a
drift vertex,P
i.e. πi ∈ D′ . Thus, if we let F := VP \ D′ , Lemma 1 implies that
w
[F U u] PuAσµ [♦T ]. Now, since
Pw
[♦T
]
=
Aσ
u∈D′ PAσ
µ
µ
X

u∈D′

=

PuAσµ [♦T ]

X

PuAσµ [♦T ] +

X

PuAσµ [♦T ] +

X

(1 − (1 − ε)j−1 )+

u∈D∩Sj−

≤

u∈D∩Sj−

≤

X

PuAσµ [♦T ]

X

(1 − (1 − ε)(1 − PAσµ [♦T ]))

u∈Dj

u∈Dj

by splitting the sum
̺(u)

by (2)
by IH and since

u∈D∩Sj−

X

(1 − (1 − ε)(1 − ε)j−1 )

∀x ∈ Dj : ̺(x) ∈ Sj−

X

(1 − (1 − ε)j )

(1 − ε)j ≤ (1 − ε)j−1

u∈Dj

≤

u∈D′

P
[F U u] ≤ 1, we have that Pw
[♦T ] ≤ 1−(1−ε)j . The induction
and u∈D′ Pw
Aσ
Aσ
µ
µ
is thus complete. Since σ is arbitrary in the calculations above, and since
j < k ≤ |V |, we find that Valµ (w) ≤ 1 − (1 − ε)|V | for all w ∈ W ⊆ Sk− .
For 0 < ε < 1 − |V1√| we have 21 < (1 − ε)|V | , as mentioned after (1), so
2

Valµ (w) ≤ 1 − (1 − ε)|V | < 12 .
11

5

Intractability of the NWR

It follows from Theorem 3 that we can decide whether a vertex is sometimes
worse than a set of vertices by guessing a partition of the vertices and verifying
that it is a drift partition. The verification can clearly be done in polynomial
time.
Corollary 1. Given a target arena A = (V, VP , E, T ), a non-empty set W ⊆ V ,
and a vertex v ∈ V , determining whether v E W is decidable and in coNP.
We will now show that the problem is in fact coNP-complete already for
Markov chains.
Theorem 4. Given a target arena A = (V, VP , E, T ), a non-empty vertex set
W ⊆ V , and a vertex v ∈ V , determining whether v E W is coNP-complete
even if |uE| = 1 for all u ∈ VP .
The idea is to reduce the 2-Disjoint Paths problem (2DP) to the existence of a drift partition witnessing that v E {w} does not hold, for some
v ∈ V . Recall that 2DP asks, given a directed graph G = (V, E) and vertex
pairs (s1 , t1 ), (s2 , t2 ) ∈ V × V , whether there exists an s1 –t1 path π1 and an
s2 –t2 path π2 such that π1 and π2 are vertex disjoint, i.e. π1 ∩ π2 = ∅. The
problem is known to be NP-complete [12, 10]. In the sequel, we assume without loss of generality that (a) t1 and t2 are reachable from all s ∈ V \ {t1 , t2 };
and (b) t1 and t2 are the only sinks G.
Proof of Theorem 4. From the 2DP input instance, we construct the target
arena A = (S, SP , R, T ) with S := V ∪ E, R := {(u, hu, vi), (hu, vi, v) ∈ S × S |
(u, v) ∈ E or u = v ∈ {t1 , t2 }}, SP := V × V , and T := {ht1 , t1 i}. We will show
there are vertex-disjoint s1 –t1 and s2 –t2 paths in G if and only if there is a drift
partition (Si )0≤i≤k and a simple s1 –t1 path π such that π ⊆ Sk and s2 ∈ Sk− .
The result will then follow from Theorem 3.
Suppose we have a drift partition (Si )0≤i≤k with s2 ∈ Sk− and a simple path
π = v0 hv0 , v1 i . . . hvn−1 , vn ivn with v0 = s1 , vn = t1 . Since the set {t2 , ht2 , t2 i}
is trapping in A, i.e. all paths from vertices in the set visit only vertices from it,
we can assume that S0 = {t2 , ht2 , t2 i}. (Indeed, for any drift partition, one can
obtain a new drift partition by moving any trapping set to a new lowest layer.)
Now, using the assumption that t2 is reachable from all s ∈ V \ {t1 , t2 } one can
show by induction that for all 0 ≤ j < k and for all ̺ = u0 ∈ Sj there is a path
−
u0 . . . um in G with um = t2 and ̺ ⊆ Sj+1
. This implies that there is a s2 –t2
−
path π2 in G such that π2 ⊆ Sk . It follows that π2 is vertex disjoint with the
s1 –t1 path v0 . . . vn in G.
Now, let us suppose that we have s1 –t1 and s2 –t2 vertex disjoint paths
π1 = u0 . . . un and π2 = v0 . . . vm . Clearly, we can assume both π1 , π2 are simple.
We will construct a partition (Si )0≤i≤m+1 and show that it is indeed a drift par−
tition, that u0 hu0 , u1 i . . . hun−1 , un iun ⊆ Sm+1 , and s2 = v0 ∈ Sm+1
. Let us set
S0 := {hvm−1 , vm i, vm , ht2 , t2 i}, Si := {hvm−i−1 , vm−i i, vm−i } for all 0 < i ≤ m,
and Sm+1 := S \ ∪0≤i≤m Si . Since π2 is simple, (Si )0≤i≤m+1 is a partition of V .
−
, and u0 hu0 , u1 i . . . hun−1 , un iun ⊆
Furthermore, we have that s2 = v0 ∈ Sm+1
Sm+1 since π1 and π2 are vertex disjoint. Thus, it only remains for us to argue
that for all 0 ≤ i ≤ m + 1: for all w ∈ Si ∩ SN we have wR ∩ Si+ = ∅,
and for all w ∈ Si ∩ VN we have wR ∩ Si+ 6= ∅ =⇒ wR ∩ Si− 6= ∅.
12

By construction of the Si , we have that eR ⊆ Si for all 0 ≤ i ≤ m and all
e ∈ Si ∩ SP . Furthermore, for all 0 < i ≤ m, for all x ∈ Si ∩ SN = {vm−i },
there exists y ∈ Si−1 ∩ SP = {hvm−i , vm−i+1 i} such that (x, y) ∈ R — induced by (vm−i , vm−1+1 ) ∈ E from π2 . To conclude, we observe that since
S0 = {hvm−1 , vm i, vm = t2 , ht2 , t2 i} and {t2 , ht2 , t2 i} is trapping in A, the set
t2 R is contained in S0 .

6

Efficiently under-approximating the NWR

Although the full NWR cannot be efficiently computed for a given MDP, we can
hope for “under-approximations” that are accurate and efficiently computable.
Definition 8 (Under-approximation of the NWR). Let A = (V, VP , E, T ) be
a target arena and consider a relation  : V × P(V ). The relation  is an
under-approximation of the NWR if and only if ⊆ E.
We denote by ∗ the pseudo transitive closure of . That is, ∗ is the
smallest relation such that ⊆∗ and for all u ∈ V, X ⊆ V if there exists
W ⊆ V such that u ∗ W and w ∗ X for all w ∈ W , then u ∗ X.
Remark 1. The empty set is an under-approximation of the NWR. For all underapproximations  of the NWR, the pseudo transitive closure ∗ of  is also an
under-approximation of the NWR.
In [2], efficiently-decidable sufficient conditions for the NWR were given. In
particular, those conditions suffice to infer relations such as those in the right
MDP from Figure 3. We recall (Proposition 1) and extend (Proposition 2) these
conditions below.
Proposition 1 (From [2]). Consider a target arena A = (V, VP , E, T ) and an
under-approximation  of the NWR. For all vertices v0 ∈ V , and sets W ⊆ V
the following hold.
(i) If there exists S ⊆ {s ∈ V | s  W } such that there exists no path
v0 . . . vn ∈ (V \ S)∗ T , then v0 E W .
0
(ii) If W = {w} and there exists S ⊆ {s ∈ VP | w  {s}} such that WinvS∪T
6=
∅, then w E {v0 }.

Proof Sketch. The main idea of the proof of item (i) is to note that S is visited
before T . The desired result then follows from Lemma 1. For item (ii), we
intuitively have that there is a strategy to visit T with some probability or visit
W , where the chances of visiting T are worse than before. We then show that
it is never worse to start from v0 to have better odds of visiting T .
The above “rules” give an iterative algorithm to obtain increasingly better under-approximations of the NWR: from i apply the rules and obtain a
new under-approximation i+1 by adding the new pairs and taking the pseudo
transitive closure; then repeat until convergence. Using the special cases from
Section 3.2 we can obtain a nontrivial initial under-approximation 0 of the
NWR in polynomial time.
The main problem is how to avoid testing all subsets W ⊆ V in every
iteration. One natural way to ensure we do not consider all subsets of vertices
13

p

q

p

q

fail

fin

fin

fail

Figure 4: Two target arenas with T = {fin} are shown. Using Propositions 1
and 2 one can conclude that p ∼ q in both target arenas.
in every iteration is to apply the rules from Proposition 1 only on the successors
of Protagonist vertices.
In the same spirit of the iterative algorithm described above, we now give
two new rules to infer NWR pairs.
Proposition 2. Consider a target arena A = (V, VP , E, T ) and  an underapproximation of the NWR.
(i) For all u ∈ VN , if for all v, w ∈ uE we have v  {w} and w  {v}, then
u ∼ x for all x ∈ uE.
(ii) For all u, v ∈ VP \ T , if for all w ∈ uE such that w  (uE \ {w}) does not
hold we have that w  vE, then u E {v}.
Proof Sketch. Item (i) follows immediately from the definition of Val. For
item (ii) one can use the Bellman optimality equations for infinite-horizon reachability in MDPs to show that since the successors of v are never worse than the
non-dominated successors of u, we must have u E {v}.
The rules stated in Proposition 2 can be used to infer relations like those
depicted in Figure 4 and are clearly seen to be computable in polynomial time
as they speak only of successors of vertices.

7

Conclusions

We have shown that the never-worse relation is, unfortunately, not computable
in polynomial time. On the bright side, we have extended the iterative polynomialtime algorithm from [2] to under-approximate the relation. In that paper, a
prototype implementation of the algorithm was used to empirically show that
interesting MDPs (from the set of benchmarks included in PRISM [18]) can be
drastically reduced.
As future work, we believe it would be interesting to implement an exact
algorithm to compute the NWR using SMT solvers. Symbolic implementations
of the iterative algorithms should also be tested in practice. In a more theoretical
direction, we observe that the planning community has also studied maximizing
the probability of reaching a target set of states under the name of MAXPROB
(see, e.g., [17, 22]). There, online approximations of the NWR would make more
sense than the under-approximation we have proposed here. Finally, one could
define a notion of never-worse for finite-horizon or quantitative objectives.

14

Acknowledgements
The research leading to these results was supported by the ERC Starting grant
279499: inVEST. Guillermo A. Pérez is an F.R.S.-FNRS Aspirant and FWA
postdoc fellow.
We thank Nathanaël Fijalkow for pointing out the relation between this
work and the study of interval MDPs and numberless MDPs. We also thank
Shaull Almagor, Michaël Cadilhac, Filip Mazowiecki, and Jean-François Raskin
for useful comments on earlier drafts of this paper.

References
[1] C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008.
[2] S. Bharadwaj, S. Le Roux, G. A. Pérez, and U. Topcu. Reduction techniques for model checking and learning in MDPs. In IJCAI, pages 4273–
4279, 2017.
[3] T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretı́nský, M. Z.
Kwiatkowska, D. Parker, and M. Ujma. Verification of Markov decision
processes using learning algorithms. In ATVA, volume 8837 of LNCS, pages
98–114, 2014.
[4] K. Chatterjee and M. Henzinger. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In SODA, pages 1318–1336. SIAM, 2011.
[5] F. Ciesinski, C. Baier, M. Größer, and J. Klein. Reduction techniques for
model checking Markov decision processes. In QEST, pages 45–54, 2008.
[6] C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857–907, 1995.
[7] P. R. D’Argenio, B. Jeannet, H. E. Jensen, and K. G. Larsen. Reachability analysis of probabilistic systems by successive refinements. In PAPMPROBMIV, volume 2165 of LNCS, pages 39–56. Springer, 2001.
[8] L. De Alfaro. Formal verification of probabilistic systems. PhD thesis,
Stanford University, 1997.
[9] C. Dehnert, S. Junges, J.-P. Katoen, and M. Volk. A storm is coming: A
modern probabilistic model checker. In CAV, 2017.
[10] T. Eilam-Tzoreff. The disjoint shortest paths problem. Discrete Applied
Mathematics, 85(2):113–138, 1998.
[11] N. Fijalkow, H. Gimbert, F. Horn, and Y. Oualhadj. Two recursively inseparable problems for probabilistic automata. In E. Csuhaj-Varjú, M. Dietzfelbinger, and Z. Ésik, editors, MFCS, volume 8634 of LNCS, pages
267–278. Springer, 2014.
[12] S. Fortune, J. E. Hopcroft, and J. Wyllie. The directed subgraph homeomorphism problem. Theor. Comput. Sci., 10:111–121, 1980.
15

[13] J. Fu and U. Topcu. Probably approximately correct MDP learning and
control with temporal logic constraints. In RSS, 2014.
[14] G. P. Huet. Confluent reductions: Abstract properties and applications
to term rewriting systems: Abstract properties and applications to term
rewriting systems. J. ACM, 27(4):797–821, 1980.
[15] L. P. Kaelbling, M. L. Littman, and A. W. Moore. Reinforcement learning:
A survey. JAIR, 4:237–285, 1996.
[16] K. Kawaguchi. Bounded optimal exploration in MDP. In AAAI, pages
1758–1764, 2016.
[17] A. Kolobov, Mausam, D. S. Weld, and H. Geffner. Heuristic search for
generalized stochastic shortest path MDPs. In F. Bacchus, C. Domshlak,
S. Edelkamp, and M. Helmert, editors, ICAPS. AAAI, 2011.
[18] M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification
of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer,
editors, CAV, volume 6806 of LNCS, pages 585–591. Springer, 2011.
[19] M. L. Puterman. Markov Decision Processes. Wiley-Interscience, 2005.
[20] S. J. Russell, D. Dewey, and M. Tegmark. Research priorities for robust
and beneficial artificial intelligence. AI Magazine, 36(4), 2015.
[21] S. J. Russell and P. Norvig. Artificial Intelligence - A Modern Approach
(3. internat. ed.). Pearson Education, 2010.
[22] M. Steinmetz, J. Hoffmann, and O. Buffet. Goal probability analysis in
probabilistic planning: Exploring and enhancing the state of the art. JAIR,
57:229–271, 2016.
[23] A. L. Strehl, L. Li, and M. L. Littman. Reinforcement learning in finite
MDPs: PAC analysis. J. Mach. Learn. Res., 10:2413–2444, 2009.
[24] L. Valiant. Probably Approximately Correct: Nature’s Algorithms for
Learning and Prospering in a Complex World. Basic Books, 2013.

16

A

Preliminaries

A.1

Definitions

Definition 9 (Memoryful strategies). A (deterministic) strategy σ in an MDP
M = (Q, A, δ, T ) is a function σ : (QA)∗ Q → A.
A finite-memory strategy σ is a strategy that can be encoded as a deterministic Mealy machine A = (S, sI , Q, A, λu , λo ) where S is a finite set of (memory)
states, sI is the initial state, λu : S × Q → S is the update function and
λo : S × Q → A is the output function. The machine encodes σ in the following
sense: σ(q0 a0 . . . qn ) = λo (sn , qn ) where s0 = sI and si+1 = λu (si , qi ) for all
0 ≤ i < n. We then say that A realizes the strategy σ and that σ has memory
|S|. In particular, strategies which have memory 1 are said to be positional (or
memoryless).

A.2

Bellman equations

The following result [1, Theorem 10.100] about MDPs will be useful.
Lemma 7. Consider an MDP M = (Q, A, δ, T ). The vector (xp )p∈Q with
xp = maxσ PpMσ [♦T ] is the unique solution of the following equation system.
• If p ∈ T then xp = 1,
• if p ∈ ZT then xp = 0,
• otherwise
xp = max
a∈A

B

X

δ(q|p, a) · xq .

q∈Q

Proof of Lemma 1

6 T . Thus, by definition, we have
Proof. Since PqC0 [(Q \ U ) U T ] = 0, then q0 ∈


 Y

X
PqC0 [♦T ] =
δ(qi , qi+1 ) q0 . . . qn ∈ (Q \ T )∗ T .
(3)


n≥1

0≤i<n

The set of runs that start at q0 and reach T is equivalent to the union of: the
set of runs that start at q0 and stay in a set S ⊆ Q until they reach T ; and the
set of runs that start at q0 and reach some state from Q \ S before eventually
reaching T . The measure of the runs from the first set is PqC0 [S U T ]. Let us
denote by P[τ(Q\S) < τT ] the measure of the runs from the second set. Since in
Markov chains we have that for all runs p0 . . . pi . . . pm the probabilities of the
prefix p0 . . . pi and the suffix pi . . . pm are independent, we can rewrite (3) as
follows.
PqC0 [♦T ] = PqC0 [(Q \ U ) U T ] + P[τU < τT ]
By assumption we have that the first summand is equal to 0, so
PqC0 [♦T ] = P[τU < τT ].

17

Also by assumption, we know that there are no runs of C starting at q0 and
staying in U ⊆ Q until reaching T . Hence, the set of runs from q0 that reach
some state in U and then eventually reach T is exactly the union, over all u ∈ U ,
of the sets of runs q0 . . . qℓ . . . qn ∈ Q∗ that satisfy
• ∀0 ≤ i < ℓ : qi 6∈ U ,
• qℓ = u,
• ∀ℓ < j < n : qj 6∈ T , and
• qn ∈ T .
Once more using the fact that events (i.e. transition probabilities) in a Markov
chain are independent of the history (i.e. run prefixes) we can write the measure
of the above set as follows.
X q
P[τU < τT ] =
PC0 [(Q \ U ) U u] PuC [♦T ]
u∈U

This concludes the proof.

C

Proof of Theorem 1

We will first prove that collapsing only the Protagonist vertices is safe.
Consider a target arena A = (V, VP , E, T ). Let C be the target arena
(S, SP , R, U ) where
• SP = {ṽ | ∃v ∈ VP },
• S = VN ∪ SP ,
• U = {t̃ | ∃t ∈ T }, and
• R = {(ũ, v) | ∃u ∈ VP ∃v ∈ VN : (u, v) ∈ E and vE \ ũ 6= ∅} ∪ {u, ṽ) | ∃u ∈
VN ∃v ∈ VP : (u, v) ∈ E}.
For a family µ = (µu ∈ D(uE))u∈VN of full-support probability distributions we
define λ = (λu ∈ D(uR))u∈VN as follows. For all u ∈ VN and all ṽ ∈ uR we have
X
µu (w).
λu (ṽ) =
w∈ṽ

Proposition 3. For all families µ = (µu ∈ D(uE))u∈VN of full-support probability distributions and all v ∈ VP we have
max PvAσµ [♦T ] = max
PṽC σ′ [♦U ],
′
σ

σ

λ

where U = {t̃ | t ∈ T }, and C and λ are as defined above.
Proof. For convenience, let us assume that extremal-probability vertices have
already been collapsed so that for all u, v ∈ VP , if u ∼ v then u and v are
not extremal-probability vertices. The argument for correctness of collapsing
extremal-probability vertices is trivial. We will reduce correctness of collapsing
NWR-equivalence classes to the correctness of collapsing end components.
18

Consider the following equation system defined for an arbitrary µ.


if u ∈ T
1
For all u ∈ VP , xu = 0
if u ∈ ZT

P

maxv∈uE w∈vE µv (w) · xw otherwise

(4)

According to Lemma 7, the system has a unique solution assignment
xu = max PuAσµ [♦T ]
σ

(5)

for all u ∈ VP . Now, by definition of the NWR we have that (5) is also a solution
to the following system of equations. For all u ∈ VP

1
if u ∈ T



0
if u ∈ ZT
P
(6)
For all u ∈ VP , xu =

max(

w∈vE µv (w) · xw v ∈ uE


∪ {xy | y ∈ ũ})
otherwise
Observe that equation system (6) corresponds to the target arena C we obtain
by modifying A as follows. For all u ∈ VP and for all v ∈ ũ we add an edge
from u to v (with an intermediate Nature vertex to preserve bipartiteness). It
thus follows from Lemma 7 that the system has a unique solution assignment
corresponding to the maximal reachability probability values of all Protagonist
vertices from C. We have already argued that (5) is a solution to the system (6).
Hence, since µ was chosen arbitrarily, we conclude that for all u ∈ VP
max PuAσµ [♦T ] = max
PuC σ′ [♦T ],
′
σ

σ

µ′

where µ′ is the same as µ for all Nature vertices from A and for all newly added
nature vertices w, µ′w assigns 1 to the unique successor of w in C.
We now remark that in C we have that for all u ∈ VP the set ũ now forms an
end component. Since collapsing end components preserves the desired value [8,
5] (and removing probability-1 self-loops clearly preserves this value too) the
result follows.
We will now argue that collapsing NWR-equivalent Nature-owned vertices
is also safe. The following result will be useful.
Lemma 8. Consider the target arena A. For all u, v ∈ VN it holds that if u ∼ v
and u 6= v then w ∼ x for all w, x ∈ (uE ∪ vE).
Proof. We proceed by contradiction: suppose u ∼ v, u 6= v, and that there exist
w, x ∈ (uE ∪ vE) such that w 6∼ x. It follows from the latter that there are
w ∈ uE and x ∈ vE such that w 6∼ x. Indeed, if this were not the case, then
we would be able to conclude that w ∼ x for all w, x ∈ (uE ∪ vE) by using the
transitivity of ∼. Without loss of generality, assume ¬(w E x).
We will now make use of the equation system (4) from the proof of Proposition 3 with µ the family that witnesses the fact that ¬(w E x), i.e. Valµ (w) >
Valµ (x). Recall that we have assumed u ∼ v and observe that
xw = max Valµ (z),
z∈wE

19

for all w 6∈ (T ∪ ZT ) in the system (4). Now let µ′ be a family of full-support
probability distributions with µ′u (w) = 1 − ε, where 0 < ε < 12 (Valµ (w) −
′
Valµ (x)), and otherwise identical to µ. Since u ∼ v we have that Valµ (u) =
′
Valµ (v) = Valµ (v) = Valµ (u) and thus by, Lemma 7, the maximal reachability
probability values for all states in A are the same for both µ and µ′ . Similarly,
we can obtain a family µ′′ such that µ′′v (x) = 1 − ε without changing the values
of the states in A. We thus have that
′′

′′

Valµ (v) ≤ Valµ (x) + ε
′′

< Valµ (w) − ε
′′

′′

since Valµ (x) = Valµ (x) < Valµ (w) = Valµ (w) and by choice of ε
′′

≤ (1 − ε)Valµ (w)
′′

≤ Valµ (u)
contradicting our initial assumption that u ∼ v.
Let us now consider the following equation system — that corresponds to
C as defined above — for an arbitrary µ and corresponding λ as defined in the
proof of Proposition 3.


if ũ ∈ U
1
(7)
For all ũ ∈ VP , xũ = 0
if ũ ∈ ZU

P

maxv∈ũR w̃∈vR λv (w̃) · xw̃ otherwise
It follows from Lemma 8 that for all v ∈ VN such that |ṽ| > 1 the set vR is
a singleton {w̃} and λz (w̃) = 1. It is then easy to see that system (7) is the
same equation system that corresponds to B as constructed for Theorem 1. The
desired result thus follows from Proposition 3 and Lemma 7.

D

Proof of Theorem 2

The argument to show correctness for the removal of an edge to a sub-optimal
vertex is very similar to the proof of Theorem 1. We first consider the equation system of A with an arbitrary µ. Then, we remove the variable from the
maximum corresponding to the edge we would remove in the target arena. The
only way in which the latter would result in the system not being the one corresponding to the reduced target arena B would be if by removing the edge, we
make some vertex become an element of ZT . That is, we have removed all its
paths to T . We will argue that this is not possible if ∼-quotienting and self-loop
removal have already been applied.
We will need to formalize the intuition that if A = A/∼ there are no cycles
with probability 1 in A.
Lemma 9. Consider a target arena A = (V, VP , E, T ) such that A/∼ = A.
For all families µ = (µu ∈ D(uE))u∈VN of full-support distributions, and all
(v, w) ∈ E ∩ (VP × VN ) we have
X
µw (x)PxAσµ [♦v] < 1.
max
σ

x∈wE

20

Proof. Towards a contradiction, suppose that there is some µ, an edge (v, w),
and a strategy σ for which
X
µw (x)PxAσµ [♦v] = 1.
x∈wE

Observe that from v, Protagonist can play w and reach wE almost surely. Also,
modifying σ, to play w from v does not affect the probability of reaching v from
any x ∈ wE. Let σ ′ denote the modified strategy. It should be clear that σ ′ is
such that for all p, q ∈ {v} ∪ wE
PpAσ′ [♦q] = 1.
µ

Let S := {v} ∪ wE. If S = {v} then we must have a probability-1 self-loop on
v, which contradicts the fact that A/∼ = A. Thus, |S| ≥ 2. It follows that S is
a non-trivial end component and by Lemma 3, also an NWR-equivalence class.
This, again, contradicts our initial assumptions.
We are now ready to prove our claim.
Proof of Theorem 2. We will only argue that w in B is not an element of ZT .
Let Y := wE \ {x}. Observe wE is non-empty. In fact, it must include at
least x and some other vertex so that x E Y holds. Thus, since since A/∼ = A,
we have that w 6∈ ZT .
Towards a contradiction, let us suppose that w in B = (V, VP , E \(w, x), T ) is
an element of ZT . It follows that for all s ∈ S := {s ∈ VP | ∃y ∈ Y : (y, s) ∈ E}
in A every s–T path goes through w. Hence, by Lemma 1, for all µ and for all
σ we have
PsAσµ [♦T ] = PsAσµ [(Q \ {w}) U w] Pw
[♦T ].
(8)
Aσ
µ
Let us now fix arbitrary µ and y ∈ Y such that
X
Valµ (w) =
µy (z)Valµ (z).
z∈yE

(The existence of such a µ and y is guaranteed by Lemma 7 and the fact that
x E Y .) We remark that Valµ (x) ≤ Valµ (y). By definition of Valµ (·) we have
that
X
Valµ (y) =
µy (z)Valµ (z).
z∈yE

Together with Equation (8) we obtain


Valµ (y) = max Pw
[♦T ] ·
Aσ
µ
σ

X

z∈yE



µy (z)PzAσµ [♦w] .

Finally, using Lemma 9, we conclude that Valµ (y) < Valµ (w), contradicting our
assumptions.

21

E

Proof of Lemma 3

Proof. Let σ be a strategy maximizing the value PqMσ [♦T ]. We can then construct a (finite-memory) strategy which, from p ensures PpMσ′ [S U q] = 1 and
from q onwards behaves as σ. If q ∈ T then we are done. Otherwise, Lemma 1
implies that PpMσ′ [♦T ] = PqMσ [♦T ]. Furthermore, we know that memoryless
strategies suffice for reachability [19, 1], so σ ′ can be replaced by a memoryless
strategy.

F

Proof of Lemma 5

Let us denote by λ the empty word.
Definition 10 (Word simplification). For an alphabet Σ, we define the word
simplification function s : Σ∗ → Σ∗ as follows.
• s(λ) := λ
• ∀w ∈ Σ∗ , ∀a ∈ Σ :
– If a ∈
/ s(w) then s(wa) := s(w)a,
– If a ∈ s(w) then s(wa) is the (shortest) prefix of s(w) that ends with
a.
Lemma 10. Let w be a word. s(w) is repetition-free; w and s(w) have the
same starting and ending letters; a letter occurs in s(w) only if it occurs in w;
a two-letter word xy occurs as a factor in s(w) only if it occurs in w.
Proof. By induction. The base case is clear. For the inductive case, let w ∈ Σ∗
and let a ∈ Σ.
First case, a ∈
/ s(w). So s(wa) = s(w)a is repetition-free like s(w) is by IH,
and wa and s(wa) share the same ending letter a. Since w and s(w) share the
same starting letter by IH, so do wa and s(wa) = s(w)a. (It is a if w = λ). Let
b ∈ s(wa). If b = a, the claim clearly holds; if b 6= a then b ∈ s(w), so b ∈ w by
IH, and b ∈ wa. Let xy occur as a two-letter factor in s(wa). If y 6= a then xy
actually occurs in s(w), so by IH it occurs in w, and thus in wa; if y = a then
s(w) ends with x, and by IH so do w, so wa ends with xy.
Second case, a ∈ s(w). Since s(wa) is a prefix of s(w), it is also repetitionfree, and s(wa) ends with a by definition. As a prefix, s(wa) starts with the
same letter as s(w), i.e. the same letter as w by IH, i.e. the same as wa. If
b ∈ s(wa) then b ∈ s(w), so b ∈ w by IH, and b ∈ wa. If xy occurs in s(wa), it
also occurs in its extension s(w), and in w by IH, and finally in wa.
Lemma 11. For all paths γ, s(γ) is a simple path starting (ending) with the
same vertex as γ. It only visits vertices that are already visited in γ, and it only
takes edges that are already taken in γ.
Proof. By Lemma 10 the word s(γ) is repetition-free, and it starts and ends like
γ. Again by Lemma 10, if two vertices xy occur consecutively in s(γ), they also
occur consecutively and in the same order in γ, i.e. (x, y) ∈ E. Therefore s(γ)
is a path, and moreover it takes only edges that are already taken in γ.

22

We can now proceed with the proof of the Lemma.
Proof of Lemma 5. Since there is a path from x to T by assumption, the set L
of all the simple paths from x to T is non-empty. Let T be the prefix closure
of L, and let T ′ be the set of the µ-non-decreasing paths in T , so that T ′ ⊆ T .
The set T is a tree by prefix-closure construction, and T ′ is a tree since the
µ-non-decreasing paths are closed by taking prefixes. Moreover, the elements of
T (and thus T ′ ) are simple paths since the prefixes of simple paths are again
simple paths. Let L′ be the prefix-wise maximal paths in T ′ . The claimed
lemma amounts to L ∩ L′ 6= ∅, equivalently L ∩ T ′ 6= ∅. Also note that a path
in T is in L if and only if it ends with T , so L ∩ T ′ 6= ∅ if and only if some path
in T ′ ends with T .
Towards a contradiction, let us assume that L ∩ L′ = ∅. We can thus let
M consist of the one-vertex extensions in T of the paths in L′ . More formally,
a path γ ∈ T is in M if and only if there exists a vertex y and a path β ∈ L′
such that βy = γ. Clearly, T ′ ∩ M = ∅ by prefix-wise maximality of L′ within
T ′ . So, the elements in M are the least not µ-non-decreasing paths in T . This
implies that
∀γyz ∈ M,

Valµ (z) < Valµ (y)

(9)

(where γ is a path and y, z are vertices), since γy ∈ L′ . Let B ′ (resp. B) be
the ending vertices of the paths in L′ (resp. M ). Let us proceed with a few
remarks:
Remark 2.
1. x occurs as the first vertex of all paths in T , and only as first
vertex, otherwise the paths would not be simple. So x ∈
/ B, since x (as a
path) is clearly in T ′ and since T ′ ∩ M = ∅.
2. Every path in L has a prefix in L′ (i.e. its longest µ-non-decreasing prefix),
and it has a prefix in M too, since L ∩ L′ = ∅. So every path in L visits
B.
3. Every path from x to T visits B: indeed, if a path γ from x to T does not
visit B, neither does s(γ) by Lemma 11. Again by Lemma 11, s(γ) is a
simple path starting at x and ending at T , so s(γ) ∈ L, so it must visit B
by Remark 2.2, contradiction
Let us now prove that for all paths γ ∈ T ′ starting with x, and for all paths
β, if γβ is a path ending with T , then β visits B (even if γβ ∈
/ T ). We proceed
by induction on γ. Base case, γ = x is a one-vertex path: since x ∈
/ B by
Remark 2.1, β visits B for all paths xβ ending with T , by Remark 2.3.
For the inductive case, let γ ′ y ∈ T ′ and let us assume that the claim holds
for the prefixes of γ ′ . Let yβ ′ be a path where β ′ ends with T . By Lemma 11,
s(yβ ′ ) can be decomposed as yβ for some β. By Lemma 11 again, every vertex
occurring in β also occurs in β ′ , and yβ is a simple path ending in T . Let us
make a case disjunction. First case, γ ′ yβ is simple, so it is in L, and it has a
prefix in M by Remark 2.2. Since T ′ ∩ M = ∅, this prefix is a proper extension
of γ ′ y ∈ T ′ , so β visits B. Second case, γ ′ yβ is not simple. Since γ ′ y and
yβ are simple, some vertex z in yβ occurs already in γ ′ , hence the following
decompositions: γ ′ = γℓ zγr and yβ = βℓ zβr . The path γℓ z is in T ′ , the path
γℓ zβr ends with T , so by induction hypothesis βr visits B, and so does β, and
so does β ′ again by Lemma 11. The induction is thus complete.
23

On the one hand, let γy ∈ L′ be such that Valµ (y) = max{Valµ (z) | z ∈ B ′ }.
So Valµ (z) < Valµ (y) for all z ∈ B by (9).
On the other hand, let σ0 be an arbitrary positional strategy for Protagonist
in the MDP. Every path from y to T visits B, as proved by induction above,
which also holds in the graph restricted by σ0 , so PyAσ0 [(V \ B) U T ] = 0. Then
µ
Lemma 1 implies
X y
PyAσ0 [♦T ] =
PAσ0 [(V \ B) U z] PzAσµ0 [♦T ]
µ

µ

z∈B

≤
=
≤

X

z∈B

PyAσ0 [(V \ B) U z] max PzAσµ0 [♦T ]

X

z∈B

PyAσ0 [(V \ B) U z] Valµ (z)

X

PyAσ0 [(V \ B) U z] max Valµ (b)

z∈B

σ

µ

µ

b∈B

µ

≤ max Valµ (b), since
b∈B

X

z∈B

PyAσ0 [(V \ B) U z] ≤ 1.
µ

Therefore, Valµ (y) = maxσ PyAσµ [♦T ] ≤ maxb∈B Valµ (b). This contradicts the
above claim that Valµ (z) < Valµ (y) for all z ∈ B.

G

Proof of Proposition 1

The following observation regarding convex combinations will be useful.
Lemma 12. Consider a finite set of values N ⊆ Q and a probability distribution
δ ∈ D(N ). There exist n, m ∈ N such that
P
• ∃m ∈ N : m ≤ n∈N δ(n) · n
P
• ∃m ∈ N : n∈N δ(n) · n ≤ m

Proof of Proposition 1. Let us start with item (i). From Lemma 1 we have that
X
PvA0σµ [♦T ] =
PvA0σµ [(VP \ S) U s] PsAσµ [♦T ]
s∈S

for all families µ of full-support distributions and strategies σ. It follows from
Lemma 12 that there is some s ∈ S such that
PvA0σµ [♦T ] ≤ PsAσµ [♦T ].
By definition, this means that v0 E S. Hence, by choice of S and Remark 1 we
have v0 E W .
For item (ii), let us assume, without loss of generality, that the vertices from
T ∪ ZT are all sinks. We thus have that there is a strategy σ such that in there
is no path from v0 to ZT without first visiting T ∪ S. We will also assume
that σ, after visiting any vertex from S ∪ T starts playing optimally in order to
maximize the probability of visiting T . (This may require memory.) We have
from Lemma 1 that
X
PvA0σµ [♦ZT ] =
PvA0σµ [VP \ (T ∪ S) U s] PsAσµ [♦ZT ]
s∈S∪T

24

for all full-support distribution families µ. Since all the vertices from T are sinks
PsAσµ [♦ZT ] = 0 for all s ∈ T . Therefore, we can rewrite the above as
PvA0σµ [♦ZT ] =

X
s∈S

PvA0σµ [VP \ (T ∪ S) U s] PsAσµ [♦ZT ].

From Lemma 12 we get that there is some s ∈ S such that
PvA0σµ [♦ZT ] ≤ PsAσµ [♦ZT ]

⇐⇒ 1 − PvA0σµ [♦T ] ≤ 1 − PsAσµ [♦T ] σ is maximizing the prob. of reaching T
⇐⇒ PsAσµ [♦T ] ≤ PvA0σµ [♦T ].

By choice of σ, this implies that s E {v0 } (recall that memoryless strategies
suffice to maximize the probability of reaching a target set of states). Then, by
choice of S ∋ s we have that w E {v0 }.

H

Proof of Proposition 2

Proof. Item (i) follows from the definition of Val.
For item (ii), we suppose the assumptions hold. Hence, by definition of E,
we have that for all families µ of full-support distributions
X
X
max
µw (x)Valµ (x) ≤ max
µy (z)Valµ (z).
w∈uE

y∈vE

x∈wE

The result thus follows from Lemma 7.

25

z∈yE

