Parity Objectives in Countable MDPs

TL;DR

This paper analyzes the memory requirements for optimal and epsilon-optimal strategies in countably infinite MDPs with parity objectives, revealing a dichotomy between objectives that require only memoryless strategies and those needing infinite memory.

Contribution

It provides a complete characterization of when optimal strategies in countable MDPs can be memoryless or require infinite memory across the Mostowski hierarchy.

Findings

Optimal strategies may not always exist in countably infinite MDPs.

A dichotomy exists: some objectives admit MD strategies, others require infinite memory.

Finitely branching MDPs have a similar but more favorable dichotomy.

Abstract

We study countably infinite MDPs with parity objectives, and special cases with a bounded number of colors in the Mostowski hierarchy (including reachability, safety, Buchi and co-Buchi). In finite MDPs there always exist optimal memoryless deterministic (MD) strategies for parity objectives, but this does not generally hold for countably infinite MDPs. In particular, optimal strategies need not exist. For countable infinite MDPs, we provide a complete picture of the memory requirements of optimal (resp., $\epsilon$-optimal) strategies for all objectives in the Mostowski hierarchy. In particular, there is a strong dichotomy between two different types of objectives. For the first type, optimal strategies, if they exist, can be chosen MD, while for the second type optimal strategies require infinite memory. (I.e., for all objectives in the Mostowski hierarchy, if finite-memory randomized strategies suffice then also MD strategies suffice.) Similarly, some objectives admit $\epsilon$-optimal MD-strategies, while for others $\epsilon$-optimal strategies require infinite memory. Such a dichotomy also holds for the subclass of countably infinite MDPs that are finitely branching, though more objectives admit MD-strategies here.

Equations

$$\mathtt{Parity}({\mathit{C}ol}):=\Big{\llbracket}\bigvee_{i\in{\mathcal{C}}}\left({\sf G}{\sf F}[S]^{{\mathit{C}ol}=2\cdot i}\wedge{\sf F}{\sf G}[S]^{{\mathit{C}ol}\leq 2\cdot i}\right)\Big{\rrbracket},$$

$$\{([S{]}^{Col=3},[S{]}^{Col=2})\}$$

$$\{([S{]}^{Col=2},S),(\varnothing ,[S{]}^{Col=3})\}$$

$$\displaystyle\big{(}\exists\sigma\in\Sigma.\,{\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s)}\big{)}$$

$${\mathcal{P}}_{\mathcal{M},s,{\sigma }^{\prime }}(\phi )={\mathtt{val}}_{\mathcal{M}}(s)$$

$$S_{\ast }=\{s\in S\mid \exists \sigma .{\mathcal{P}}_{\mathcal{M},s,\sigma }(\phi )={\mathtt{val}}_{\mathcal{M}}(s)>0\}$$

$${⟶}_{\ast }=\{(s,t)\in S_{\ast }\times S_{\ast }\mid$$

$$\text{ then valM(s)=valM(t)}\}$$

$$P_{\ast }(s)(t)=P(s)(t)\cdot \frac{{\mathtt{val}}_{\mathcal{M}}(t)}{{\mathtt{val}}_{\mathcal{M}}(s)}$$

$${\mathcal{P}}_{{\mathcal{M}}_{\ast },s_0,\sigma }$$

$${\mathcal{P}}_{\mathcal{M},s_0,\sigma }(s_0{s}_1\cdots s_n{S}^{\omega })\cdot \frac{{\mathtt{val}}_{\mathcal{M}}(s_n)}{{\mathtt{val}}_{\mathcal{M}}(s_0)}$$

$$\big{(}\exists\sigma\in\Sigma.\,{\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1\big{)}\quad\Longrightarrow\quad{\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$$

$${\mathcal{P}}_{{\mathcal{M}}_{\ast },s_0,{\sigma }^{\prime }}(s_0{s}_1\cdots s_n{S}^{\omega })$$

$$=$$

$${\mathtt{val}}_{\mathcal{M}}(s_0)\cdot {\mathcal{P}}_{{\mathcal{M}}_{\ast },s_0,{\sigma }^{\prime }}(s_0{s}_1\cdots s_n{S}^{\omega })$$

$$\le$$

$${\mathtt{val}}_{\mathcal{M}}(s_0)\cdot {\mathcal{P}}_{{\mathcal{M}}_{\ast },s_0,{\sigma }^{\prime }}(\mathfrak{R})\le {\mathcal{P}}_{\mathcal{M},s_0,{\sigma }^{\prime }}(\mathfrak{R})$$

$$\displaystyle\big{(}\exists\sigma\in\Sigma.\,{\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s)}\big{)}$$

$${\mathcal{P}}_{\mathcal{M},s,{\sigma }^{\prime }}(\phi )={\mathtt{val}}_{\mathcal{M}}(s)$$

$$Saf{e}_{\mathcal{M}}(\tau ):=\{s\in S\mid {\mathcal{P}}_{\mathcal{M},s,{\sigma }_{opt\text{mathchar}45av}}(\phi )\ge \tau \},$$

$${\tau }_2$$

$$={\mathcal{P}}_{\mathcal{M},s,{\sigma }_{opt\text{mathchar}45av}}(\mathsf{G}[S{]}^{Col=0}\mid \mathsf{G}Safe({\tau }_1))\cdot x$$

$$\text{mbox}+{\mathcal{P}}_{\mathcal{M},s,{\sigma }_{opt\text{mathchar}45av}}(\mathsf{G}[S{]}^{Col=0}\mid \neg \mathsf{G}Safe({\tau }_1))\cdot (1-x)$$

$$\le x+{\tau }_1\cdot (1-x)$$

$$\displaystyle\big{(}\exists\sigma\in\Sigma.\,{\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s)}\big{)}$$

$${\mathcal{P}}_{\mathcal{M},s,{\sigma }^{\prime }}(\phi )={\mathtt{val}}_{\mathcal{M}}(s)$$

$${\mathcal{P}}_{{\mathcal{M}}^{\prime },s_0,{\sigma }_{\delta }^{\prime }}(\phi )$$

$$={\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\phi )$$

$$-{\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))\cdot {\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\phi |\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))$$

$$+{\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))\cdot {\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }^{\prime }}(\phi |\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))$$

$$\ge {\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\phi )$$

$$-{\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))\cdot {\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\phi |\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))$$

$$+{\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))\cdot {\tau }_1$$

$$\ge {\mathtt{val}}_{\mathcal{M}}(s_0)-\delta -{\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{\delta }}(\mathsf{F}Saf{e}_{\mathcal{M}}({\tau }_1))(1-{\tau }_1)$$

$$\ge {\mathtt{val}}_{\mathcal{M}}(s_0)-\delta -{ϵ}_1$$

$${\mathcal{P}}_{\mathcal{M},s,{\sigma }_{opt\text{mathchar}45av}}(\mathsf{G}Safe({\tau }_1))$$

$$=\frac{(1-{ϵ}_1/k)-(1-{ϵ}_1)}{{ϵ}_1}$$

$$=1-\frac{1}{k}.$$

$${\mathcal{P}}_{\mathcal{M},s_0,{\sigma }_{ϵ}}(\phi )$$

$$\bigcap _{k=1}^{\infty }\bigcup _{n=k}^{\infty }{E}_n,$$

$${\mathcal{P}}_{{\mathcal{M}}^{\mathsf{T}},({\mathsf{m}}_0,s_0)}(\mathsf{G}\mathsf{F}(\mathsf{m},s_0)\wedge \mathsf{F}\mathsf{G}[\mathsf{M}\times S{]}^{Col\ne 3})=0.$$

Full text

In finite MDPs there always exist optimal memoryless deterministic (MD) strategies for parity objectives, but this does not generally hold for countably infinite MDPs. In particular, optimal strategies need not exist.

For countable infinite MDPs, we provide a complete picture of the memory requirements of optimal (resp., $\epsilon$-optimal) strategies for all objectives in the Mostowski hierarchy.

In particular, there is a strong dichotomy between two different types of objectives. For the first type, optimal strategies, if they exist, can be chosen MD, while for the second type optimal strategies require infinite memory. (I.e., for all objectives in the Mostowski hierarchy, if finite-memory randomized strategies suffice then also MD-strategies suffice.) Similarly, some objectives admit $\epsilon$-optimal MD-strategies, while for others $\epsilon$-optimal strategies require infinite memory. Such a dichotomy also holds for the subclass of countably infinite MDPs that are finitely branching, though more objectives admit MD-strategies here.

I Introduction

Markov decision processes (MDPs) are a standard model for dynamic systems that exhibit both stochastic and controlled behavior [23]. The system starts in the initial state and makes a sequence of transitions between states. Depending on the type of the current state, either the controller gets to choose an enabled transition (or a distribution over transitions), or the next transition is chosen randomly according to a defined distribution. By fixing a strategy for the controller, one obtains a probability space of plays of the MDP. The goal of the controller is to optimize the expected value of some objective function on the plays of the MDP. The fundamental questions are “what is the optimal value that the controller can achieve?”, “does there exist an optimal strategy, or only $\epsilon$-optimal approximations?”, and “which types of strategies are optimal or $\epsilon$-optimal?”.

Such questions have been studied extensively for finite MDPs (see e.g. [10] for a survey) and also for certain types of countably infinite MDPs [23, 21]. However, the literature on countable MDPs is mainly focused on objective functions defined w.r.t. numeric costs (or rewards) that are assigned to transitions, e.g. (discounted) expected total reward or limit-average reward. In contrast, we study qualitative objectives that are expressed by Parity conditions and which are motived by formal verification questions.

There are works that studied particular classes of countably infinite, but finitely branching, MDPs that arise from models in automata theory [14, 2, 8, 6, 1]. In each of these papers, a crucial part of the analysis is establishing the existence of optimal strategies of particular structure and memory requirements, but none of them looked at proving such properties for general countable MDPs. Countable MDPs also naturally occur in the analysis of queueing systems [17], gambling [4], and branching processes [22], which have multiple applications. They also show up in the analysis of finite-state models, e.g. in two-player stochastic games [24, 13] when reasoning about an optimal strategy against a fixed (randomised and memory-full) strategy of the opponent.

Finite MDPs vs. Infinite MDPs: It should be noted that many standard properties (and proof techniques) of finite MDPs do not carry over to infinite MDPs.

E.g., given some objective, consider the set of all states in an MDP that have nonzero value. If the MDP is finite then this set is finite and thus there exists some minimal nonzero value. This property does not carry over to infinite MDPs. Here the set of states is infinite and the infimum over the nonzero values can be zero. As a consequence, even for a reachability objective, it is possible that all states have value $>0$, but still the value of some states is $<1$. Such phenomena appear already in infinite-state Markov chains like the classic Gambler’s ruin problem with unfair coin tosses in the player’s favor (0.6 win, 0.4 lose). The value, i.e., the probability of ruin, is always $>0$, but still $<1$ in every state except the ruin state itself; cf. [15] (Chapt. 14). Another difference is that optimal strategies need not exist, even for qualitative objectives like reachability or parity. Even if some state has value $1$, there might not be any single strategy that attains the value $1$, but only an infinite family of $\epsilon$-optimal strategies for every $\epsilon>0$.

Parity objectives: We study general countably infinite MDPs with parity objectives. Parity conditions are widely used in temporal logic and formal verification, e.g., they can express $\omega$-regular languages and modal $\mu$-calculus [16]. Every state has a color, out of a finite set of colors encoded as natural numbers. An infinite play is winning iff the highest color that is seen infinitely often in the play is even. The controller wants to maximize the probability of winning plays. Subclasses of parity objectives are defined by restricting the set of used colors; these are classified in the Mostowski hierarchy [20] which includes, e.g., Büchi and co-Büchi objectives. Such prefix-independent infinitary objectives cannot generally be encoded by numeric transition rewards as in [23], though both types subsume the simpler reachability and safety objectives.

There are different types of strategies, depending on whether one can take the whole history of the play into account (history-dependent; (H)), or whether one is limited to a finite amount of memory (finite memory; (F)) or whether decisions are based only on the current state (memoryless; (M)). Moreover, the strategy type depends on whether the controller can randomize (R) or is limited to deterministic choices (D). The simplest type MD refers to memoryless deterministic strategies.

The type of strategy needed for an optimal (resp. $\epsilon$-optimal) strategy for some objective is also called the strategy complexity of the objective. For finite MDPs, MD-strategies are sufficient for all types of qualitative and quantitative parity objectives [9, 11], but the picture is more complex for countably infinite MDPs.

Since optimal strategies need not exist in general, we consider both the strategy complexity of $\epsilon$-optimal strategies, and the strategy complexity of optimal strategies under the assumption that they exist. E.g., if an optimal strategy exists, can it be chosen MD?

We provide a complete picture of the memory requirements for objectives in the Mostowski hierarchy, which is summarized in Figure 1.

In particular, our results show that there is a strong dichotomy between two different classes of objectives. For objectives of the first class, optimal strategies, where they exist, can be chosen MD. For objectives of the second class, optimal strategies require infinite memory in general, in the sense that all FR-strategies achieve the objective only with probability zero. A similar dichotomy applies to $\epsilon$-optimal strategies. For certain objectives, $\epsilon$-optimal MD-strategies exist, while for all others even $\epsilon$-optimal strategies require infinite memory in general. This is a strong dichotomy because there are no objectives in the Mostowski hierarchy for which other types of strategies (MR, FD, or FR) are both necessary and sufficient. Put differently, for all objectives in the Mostowski hierarchy, if FR-strategies suffice then MD-strategies suffice as well.

We also consider the subclass of countable MDPs that are finitely branching. (Note that these generally still have an infinite number of states.) The above mentioned dichotomies apply here as well, though the classes of objectives where optimal (resp. $\epsilon$-optimal) strategies can be chosen MD are larger than for general countable MDPs.

Outline of the results: In Section II we define countably infinite MDPs, strategies and parity objectives. In Section III we show examples that demonstrate that certain objectives require infinite memory. For some of these we refer to previous work. The main new result in this section is Theorem 1 that shows that even almost-sure ${\{1,2,3\}}\text{-}\mathtt{Parity}$ on finitely branching MDPs requires infinite memory. These negative results highlight the questions which other objectives still allow MD-strategies. Apart from the case of reachability objectives, these questions were open. We provide complete answers in several steps. First, in Section IV, we prove a general result (Theorem 5) that relates the strategy complexity of almost-sure winning strategies and optimal strategies. The complexity of the proof is due to the fact that we consider infinite MDPs (which do not satisfy basic properties of finite MDPs in general; see above). We then use this theorem to establish MD-strategies for Büchi, co-Büchi and ${\{0,1,2\}}\text{-}\mathtt{Parity}$ objectives in the following sections. In Section V we show that optimal strategies for Büchi objectives, where they exist, can be chosen MD, even for infinitely branching MDPs. In Section VI we consider finitely branching MDPs. We show that optimal strategies for ${\{0,1,2\}}\text{-}\mathtt{Parity}$, where they exist, can be chosen MD (Theorem 16). This is a very general result. E.g., this question had been open (and is non-trivial) even for almost-sure co-Büchi objectives. Moreover, we show that $\epsilon$-optimal strategies for co-Büchi objectives can be chosen MD (Theorem 19). We conclude the paper with a discussion of how some results change when one considers uncountable MDPs.

II Preliminaries

A probability distribution over a countable (not necessarily finite) set $S$ is a function $f:S\to[0,1]$ s.t. $\sum_{s\in S}f(s)=1$. We use ${\sf supp}(f)=\{s\in S\mid f(s)>0\}$ to denote the support of $f$. Let $\mathcal{D}(S)$ be the set of all probability distributions over $S$.

We consider countably infinite Markov decision processes (MDPs) ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ where the countable set $S$ of states is partitioned into the set $S_{\Box}$ of states of the player and random states $S_{\scriptscriptstyle\bigcirc}$. The relation $\mathord{{\longrightarrow}}\subseteq S\times S$ is the transition relation. We write $s{\longrightarrow}{}s^{\prime}$ if $(s,s^{\prime})\in{\longrightarrow}$, and we assume that each state $s$ has a successor state $s^{\prime}$ with $s{\longrightarrow}s^{\prime}$. The probability function $P:S_{\scriptscriptstyle\bigcirc}\to\mathcal{D}(S)$ assigns to each random state $s\in S_{\scriptscriptstyle\bigcirc}$ a probability distribution over its successor states. A set $T\subseteq S$ is a sink in ${\mathcal{M}}$ if for all $s\in T$ all successors of $s$ are in $T$. The MDP ${\mathcal{M}}$ is called finitely branching if each state has only finitely many successors; otherwise, it is infinitely branching. A Markov chain is an MDP where $S_{\Box}=\emptyset$, i.e., all states are random states.

We describe the behavior of an MDP as a one-player stochastic game played for infinitely many rounds. The game starts in a given initial state $s_{0}$. In each round, if the game is in state $s\in S_{\Box}$ then the player (or controller) chooses a successor state $s^{\prime}$ with $s{\longrightarrow}{}s^{\prime}$; otherwise the game is in a random state $s\in S_{\scriptscriptstyle\bigcirc}$ and proceeds randomly to $s^{\prime}$ with probability $P(s)(s^{\prime})$.

Strategies. A play $w$ is an infinite sequence $s_{0}s_{1}\cdots$ of states such that $s_{i}{\longrightarrow}{}s_{i+1}$ for all $i\geq 0$; let $w(i)=s_{i}$ denote the $i$-th state along $w$. A partial play is a finite prefix of a play. We say that (partial) play $w$ visits $s$ if $s=w(i)$ for some $i$, and that $w$ starts in $s$ if $s=w(0)$. A strategy is a function $\sigma:S^{*}S_{\Box}\to\mathcal{D}(S)$ that assigns to partial plays $ws\in S^{*}S_{\Box}$ a distribution over the successors $\{s^{\prime}\in S\mid s{\longrightarrow}{}s^{\prime}\}$. The set of all strategies in ${\mathcal{M}}$ is denoted by $\Sigma_{\mathcal{M}}$ (we omit the subscript and write $\Sigma$ if ${\mathcal{M}}$ is clear). A (partial) play $s_{0}s_{1}\cdots$ is induced by strategy $\sigma$ if $s_{i+1}\in{\sf supp}(\sigma(s_{0}s_{1}\cdots s_{i}))$ for all $i$ with $s_{i}\in S_{\Box}$, and $s_{i+1}\in{\sf supp}(P(s_{i}))$ for all $i$ with  $s_{i}\in S_{\scriptscriptstyle\bigcirc}$.

Since this paper focuses on the memory requirements of strategies, we present an equivalent formulation of strategies, emphasizing the amount of memory required to implement a strategy. Strategies can be implemented by probabilistic transducers ${\sf T}=({\sf M},{\sf m}_{0},\pi_{u},\pi_{s})$ where ${\sf M}$ is a countable set (the memory of the strategy), ${\sf m}_{0}\in{\sf M}$ is the initial memory mode and $S$ is the input and output alphabet. The probabilistic transition function $\pi_{u}:{\sf M}\times S\to\mathcal{D}({\sf M})$ updates the memory mode of transducer. The probabilistic successor function $\pi_{s}:{\sf M}\times S_{\Box}\to\mathcal{D}(S)$ outputs the next successor, where $s^{\prime}\in{\sf supp}(\pi_{s}({\sf m},s))$ implies $s{\longrightarrow}{}s^{\prime}$. We extend $\pi_{u}$ to $\mathcal{D}({\sf M})\times S\to\mathcal{D}({\sf M})$ and $\pi_{s}$ to $\mathcal{D}({\sf M})\times S_{\Box}\to\mathcal{D}(S)$, in the natural way. Moreover, we extend $\pi_{u}$ to paths by $\pi_{u}({\sf m},\varepsilon)={\sf m}$ and $\pi_{u}({\sf m},s_{0}\cdots s_{n})=\pi_{u}(\pi_{u}(s_{0}\cdots s_{n-1},{\sf m}),s_{n})$. The strategy $\sigma_{{\sf T}}:S^{*}S_{\Box}\to\mathcal{D}(S)$ induced by the transducer ${\sf T}$ is given by $\sigma_{{\sf T}}(s_{0}\cdots s_{n}):=\pi_{s}(s_{n},\pi_{u}(s_{0}\cdots s_{n-1},{\sf m}_{0}))$. Note that such strategies allow for randomized memory updates and probabilistic successor functions.

Strategies are in general history dependent (H) and randomized (R). An H-strategy $\sigma$ is finite memory (F) if there exists some transducer ${\sf T}$ with memory ${\sf M}$ such that $\sigma_{{\sf T}}=\sigma$ and $\lvert{\sf M}\rvert<\infty$; otherwise we say $\sigma$ requires infinite memory. An F-strategy is memoryless (M) (also called positional) if $\lvert{\sf M}\rvert=1$. We may view M-strategies as functions $\sigma:S_{\Box}\to\mathcal{D}(S)$. An R-strategy $\sigma$ is deterministic (D) if $\pi_{u}$ and $\pi_{s}$ map to Dirac distributions; it implies that $\sigma(w)$ is a Dirac distribution for all partial plays $w$. All combinations of the properties in $\{\text{M},\text{F},\text{H}\}\times\{\text{D},\text{R}\}$ are possible, e.g., MD stands for memoryless deterministic. HR strategies are the most general type.

Probability Measures. An MDP ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$, an initial state $s_{0}$, and a strategy $\sigma$ induce a standard probability measure on sets of infinite plays. We write ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({{\mathfrak{R}}})$ for the probability of a measurable set ${\mathfrak{R}}\subseteq s_{0}S^{\omega}$ of plays starting from $s_{0}$. It is defined, as usual, by first defining it on the cylinders $s_{0}s_{1}\ldots s_{n}S^{\omega}$, where $s_{1},\ldots,s_{n}\in S$: if $s_{0}s_{1}\ldots s_{n}$ is not a partial play induced by $\sigma$ then set ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(s_{0}s_{1}\ldots s_{n}S^{\omega})=0$; otherwise set ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(s_{0}s_{1}\ldots s_{n}S^{\omega})=\prod_{i=0}^{n-1}\bar{\sigma}(s_{0}s_{1}\ldots s_{i})(s_{i+1})$, where $\bar{\sigma}$ is the map that extends $\sigma$ by $\bar{\sigma}(ws)=P(s)$ for any $ws\in S^{*}S_{\scriptscriptstyle\bigcirc}$. Using Carathéodory’s extension theorem [5], this defines a unique probability measure ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}$ on measurable subsets of $s_{0}S^{\omega}$.

Objectives. Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be an MDP. The objective of the player is determined by a predicate on infinite plays. We assume familiarity with the syntax and semantics of the temporal logic LTL [12]. Formulas are interpreted on the structure $(S,{\longrightarrow})$. We use $\llbracket{\varphi}\rrbracket^{s}\subseteq sS^{\omega}$ to denote the set of plays starting from $s$ that satisfy the LTL formula ${\varphi}$. This set is measurable [25], and we just write ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})$ instead of ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}(\llbracket{\varphi}\rrbracket^{s})$. We also write $\llbracket{\varphi}\rrbracket$ for $\bigcup_{s\in S}\llbracket{\varphi}\rrbracket^{s}$.

Given a target set $T\subseteq S$, the reachability objective is defined by $\mathtt{Reach}(T)=\llbracket{\sf F}\,T\rrbracket$, i.e., $s_{0}s_{1}\cdots\in\mathtt{Reach}(T)\,\Leftrightarrow\,\exists i.\,s_{i}\in T$. The safety objective is defined by $\mathtt{Safety}(T)=\llbracket{\sf G}\,\neg T\rrbracket$, i.e., $s_{0}s_{1}\cdots\in\mathtt{Safety}(T)\,\Leftrightarrow\,\forall i.\,s_{i}\not\in T$. Given a reachability or a safety objective, we can assume without loss of generality that $T$ is a sink in ${\mathcal{M}}$.

Let ${\mathcal{C}}\subseteq\mathbb{N}$ be a finite set of colors. A color function ${\mathit{C}ol}:S\to{\mathcal{C}}$ assigns to each state $s$ its color ${\mathit{C}ol}({s})$. For $n\in\mathbb{N}$, $\mathord{\rhd}\in\{\mathord{<},\mathord{\leq},\mathord{=},\mathord{\geq},\mathord{>}\}$ and $Q\subseteq S$, let $[Q]^{{\mathit{C}ol}\rhd n}:=\{{s\in Q}\mid{{\mathit{C}ol}({s})\rhd n}\}$ be the set of states in $Q$ with color $\rhd n$. The parity objective is defined by

[TABLE]

i.e., $\mathtt{Parity}({\mathit{C}ol})$ is the set of infinite plays such that the largest color that occurs infinitely often along the play is even.

The Mostowski hierarchy [20] classifies parity objectives by restricting the range of the function ${\mathit{C}ol}$ to a set of colors ${\mathcal{C}}\subseteq\mathbb{N}$. We write ${{\mathcal{C}}}\text{-}\mathtt{Parity}$ for such restricted parity objectives. In particular, Büchi objectives correspond to ${\{1,2\}}\text{-}\mathtt{Parity}$, and co-Büchi objectives correspond to ${\{0,1\}}\text{-}\mathtt{Parity}$. The objectives ${\{0,1,2\}}\text{-}\mathtt{Parity}$ and ${\{1,2,3\}}\text{-}\mathtt{Parity}$ are incomparable, but they both subsume (modulo renaming of colors) Büchi and co-Büchi objectives. Moreover, both ${\{0,1\}}\text{-}\mathtt{Parity}$ and ${\{1,2\}}\text{-}\mathtt{Parity}$ subsume the reachability objective $\mathtt{Reach}(T)$ (for MDPs with a sink $T$), by defining the color function so that ${\mathit{C}ol}(s)=1\,\Leftrightarrow\,s\not\in T$. Similarly, both ${\{0,1\}}\text{-}\mathtt{Parity}$ and ${\{1,2\}}\text{-}\mathtt{Parity}$ subsume $\mathtt{Safety}(T)$, by defining ${\mathit{C}ol}(s)=1\,\Leftrightarrow\,s\in T$.

Optimal and $\epsilon$-Optimal Strategies. Given an objective ${\varphi}$, the value of state $s$ in an MDP ${\mathcal{M}}$, denoted by ${\mathtt{val}_{{\mathcal{M}}}(s)}$, is the supremum probability of achieving ${\varphi}$, i.e., ${\mathtt{val}_{{\mathcal{M}}}(s)}:=\sup_{\sigma\in\Sigma}{\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})$. For $\epsilon\geq 0$ and $s\in S$, we say that a strategy $\sigma$ is $\epsilon$-optimal iff ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}}(s)}-\epsilon$. A [math]-optimal strategy is called optimal. An optimal strategy is almost-surely winning if ${\mathtt{val}_{{\mathcal{M}}}(s)}=1$. Unlike in finite-state MDPs, optimal strategies need not exist in countable MDPs, not even for reachability objectives in finitely branching MDPs. However, by the definition of the value, for all $\epsilon>0$, an $\epsilon$-optimal strategy exists.

For an objective ${\varphi}$ and $\rhd\in\{\geq,>\}$ and $c\in[0,1]$, we define \big{[}{\varphi}\big{]}^{{\rhd c}} as the set of states $s$ for which there exists a strategy $\sigma$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})\rhd c$. We call a state $s$ almost-surely winning if s\in\big{[}{\varphi}\big{]}^{{\geq 1}}, and we call $s$ limit-surely winning if s\in\big{[}{\varphi}\big{]}^{{\geq c}} for every constant $c<1$ (which is iff ${\mathtt{val}_{{\mathcal{M}}}(s)}=1$). On infinite arenas, limit-surely winning states are not necessarily almost-surely winning.

III Objectives that require infinite memory

In this section we consider those objectives in the Mostowski hierarchy where optimal (resp., $\epsilon$-optimal) strategies require infinite memory. In each such case we construct an MDP that witnesses this requirement. In these MDPs, all FR-strategies achieve the objective only with probability [math], while some HD-strategy achieves the objective almost-surely (resp., with arbitrarily high probability).

Theorem 1**.**

Let ${\varphi}={\{1,2,3\}}\text{-}\mathtt{Parity}$. There exists a finitely branching MDP ${\mathcal{M}}$ with initial state $s_{0}$ such that

• •

for all FR-strategies $\sigma$, we have ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=0$,

• •

there exists an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$.

Hence, optimal (and even almost-surely winning) and $\epsilon$-optimal strategies require infinite memory for ${\{1,2,3\}}\text{-}\mathtt{Parity}$, even in finitely branching MDPs.

The MDP in Theorem 1 is depicted in Figure 2 (left), where ${\mathit{C}ol}(s_{i})=1$ and ${\mathit{C}ol}(r_{i})=2$ for all $i\in\mathbb{N}$, and ${\mathit{C}ol}(t)=3$. For every FR-strategy there is a uniform lower bound on the probability of visiting $t$ between consecutive visits to $s_{0}$. Hence, unless the strategy with positive probability eventually always stays in states $s_{i}$ (and thus also loses the almost-sure parity objective), in the long-run, the probability of visiting $t$ (with color three) tends to $1$, and the parity condition is satisfied with probability [math]. Although the player cannot win by any FR-strategy, we construct an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$. This strategy is such that upon the $i^{\text{th}}$ visit to $s_{0}$, the ladder $s_{0}s_{1}\cdots s_{i}$ is traversed and the transition $s_{i}{\longrightarrow}r_{i}$ is chosen. Moving further along the ladder $s_{0}s_{1}s_{2}\cdots$ decreases the probability of visiting $t$ between the previous and successive visits to $s_{0}$. Hence, the probability of visiting color three infinitely often is [math].

Remark 1**.**

A strict subclass of finitely branching MDPs are $1$-counter MDPs, where a finite-state MDP is augmented with an integer counter [6]. The MDP in Theorem 1 (plus some auxiliary states) is implementable by a $1$-counter MDP.

Remark 2**.**

The classical Rabin and Streett conditions can encode ${\{1,2,3\}}\text{-}\mathtt{Parity}$. Thus, optimal and $\epsilon$-optimal strategies for Rabin/Streett require infinite memory, even in finitely branching countable MDPs.

On finite MDPs, optimal strategies can be chosen MD for parity and Rabin objectives, but not for Streett objectives. Optimal strategies for Streett objectives can be chosen MR or FD [9].

Proof.

For an infinite play $\pi^{\infty}$, let ${\sf Inf}(\pi^{\infty})$ be the set of states that $\pi^{\infty}$ visits infinitely often. Let us recall the Rabin and Streett conditions.

Given a Rabin condition $\{(E_{1},F_{1}),(E_{2},F_{2}),\cdots,(E_{n},F_{n})\}$ with $n$ pairs (or $n$ disjunctions), an infinite play $\pi^{\infty}$ satisfies the Rabin condition if there exists a pair $(E_{i},F_{i})$ such that ${\sf Inf}(\pi^{\infty})\cap E_{i}=\emptyset$ and ${\sf Inf}(\pi^{\infty})\cap F_{i}\neq\emptyset$. The Rabin condition

[TABLE]

encodes ${\{1,2,3\}}\text{-}\mathtt{Parity}$, since all satisfying runs must visit states with color $2$ infinitely often and states with color $3$ only finitely often. Note that ${\{1,2,3\}}\text{-}\mathtt{Parity}$ is encoded in a Rabin condition with only one disjunction.

Given a Streett condition $\{(E_{1},F_{1}),(E_{2},F_{2}),\cdots,(E_{n},F_{n})\}$ with $n$ pairs (or $n$ conjunctions), an infinite play $\pi^{\infty}$ satisfies the Streett condition if ${\sf Inf}(\pi^{\infty})\cap E_{i}=\emptyset$ implies ${\sf Inf}(\pi^{\infty})\cap F_{i}=\emptyset$ for all pairs $(E_{i},F_{i})$. The Streett condition

[TABLE]

encodes ${\{1,2,3\}}\text{-}\mathtt{Parity}$, since all satisfying runs must visit states with color $2$ infinitely often and states with color $3$ only finitely often.

Note that a conjunction of two Streett pairs are needed to encode ${\{1,2,3\}}\text{-}\mathtt{Parity}$. A single Streett pair $\{(X,Y)\}$ means “infinitely often $X$ or only finitely often $Y$”, which can be encoded as a ${\{0,1,2\}}\text{-}\mathtt{Parity}$ condition by assigning color $2$ to $X$ and color $1$ to $Y$. Unlike for ${\{1,2,3\}}\text{-}\mathtt{Parity}$, optimal strategies for ${\{0,1,2\}}\text{-}\mathtt{Parity}$ (and thus also for a single Streett pair) can be chosen MD in finitely branching MDPs (Theorem 16). ∎

It was known that quantitative Büchi objectives require infinite memory [18, 2]. For the sake of completeness, we present an example MDP for Proposition 2 in Figure 2 (right).

Proposition 2** ([18]).**

Let ${\varphi}={\{1,2\}}\text{-}\mathtt{Parity}$ be the Büchi objective. There exists a finitely branching MDP ${\mathcal{M}}$ with initial state $s_{0}$ such that

• •

for all FR-strategies $\sigma$, we have ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=0$,

• •

for every $c\in[0,1)$, there exists an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})\geq c$.

*Hence, $\epsilon$-optimal strategies for Büchi objectives require infinite memory. *

Theorem 3**.**

Let ${\varphi}=\mathtt{Safety}(T)$. There exists an infinitely branching MDP ${\mathcal{M}}$ with initial state $s$ such that

• •

for all FR-strategies $\sigma$, we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=0$,

• •

for every $c\in[0,1)$, there exists an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})\geq c$.

Hence, $\epsilon$-optimal strategies for safety require infinite memory.

The MDP in Theorem 3, depicted in Figure 3 (left), was first introduced in [19]. Since our notion of finite-memory strategies allows for randomized memory updates (in contrast to [19]), our proof is somewhat more general. The target is $T=\{t\}$. For every FR-strategy there is a uniform lower bound on the probability of reaching $t$ between consecutive visits to $s_{0}$. Since $t$ is absorbing, it will be reached with probability $1$. Thus every FR-strategy satisfies the safety objective with probability [math]. However, for all $n\in\mathbb{N}$, we construct an HD-strategy $\sigma_{n}$ such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{n}}(\mathtt{Safety}(\{t\}))\geq 1-\frac{1}{2^{n}}$. This strategy is such that upon the $i^{\text{th}}$ visit to $s$, the transition $s{\longrightarrow}r_{i+n}$ is chosen. Hence, the probability of visiting $t$ between two successive visits to $s$ decreases. A more detailed analysis shows that the probability of ever visiting $t$ is bounded by $\frac{1}{2^{n}}$.

Theorem 4**.**

Let ${\varphi}={\{0,1\}}\text{-}\mathtt{Parity}$ be the co-Büchi objective. There exists an infinitely branching MDP ${\mathcal{M}}$ with initial state $s$ such that

• •

for all FR-strategies $\sigma$, we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=0$,

• •

there exists an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$.

Hence, optimal (and even almost-surely winning) strategies and $\epsilon$-optimal strategies for co-Büchi require infinite memory.

The MDP in Theorem 4 is depicted in Figure 3 (right). By a similar argument as in Theorem 3, every FR-strategy achieves co-Büchi with probability [math]. However, the HD-strategy $\sigma$ that chooses the transition $s{\longrightarrow}r_{i}$ upon the $i^{\text{th}}$ visit to $s$ is such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$.

IV From almost-sure winning to optimal strategies

In this section we prove Theorem 5. It says that, for certain objectives, if almost-surely winning strategies (where they exist) can be chosen MD, then optimal strategies (where they exist) can also be chosen MD.

We call a class ${\mathcal{C}}$ of MDPs downward-closed if every MDP whose transition relation is a subset of the transition relation of some MDP in ${\mathcal{C}}$ is also in ${\mathcal{C}}$. The class of finitely branching MDPs is downward-closed, and so is the class of MDPs with a fixed sink $T$.

We call an objective ${\varphi}$ prefix-independent in ${\mathcal{C}}$ (where ${\mathcal{C}}$ is a class of MDPs) if for all $w_{1},w_{2}\in S^{*}$ and all $w\in S^{\omega}$ such that $w_{1}w$ and $w_{2}w$ are infinite plays in an MDP in ${\mathcal{C}}$ we have $w_{1}w\in\llbracket{\varphi}\rrbracket\Longleftrightarrow w_{2}w\in\llbracket{\varphi}\rrbracket$. Parity objectives are prefix-independent in the class of all MDPs. Both objectives $\mathtt{Reach}(T)$ and $\mathtt{Safety}(T)$ are prefix-independent in the class of MDPs with sink $T$.

The following theorem provides, under certain conditions, an optimal MD-strategy for all states that have an optimal strategy. In fact, a single MD-strategy is optimal for all states that have an optimal strategy:

Theorem 5**.**

Let ${\varphi}$ be an objective that is prefix-independent in a downward-closed class ${\mathcal{C}}$ of MDPs. Suppose that for any ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)\in{\mathcal{C}}$ and any $s\in S$ and any strategy $\sigma$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$ there exists an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$.

Under this condition, for each ${\mathcal{M}}\in{\mathcal{C}}$ there is an MD-strategy $\sigma^{\prime}$ such that for all $s\in S$:

[TABLE]

The remainder of the section is devoted to the proof of Theorem 5.

For prefix-independent winning conditions, whenever an optimal strategy visits some state, it achieves the value of this state; see Lemma 20 in the appendix. We use this to show that the MDP constructed in the following lemma is well-defined. This MDP, ${\mathcal{M}}_{*}$, will be crucial for the proof of Theorem 5. Loosely speaking, ${\mathcal{M}}_{*}$ is the MDP ${\mathcal{M}}$ conditioned under ${\varphi}$.

Lemma 6**.**

Let ${\varphi}$ be an objective that is prefix-independent in a class ${\mathcal{C}}$ of MDPs. Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)\in{\mathcal{C}}$. Construct an MDP ${\mathcal{M}}_{*}=(S_{*},S_{*\Box},S_{*{\scriptscriptstyle\bigcirc}},{\longrightarrow}_{*},P_{*})$ by setting

[TABLE]

and $S_{*\Box}=S_{*}\cap S_{\Box}$ and $S_{*{\scriptscriptstyle\bigcirc}}=S_{*}\cap S_{\scriptscriptstyle\bigcirc}$ and

[TABLE]

and $P_{*}:S_{*{\scriptscriptstyle\bigcirc}}\to\mathcal{D}(S_{*})$ so that

[TABLE]

for all $s\in S_{*{\scriptscriptstyle\bigcirc}}$ and $t\in S_{*}$ with $s\,{\longrightarrow}_{*}\,t$. Then:

For all $\sigma\in\Sigma_{{\mathcal{M}}_{*}}$ and all $n\geq 0$ and all $s_{0},\ldots,s_{n}\in S_{*}$ with $s_{0}{\longrightarrow}_{*}\,s_{1}{\longrightarrow}_{*}\,\cdots{\longrightarrow}_{*}\,s_{n}$:

[TABLE] 2. 2.

For all $s_{0}\in S_{*}$ and all $\sigma\in\Sigma_{{\mathcal{M}}}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s_{0})}>0$ and all measurable ${\mathfrak{R}}\subseteq s_{0}S^{\omega}$ we have ${\mathcal{P}}_{{\mathcal{M}}_{*},s_{0},\sigma}({\mathfrak{R}})={\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\mathfrak{R}}\mid\llbracket{\varphi}\rrbracket^{s_{0}})$.

The following lemma provides, under certain conditions, a uniform almost-surely winning MD-strategy, i.e., one that works for all initial states at the same time:

Lemma 7**.**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be an MDP. Let ${\varphi}$ be an objective that is prefix-independent in $\{{\mathcal{M}}\}$. Suppose that for any $s\in S$ and any strategy $\sigma$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$ there exists an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$. Then there is an MD-strategy $\sigma^{\prime}$ such that for all $s\in S$:

[TABLE]

Proof.

We can assume that all states are almost-surely winning, since in order to achieve an almost-sure winning objective, the player must forever remain in almost-surely winning states. So we need to define an MD-strategy $\sigma^{\prime}$ so that for all $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$.

Fix an arbitrary state $s_{1}\in S$. By assumption there is an MD-strategy $\sigma_{1}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{1},\sigma_{1}}({\varphi})=1$. Let $U_{1}\subseteq S$ be the set of states that occur in plays that both start from $s_{1}$ and are induced by $\sigma_{1}$. We have ${\mathcal{P}}_{{\mathcal{M}},s_{1},\sigma_{1}}(\llbracket{\varphi}\rrbracket^{s_{1}}\cap U_{1}^{\omega})=1$. In fact, for any $s\in U_{1}$ and any strategy $\sigma$ that agrees with $\sigma_{1}$ on $U_{1}$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}(\llbracket{\varphi}\rrbracket^{s}\cap U_{1}^{\omega})=1$.

If $U_{1}=S$ we are done. Otherwise, consider the MDP ${\mathcal{M}}_{1}$ obtained from ${\mathcal{M}}$ by fixing $\sigma_{1}$ on $U_{1}$ (i.e., in ${\mathcal{M}}_{1}$ we can view the states in $U_{1}$ as random states). We argue that, in ${\mathcal{M}}_{1}$, for any state $s$ there is an MD-strategy $\sigma_{1}^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}}_{1},s,\sigma_{1}^{\prime}}({\varphi})=1$. Indeed, let $s\in S$ be any state. Recall that there is an MD-strategy $\sigma$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$. Let $\sigma_{1}^{\prime}$ be the MD-strategy obtained by restricting $\sigma$ to the non-$U_{1}$ states (recall that the $U_{1}$ states are random states in ${\mathcal{M}}_{1}$). This strategy $\sigma_{1}^{\prime}$ almost surely generates a play that either satisfies ${\varphi}$ without ever entering $U_{1}$ or at some point enters $U_{1}$. In the latter case, ${\varphi}$ is satisfied almost surely: this follows from prefix-independence and the fact that $\sigma_{1}^{\prime}$ agrees with $\sigma_{1}$ on $U_{1}$. We conclude that ${\mathcal{P}}_{{\mathcal{M}}_{1},s,\sigma_{1}^{\prime}}({\varphi})=1$.

Let $s_{2}\in S\setminus U_{1}$. We repeat the argument from above, with $s_{2}$ instead of $s_{1}$, and with ${\mathcal{M}}_{1}$ instead of ${\mathcal{M}}$. This yields an MD-strategy $\sigma_{2}$ and a set $U_{2}\ni s_{2}$ with ${\mathcal{P}}_{{\mathcal{M}}_{1},s_{2},\sigma_{2}}(\llbracket{\varphi}\rrbracket^{s_{2}}\cap U_{2}^{\omega})=1$. In fact, for any $s\in U_{2}$ and any strategy $\sigma$ that agrees with $\sigma_{2}$ on $U_{2}$ and with $\sigma_{1}$ on $U_{1}$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}(\llbracket{\varphi}\rrbracket^{s}\cap U_{2}^{\omega})=1$.

If $U_{1}\cup U_{2}=S$ we are done. Otherwise we continue in the same manner, and so forth. Since $S$ is countable, we can pick $s_{1},s_{2},\ldots$ to have $\bigcup_{i\geq 1}U_{i}=S$. Define an MD-strategy $\sigma^{\prime}$ such that for any $s\in S_{\Box}$ we have $\sigma^{\prime}(s)=\sigma_{i}(s)$ for the smallest $i$ with $s\in U_{i}$. Thus, if $s\in U_{i}$, we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})\geq{\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}(\llbracket{\varphi}\rrbracket^{s}\cap U_{i}^{\omega})=1$. ∎

The following measure-theoretic lemma will be used to connect probability measures induced by the MDPs ${\mathcal{M}}$ and ${\mathcal{M}}_{*}$ from Lemma 6.

Lemma 8**.**

Let $S$ be countable and $s\in S$. Call a set of the form $swS^{\omega}$ for $w\in S^{*}$ a cylinder. Let ${\mathcal{P}},{\mathcal{P}}^{\prime}$ be probability measures on $sS^{\omega}$ defined in the standard way, i.e., first on cylinders and then extended to all measurable sets ${\mathfrak{R}}\subseteq sS^{\omega}$. Suppose there is $x\geq 0$ such that $x\cdot{\mathcal{P}}(\mathfrak{C})\leq{\mathcal{P}}^{\prime}(\mathfrak{C})$ for all cylinders $\mathfrak{C}$. Then $x\cdot{\mathcal{P}}({\mathfrak{R}})\leq{\mathcal{P}}^{\prime}({\mathfrak{R}})$ holds for all measurable ${\mathfrak{R}}\subseteq sS^{\omega}$.

We are ready to prove Theorem 5.

Proof of Theorem 5.

As in the statement of the theorem, suppose that ${\varphi}$ is an objective that is prefix-independent in a downward-closed class ${\mathcal{C}}$ of MDPs so that for any ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)\in{\mathcal{C}}$ and any $s\in S$ and any strategy $\sigma$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$ there exists an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$. Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)\in{\mathcal{C}}$. Let ${\mathcal{M}}_{*}=(S_{*},S_{*\Box},S_{*{\scriptscriptstyle\bigcirc}},{\longrightarrow}_{*},P_{*})$ be the MDP defined in Lemma 6. Since ${\mathcal{C}}$ is downward-closed, we have ${\mathcal{M}}_{*}\in{\mathcal{C}}$. In particular, ${\varphi}$ is prefix-independent in $\{{\mathcal{M}}_{*}\}$.

First we show that for any $s\in S_{*}$ there exists an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}}_{*},s,\sigma^{\prime}}({\varphi})=1$. Indeed, let $s\in S_{*}$. By the definition of $S_{*}$, there is a strategy $\sigma$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s)}>0$. By Lemma 6.2, we have ${\mathcal{P}}_{{\mathcal{M}}_{*},s,\sigma}({\varphi})=1$. By our assumption on ${\mathcal{C}}$ there exists an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}}_{*},s,\sigma^{\prime}}({\varphi})=1$.

By Lemma 7, it follows that there is an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}}_{*},s,\sigma^{\prime}}({\varphi})=1$ for all $s\in S_{*}$. We show that this strategy $\sigma^{\prime}$ satisfies the property claimed in the statement of the theorem.

To this end, let $n\geq 0$ and $s_{0},s_{1},\ldots,s_{n}\in S$. If $s_{0}s_{1}\cdots s_{n}$ is a partial play in ${\mathcal{M}}_{*}$ then, by Lemma 6.1,

[TABLE]

If $s_{0}s_{1}\cdots s_{n}$ is not a partial play in ${\mathcal{M}}_{*}$ then ${\mathcal{P}}_{{\mathcal{M}}_{*},s_{0},\sigma^{\prime}}(s_{0}s_{1}\cdots s_{n}S^{\omega})=0$ and the previous inequality holds as well. Therefore, by Lemma 8, we get for all measurable sets ${\mathfrak{R}}\subseteq s_{0}S^{\omega}$:

[TABLE]

In particular, since ${\mathcal{P}}_{{\mathcal{M}}_{*},s_{0},\sigma^{\prime}}({\varphi})=1$, we obtain ${\mathtt{val}_{{\mathcal{M}}}(s_{0})}\leq{\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma^{\prime}}({\varphi})$. The converse inequality ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma^{\prime}}({\varphi})\leq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}$ holds by the definition of ${\mathtt{val}_{{\mathcal{M}}}(s_{0})}$, hence we conclude ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma^{\prime}}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s_{0})}$. ∎

V When MD-strategies suffice in general countable MDPs

Ornstein [21] shows that $\epsilon$-optimal and optimal strategies for reachability can be chosen MD:

Theorem 9** (from Theorem B in [21]).**

For every countable MDP ${\mathcal{M}}$ there exist uniform $\epsilon$-optimal MD-strategies for reachability objectives ${\varphi}=\mathtt{Reach}(T)$, i.e., for every $\epsilon>0$ there is an MD-strategy $\sigma_{\epsilon}$ such that for all $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\epsilon}}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}}(s)}-\epsilon$.

Theorem 10** (follows from Proposition B in [21]).**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be an MDP, and ${\varphi}=\mathtt{Reach}(T)$. Let $s_{0}\in S$ and $\sigma$ be a strategy with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$. Then there is an MD-strategy $\hat{\sigma}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\hat{\sigma}}({\varphi})=1$.

Both theorems are due to [21]; we give an alternative proof of Theorem 10 in the appendix. We generalize Theorem 10 to Büchi objectives, using the principle that Büchi is repeated reachability:

Proposition 11**.**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be an MDP, and $s_{0}\in S$, and $\sigma$ a strategy, and ${\mathit{C}ol}:S\to\{1,2\}$, and ${\varphi}=\mathtt{Parity}({\mathit{C}ol})$. Suppose ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$. Then there is an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma^{\prime}}({\varphi})=1$.

By appealing to Theorem 5 it follows:

Theorem 12**.**

Let ${\mathcal{M}}$ be an MDP, ${\mathit{C}ol}:S\to\{1,2\}$, and ${\varphi}=\mathtt{Parity}({\mathit{C}ol})$ be a Büchi-objective (subsuming reachability and safety). Then there exists an MD-strategy $\sigma^{\prime}$ that is optimal for all states that have an optimal strategy:

[TABLE]

VI When MD-strategies suffice in finitely branching MDPs

In this section we prove that optimal strategies for ${\{0,1,2\}}\text{-}\mathtt{Parity}$, where they exist, can be chosen MD (Theorem 16) and that $\epsilon$-optimal strategies for co-Büchi objectives can be chosen MD (Theorem 19). To prepare the ground for these results, we first consider safety objectives.

VI-A Optimal MD-strategies for Safety

The following proposition asserts in particular that for safety in finitely branching MDPs, there is no need for merely $\epsilon$-optimal strategies, as there always exists an optimal MD-strategy.

Proposition 13** (from Theorem 7.3.6(a) in [23]).**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, and $T\subseteq S$, and ${\varphi}=\mathtt{Safety}(T)$. Define an MD-strategy $\sigma_{\mathit{opt\mathchar 45\relax av}}$ (for “optimal avoiding”) that, in each state $s$, picks a successor state with the largest value ${\mathtt{val}_{{\mathcal{M}}}(s)}=\sup_{\sigma\in\Sigma}{\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})$. Then for all states $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\mathit{opt\mathchar 45\relax av}}}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s)}$, i.e., $\sigma_{\mathit{opt\mathchar 45\relax av}}$ is uniformly optimal.

Note that, for infinitely branching MDPs, this definition of $\sigma_{\mathit{opt\mathchar 45\relax av}}$ would be unsound, as “the largest value” might not exist.

Definition 1**.**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, ${\mathit{C}ol}:S\to\mathbb{N}$ a color function, ${\varphi}=\mathtt{Safety}([S]^{{\mathit{C}ol}\neq 0})$, $\sigma_{\mathit{opt\mathchar 45\relax av}}$ the strategy from Proposition 13 and $\tau\in[0,1]$. We define

[TABLE]

i.e., ${\it Safe_{{\mathcal{M}}}}(\tau)$ is the set of states from which the player can remain within color-0 states forever with probability $\geq\tau$. We drop the subscript ${\mathcal{M}}$ when the MDP ${\mathcal{M}}$ is understood.

Loosely speaking, the following lemma gives a lower bound on the probability that, starting from a “safe” state, “unsafe” states are forever avoided by $\sigma_{\mathit{opt\mathchar 45\relax av}}$:

Lemma 14**.**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, ${\mathit{C}ol}:S\to\mathbb{N}$ a color function and $\sigma_{\mathit{opt\mathchar 45\relax av}}$ the strategy from Proposition 13. Let $0<\tau_{1}\leq\tau_{2}\leq 1$, and $s\in{\it Safe}(\tau_{2})$. Then ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\mathit{opt\mathchar 45\relax av}}}({\sf G}{\it Safe}(\tau_{1}))\geq\frac{\tau_{2}-\tau_{1}}{1-\tau_{1}}$.

Proof.

We compute probabilities conditioned under the event ${\sf G}{\it Safe}(\tau_{1})$. Since ${\it Safe}(\tau_{1})\subseteq[S]^{{\mathit{C}ol}=0}$, we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\mathit{opt\mathchar 45\relax av}}}({\sf G}[S]^{{\mathit{C}ol}=0}\mid{\sf G}{\it Safe}(\tau_{1}))=1$. From the definition of ${\it Safe}(\tau_{1})$ and the Markov property we get ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\mathit{opt\mathchar 45\relax av}}}({\sf G}[S]^{{\mathit{C}ol}=0}\mid\neg{\sf G}{\it Safe}(\tau_{1}))\leq\tau_{1}$. Applying the law of total probability and writing $x$ for ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\mathit{opt\mathchar 45\relax av}}}({\sf G}{\it Safe}(\tau_{1}))$ we obtain:

[TABLE]

It follows $x\geq\frac{\tau_{2}-\tau_{1}}{1-\tau_{1}}$. ∎

The following lemma states for all $\tau<1$ that eventually remaining in color-0 states but outside ${\it Safe}(\tau)$ has probability zero.

Lemma 15**.**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, and ${\mathit{C}ol}:S\to\mathbb{N}$ a color function. Let $s$ be a state, and $\sigma$ a strategy, and $\tau<1$. Then ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\sf F}{\sf G}\neg{\it Safe}(\tau)\land{\sf F}{\sf G}[S]^{{\mathit{C}ol}=0})=0$.

VI-B Optimal MD-strategies for ${\{0,1,2\}}\text{-}\mathtt{Parity}$

Theorem 16**.**

Let ${\mathcal{M}}$ be a finitely branching MDP, ${\mathit{C}ol}:S\to\{0,1,2\}$, and ${\varphi}=\mathtt{Parity}({\mathit{C}ol})$. Then there exists an MD-strategy $\sigma^{\prime}$ that is optimal for all states that have an optimal strategy:

[TABLE]

By appealing to Theorem 5 it suffices to show:

Proposition 17**.**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, and $s_{0}\in S$, and $\sigma$ a strategy, and ${\mathit{C}ol}:S\to\{0,1,2\}$, and ${\varphi}=\mathtt{Parity}({\mathit{C}ol})$. Suppose ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$. Then there is an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma^{\prime}}({\varphi})=1$.

The following simple lemma provides a scheme for proving almost-sure properties.

Lemma 18**.**

Let ${\mathcal{P}}$ be a probability measure over the sample space $\Omega$. Let $({\mathfrak{R}}_{i})_{i\in I}$ be a countable partition of $\Omega$ in measurable events. Let $E\subseteq\Omega$ be a measurable event. Suppose ${\mathcal{P}}({\mathfrak{R}}_{i}\cap E)={\mathcal{P}}({\mathfrak{R}}_{i})$ holds for all $i\in I$. Then ${\mathcal{P}}(E)=1$.

We are ready to prove Proposition 17.

Proof of Proposition 17.

To achieve an almost-sure winning objective, the player must forever remain in states from which the objective can be achieved almost surely. So we can assume without loss of generality that all states are almost-sure winning, i.e., for all $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$ for some $\sigma$.

We will define an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$ for all $s\in S$. We first define the MD-strategy $\sigma^{\prime}$ partially for the states in ${\it Safe_{{\mathcal{M}}}}(\frac{1}{3})$ and then extend the definition of $\sigma^{\prime}$ to all states. For the states in ${\it Safe_{{\mathcal{M}}}}(\frac{1}{3})$ define $\sigma^{\prime}:=\sigma_{\mathit{opt\mathchar 45\relax av}}$ as in Proposition 13, see Figure 4. Let ${\mathcal{M}}^{\prime}$ be the MDP obtained from ${\mathcal{M}}$ by restricting the transition relation as prescribed by the partial MD-strategy $\sigma^{\prime}$.

For any $\tau\in[0,1]$, we have ${\it Safe_{{\mathcal{M}}}}(\tau)={\it Safe_{{\mathcal{M}}^{\prime}}}(\tau)$. Indeed, since ${\mathcal{M}}^{\prime}$ restricts the options of the player, we have ${\it Safe_{{\mathcal{M}}}}(\tau)\supseteq{\it Safe_{{\mathcal{M}}^{\prime}}}(\tau)$. Conversely, let $s\in{\it Safe_{{\mathcal{M}}}}(\tau)$. The strategy $\sigma_{\mathit{opt\mathchar 45\relax av}}$ from Proposition 13 achieves ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\mathit{opt\mathchar 45\relax av}}}({\sf G}[S]^{{\mathit{C}ol}=0})\geq\tau$. Since $\sigma_{\mathit{opt\mathchar 45\relax av}}$ can be applied in ${\mathcal{M}}^{\prime}$, and results in the same Markov chain as applying it in ${\mathcal{M}}$, we conclude $s\in{\it Safe_{{\mathcal{M}}^{\prime}}}(\tau)$. This justifies to write ${\it Safe}(\tau)$ for ${\it Safe_{{\mathcal{M}}}}(\tau)={\it Safe_{{\mathcal{M}}^{\prime}}}(\tau)$ in the remainder of the proof.

Next we show that, also in ${\mathcal{M}}^{\prime}$, for all states $s\in S$ there exists a strategy $\sigma_{1}$ with ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\varphi})=1$. This strategy $\sigma_{1}$ is defined as follows. First play according to a strategy $\sigma$ from the statement of the theorem. If and when the play visits ${\it Safe}(\frac{1}{3})$, switch to the MD-strategy $\sigma_{\mathit{opt\mathchar 45\relax av}}$ from Proposition 13. If and when the play then visits $[S]^{{\mathit{C}ol}\neq 0}$, switch back to a strategy $\sigma$ from the statement of the theorem, and so forth.

We show that $\sigma_{1}$ achieves ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\varphi})=1$. To this end we will use Lemma 18. We partition the runs of $sS^{\omega}$ in three events ${\mathfrak{R}}_{0},{\mathfrak{R}}_{1},{\mathfrak{R}}_{2}$ as follows:

• •

${\mathfrak{R}}_{0}$ contains the runs where $\sigma_{1}$ switches between $\sigma_{\mathit{opt\mathchar 45\relax av}}$ and $\sigma$ infinitely often.

• •

${\mathfrak{R}}_{1}$ contains the runs where $\sigma_{1}$ eventually only plays according to $\sigma_{\mathit{opt\mathchar 45\relax av}}$.

• •

${\mathfrak{R}}_{2}$ contains the runs where $\sigma_{1}$ eventually only plays according to $\sigma$.

Each time $\sigma_{1}$ switches to $\sigma_{\mathit{opt\mathchar 45\relax av}}$, there is, by Proposition 13, a probability of at least $\frac{1}{3}$ of never visiting a color-$\{1,2\}$ state again and thus of never again switching to $\sigma$. It follows that ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{0})=0$. By the definition of $\sigma_{\mathit{opt\mathchar 45\relax av}}$ we have ${\mathfrak{R}}_{1}\subseteq\llbracket{\sf F}{\sf G}[S]^{{\mathit{C}ol}=0}\rrbracket\subseteq\llbracket{\varphi}\rrbracket$, and hence ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{1}\cap\llbracket{\varphi}\rrbracket)={\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{1})$. Since ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$ and ${\varphi}$ is prefix-independent, we have ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{2}\cap\llbracket{\varphi}\rrbracket)={\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{2})$. Using Lemma 18, we obtain ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\varphi})=1$.

Next we show that for all $s\in S$ the strategy $\sigma_{1}$ defined above achieves ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\sf F}{\it Safe}(\frac{2}{3})\lor{\sf F}[S]^{{\mathit{C}ol}=2})=1$. To this end we will use Lemma 18 again. We partition the runs of $sS^{\omega}$ into three events ${\mathfrak{R}}_{1}^{\prime},{\mathfrak{R}}_{2}^{\prime},{\mathfrak{R}}_{0}^{\prime}$ as follows:

• •

${\mathfrak{R}}_{1}^{\prime}=\llbracket{\sf F}{\sf G}[S]^{{\mathit{C}ol}=0}\rrbracket^{s}$

• •

${\mathfrak{R}}_{2}^{\prime}=\llbracket{\sf G}{\sf F}[S]^{{\mathit{C}ol}=2}\rrbracket^{s}$

• •

${\mathfrak{R}}_{0}^{\prime}=sS^{\omega}\setminus\llbracket{\varphi}\rrbracket^{s}$

We have previously shown that ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\varphi})=1$, hence ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{0}^{\prime})=0$. By Lemma 15, almost all runs in ${\mathfrak{R}}_{1}^{\prime}$ satisfy ${\sf G}{\sf F}{\it Safe}(\frac{2}{3})$. Since $\llbracket{\sf G}{\sf F}{\it Safe}(\frac{2}{3})\rrbracket\subseteq\llbracket{\sf F}{\it Safe}(\frac{2}{3})\rrbracket$, we have ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{1}^{\prime}\cap\llbracket{\sf F}{\it Safe}(\frac{2}{3})\lor{\sf F}[S]^{{\mathit{C}ol}=2}\rrbracket)={\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{1}^{\prime})$. Since ${\mathfrak{R}}_{2}^{\prime}\subseteq\llbracket{\sf F}[S]^{{\mathit{C}ol}=2}\rrbracket$, we also have ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{2}^{\prime}\cap\llbracket{\sf F}{\it Safe}(\frac{2}{3})\lor{\sf F}[S]^{{\mathit{C}ol}=2}\rrbracket)={\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\mathfrak{R}}_{2}^{\prime})$. Using Lemma 18 we obtain ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\sf F}{\it Safe}(\frac{2}{3})\lor{\sf F}[S]^{{\mathit{C}ol}=2})=1$.

Writing $T={\it Safe}(\frac{2}{3})\cup[S]^{{\mathit{C}ol}=2}$ we have just shown that for all $s\in S$ there is a strategy $\sigma_{1}$ with ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\sigma_{1}}({\sf F}T)=1$. By Lemma 7 there is an MD-strategy $\hat{\sigma}$ for ${\mathcal{M}}^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s,\hat{\sigma}}({\sf F}T)=1$ for all $s\in S$. We extend the (so far partially defined) strategy $\sigma^{\prime}$ by $\hat{\sigma}$. Thus we obtain a (fully defined) strategy $\sigma^{\prime}$ for ${\mathcal{M}}$ such that for all $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\sf F}T)=1$.

It remains to show that for all $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$. To this end we will use Lemma 18 again. We partition the runs of $sS^{\omega}$ in two events ${\mathfrak{R}}_{1}^{\prime\prime},{\mathfrak{R}}_{2}^{\prime\prime}$:

• •

${\mathfrak{R}}_{1}^{\prime\prime}=\llbracket{\sf G}{\sf F}{\it Safe}(\frac{2}{3})\rrbracket^{s}$, i.e., ${\mathfrak{R}}_{1}^{\prime\prime}$ contains the runs that visit ${\it Safe}(\frac{2}{3})$ infinitely often.

• •

${\mathfrak{R}}_{2}^{\prime\prime}=\llbracket{\sf F}{\sf G}\neg{\it Safe}(\frac{2}{3})\rrbracket^{s}$, i.e., ${\mathfrak{R}}_{2}^{\prime\prime}$ contains the runs that from some point on never visit ${\it Safe}(\frac{2}{3})$.

Every time a run enters ${\it Safe}(\frac{2}{3})$, by Lemma 14, the probability is at least $\frac{1}{2}$ that the run remains in ${\it Safe}(\frac{1}{3})$ forever. It follows that almost all runs in ${\mathfrak{R}}_{1}^{\prime\prime}$ eventually remain in ${\it Safe}(\frac{1}{3})$ forever, i.e., ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\mathfrak{R}}_{1}^{\prime\prime}\cap\llbracket{\sf F}{\sf G}{\it Safe}(\frac{1}{3})\rrbracket)={\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\mathfrak{R}}_{1}^{\prime\prime})$. Since ${\it Safe}(\frac{1}{3})\subseteq[S]^{{\mathit{C}ol}=0}$, we have $\llbracket{\sf F}{\sf G}{\it Safe}(\frac{1}{3})\rrbracket\subseteq\llbracket{\sf F}{\sf G}[S]^{{\mathit{C}ol}=0}\rrbracket\subseteq\llbracket{\varphi}\rrbracket$. Hence also ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\mathfrak{R}}_{1}^{\prime\prime}\cap\llbracket{\varphi}\rrbracket)={\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\mathfrak{R}}_{1}^{\prime\prime})$.

We have previously shown that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\sf F}T)=1$ holds for all $s\in S$. Hence also ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\sf G}{\sf F}T)=1$ holds for all $s\in S$. In particular, almost all runs in ${\mathfrak{R}}_{2}^{\prime\prime}$ satisfy ${\sf G}{\sf F}T$. By comparing the definitions of ${\mathfrak{R}}_{2}^{\prime\prime}$ and $T$ we see that almost all runs in ${\mathfrak{R}}_{2}^{\prime\prime}$ even satisfy ${\sf G}{\sf F}[S]^{{\mathit{C}ol}=2}$. Since $\llbracket{\sf G}{\sf F}[S]^{{\mathit{C}ol}=2}\rrbracket\subseteq\llbracket{\varphi}\rrbracket$, we obtain ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\mathfrak{R}}_{2}^{\prime\prime}\cap\llbracket{\varphi}\rrbracket)={\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\mathfrak{R}}_{2}^{\prime\prime})$.

A final application of Lemma 18 yields ${\mathcal{P}}_{{\mathcal{M}},s,\sigma^{\prime}}({\varphi})=1$ for all $s\in S$. ∎

VI-C $\epsilon$-Optimal MD-strategies for Co-Büchi

Theorem 19**.**

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, ${\mathit{C}ol}:S\to\{0,1\}$, and ${\varphi}=\mathtt{Parity}({\mathit{C}ol})$ be the co-Büchi objective. Then there exist uniform $\epsilon$-optimal MD-strategies. I.e., for every $\epsilon>0$ there is an MD-strategy $\sigma_{\epsilon}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{\epsilon}}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}-\epsilon$ for every $s_{0}\in S$.

Proof.

Let $\epsilon_{1}>0$ be a suitably small number (to be determined later), $\tau_{1}:=1-\epsilon_{1}$ and ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$ defined as in Definition 1. Let $\sigma_{\mathit{opt\mathchar 45\relax av}}$ be the MD-strategy from Proposition 13. From ${\mathcal{M}}$ we obtain a modified MDP ${\mathcal{M}}^{\prime}$ by fixing all player choices from states in ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$ according to $\sigma_{\mathit{opt\mathchar 45\relax av}}$.

We show that ${\mathtt{val}_{{\mathcal{M}}^{\prime}}(s_{0})}\geq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}-\epsilon_{1}$. By definition of the value ${\mathtt{val}_{{\mathcal{M}}}(s_{0})}$, for every $\delta>0$ there exists a strategy $\sigma_{\delta}$ in ${\mathcal{M}}$ s.t. ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{\delta}}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}-\delta$. We define a strategy $\sigma_{\delta}^{\prime}$ in ${\mathcal{M}}^{\prime}$ from state $s_{0}$ as follows. First play like $\sigma_{\delta}$. If and when a state in ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$ is reached, play like $\sigma_{\mathit{opt\mathchar 45\relax av}}$. This is possible, since no moves from states outside ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$ have been fixed in ${\mathcal{M}}^{\prime}$, and all moves from states inside ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$ have been fixed according to $\sigma_{\mathit{opt\mathchar 45\relax av}}$. Then we have:

[TABLE]

Since this holds for every $\delta>0$ we obtain ${\mathtt{val}_{{\mathcal{M}}^{\prime}}(s_{0})}\geq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}-\epsilon_{1}$.

Now let $\tau_{2}:=1-\epsilon_{1}/k$ for a suitably large $k\geq 1$ (to be determined later) and ${\it Safe_{{\mathcal{M}}^{\prime}}}(\tau_{2})$ be defined as in Definition 1. In particular, ${\it Safe_{{\mathcal{M}}^{\prime}}}(\tau_{2})={\it Safe_{{\mathcal{M}}}}(\tau_{2})$ (by the same argument as in the proof of Proposition 17).

By definition of the value, for every $\epsilon_{2}>0$ there exists a strategy $\sigma_{\epsilon_{2}}$ in ${\mathcal{M}}^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s_{0},\sigma_{\epsilon_{2}}}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}^{\prime}}(s_{0})}-\epsilon_{2}$. Moreover, by Lemma 15 and $\tau_{2}<1$, ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s_{0},\sigma}({\sf F}{\it Safe_{{\mathcal{M}}^{\prime}}}(\tau_{2}))\geq{\mathcal{P}}_{{\mathcal{M}}^{\prime},s_{0},\sigma}({\varphi})$ for every strategy $\sigma$ and thus in particular for $\sigma_{\epsilon_{2}}$. Therefore, ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s_{0},\sigma_{\epsilon_{2}}}({\sf F}{\it Safe_{{\mathcal{M}}^{\prime}}}(\tau_{2}))\geq{\mathtt{val}_{{\mathcal{M}}^{\prime}}(s_{0})}-\epsilon_{2}$. By Theorem 9, for every $\epsilon_{3}>0$ there exists an MD-strategy $\sigma^{\prime}$ in ${\mathcal{M}}^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}}^{\prime},s_{0},\sigma^{\prime}}({\sf F}{\it Safe_{{\mathcal{M}}^{\prime}}}(\tau_{2}))\geq{\mathtt{val}_{{\mathcal{M}}^{\prime}}(s_{0})}-\epsilon_{2}-\epsilon_{3}$. In particular, $\sigma^{\prime}$ must coincide with $\sigma_{\mathit{opt\mathchar 45\relax av}}$ at all states in ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$, since in ${\mathcal{M}}^{\prime}$ these choices are already fixed.

We obtain the MD-strategy $\sigma_{\epsilon}$ in ${\mathcal{M}}$ by combining the MD-strategies $\sigma^{\prime}$ and $\sigma_{\mathit{opt\mathchar 45\relax av}}$. The strategy $\sigma_{\epsilon}$ plays like $\sigma^{\prime}$ at all states outside ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$ and like $\sigma_{\mathit{opt\mathchar 45\relax av}}$ at all states inside ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$.

In order to show that $\sigma_{\epsilon}$ has the required property ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{\epsilon}}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}-\epsilon$, we first estimate the probability that a play according to $\sigma_{\epsilon}$ will never leave the set ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$ after having visited a state in ${\it Safe_{{\mathcal{M}}^{\prime}}}(\tau_{2})$.

Let $s\in{\it Safe_{{\mathcal{M}}^{\prime}}}(\tau_{2})$. Then, by Lemma 14,

[TABLE]

In particular we also have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\epsilon}}({\sf G}{\it Safe}(\tau_{1}))\geq 1-\frac{1}{k}$, since $\sigma_{\epsilon}$ coincides with $\sigma_{\mathit{opt\mathchar 45\relax av}}$ inside the set ${\it Safe_{{\mathcal{M}}}}(\tau_{1})$. Finally we obtain:

[TABLE]

This holds for every $\epsilon_{1},\epsilon_{2},\epsilon_{3}>0$ and every $k\geq 1$, and moreover ${\mathtt{val}_{{\mathcal{M}}}(s_{0})}\leq 1$. Thus we can set $\epsilon_{1}=\epsilon_{2}=\epsilon_{3}:=\epsilon/6$ and $k:=\frac{2}{\epsilon}$ and obtain ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{\epsilon}}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}-\epsilon$ for every $s_{0}\in S$ as required. ∎

VII Discussion

Our results on the memory requirements of ($\epsilon$)-optimal strategies (Figure 1) directly imply how much memory is needed to win quantitative objectives of type \big{[}{\varphi}\big{]}^{{\rhd c}} (considered, e.g., in [7]). For $c<1$ the assumed winning strategy might have to be an $\epsilon$-optimal one, since optimal strategies do not always exist. Thus MD-strategies are only sufficient for reachability objectives in countable MDPs (resp., for ${\{0,1\}}\text{-}\mathtt{Parity}$, safety and reachability objectives in finitely branching MDPs). In the special case of \big{[}{\varphi}\big{]}^{{\geq 1}} objectives (i.e., winning almost-surely), the winning strategy (assuming it exists) must be optimal. Thus MD-strategies are only sufficient for safety, reachability and ${\{1,2\}}\text{-}\mathtt{Parity}$ in countable MDPs (resp., for all objectives subsumed by ${\{0,1,2\}}\text{-}\mathtt{Parity}$ in finitely branching MDPs).

In this paper we have studied countable MDPs. Not all our results carry over to uncountable MDPs. The first issue is measurability. The probabilities are only well-defined if the strategies are measurable functions, which might not exist without further conditions on the MDP; cf. Section 2.3 in [23]. Another issue is that strategies cannot generally be chosen uniform, i.e., independent of the initial state. E.g., in countable MDPs $\epsilon$-optimal strategies for reachability can be chosen uniform MD (Theorem 9), but this does not carry over to uncountable MDPs (Thm. A in [21]). However, optimal strategies for reachability, if they exist, can be chosen uniform MD (Proposition B in [21]).

Acknowledgements. This work was partially supported by the EPSRC through grants EP/M027287/1, EP/M027651/1, EP/P020909/1 and EP/M003795/1 and by St. John’s College, Oxford.

-A Proofs of Section III

We recall two results that are used throughout the proofs in this section:

Strong fairness of probabilistic choices in Markov chains.

Given a Markov chain, let ${\mathcal{P}}_{q}(\cdot)$ denotes the probability of events starting in state $q$ of the chain. Let $p,q$ be two states and $\pi$ a finite path starting in $p$ with strictly positive probability. Strong fairness of probabilistic choices states that ${\mathcal{P}}_{q}({\sf G}{\sf F}\pi)={\mathcal{P}}_{q}({\sf G}{\sf F}p)$. Intuitively, it means that under the condition that state $p$ is visited infinitely often, any finite path starting in $p$ will be taken infinitely often, almost surely [3, Theorem 10.25].

The Borel-Cantelli lemma.

Suppose that $(E_{n})_{n\in\mathbb{N}}$ is a sequence of events in a probability space. Denote by $E^{\infty}$ the event

[TABLE]

that intuitively is the event “$E_{n}$ occurs for infinitely many $n$”. The Borel-Cantelli lemma asserts that if $\sum_{n=1}^{\infty}{\mathcal{P}}(E_{n})<\infty$ then ${\mathcal{P}}(E^{\infty})=0$. Informally speaking, if the sum of probabilities of the events $E_{n}$ is bounded then the probability that infinitely many of them occur is zero [5].

Theorem 1. *

Let ${\varphi}={\{1,2,3\}}\text{-}\mathtt{Parity}$. There exists a finitely branching MDP ${\mathcal{M}}$ with initial state $s_{0}$ such that*

• •

for all FR-strategies $\sigma$, we have ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=0$,

• •

there exists an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$.

*Hence, optimal (and even almost-surely winning) and $\epsilon$-optimal strategies require infinite memory for ${\{1,2,3\}}\text{-}\mathtt{Parity}$, even in finitely branching MDPs. *

Proof.

Consider the MDP ${\mathcal{M}}$ shown (on the left side) in Figure 2 where $S_{\scriptscriptstyle\bigcirc}=\{r_{i}\}_{i\in\mathbb{N}}$ and $S_{\Box}=\{t\}\cup\{s_{i}\}_{i\in\mathbb{N}}$. For all $i\in\mathbb{N}$, there are transitions $s_{i}{\longrightarrow}r_{i}$ and $s_{i}{\longrightarrow}s_{i+1}$ in $s_{i}$ states, whereas $P(r_{i},t)=2^{-i}$ and $P(r_{i},s_{0})=1-2^{-i}$ in random states.

Let $\sigma$ be an arbitrary FR-strategy. We prove that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=0$. By definition there is a transducer ${\sf T}$ with finite memory ${\sf M}$ and initial mode ${\sf m}_{0}$ such that $\sigma_{{\sf T}}=\sigma$. Let ${\mathcal{M}}^{{\sf T}}$ be the Markov chain obtained by the product of the MDP ${\mathcal{M}}$ and the transducer ${\sf T}$. The set of states in ${\mathcal{M}}^{{\sf T}}$ is ${\sf M}\times S$. We define a coloring function for ${\mathcal{M}}^{{\sf T}}$ such that it ignores the memory mode and assigns to $({\sf m},s)$ the same color as state $s$ in ${\mathcal{M}}$. By a slight abuse of notation, we use the same notation ${\mathit{C}ol}$ for the coloring functions of both ${\mathcal{M}}$ and ${\mathcal{M}}^{{\sf T}}$. We also denote by ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},q}({\mathfrak{R}})$ the probability of a measurable set ${\mathfrak{R}}$ of infinite paths (i.e., infinite plays), starting in the state $q$ of ${\mathcal{M}}^{{\sf T}}$.

We prove that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\sf G}{\sf F}[S]^{{\mathit{C}ol}=2}\wedge{\sf F}{\sf G}[S]^{{\mathit{C}ol}\neq 3})=0$. Equivalently, we show that ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s_{0})}({\varphi}^{{\sf T}})=0$ where ${\varphi}^{{\sf T}}={\sf G}{\sf F}[{\sf M}\times S]^{{\mathit{C}ol}=2}\wedge{\sf F}{\sf G}[{\sf M}\times S]^{{\mathit{C}ol}\neq 3}$. We proceed in three steps: we will show, using strong fairness of probabilistic choices in Markov chains, that for all modes ${\sf m}\in{\sf M}$,

[TABLE]

Moreover,

[TABLE]

Since the memory of strategy $\sigma$ is finite ($\lvert{\sf M}\rvert<\infty$), we will show that

[TABLE]

Using (1)-(3) we complete the proof as follows:

[TABLE]

As a result ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=0$. Below, we prove (1), (2) and (3).

We first highlight two properties of the Markov chain ${\mathcal{M}}^{{\sf T}}$. Consider the MDP ${\mathcal{M}}$: ($i$) the only states with color $2$ are random states $r_{i}\in S_{\scriptscriptstyle\bigcirc}$, wherein the only successors are $s_{0}$ and $t$. Hence, from all states $({\sf m},r_{i})\in{\sf M}\times S_{\scriptscriptstyle\bigcirc}$ in ${\mathcal{M}}^{{\sf T}}$, there are successors $q_{1},q_{2}$ such that $q_{1}\in{\sf M}\times\{s_{0}\}$ and $q_{2}\in{\sf M}\times\{t\}$; moreover, all successors are in ${\sf M}\times\{s_{0},t\}$. ($ii$) The state $t$ has the unique successor $s_{0}$. Hence, in ${\mathcal{M}}^{{\sf T}}$, from all states $({\sf m},t)\in{\sf M}\times S_{\scriptscriptstyle\bigcirc}$ all successors $q$ are such that $q\in{\sf M}\times\{s_{0}\}$.

To establish (1), let $({\sf m},s_{0})\in{\sf M}\times\{s_{0}\}$ be some state in the Markov chain ${\mathcal{M}}^{{\sf T}}$. For the case ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s_{0})}({\sf G}{\sf F}({\sf m},s_{0}))=0$, we trivially have (1). Therefore, we assume that ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s_{0})}({\sf G}{\sf F}({\sf m},s_{0}))>0$. So, there exists an infinite path satisfying ${\sf G}{\sf F}({\sf m},s_{0})$. Hence, there exists a finite path $\pi$ from $({\sf m},s_{0})$ to itself. By the structure of the chain, $\pi$ has a prefix $({\sf m}_{s_{0}},s_{0})({\sf m}_{s_{1}},s_{1})\cdots({\sf m}_{s_{i}},s_{i})\in({\sf M}\times S_{\Box})^{*}$ traversing player’s states, with ${\sf m}_{s_{0}}={\sf m}$, and next visiting some state $({\sf m}_{r_{i}},r_{i})$. By property ($i$), we know that $({\sf m}_{r_{i}},r_{i})$ has a successor $({\sf m}_{t},t)\in{\sf M}\times\{t\}$. It implies that

[TABLE]

is a finite path in ${\mathcal{M}}^{{\sf T}}$, starting in $({\sf m},s_{0})$ with positive probability. By strong fairness of probabilistic choices, ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s_{0})}({\sf G}{\sf F}\pi_{t})={\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s_{0})}({\sf G}{\sf F}({\sf m},s_{0}))$. In other words, under the condition that state $({\sf m},s_{0})$ is visited infinitely often, the finite path $\pi_{t}$ will be taken infinitely often, almost-surely. As an immediate result of this and the fact that $({\sf m}_{t},t)$ has color $3$, we conclude (1).

To establish (2), we need to show that, for all infinite plays $\pi^{\infty}$ of ${\mathcal{M}}^{{\sf T}}$, if $\pi^{\infty}\in\llbracket{\sf G}{\sf F}[{\sf M}\times S]^{{\mathit{C}ol}=2}\rrbracket$ then $\pi^{\infty}\in\llbracket{\sf G}{\sf F}({\sf M}\times\{s_{0}\})\rrbracket$. By the properties ($i$) and ($ii$) of ${\mathcal{M}}^{{\sf T}}$, whenever $\pi^{\infty}$ visits some state from ${\sf M}\times S_{\scriptscriptstyle\bigcirc}$, which are the only states with color $2$, then $\pi^{\infty}$ must visit some state from ${\sf M}\times\{s_{0}\}$ within two steps. This results in (2).

To establish (3), we observe that the inclusion $\supseteq$ is trivial. To show $\subseteq$, let $\pi^{\infty}\in\llbracket{\sf G}{\sf F}({\sf M}\times\{s_{0}\})\rrbracket$ be an infinite path in the chain. As $\pi^{\infty}$ visits infinitely many elements from the finite set ${\sf M}\times\{s_{0}\}$, there must exist some element $({\sf m},s_{0})$ that is visited infinitely often. Hence, $\pi^{\infty}\in\llbracket\bigvee_{{\sf m}\in{\sf M}}{\sf G}{\sf F}({\sf m},s_{0})\rrbracket$, which gives the inclusion and thus (3).

Now, we construct an HD-strategy $\sigma_{h}$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{h}}({\varphi})=1$. The strategy $\sigma_{h}$ is defined, for all partial plays $\rho$, as follows:

[TABLE]

Intuitively, $\sigma_{h}$ is such that upon the $k$-th visit to state $s_{0}$, the path $s_{0}s_{1}\cdots s_{k}$ is traversed and then the transition $s_{k}{\longrightarrow}r_{k}$ is chosen. Observe that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{h}}({\sf G}{\sf F}[S]^{{\mathit{C}ol}=2})=1$. Below, we argue that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{h}}({\sf G}{\sf F}[S]^{{\mathit{C}ol}=3})=0$, which proves that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{h}}({\varphi})=1$.

We define the sequence of events $E_{k}$ of visiting $t$ between the $k$th and $k+1$st visits of $s_{0}$. For $k\geq 1$, let

[TABLE]

Observe that

[TABLE]

We use the Borel-Cantelli lemma to prove that infinitely many of $E_{k}$’s occur with zero probability, that is the probability of ${\sf G}{\sf F}[S]^{{\mathit{C}ol}=3}$. In fact, by construction of $\sigma_{h}$, observe that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{h}}(E_{k})=2^{-k}$. Consequently, we have

[TABLE]

By the Borel-Cantelli lemma, we then have ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{h}}({\sf G}{\sf F}[S]^{{\mathit{C}ol}=3})=0$, and thus ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{h}}({\varphi})=1$. The proof is complete. ∎

Remark 1. *

A strict subclass of finitely branching MDPs are $1$-counter MDPs, where a finite-state MDP is augmented with an integer counter [6]. The MDP in Theorem 1 (plus some auxiliary states) is implementable by a $1$-counter MDP. *

Proof.

Figure 5 shows a $1$-counter MDP with control-states $\{s,r,r^{\prime},t\}$ that is functionally equivalent to the one used in Theorem 1 (Figure 2 (left)). It just uses some auxiliary states that have no influence on the parity objective. Starting in $s$, the player can choose whether to increase the counter by $1$ or to go to $r$. In the random state $r$ the behavior depends on the counter value. If the counter is non-zero then the successors $r,r^{\prime}$ are chosen with equal probability and the counter is decreased by $1$. If the counter is zero then $t$ is the unique successor. In state $r^{\prime}$ the counter is deterministically decreased until it becomes zero, and then one goes to state $s$. The color function is ${\mathit{C}ol}(s)=1$, ${\mathit{C}ol}(r)={\mathit{C}ol}(r^{\prime})=2$ and ${\mathit{C}ol}(t)=3$. If one is in state $r$ with counter value $n$, then the probability of seeing state $t$ before returning to state $s$ is $2^{-n}$.

∎

Theorem 3. *

Let ${\varphi}=\mathtt{Safety}(T)$. There exists an infinitely branching MDP ${\mathcal{M}}$ with initial state $s$ such that*

• •

for all FR-strategies $\sigma$, we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=0$,

• •

for every $c\in[0,1)$, there exists an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})\geq c$.

*Hence, $\epsilon$-optimal strategies for safety require infinite memory. *

Proof.

Consider the MDP ${\mathcal{M}}$ shown (on the left side) in Figure 3 where $S_{\Box}=\{s,t\}$ and $S_{\scriptscriptstyle\bigcirc}=\{r_{i}\}_{i\geq 1}$. The state $s$ is infinitely branching: $s{\longrightarrow}r_{i}$ for all $i\geq 1$. For all random states $r_{i}$, there are two successors $P(r_{i},t)=2^{-i}$ and $P(r_{i},s_{0})=1-2^{-i}$. The state $t$ is a sink state.

Let $\sigma$ be an arbitrary FR-strategy. By definition there is a transducer ${\sf T}$ with finite memory ${\sf M}$ and initial mode ${\sf m}_{0}$ such that $\sigma_{{\sf T}}=\sigma$. Let ${\mathcal{M}}^{{\sf T}}$ be the Markov chain obtained by the product of the MDP ${\mathcal{M}}$ and the transducer ${\sf T}$. The set of states in ${\mathcal{M}}^{{\sf T}}$ is ${\sf M}\times S$. We denote by ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},q}({\mathfrak{R}})$ the probability of a measurable set ${\mathfrak{R}}$ of infinite paths (i.e., infinite plays), starting in the state $q$ of ${\mathcal{M}}^{{\sf T}}$.

Below, we prove that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}(\mathtt{Safety}(\{t\}))=0$. Equivalently, we show that ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}(\mathtt{Safety}({\sf M}\times\{t\}))=0$. We proceed in the following three steps: We will show, using strong fairness of probabilistic choices in Markov chains, that for all modes ${\sf m}\in{\sf M}$,

[TABLE]

Since the memory of strategy $\sigma$ is finite ($\lvert{\sf M}\rvert<\infty$), we will show that

[TABLE]

Moreover, we will prove that

[TABLE]

Using (4)-(6), we complete the proof as follows:

[TABLE]

As a result, ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\mathtt{Safety}(\{t\}))=0$. Below we prove (4), (5) and (6).

To establish (4), let $({\sf m},s)\in{\sf M}\times\{s\}$ be some state in the Markov chain ${\mathcal{M}}^{{\sf T}}$. For the case ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf G}{\sf F}({\sf m},s))=0$, we trivially have (4). Therefore, we assume that ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf G}{\sf F}({\sf m},s))>0$. So, there exists an infinite path satisfying ${\sf G}{\sf F}({\sf m},s)$. Hence, there exists a finite path $\pi$ from $({\sf m},s)$ to itself. By the structure of the chain, $\pi$ visits some state $({\sf m}_{r_{i}},r_{i})$. In ${\mathcal{M}}$, for all random states $r_{i}\in S_{\scriptscriptstyle\bigcirc}$, the only successors are $s$ and $t$. Hence, from all states $({\sf m},r_{i})\in{\sf M}\times S_{\scriptscriptstyle\bigcirc}$ in ${\mathcal{M}}^{{\sf T}}$, there is some successor $q\in{\sf M}\times\{t\}$. It implies that $\pi_{t}=({\sf m},s)({\sf m}_{r_{i}},r_{i})({\sf m}_{t},t)$ is a finite path in ${\mathcal{M}}^{{\sf T}}$, that starts in $({\sf m},s)$ with positive probability. By strong fairness of probabilistic choices, ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf F}\pi_{t})={\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf G}{\sf F}({\sf m},s))$. As a result, we conclude (4).

To establish (5), we observe that the inclusion $\supseteq$ is trivial. To show $\subseteq$, let $\pi^{\infty}\in\llbracket{\sf G}{\sf F}({\sf M}\times\{s_{0}\})\rrbracket$ be an infinite path in the chain. As $\pi^{\infty}$ visits infinitely many elements from the finite set ${\sf M}\times\{s_{0}\}$, there must exist some element $({\sf m},s_{0})$ that is visited infinitely often. Hence, $\pi^{\infty}\in\llbracket\bigvee_{{\sf m}\in{\sf M}}{\sf G}{\sf F}({\sf m},s_{0})\rrbracket$, which gives the inclusion and thus (5).

To establish (6), note that in ${\mathcal{M}}$, all successors of $s$ are from random states, from which the only successors are $s$ and $t$. Hence, for all infinite plays $\pi^{\infty}\not\in\llbracket{\sf F}({\sf M}\times\{t\})\rrbracket$ in ${\mathcal{M}}^{{\sf T}}$, $\pi^{\infty}$ alternates between some states from ${\sf M}\times\{s\}$ and next some state from ${\sf M}\times S_{\scriptscriptstyle\bigcirc}$. It implies that $\pi\in\llbracket{\sf G}{\sf F}({\sf M}\times\{s\})\rrbracket$.

Now, let $c\in[0,1)$. Let $n$ be such that $c\leq 1-\frac{1}{2^{n}}$. We construct an HD-strategy $\sigma_{n}$ such that

[TABLE]

For all partial plays $\rho$, we define $\sigma_{n}(\rho)=r_{n+k}$ where $k$ is the number of times $\rho$ has visited $s$. Intuitively, upon the $k$-th visit to $s$, the strategy $\sigma_{n}$ chooses the transition $s{\longrightarrow}r_{n+k}$.

For all $k\geq 1$, let $E_{k}$ be the event of visiting $t$ after the $k$-th visit of $s$, defined as follows

[TABLE]

Observe that $\llbracket{\sf F}\{t\}\rrbracket$ is the disjoint union of all $E_{k}$ events. Hence, we have

[TABLE]

This proves that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{n}}(\mathtt{Safety}(\{t\}))=1-{\mathcal{P}}_{{\mathcal{M}},s,\sigma_{n}}({\sf F}\{t\})\geq 1-\frac{1}{2^{n}}\geq c$. ∎

Theorem 4. *

Let ${\varphi}={\{0,1\}}\text{-}\mathtt{Parity}$ be the co-Büchi objective. There exists an infinitely branching MDP ${\mathcal{M}}$ with initial state $s$ such that*

• •

for all FR-strategies $\sigma$, we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=0$,

• •

there exists an HD-strategy $\sigma$ such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=1$.

*Hence, optimal (and even almost-surely winning) strategies and $\epsilon$-optimal strategies for co-Büchi require infinite memory. *

Proof.

Consider the MDP ${\mathcal{M}}$ shown (on the right side) in Figure 3 where $S_{\Box}=\{s,t\}$ and $S_{\scriptscriptstyle\bigcirc}=\{r_{i}\}_{i\geq 1}$. The state $s$ is infinitely branching: $s{\longrightarrow}r_{i}$ for all $i\geq 1$. For all random states $r_{i}$, there are two successors $P(r_{i},t)=2^{-i}$ and $P(r_{i},s)=1-2^{-i}$. The state $t$ has the unique successor $s$.

Let $\sigma$ be an arbitrary FR-strategy. By definition there is a transducer ${\sf T}$ with finite memory ${\sf M}$ and initial mode ${\sf m}_{0}$ such that $\sigma_{{\sf T}}=\sigma$. Let ${\mathcal{M}}^{{\sf T}}$ be the Markov chain obtained by the product of the MDP ${\mathcal{M}}$ and the transducer ${\sf T}$. The set of states in ${\mathcal{M}}^{{\sf T}}$ is ${\sf M}\times S$. We define a coloring function for ${\mathcal{M}}^{{\sf T}}$ such that it ignores the memory mode and assigns to $({\sf m},s)$ the same color as state $s$ in ${\mathcal{M}}$. In particular, all states $q\in{\sf M}\times\{t\}$ have color $1$. We use the same notation ${\mathit{C}ol}$ for the coloring functions of both ${\mathcal{M}}$ and ${\mathcal{M}}^{{\sf T}}$. We denote by ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},q}({\mathfrak{R}})$ the probability of a measurable set ${\mathfrak{R}}$ of infinite paths (i.e., infinite plays), starting in the state $q$ of ${\mathcal{M}}^{{\sf T}}$.

We prove that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\sf F}{\sf G}[S]^{{\mathit{C}ol}\neq 1})=0$. Equivalently, we show that ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf F}{\sf G}[{\sf M}\times S]^{{\mathit{C}ol}\neq 1})=0$. We proceed in three steps: we will show, using strong fairness of probabilistic choices in Markov chains, that for all modes ${\sf m}\in{\sf M}$,

[TABLE]

Since the memory of strategy $\sigma$ is finite ($\lvert{\sf M}\rvert<\infty$), we will show that

[TABLE]

Moreover, we show that

[TABLE]

Using (7), (8) and (9), we complete the proof as follows:

[TABLE]

As a result, ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})=0$. Below we prove (7), (8) and (9).

To establish (7), let $({\sf m},s)\in{\sf M}\times\{s\}$ be some state in the Markov chain ${\mathcal{M}}^{{\sf T}}$. For the case ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf G}{\sf F}({\sf m},s))=0$, we trivially have (7). Therefore, we assume that ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf G}{\sf F}({\sf m},s))>0$. So, there exists an infinite path satisfying ${\sf G}{\sf F}({\sf m},s)$. Hence, there exists a finite path $\pi$ from $({\sf m},s)$ to itself. By the structure of the chain, $\pi$ visits some state $({\sf m}_{r_{i}},r_{i})$. Consider the MDP ${\mathcal{M}}$, for all random states $r_{i}\in S_{\scriptscriptstyle\bigcirc}$, the only successors are $s$ and $t$. Hence, from all states $({\sf m},r_{i})\in{\sf M}\times S_{\scriptscriptstyle\bigcirc}$ in ${\mathcal{M}}^{{\sf T}}$, there is some successor $q$ such that $q\in{\sf M}\times\{t\}$. It implies that $\pi_{t}=({\sf m},s)({\sf m}_{r_{i}},r_{i})({\sf m}_{t},t)$ is a finite path in ${\mathcal{M}}^{{\sf T}}$, that starts in $({\sf m},s)$ with positive probability. By strong fairness of probabilistic choices, ${\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf G}{\sf F}\pi_{t})={\mathcal{P}}_{{\mathcal{M}}^{{\sf T}},({\sf m}_{0},s)}({\sf G}{\sf F}({\sf m},s))$. As a result, we conclude (7).

To establish (8), we observe that the inclusion $\supseteq$ is trivial. To show $\subseteq$, let $\pi^{\infty}\in\llbracket{\sf G}{\sf F}({\sf M}\times\{s\})\rrbracket$ be an infinite path in the chain. As $\pi^{\infty}$ visits infinitely many elements from the finite set ${\sf M}\times\{s\}$, there must exist some element $({\sf m},s)$ that is visited infinitely often. Hence, $\pi^{\infty}\in\llbracket\bigvee_{{\sf m}\in{\sf M}}{\sf G}{\sf F}({\sf m},s)\rrbracket$, which gives the inclusion and thus (8).

To establish (9), note that in ${\mathcal{M}}$, all infinite plays must visit $s$ infinitely often. Thus all runs in ${\mathcal{M}}^{{\sf T}}$ must visit ${\sf M}\times\{s\}$ infinitely often. In particular, this holds for those infinite runs $\pi^{\infty}\in\llbracket{\sf F}{\sf G}[{\sf M}\times S]^{{\mathit{C}ol}\neq 1}\rrbracket$ in ${\mathcal{M}}^{{\sf T}}$. Thus $\pi^{\infty}\in\llbracket{\sf G}{\sf F}({\sf M}\times\{s\})\rrbracket$.

Now we construct an HD-strategy $\sigma_{h}$ such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{h}}({\varphi})=1$. For all partial plays $\rho$, we define $\sigma_{h}(\rho)=r_{k}$ where $k$ is the number of times $\rho$ has visited $s$. Intuitively, upon the $k$-th visit to $s$, the strategy $\sigma_{h}$ chooses the transition $s{\longrightarrow}r_{k}$. Below we argue that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{h}}({\sf G}{\sf F}[S]^{{\mathit{C}ol}=1})=0$, which proves that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{h}}({\varphi})=1$.

We define the sequence of events $E_{k}$ of visiting $t$ between the $k$-th and $k+1$st visits of $s$. For $k\geq 1$, let

[TABLE]

Observe that

[TABLE]

We use the Borel-Cantelli lemma to prove that infinitely many of $E_{k}$’s occur with zero probability, that is the probability of ${\sf G}{\sf F}[S]^{{\mathit{C}ol}=1}$. In fact, by construction of $\sigma_{h}$, observe that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{h}}(E_{k})=2^{-k}$. Consequently, we have

[TABLE]

By the Borel-Cantelli lemma, we then have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{h}}({\sf G}{\sf F}[S]^{{\mathit{C}ol}=1})=0$, and thus ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{h}}({\varphi})=1$. The proof is complete. ∎

-B Proofs of Section IV

Lemma 20**.**

Let ${\varphi}$ be an objective that is prefix-independent in a class ${\mathcal{C}}$ of MDPs. Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)\in{\mathcal{C}}$, and $s_{0}\in S$, and $\sigma$ be a strategy with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s_{0})}$. Suppose that $s_{0}s_{1}\cdots s_{n}$ for some $n\geq 0$ is a partial play starting in $s_{0}$ and induced by $\sigma$. Then:

${\mathtt{val}_{{\mathcal{M}}}(s_{n})}={\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\mid s_{0}s_{1}\cdots s_{n}S^{\omega})$. 2. 2.

If $s_{n}\in S_{\scriptscriptstyle\bigcirc}$ then ${\mathtt{val}_{{\mathcal{M}}}(s_{n})}=\sum_{s_{n+1}\in S}P(s_{n})(s_{n+1})\cdot{\mathtt{val}_{{\mathcal{M}}}(s_{n+1})}$. 3. 3.

If $s_{n}\in S_{\Box}$ then ${\mathtt{val}_{{\mathcal{M}}}(s_{n})}={\mathtt{val}_{{\mathcal{M}}}(s_{n+1})}$ for all $s_{n+1}\in{\sf supp}(\sigma(s_{0}s_{1}\cdots s_{n}))$.

Proof.

First we show ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\mid s_{0}s_{1}\cdots s_{n}S^{\omega})\leq{\mathtt{val}_{{\mathcal{M}}}(s_{n})}$. Define a strategy $\sigma^{\prime}:S^{*}S_{\Box}\to\mathcal{D}(S)$ by $\sigma^{\prime}(w)=\sigma(s_{0}s_{1}\cdots s_{n-1}w)$ for all $w\in S^{*}S_{\Box}$. Then we have ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\mid s_{0}s_{1}\cdots s_{n}S^{\omega})={\mathcal{P}}_{{\mathcal{M}},s_{n},\sigma^{\prime}}(\llbracket{\varphi}\rrbracket^{s_{n}})\leq{\mathtt{val}_{{\mathcal{M}}}(s_{n})}$.

Next we show ${\mathtt{val}_{{\mathcal{M}}}(s_{n})}\leq{\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\mid s_{0}s_{1}\cdots s_{n}S^{\omega})$. Towards a contradiction, suppose that ${\mathtt{val}_{{\mathcal{M}}}(s_{n})}>{\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\mid s_{0}s_{1}\cdots s_{n}S^{\omega})$. Then, by the definition of ${\mathtt{val}_{{\mathcal{M}}}(s_{n})}$, there is a strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{n},\sigma^{\prime}}(\llbracket{\varphi}\rrbracket^{s_{n}})>{\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\mid s_{0}s_{1}\cdots s_{n}S^{\omega})$. Define a strategy $\sigma^{\prime\prime}$ that plays according to $\sigma$; if and when partial play $s_{0}s_{1}\cdots s_{n}$ is played, then $\sigma^{\prime\prime}$ acts like $\sigma^{\prime}$ henceforth; otherwise $\sigma^{\prime\prime}$ continues with $\sigma$ forever. Using prefix-independence we get:

[TABLE]

This contradicts the definition of ${\mathtt{val}_{{\mathcal{M}}}(s_{0})}$. Hence we have shown item 1.

Towards items 2 and 3, we extend $\sigma:S^{*}S_{\Box}\to\mathcal{D}(S)$ to $\sigma:S^{*}S\to\mathcal{D}(S)$ by defining $\sigma(ws)=P(s)$ for $w\in S^{*}$ and $s\in S_{\scriptscriptstyle\bigcirc}$. Then we have for all $s_{n+1}\in S$:

[TABLE]

Further we have:

[TABLE]

Thus we have shown item 2. Towards item 3, suppose $s_{n}\in S_{\Box}$. Then prefix-independence implies ${\mathtt{val}_{{\mathcal{M}}}(s_{n})}\geq{\mathtt{val}_{{\mathcal{M}}}(s_{n+1})}$ for all $s_{n+1}$ with $s_{n}{\longrightarrow}s_{n+1}$. Since $\sigma(s_{0}s_{1}\cdots s_{n})$ is a probability distribution, the equality chain above shows that ${\mathtt{val}_{{\mathcal{M}}}(s_{n})}={\mathtt{val}_{{\mathcal{M}}}(s_{n+1})}$ for all $s_{n+1}\in{\sf supp}(\sigma(s_{0}s_{1}\cdots s_{n}))$. Thus we have shown item 3. ∎

Lemma 6. *

Let ${\varphi}$ be an objective that is prefix-independent in a class ${\mathcal{C}}$ of MDPs. Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)\in{\mathcal{C}}$. Construct an MDP ${\mathcal{M}}_{*}=(S_{*},S_{*\Box},S_{*{\scriptscriptstyle\bigcirc}},{\longrightarrow}_{*},P_{*})$ by setting*

[TABLE]

and $S_{*\Box}=S_{*}\cap S_{\Box}$ and $S_{*{\scriptscriptstyle\bigcirc}}=S_{*}\cap S_{\scriptscriptstyle\bigcirc}$ and

[TABLE]

and $P_{*}:S_{*{\scriptscriptstyle\bigcirc}}\to\mathcal{D}(S_{*})$ so that

[TABLE]

for all $s\in S_{*{\scriptscriptstyle\bigcirc}}$ and $t\in S_{*}$ with $s\,{\longrightarrow}_{*}\,t$. Then:

For all $\sigma\in\Sigma_{{\mathcal{M}}_{*}}$ and all $n\geq 0$ and all $s_{0},\ldots,s_{n}\in S_{*}$ with $s_{0}{\longrightarrow}_{*}\,s_{1}{\longrightarrow}_{*}\,\cdots{\longrightarrow}_{*}\,s_{n}$:

[TABLE] 2. 2.

For all $s_{0}\in S_{*}$ and all $\sigma\in\Sigma_{{\mathcal{M}}}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s_{0})}>0$ and all measurable ${\mathfrak{R}}\subseteq s_{0}S^{\omega}$ we have ${\mathcal{P}}_{{\mathcal{M}}_{*},s_{0},\sigma}({\mathfrak{R}})={\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\mathfrak{R}}\mid\llbracket{\varphi}\rrbracket^{s_{0}})$.

Proof.

Note that by Lemma 20.2 we have that $P_{*}(s)$ is a probability distribution for all $s\in S_{*{\scriptscriptstyle\bigcirc}}$; hence the MDP ${\mathcal{M}}_{*}$ is well-defined.

We prove item 1 by induction on $n$. For $n=0$ it is trivial. For the step, suppose that the equality in item 1 holds for some $n$. If $s_{n}\in S_{*{\scriptscriptstyle\bigcirc}}$ then we have:

[TABLE]

Let now $s_{n}\in S_{*\Box}$. If $\sigma(s_{0}s_{1}\ldots s_{n})(s_{n+1})=0$ then the inductive step is trivial. Otherwise we have:

[TABLE]

This completes the inductive step, and we have proved item 1.

Towards item 2, let $s_{0}\in S_{*}$ and $\sigma\in\Sigma_{{\mathcal{M}}}$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s_{0})}>0$. Observe that $\sigma$ can be applied also in the MDP ${\mathcal{M}}_{*}$. Indeed, for any $s\in S_{*\Box}$, if $t$ is a possible successor state of $s$ under $\sigma$, then ${\mathtt{val}_{{\mathcal{M}}}(s)}={\mathtt{val}_{{\mathcal{M}}}(t)}$ by Lemma 20.3 and thus $t\in S_{*}$.

Let again $n\geq 0$ and $s_{0},s_{1},\ldots,s_{n}\in S$.

• •

Suppose $s_{0}s_{1}\cdots s_{n}$ is a partial play in ${\mathcal{M}}_{*}$ induced by $\sigma$. Then we have:

[TABLE]

• •

Suppose $s_{0}s_{1}\cdots s_{n}$ is not a partial play in ${\mathcal{M}}_{*}$ induced by $\sigma$. Hence ${\mathcal{P}}_{{\mathcal{M}}_{*},s_{0},\sigma}(s_{0}s_{1}\cdots s_{n}S^{\omega})=0$. If $s_{0}s_{1}\cdots s_{n}$ is not a partial play in ${\mathcal{M}}$ induced by $\sigma$ then ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(s_{0}s_{1}\cdots s_{n}S^{\omega})=0$. Otherwise, since $\sigma$ is optimal, there is $i\leq n$ with ${\mathtt{val}_{{\mathcal{M}}}(s_{i})}=0$, hence ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap s_{0}s_{1}\cdots s_{n}S^{\omega})$. In either case we have ${\mathcal{P}}_{{\mathcal{M}}_{*},s_{0},\sigma}(s_{0}s_{1}\cdots s_{n}S^{\omega})\cdot{\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=0={\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap s_{0}s_{1}\cdots s_{n}S^{\omega})$.

In either case we have the equality ${\mathcal{P}}_{{\mathcal{M}}_{*},s_{0},\sigma}({\mathfrak{R}})={\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\mathfrak{R}}\mid\llbracket{\varphi}\rrbracket^{s_{0}})$ for cylinders ${\mathfrak{R}}=s_{0}s_{1}\cdots s_{n}S^{\omega}$. Since probability measures extend uniquely from cylinders [5], the equality holds for all measurable ${\mathfrak{R}}\subseteq s_{0}S^{\omega}$. Thus we have shown item 2. ∎

Lemma 8. *

Let $S$ be countable and $s\in S$. Call a set of the form $swS^{\omega}$ for $w\in S^{*}$ a cylinder. Let ${\mathcal{P}},{\mathcal{P}}^{\prime}$ be probability measures on $sS^{\omega}$ defined in the standard way, i.e., first on cylinders and then extended to all measurable sets ${\mathfrak{R}}\subseteq sS^{\omega}$. Suppose there is $x\geq 0$ such that $x\cdot{\mathcal{P}}(\mathfrak{C})\leq{\mathcal{P}}^{\prime}(\mathfrak{C})$ for all cylinders $\mathfrak{C}$. Then $x\cdot{\mathcal{P}}({\mathfrak{R}})\leq{\mathcal{P}}^{\prime}({\mathfrak{R}})$ holds for all measurable ${\mathfrak{R}}\subseteq sS^{\omega}$. *

Proof.

Let $\mathcal{C}=\{\mathfrak{C}\subseteq sS^{\omega}\mid\mathfrak{C}\text{ cylinder}\}$ denote the class of cylinders. This class generates an algebra $\mathcal{C}_{*}\supseteq\mathcal{C}$, which is the closure of $\mathcal{C}$ under finite union and complement. The classes $\mathcal{C}$ and $\mathcal{C}_{*}$ generate the same $\sigma$-algebra $\sigma(\mathcal{C})$. The class $\mathcal{C}_{*}$ is the set of finite disjoint unions of cylinders [5, Section 2]. Hence $x\cdot{\mathcal{P}}({\mathfrak{R}})\leq{\mathcal{P}}^{\prime}({\mathfrak{R}})$ for all ${\mathfrak{R}}\in\mathcal{C}_{*}$.

Define

[TABLE]

We have $\mathcal{C}\subseteq\mathcal{C}_{*}\subseteq\mathcal{Q}\subseteq\sigma(\mathcal{C})$. We show that $\mathcal{Q}$ is a monotone class, i.e., if ${\mathfrak{R}}_{1},{\mathfrak{R}}_{2},\ldots\in\mathcal{Q}$, then ${\mathfrak{R}}_{1}\subseteq{\mathfrak{R}}_{2}\subseteq\cdots$ implies $\bigcup_{i}{\mathfrak{R}}_{i}\in\mathcal{Q}$, and ${\mathfrak{R}}_{1}\supseteq{\mathfrak{R}}_{2}\supseteq\cdots$ implies $\bigcap_{i}{\mathfrak{R}}_{i}\in\mathcal{Q}$. Suppose ${\mathfrak{R}}_{1},{\mathfrak{R}}_{2},\ldots\in\mathcal{Q}$ and ${\mathfrak{R}}_{1}\subseteq{\mathfrak{R}}_{2}\subseteq\cdots$. Then:

[TABLE]

So $\bigcup_{i}{\mathfrak{R}}_{i}\in\mathcal{Q}$. Using the fact that measures are continuous from above, one can similarly show that if ${\mathfrak{R}}_{1},{\mathfrak{R}}_{2},\ldots\in\mathcal{Q}$ and ${\mathfrak{R}}_{1}\supseteq{\mathfrak{R}}_{2}\supseteq\cdots$ then $\bigcap_{i}{\mathfrak{R}}_{i}\in\mathcal{Q}$. Hence $\mathcal{Q}$ is a monotone class.

Now the monotone class theorem (see, e.g., [5, Theorem 3.4]) implies that $\sigma(\mathcal{C})\subseteq\mathcal{Q}$, thus $\mathcal{Q}=\sigma(\mathcal{C})$. Hence $x\cdot{\mathcal{P}}({\mathfrak{R}})\leq{\mathcal{P}}^{\prime}({\mathfrak{R}})$ for all ${\mathfrak{R}}\in\sigma(\mathcal{C})$. ∎

-C Proofs of Section V

Theorem 10. *

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be an MDP, and ${\varphi}=\mathtt{Reach}(T)$. Let $s_{0}\in S$ and $\sigma$ be a strategy with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$. Then there is an MD-strategy $\hat{\sigma}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\hat{\sigma}}({\varphi})=1$. *

Proof.

We can assume that $T=\{t\}$ for some $t\in S$. We can also assume that all states are almost-surely winning, since in order to achieve an almost-sure winning objective, the player must forever remain in almost-surely winning states.

Let $\epsilon_{1}:=1/2$. By Theorem 9 there exists an MD-strategy $\sigma_{1}$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{1}}({\varphi})\geq 1-\epsilon_{1}$. In fact, by the proof of Theorem 9 there exists a finite subset $V_{1}\subseteq S$ such that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{1}}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap V_{1}^{\omega})\geq 1-\epsilon_{1}$. Let $U_{1}$ denote the states that occur in those plays that are both contained in $\llbracket{\varphi}\rrbracket^{s_{0}}\cap V_{1}^{\omega}$ and induced by $\sigma_{1}$. Then ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{1}}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap U_{1}^{\omega})={\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{1}}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap V_{1}^{\omega})\geq 1-\epsilon_{1}$. By the definition of $U_{1}$, for all $s\in U_{1}$ the MD-strategy $\sigma_{1}$ induces a play from $s_{0}$ to $t$ via $s$. Hence we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{1}}(\llbracket{\varphi}\rrbracket^{s}\cap U_{1}^{\omega})>0$. Since $U_{1}\subseteq V_{1}$ is finite, there are $c>0$ and $\ell\in\mathbb{N}$ such that for all $s\in U_{1}$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{1}}(sU_{1}^{\leq\ell-1}\{t\}^{\omega})\geq c$, i.e., from any state in $U_{1}$ the probability that $t$ is reached in $\leq\ell$ steps is at least $c$.

Consider the MDP ${\mathcal{M}}_{1}$ obtained from ${\mathcal{M}}$ by fixing $\sigma_{1}$ on $U_{1}$ (i.e., in ${\mathcal{M}}_{1}$ the states in $U_{1}$ are random states). We argue that all states are almost-surely winning in ${\mathcal{M}}_{1}$. Indeed, let $s\in S$ be any state. Recall that $s$ is almost-surely winning in ${\mathcal{M}}$. Define an HR-strategy $\sigma$ in ${\mathcal{M}}_{1}$ as follows: first play a strategy that is almost-surely winning for $s$ in ${\mathcal{M}}$; if and when $U_{1}$ is entered and then left again (entering some state $s^{\prime}\in S\setminus U_{1}$) then forget the history and play again a strategy that is almost-surely winning for $s^{\prime}$ in ${\mathcal{M}}$; and so forth. This strategy $\sigma$ reaches $\{t\}$ with probability $1$ whenever the play stays outside of $U_{1}$. I.e., almost all plays that eventually always avoid $U_{1}$ reach $\{t\}$. Moreover, whenever the play enters $U_{1}$, the probability that $t$ is reached in $\leq\ell$ steps is at least $c$, i.e., there is a uniform bound. Thus almost all plays that enter $U_{1}$ infinitely often reach $\{t\}$. It follows that we have ${\mathcal{P}}_{{\mathcal{M}}_{1},s,\sigma}({\varphi})=1$.

Now we repeat the argument, but with ${\mathcal{M}}_{1}$ instead of ${\mathcal{M}}$ and with $\epsilon_{2}=1/4$ instead of $\epsilon_{1}$. This yields a set $U_{2}\supseteq U_{1}$ and an MD-strategy $\sigma_{2}$ that agrees with $\sigma_{1}$ on $U_{1}$ so that ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{2}}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap U_{2}^{\omega})={\mathcal{P}}_{{\mathcal{M}}_{1},s_{0},\sigma_{2}}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap U_{2}^{\omega})=1-\epsilon_{2}$. Similarly as before, obtain an MDP ${\mathcal{M}}_{2}$ from ${\mathcal{M}}_{1}$ by fixing $\sigma_{2}$ on $U_{2}$. Then repeat again, and so forth, with $\epsilon_{i}=1/2^{i}$ for $i=1,2,\ldots$

Define $U:=\bigcup_{i\geq 1}U_{i}$. Observe that on all $s\in U$ almost all (i.e., all except finitely many) strategies $\sigma_{i}$ agree. Let $\hat{\sigma}$ be an MD-strategy that on all states in $U$ agrees with almost all MD-strategies $\sigma_{i}$. By our construction we have ${\mathcal{P}}_{{\mathcal{M}},s_{0},\hat{\sigma}}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap U^{\omega})\geq 1-\epsilon$ for all $\epsilon>0$. Hence ${\mathcal{P}}_{{\mathcal{M}},s_{0},\hat{\sigma}}(\llbracket{\varphi}\rrbracket^{s_{0}}\cap U^{\omega})=1$. ∎

Proposition 11.*

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be an MDP, and $s_{0}\in S$, and $\sigma$ a strategy, and ${\mathit{C}ol}:S\to\{1,2\}$, and ${\varphi}=\mathtt{Parity}({\mathit{C}ol})$. Suppose ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma}({\varphi})=1$. Then there is an MD-strategy $\sigma^{\prime}$ with ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma^{\prime}}({\varphi})=1$. *

Proof.

We can assume that all states are almost-surely winning, since in order to achieve an almost-sure winning objective, the player must forever remain in almost-surely winning states. We provide an MD-strategy $\hat{\sigma}$ such that for all states $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\hat{\sigma}}({\varphi})=1$.

Set ${\varphi}^{\prime}=\mathtt{Reach}([S]^{{\mathit{C}ol}=2})$. Note that $\llbracket{\varphi}\rrbracket\subseteq\llbracket{\varphi}^{\prime}\rrbracket$. Since all states are almost-surely winning for ${\varphi}$, all states are almost-surely winning for ${\varphi}^{\prime}$. By Theorem 10 and Lemma 7 there is an MD-strategy $\hat{\sigma}$ such that for all states $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\hat{\sigma}}({\varphi}^{\prime})=1$. That is, $\hat{\sigma}$ reaches the set $[S]^{{\mathit{C}ol}=2}$ with probability $1$, regardless of the start state. It follows that it reaches, with probability $1$, the set $[S]^{{\mathit{C}ol}=2}$ infinitely often. Hence ${\mathcal{P}}_{{\mathcal{M}},s,\hat{\sigma}}({\varphi})=1$ holds for all $s\in S$. ∎

-D Proofs of Subsection VI-A

Proposition 13.*

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, and $T\subseteq S$, and ${\varphi}=\mathtt{Safety}(T)$. Define an MD-strategy $\sigma_{\mathit{opt\mathchar 45\relax av}}$ (for “optimal avoiding”) that, in each state $s$, picks a successor state with the largest value ${\mathtt{val}_{{\mathcal{M}}}(s)}=\sup_{\sigma\in\Sigma}{\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\varphi})$. Then for all states $s\in S$ we have ${\mathcal{P}}_{{\mathcal{M}},s,\sigma_{\mathit{opt\mathchar 45\relax av}}}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s)}$, i.e., $\sigma_{\mathit{opt\mathchar 45\relax av}}$ is uniformly optimal. *

Proof.

We can assume that $T$ is a sink. Fix a state $s_{0}$. Write $s_{0}s_{1}s_{2}\cdots\in sS^{\omega}$ for a random run, i.e., $s_{1},s_{2},\ldots$ denote random states. For any $n\in\mathbb{N}$ let $[{\sf X}^{n}\neg T]:s_{0}S^{\omega}\to\{0,1\}$ be the random variable that indicates if $s_{n}\not\in T$. Note that $[{\sf X}^{n}\neg T]\geq{\mathtt{val}_{{\mathcal{M}}}(s_{n})}$. Writing $\mathcal{E}_{{\mathcal{M}},s_{0},\sigma_{\mathit{opt\mathchar 45\relax av}}}$ for the expectation with respect to ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{\mathit{opt\mathchar 45\relax av}}}$, we have:

[TABLE]

A straightforward induction on $n$, using the definition of $\sigma_{\mathit{opt\mathchar 45\relax av}}$, shows that $\mathcal{E}_{{\mathcal{M}},s_{0},\sigma_{\mathit{opt\mathchar 45\relax av}}}({\mathtt{val}_{{\mathcal{M}}}(s_{n})})={\mathtt{val}_{{\mathcal{M}}}(s_{0})}$ holds for all $n\in\mathbb{N}$. Hence ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{\mathit{opt\mathchar 45\relax av}}}({\varphi})\geq{\mathtt{val}_{{\mathcal{M}}}(s_{0})}$. The converse inequality holds by the definition of the value. Hence ${\mathcal{P}}_{{\mathcal{M}},s_{0},\sigma_{\mathit{opt\mathchar 45\relax av}}}({\varphi})={\mathtt{val}_{{\mathcal{M}}}(s_{0})}$. ∎

Lemma 15. *

Let ${\mathcal{M}}=(S,S_{\Box},S_{\scriptscriptstyle\bigcirc},{\longrightarrow},P)$ be a finitely branching MDP, and ${\mathit{C}ol}:S\to\mathbb{N}$ a color function. Let $s$ be a state, and $\sigma$ a strategy, and $\tau<1$. Then ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}({\sf F}{\sf G}\neg{\it Safe}(\tau)\land{\sf F}{\sf G}[S]^{{\mathit{C}ol}=0})=0$. *

Proof.

For any $n\in\mathbb{N}$ define $Z_{n}=\left([S]^{{\mathit{C}ol}=0}\right)^{n}$. That is, $Z_{n}S^{\omega}$ is the event that the first $n$ visited states have color [math]. For any state $s\not\in{\it Safe}(\tau)$, let $n(s)\in\mathbb{N}$ be the smallest number such that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}(Z_{n(s)}S^{\omega})\leq(1+\tau)/2$. This is well-defined.

Let $L\subseteq S^{*}$ be the set of finite sequences $s_{0}s_{1}\cdots s_{n-1}$ such that $s_{0}\not\in{\it Safe}(\tau)$ and $n=n(s_{0})$ and $\forall i<n.\,s_{i}\in[S]^{{\mathit{C}ol}=0}\setminus{\it Safe}(\tau)$. We show for all $s\in S\setminus{\it Safe}(\tau)$ and all $k\in\mathbb{N}$ that ${\mathcal{P}}_{{\mathcal{M}},s,\sigma}(L^{k}S^{\omega})\leq\left(\frac{1+\tau}{2}\right)^{k}$. We proceed by induction on $k$. The case $k=0$ is trivial. For the induction step, let $k\geq 0$. We have:

[TABLE]

This completes the induction proof. Write ${\varphi}:={\sf G}\neg{\it Safe}(\tau)\land{\sf G}[S]^{{\mathit{C}ol}=0}$. We have for all $s\in S$:

[TABLE]

It follows:

[TABLE]

Thus we have:

[TABLE]

∎

-E Proofs of Subsection VI-B

Lemma 18. *

Let ${\mathcal{P}}$ be a probability measure over the sample space $\Omega$. Let $({\mathfrak{R}}_{i})_{i\in I}$ be a countable partition of $\Omega$ in measurable events. Let $E\subseteq\Omega$ be a measurable event. Suppose ${\mathcal{P}}({\mathfrak{R}}_{i}\cap E)={\mathcal{P}}({\mathfrak{R}}_{i})$ holds for all $i\in I$. Then ${\mathcal{P}}(E)=1$. *

Proof.

We have:

[TABLE]

∎