



\section{Introduction}


\noindent{\bf Markov decision processes.} A \emph{Markov decision process
(MDP)} is a model for systems that exhibit both probabilistic and 
nondeterministic behavior.
MDPs have been used to model and solve control problems 
for stochastic systems: there, nondeterminism represents the freedom of the controller 
to choose a control action, while the probabilistic component of the behavior 
describes the system response to control actions. 
MDPs have also been adopted as models for concurrent probabilistic systems, 
probabilistic systems operating in open environments~\cite{SegalaT}, and 
under-specified probabilistic systems \cite{BdA95}.

\smallskip\noindent{\bf System specifications.} 
The \emph{specification} describes the set of desired behaviors of
the system,
and is typically an $\omega$-regular set of paths.
Parity objectives are a canonical way to define such specifications in MDPs.  
They include reachability, safety, B\"uchi
and coB\"uchi
objectives as special cases.
Thus MDPs with parity objectives provide the theoretical framework to 
study problems such as the verification
and the control of stochastic systems.

\smallskip\noindent{\bf Perfect vs. partial observations.} 
Most results about MDPs make the hypothesis of \emph{perfect observation}. 
In this setting, the controller always knows, while interacting with the system (or MDP), 
the exact state of the MDP. 
In practice, this hypothesis is often unrealistic. 
For example, in the control of multiple processes, each process has only access 
to the public variables of the other processes, but not to their private variables.
In the control of hybrid systems~\cite{BouyerDMP03,DDR06}, or in automated planning~\cite{MadaniHC03}, 
the controller usually has noisy information about the state of the systems due to finite-precision sensors.
In such applications, MDPs with \emph{partial observation} (POMDPs) provide a more appropriate model.


\smallskip\noindent{\bf Qualitative and quantitative analysis.} 
Given an MDP with parity objective, the \emph{qualitative analysis} 
asks for the computation of the set of \emph{almost-sure winning} states
(resp., \emph{positive winning} states) in which the controller can 
achieve the parity objective with probability~1 (resp., positive probability);
the more general \emph{quantitative analysis} asks for the computation 
at each state of the maximal probability with which the controller can satisfy the 
parity objective. 
The analysis of POMDPs is considerably more complicated than the analysis of MDPs.
First, the decision problems for POMDPs usually lie in higher
complexity classes than their perfect-observation counterparts: for example,
the quantitative analysis of POMDPs with reachability and safety objectives is 
undecidable~\cite{Paz-Book}, whereas for MDPs with perfect observation, this question can be 
solved in polynomial time~\cite{luca-thesis,CJH04}.
Second, in the context of POMDPs, witness winning strategies for the controller need memory 
even for the simple objectives of safety and reachability. 
This is again in contrast to the perfect-observation case, where memoryless 
strategies suffice for all parity objectives.
Since the quantitative analysis of POMDPs is undecidable (even for computing 
approximations of the maximal probabilities~\cite{MadaniHC03}),
we study the qualitative analysis of POMDPs with parity objective and its subclasses.

\smallskip\noindent{\bf Contribution.}
For the qualitative analysis of POMDPs, the following results are known:
(a)~the problems of deciding if a state is almost-sure winning for 
reachability and B\"uchi objectives can be solved in EXPTIME~\cite{BBG08};
(b)~the problems for almost-sure winning for coB\"uchi objectives and 
positive winning for B\"uchi objectives are undecidable~\cite{BBG08,GIMBERT:2009:HAL-00403463:3}; and
(c)~the EXPTIME-completeness of almost-sure winning for 
safety objectives follows from the results on games with partial observation~\cite{CDHR07,BD08}.
Our new contributions are as follows:
\begin{enumerate}
\item  First, we show that
(a)~positive winning for reachability objectives is NLOGSPACE-complete;
and (b)~almost-sure winning for reachability and B\"uchi objectives, and positive winning for safety and 
coB\"uchi objectives are EXPTIME-hard\footnote{A very brief (two line) 
proof of EXPTIME-hardness is sketched in~\cite{dA99} (see the discussion before Theorem~\ref{thrm_complexity} 
for more details).\label{pos-safety-hard}}.
We also present a new proof that positive winning for safety and coB\"uchi objectives can be 
solved in EXPTIME\footnote{A different proof  that positive safety can be solved in EXPTIME is given in~\cite{GriponS09} (see the discussion after Theorem~\ref{thrm_pos_safe} for a comparison).}.  
It follows that almost-sure  winning for reachability and B\"uchi, 
and positive winning for safety and coB\"uchi, are EXPTIME-complete.
This completes the picture for the complexity of the qualitative analysis for POMDPs 
with parity objectives.
Moreover our new proofs of EXPTIME upper-bound proofs yield efficient and symbolic algorithms 
to solve positive winning for safety and coB\"uchi objectives in POMDPs.


\item Second, we present a complete characterization of the amount of memory required by 
pure (deterministic) and randomized strategies for the qualitative 
analysis of POMDPs.   
For the first time, we present optimal memory bounds (matching upper and lower 
bounds) for pure and randomized strategies: we show that
(a)~for positive winning of reachability objectives, randomized memoryless 
strategies suffice, while for pure strategies linear memory is necessary and 
sufficient; (b)~for almost-sure winning of safety, reachability, and 
B\"uchi objectives, and for positive winning of safety and coB\"uchi 
objectives,
exponential memory is necessary and sufficient for both pure and 
randomized strategies.


\end{enumerate}


\smallskip\noindent{\bf Related work.} Though MDPs have been widely 
studied under the hypothesis of perfect observations, there are a few works 
that consider POMDPs, e.g.,~\cite{PapaTsi,Littman-thesis} for several 
finite-horizon quantitative objectives.
The results of~\cite{BBG08} shows the upper bounds for almost-sure winning for 
reachability and B\"uchi objectives,
and the work of~\cite{CSV09} considers a subclass of {\sf POMDP} s with B\"uchi objectives 
and presents a PSPACE upper bound for the subclass.
The undecidability of almost-sure winning for coB\"uchi and positive winning for 
B\"uchi objectives is established by~\cite{BBG08,GIMBERT:2009:HAL-00403463:3}.
We present a solution to the remaining problems related to the qualitative 
analysis of POMDPs with parity objectives, and complete the picture.
Partial information has been studied in the context of two-player games~\cite{Reif84,CDHR07}, 
a model that is incomparable to MDPs, though some techniques (like the subset construction) can
be adapted to the context of POMDPs. More general models of stochastic games with partial information 
have been studied in~\cite{BGG09,GriponS09}, and lie in higher complexity classes. 
For example, a result of~\cite{BGG09} shows
that the decision problem for positive winning of safety objectives is 2EXPTIME-complete in the general model,
while for POMDPs, we show that the same problem is EXPTIME-complete.


\section{Definitions}\label{sec:definitions}

A \emph{probability distribution} on a finite set $A$ is a function
$\kappa: A \to [0,1]$ such that $\sum_{a \in A} \kappa(a) = 1$. 
The \emph{support} of $\kappa$ is the set ${\sf Supp}(\kappa) = \{a \in A \mid \kappa(a) > 0\}$.
We denote by ${\cal D}(A)$ the set of probability distributions on $A$. 


\smallskip\noindent{\em Games and MDPs.}
A \emph{two-player game structure} or a \emph{Markov decision process (MDP)} 
(\emph{of partial observation}) is a tuple $G=\tuple{L,\Sigma,{\delta},{\cal{O}}}$, where 
$L$ is a finite set of states, 
$\Sigma$ is a finite set of actions, 
${\cal{O}} \subseteq 2^L$ is a set of observations that partition\footnote{A slightly more general model with 
overlapping observations can be reduced in polynomial time to partitioning observations~\cite{CDHR07}.} the state space $L$. 
We denote by $o(\l)$ the unique observation $o \in {\cal{O}}$ such that $\l \in o$.
In the case of games, ${\delta} \subseteq L \times \Sigma \times L$ is a set of labeled transitions; 
in the case of MDPs, ${\delta}: L \times \Sigma \to {\cal D}(L)$ is a probabilistic transition function.
For games, we require that for all $\l \in L$ and all $\sigma \in \Sigma$, there exists 
$\l' \in L$ such that $(\l, \sigma, \l') \in {\delta}$. 
We refer to a game of partial observation as a {\sf POG}\/ and 
to an MDP of partial observation as a {\sf POMDP}.
We say that $G$  is a game or MDP of \emph{perfect observation}
if ${\cal{O}} = \{ \{\l\} \mid \l \in L \}$.
For $\sigma \in \Sigma$ and $s \subseteq L$,
define $\mathsf{Post}^G_\sigma(s) = \{\l' \in L \mid \exists \l \in s: (\l,\sigma,\l') \in {\delta} \}$
when $G$ is a game, and $\mathsf{Post}^G_\sigma(s) = \{\l' \in L \mid \exists \l \in s: {\delta}(\l,\sigma)(\l') >0 \}$
when $G$ is an MDP.

\medskip\noindent{\em Plays.}
Games are played in rounds in which Player~$1$ chooses
an action in $\Sigma$, and Player~$2$ resolves
nondeterminism by choosing the successor state;
in MDPs the successor state is chosen according to the probabilistic 
transition function.
A \emph{play} in $G$ is an infinite sequence 
$\pi=\l_0 \sigma_0 \l_1 \ldots \sigma_{n-1} \l_n \sigma_n \ldots$ such that 
$\l_{i+1} \in \mathsf{Post}^G_{\sigma_i}(\{\l_i\})$ for all $i \geq 0$.
The infinite sequence 
$o(\pi)=o(\l_0) \sigma_0 o(\l_1) \ldots \sigma_{n-1} o(\l_n) \sigma_{n} \ldots$
is the \emph{observation} of $\pi$.

The set of infinite plays in $G$ is denoted ${\sf Plays}(G)$,
and the set of finite prefixes $\l_0 \sigma_0 \ldots \sigma_{n-1} \l_n$ of plays is denoted ${\sf Prefs}(G)$.
A state $\l \in L$ is \emph{reachable} in $G$ if there exists a prefix 
$\rho \in {\sf Prefs}(G)$ such that ${\sf Last}(\rho) = \l$ where ${\sf Last}(\rho)$
is the last state of $\rho$.

\begin{comment}
\begin{lemma}\label{lem:knowledge}
Let $G=\tuple{L,\Sigma,{\delta},{\cal{O}}}$
be a {\sf POG}\/ or a {\sf POMDP}. 
For $\sigma \in \Sigma$,  $\l \in L$, and $\rho,\rho' \in {\sf Prefs}(G)$ with 
$\rho' = \rho \cdot \sigma \cdot \l$,
Then ${\sf K}(o(\rho')) = \mathsf{Post}^G_\sigma({\sf K}(o(\rho))) \cap o(\l)$.
\end{lemma}
\end{comment}


\medskip\noindent{\em Strategies.}
A \emph{pure strategy} in $G$ for Player~$1$ is a function 
$\alpha:{\sf Prefs}(G) \to \Sigma$. 
A \emph{randomized strategy} in $G$ for Player~$1$ is a function 
$\alpha:{\sf Prefs}(G) \to {\cal D}(\Sigma)$. 
A (pure or randomized) strategy $\alpha$ for Player~$1$ is 
\emph{observation-based} if for all prefixes $\rho,\rho' \in {\sf Prefs}(G)$, 
if $o(\rho) = o(\rho')$, then $\alpha(\rho)=\alpha(\rho')$. 
In the sequel, we are interested in the existence of observation-based
strategies for Player~$1$.
A \emph{pure strategy} in $G$ for Player~$2$ is a function 
$\beta:{\sf Prefs}(G) \times \Sigma \to L$
such that for all $\rho \in {\sf Prefs}(G)$ and all $\sigma \in \Sigma$, we have
$({\sf Last}(\rho), \sigma, \beta(\rho,\sigma)) \in {\delta}$.
A \emph{randomized strategy} in $G$ for Player~$2$ is a function 
$\beta:{\sf Prefs}(G) \times \Sigma \to {\cal D}(L)$
such that for all $\rho \in {\sf Prefs}(G)$, all $\sigma \in \Sigma$, and all 
$\l \in {\sf Supp}(\beta(\rho,\sigma))$, we have 
$({\sf Last}(\rho), \sigma, \l) \in {\delta}$.
We denote by ${\cal A}_G$, ${\cal A}_G^O$, and ${\cal B}_G$ the set of all 
Player-$1$ strategies, the set of all observation-based Player-$1$ 
strategies, and the set of all Player-$2$ strategies in $G$, respectively.

\newcommand{{\sf Mem}}{{\sf Mem}}

\smallskip\noindent{\em Memory requirement of strategies.} 
An equivalent definition of strategies is as follows.
Let ${\sf Mem}$ be a set called \emph{memory}.
An observation-based strategy with memory can be described by two functions,
a \emph{memory-update} function $\alpha_{u}$: ${\sf Mem} \times {\cal{O}} \times \Sigma \to {\sf Mem}$ 
that given the current memory, observation and the action updates the memory, 
and a \emph{next-action} function $\alpha_{n}$: ${\sf Mem} \times {\cal{O}} \to {\cal D}(\Sigma)$
that given the current memory and current observation specifies the probability 
distribution\footnote{For a pure strategy, the next-action
function specifies a single action rather than a probability distribution.} 
of the next action, respectively.
A strategy is \emph{finite-memory} if the memory ${\sf Mem}$ is finite
and the size of a finite-memory strategy $\alpha$ is the size $\abs{{\sf Mem}}$ of its memory.
A strategy is \emph{memoryless} if $\abs{{\sf Mem}} = 1$.
The memoryless strategies do not depend on the history of a play, 
but only on the current state. 
Memoryless strategies for player~1 can be viewed as functions
$\alpha$: ${\cal{O}} \to {\cal D}(\Sigma)$.

\begin{comment}
The \emph{outcome} of two deterministic strategies $\alpha$ (for
Player~$1$) and $\beta$ (for Player~$2$) in $G$ is the play $\pi=\l_0
\sigma_0 \l_1 \ldots \sigma_{n-1} \l_n \sigma_n \ldots \in {\sf Plays}(G)$
such that for all $i \geq 0$, we have $\sigma_i = \alpha(\pi(i))$ and
$\l_{i+1} = \beta(\pi(i),\sigma_i)$.  
This play is denoted $\mathsf{outcome}(G,\alpha,\beta)$.
The \emph{outcome} of two randomized strategies $\alpha$ (for
Player~$1$) and $\beta$ (for Player~$2$) in $G$ is the set of plays
$\pi=\l_0 \sigma_0 \l_1 \ldots \sigma_{n-1} \l_n \sigma_n \ldots \in
{\sf Plays}(G)$ such that for all $i \geq 0$, we have
$\alpha(\pi(i))(\sigma_i)>0$ and $\beta(\pi(i),\sigma_i)(\l_{i+1})>0$.
This set is denoted $\mathsf{outcome}(G,\alpha,\beta)$.
The \emph{outcome set} of the deterministic (resp.\ randomized)
strategy $\alpha$ for Player~$1$ in $G$ is the set
${\mathsf{Outcome}}_i(G,\alpha)$ of plays $\pi$ such that there exists a
deterministic (resp.\ randomized) strategy $\beta$ for
Player~$2$ with 
$\pi=\mathsf{outcome}(G,\alpha,\beta)$ 
(resp.\ $\pi\in\mathsf{outcome}(G,\alpha,\beta)$).
The outcome sets for Player~2 are defined symmetrically.


\smallskip\noindent{\em Outcome in imperfect-information games.}
In an imperfect-information game $G$,
the \emph{outcome} of two deterministic strategies $\alpha$ (for
Player~$1$) and $\beta$ (for Player~$2$)  is the play 
$\pi=s_0 s_1 s_2 \ldots \in {\sf Plays}(G)$ such that for all $i \geq 0$, 
we have $s_{i+1} = \alpha(\pi(i))$ if $s_i \in S_1$ and
$s_{i+1} = \beta(\pi(i))$ if $s_i \in S_2$.  
This play is denoted $\mathsf{outcome}(G,\alpha,\beta)$.
The \emph{outcome} of two randomized strategies $\alpha$ (for
Player~$1$) and $\beta$ (for Player~$2$) in $G$ is the set of plays
$\pi=s_0 s_1 s_2 \ldots \in {\sf Plays}(G)$ such that for all $i \geq 0$, we have
$\alpha(\pi(i))(s_{i+1})>0$ if $s_i \in S_1$ and 
$\beta(\pi(i))(s_{i+1})>0$ if $s_i \in S_2$.
This set is denoted $\mathsf{outcome}(G,\alpha,\beta)$.
In an imperfect-information game,
the \emph{outcome set} of the deterministic (resp.\ randomized)
strategy $\alpha$ for Player~$1$ in $G$ is the set
${\mathsf{Outcome}}_1(G,\alpha)$ of plays $\pi$ such that there exists a
deterministic (resp.\ randomized) strategy $\beta$ for
Player~$2$ with 
$\pi=\mathsf{outcome}(G,\alpha,\beta)$ 
(resp.\ $\pi\in\mathsf{outcome}(G,\alpha,\beta)$).
The outcome sets for Player~2 are defined symmetrically.

\smallskip\noindent{\em Outcomes in POMDPs.}
The outcome of a deterministic strategy $\alpha$ for Player~1 in a POMDP $G$ 
is the set of plays $\pi=s_0 s_1 s_2 \ldots \in {\sf Plays}(G)$ such that for 
all $i \geq 0$, we have $s_{i+1} = \alpha(\pi(i))$ if $s_i \in S_1$ and
$s_{i+1} \in E(s_i)$ if $s_i \in S_R$.
The outcome of a randomized strategy $\alpha$ for Player~1 in a POMDP 
is the set of plays $\pi=s_0 s_1 s_2 \ldots \in {\sf Plays}(G)$ such that for 
all $i \geq 0$, we have $  \alpha(\pi(i))(s_{i+1})>0$ if $s_i \in S_1$ and
$s_{i+1} \in E(s_i)$ if $s_i \in S_R$.  
The set of outcomes in a POMDP for a deterministic or a randomized 
strategy $\alpha$ is denoted as ${\mathsf{Outcome}}_1(G,\alpha)$.
\end{comment}


\begin{comment}
\medskip\noindent{\em Objectives.}
An \emph{objective} for $G$ is a set $\phi$ of infinite sequences of  observations and actions, 
that is, $\phi \subseteq ({\cal{O}}\times \Sigma )^\omega$. 
A play $\pi = \l_0 \sigma_0 \l_1 \ldots \sigma_{n-1} \l_n \sigma_n \ldots \in {\sf Plays}(G)$ 
\emph{satisfies} the objective $\phi$, denoted $\pi \models \phi$, if 
$\gamma^{-1}(\pi) \in \phi$.
Objectives are generally Borel measurable: 
a Borel objective is a Borel set
in the Cantor topology on $({\cal{O}}\times\Sigma)^\omega$~\cite{Kechris}.
We specifically consider reachability, safety,
B\"uchi, coB\"uchi, and parity objectives, all of them being Borel measurable.
The parity objectives are a canonical form to express all $\omega$-regular 
objectives~\cite{Thomas97}.
For a play $\pi=\l_0\sigma_0\l_1\dots$, we write 
$\mathsf{Inf}(\pi)$ for the set of observations that 
appear infinitely often in $\gamma^{-1}(\pi)$, that is,
$\mathsf{Inf}(\pi)=\{ o \in {\cal{O}} \mid \l_i \in \gamma(o)
\mbox{ for infinitely many } i\mbox{'s} \}$.

\begin{itemize}
\item \emph{Reachability and safety objectives.}
Given a set ${\cal T} \subseteq {\cal{O}}$ of target observations, the \emph{reachability} objective 
$\mathsf{Reach}({\cal T})$ requires that an observation in ${\cal T}$ be visited at least once, that is, 
$\mathsf{Reach}({\cal T})=\set{ \l_0 \sigma_0 \l_1 \sigma_1 \ldots 
\in {\sf Plays}(G) \mid \exists k \geq 0 \cdot \exists o \in {\cal T}:  \l_k \in o}$.
Dually, the \emph{safety} objective $\mathsf{Safe}({\cal T})$ requires that only observations in ${\cal T}$ be 
visited.
Formally,
$\mathsf{Safe}({\cal T})=\set{ \l_0 \sigma_0 \l_1 \sigma_1 \ldots 
\in {\sf Plays}(G) \mid \forall k \geq 0 \cdot \exists o \in {\cal T}:  \l_k \in \gamma(o)}$.
\item \emph{B\"uchi and coB\"uchi objectives.}
The \emph{B\"uchi} objective ${\sf B\ddot{u}chi}({\cal T})$ 
requires that an observation in ${\cal T}$ be visited infinitely often, 
that is,
${\sf B\ddot{u}chi}({\cal T})=\set{ \pi \mid \mathsf{Inf}(\pi) \cap {\cal T} \neq \emptyset}$.
Dually, the \emph{coB\"uchi} objective $\mathsf{coB\ddot{u}chi}({\cal T})$ requires that 
only observations in ${\cal T}$ be visited infinitely often.
Formally, $\mathsf{coB\ddot{u}chi}({\cal T}) =\set{\pi \mid \mathsf{Inf}(\pi) \subseteq {\cal T}}$.
\item\emph{Parity objectives.} 
For $d \in \mathbb{N}$, let $p:{\cal{O}} \to \set{0,1,\ldots,d}$ be a 
\emph{priority function}, 
which maps each observation to a nonnegative integer priority.
The \emph{parity} objective $\mathsf{Parity}(p)$ requires that the minimum priority 
that appears infinitely often be even.
Formally,
$\mathsf{Parity}(p)=\set{\pi \mid \min\set{ p(o) \mid o \in \mathsf{Inf}(\pi)} 
\mbox{ is even} }$.
\end{itemize}
Note that by definition, for all objectives $\phi$, if $\pi \models \phi$ 
and $\gamma^{-1}(\pi)=\gamma^{-1}(\pi')$, then $\pi'\models \phi$.
Given a B\"uchi objective ${\sf B\ddot{u}chi}({\cal T})$ consider the priority function 
$p:{\cal{O}} \to \set{0,1}$ such that $p(o)=0$ if $o \in {\cal T}$, and~1 
otherwise; then we have $\mathsf{Parity}(p)={\sf B\ddot{u}chi}({\cal T})$. 
Similarly, given a coB\"uchi objective $\mathsf{coB\ddot{u}chi}({\cal T})$ consider the 
priority function $p:{\cal{O}} \to \set{1,2}$ such that $p(o)=2$ if 
$o \in {\cal T}$, and~1 otherwise; then we have 
$\mathsf{Parity}(p)=\mathsf{coB\ddot{u}chi}({\cal T})$. 
Hence B\"uchi and coB\"uchi objectives are special cases of parity objectives
with two priorities.
\end{comment}


\medskip\noindent{\em Objectives.}
An \emph{objective} for $G$ is a set $\phi$ of infinite sequences of states and actions, 
that is, $\phi \subseteq (L \times \Sigma)^\omega$. 
We consider objectives that are Borel measurable, i.e., sets in the Cantor topology 
on $(L \times \Sigma)^\omega$~\cite{Kechris}.
We specifically consider reachability, safety,
B\"uchi, coB\"uchi, and parity objectives, all of them being Borel measurable.
The parity objectives are a canonical form to express all $\omega$-regular 
objectives~\cite{Thomas97}.
For a play $\pi=\l_0\sigma_0\l_1\dots$, we denote 
by $\mathsf{Inf}(\pi) = \{ \l \in L \mid \l = \l_i \mbox{ for infinitely many } i\mbox{'s} \}$ 
the set of states that appear infinitely often in $\pi$.

\begin{itemize}
 	\item \emph{Reachability and safety objectives.}
	Given a set ${\cal T} \subseteq L$ of target states, the \emph{reachability} objective 
	$\mathsf{Reach}({\cal T}) = \set{ \l_0 \sigma_0 \l_1 \sigma_1 \ldots \in {\sf Plays}(G) \mid \exists k \geq 0:  \l_k \in {\cal T}}$
	requires that a target state in ${\cal T}$ be visited at least once.
	Dually, the \emph{safety} objective $\mathsf{Safe}({\cal T}) = \set{ \l_0 \sigma_0 \l_1 \sigma_1 \ldots \in {\sf Plays}(G) \mid 
	\forall k \geq 0:  \l_k \in {\cal T}}$ 
	requires that only states in ${\cal T}$ be visited; the objective $\mathsf{Until}({\cal T}_1,{\cal T}_2) = 
	\{ \l_0 \sigma_0 \l_1 \sigma_1 \ldots \in {\sf Plays}(G) \mid \exists k \geq 0:  \l_k \in {\cal T}_2 \land \forall j \leq k: \l_j \in {\cal T}_1\}$
	requires that only states in ${\cal T}_1$ be visited before a state in ${\cal T}_2$ is visited;

	\item \emph{B\"uchi and coB\"uchi objectives.}

	The \emph{B\"uchi} objective ${\sf B\ddot{u}chi}({\cal T}) = \set{ \pi \mid \mathsf{Inf}(\pi) \cap {\cal T} \neq \emptyset}$ 
	requires that a state
	in ${\cal T}$ be visited infinitely often. 
	Dually, the \emph{coB\"uchi} objective $\mathsf{coB\ddot{u}chi}({\cal T}) =\set{\pi \mid \mathsf{Inf}(\pi) \subseteq {\cal T}}$ 
	requires that only states
	in ${\cal T}$ be visited infinitely often; and



	
	\item\emph{Parity objectives.} 
	For $d \in \mathbb{N}$, let $p:L \to \set{0,1,\ldots,d}$ be a 
	\emph{priority function} that maps each state
	to a nonnegative integer priority.
	The \emph{parity} objective $\mathsf{Parity}(p) = \set{\pi \mid \min\set{ p(\l) \mid \l \in \mathsf{Inf}(\pi)} 
	\text{ is even} }$ requires that the smallest priority that appears infinitely often be even.
\end{itemize}

Note that the objectives ${\sf B\ddot{u}chi}({\cal T})$ and $\mathsf{coB\ddot{u}chi}({\cal T})$ 
are special cases of parity objectives defined by respective priority functions
$p_1,p_2$ such that $p_1(\l) = 0$ and $p_2(\l) = 2$ if $\l \in {\cal T}$,
and $p_1(\l) = p_2(\l) = 1$ otherwise. 
An objective $\phi$ is \emph{visible} if it depends only on the observations;
formally, $\phi$ is visible if, whenever $\pi \in \phi$ 
and $o(\pi)=o(\pi')$, then $\pi'\in \phi$.
In this work, all our upper bound results are for the general parity objectives 
(not necessarily visible), and all the lower bound results for {\sf POMDP} s are for the 
special case of visible objectives (and hence the lower bounds also hold for general
objectives).


\begin{comment}
\smallskip\noindent{\em Outcomes and sure winning.}
In an imperfect-information game $G$,
the \emph{outcome} of two randomized strategies $\alpha$ (for
Player~$1$) and $\beta$ (for Player~$2$) in $G$ from a state $\l$ 
is the set of plays $\pi=\l_0 \sigma_0 \l_1 \ldots \sigma_{n-1} \l_n \sigma_n 
\ldots \in {\sf Plays}(G)$ such that (a)~$\l_0=\l$ and (b)~for all $i \geq 0$, we have
$\alpha(\pi(i))(\sigma_i)>0$ and $\beta(\pi(i),\sigma_i)(\l_{i+1})>0$, where $\pi(i)$
is the prefix of length $i$ of $\pi$.
This set is denoted $\mathsf{outcome}(G,\alpha,\beta,\l)$.
The \emph{outcome set} of the randomized strategy $\alpha$ for Player~$1$ 
in $G$ is the set ${\mathsf{Outcome}}_1(G,\alpha)$ of plays $\pi$ such that there exists a
randomized strategy $\beta$ for Player~$2$ with 
$\pi\in\mathsf{outcome}(G,\alpha,\beta)$.
The outcome sets for Player~2 are defined symmetrically.
The outcome of a randomized strategy $\alpha$ for Player~1 in a POMDP 
from a state $\l$ is the set of plays 
is the set of plays $\pi=\l_0 \sigma_0 \l_1 \ldots \sigma_{n-1} \l_n \sigma_n 
\ldots \in {\sf Plays}(G)$ such that (a)~$\l_0=\l$ and (b)~for all $i \geq 0$, we have
$\alpha(\pi(i))(\sigma_i)>0$ and ${\delta}(\l_i,\sigma_i)(\l_{i+1})>0$.
The set of outcomes in a POMDP for a randomized 
strategy $\alpha$ from $\l$ is denoted as ${\mathsf{Outcome}}_1(G,\alpha,\l)$.
Given an imperfect-information game or an POMDP $G$ and a state $\l$, 
a strategy $\alpha$ for Player~$1$ is \emph{sure winning} for the 
objective $\phi$ from $\l$ if ${\mathsf{Outcome}}_1(G,\alpha,\l) \subseteq \phi$
We also say that state $\l$ is sure winning for $\phi$.
\end{comment}


\medskip\noindent{\em Almost-sure and positive winning.}
An \emph{event} is a measurable set of plays, and 
given strategies $\alpha$ and $\beta$ for the two players (resp., a strategy
$\alpha$ for Player~1 in MDPs), the probabilities of events are uniquely defined~\cite{Var85}. 
For a Borel objective~$\phi$, we denote by $\mathrm{Pr}_{\l}^{\alpha,\beta}(\phi)$ 
(resp., $\mathrm{Pr}_{\l}^{\alpha}(\phi)$ for MDPs) the probability that $\phi$ is 
satisfied from the starting state~$\l$ given the strategies~$\alpha$ and 
$\beta$ (resp., given the strategy~$\alpha$).
Given a game $G$ and a state $\l$, a strategy $\alpha$ for 
Player~$1$ is \emph{almost-sure winning}
(resp., \emph{positive winning}) for the objective $\phi$ from $\l$ if 
for all randomized strategies $\beta$ for 
Player~$2$, we have $\mathrm{Pr}_{\l}^{\alpha,\beta}(\phi)=1$ 
(resp., $\mathrm{Pr}_{\l}^{\alpha,\beta}(\phi)>0$).
Given an MDP $G$ and a state $\l$, a strategy $\alpha$ for Player~$1$  
is almost-sure winning (resp. positive winning) for the objective $\phi$ from $\l$
if we have $\mathrm{Pr}_{\l}^{\alpha}(\phi)=1$ (resp., $\mathrm{Pr}_{\l}^{\alpha}(\phi)>0$).
We also say that state $\l$ is almost-sure winning, or positive winning for $\phi$ respectively.
We are interested in the problems of deciding the existence of an
observation-based strategy for Player~1 
that is almost-sure winning (resp., positive winning) from a given state $\l$.

\begin{comment}

\begin{theorem}[Determinacy] {\rm\cite{Mar75}}
\label{thrm:boreldeterminacy}
For all perfect-information game structures $G$
and all Borel objectives $\phi$,
either there exists a deterministic sure-winning strategy for Player~$1$ for 
the objective $\phi$, or there exists a deterministic sure-winning strategy 
for Player~$2$ for the complementary objective ${\sf Plays}(G) \setminus \phi$. 
\end{theorem}

Notice that deterministic strategies suffice for sure winning a game:
given a randomized strategy $\alpha$ for Player~$1$, let $\alpha^D$
be the deterministic strategy such that for all $\rho \in {\sf Prefs}(G)$, 
the strategy 
$\alpha^D(\rho)$ chooses an action from $\Supp(\alpha(\rho))$. 
Then ${\mathsf{Outcome}}_1(G,\alpha^D) \subseteq {\mathsf{Outcome}}_1(G,\alpha)$, and
thus, if $\alpha$ is sure winning, then so is~$\alpha^D$.
The result also holds for observation-based strategies
and for perfect-information games.
However, for almost winning, randomized strategies are more powerful 
than deterministic strategies as shown by Example~\ref{ex:example-one}.

\end{comment}



\section{Upper Bounds for the Qualitative Analysis of {\sf POMDP} s}
In this section, we present upper bounds for the qualitative analysis of 
{\sf POMDP} s.
We first describe the known results.
For qualitative analysis of MDPs, polynomial time upper bounds are known for all 
parity objectives~\cite{luca-thesis,CJH04}.
It follows from the results of~\cite{CDHR07,BBG08} that the decision 
problems for almost-sure winning for {\sf POMDP} s with reachability,
safety, and B\"uchi objectives can be solved in EXPTIME. 
It also follows from the results of~\cite{BBG08} that the decision problem 
for almost-sure winning with coB\"uchi objectives and for positive winning with B\"uchi objectives is undecidable if the
strategies are restricted to be pure, and the 
results of~\cite{GIMBERT:2009:HAL-00403463:3} shows that the problem 
remains undecidable even if randomized strategies are considered.
In this section, we complete the results on upper bounds for the 
qualitative analysis of {\sf POMDP} s: we present complexity upper bounds for the 
decision problems of positive winning with reachability, safety and 
coB\"uchi objectives. 
The following result for reachability objectives is simple, and 
for a complete and  systematic analysis we present the proof. 



\begin{theorem}\label{thrm_pos_reach}
Given a {\sf POMDP}\/ $G$ with a reachability objective and a starting state $\l$,
the problem of deciding whether there is a positive winning strategy from $\l$ 
in $G$ is NLOGSPACE-complete.
\end{theorem}
\begin{myProof}
The NLOGSPACE-completeness
result for positive reachability for MDPs follows from reductions 
to and from graph reachability.

\smallskip\noindent{\em Reduction to graph reachability.} Given a
{\sf POMDP}\/ $G= \tuple{L,\Sigma,{\delta},{\cal{O}}}$ 
and a set of target states ${\cal T} \subseteq L$,
consider the graph $\overline{G}=\tuple{L,E}$ where
$(\l,\l') \in E$ if there exists an action  $\sigma \in \Sigma$ such 
that ${\delta}(\l,\sigma)(\l')>0$.
Let $\l$ be a starting state, then the following assertions hold:
(a)~if there is a path $\pi$ in $\overline{G}$ from $\l$ to a state $t \in {\cal T}$,
then the randomized memoryless strategy for Player~1 in $G$ that plays
all actions uniformly at random ensures that the path $\pi$ is 
executed in $G$ with positive probability (i.e., ensures positive 
winning for $\mathsf{Reach}({\cal T})$ in $G$ from $\l$); and
(b)~if there is no path in $\overline{G}$ to reach $T$ from $\l$, then 
there is no strategy (and hence no observation-based strategy) for 
Player~1 in $G$ to achieve $\mathsf{Reach}({\cal T})$.
This shows that positive winning in {\sf POMDP} s can be decided in NLOGSPACE.
Graphs are a special case of {\sf POMDP} s and hence graph reachability 
can be reduced to reachability with positive probability in {\sf POMDP} s,
therefore the problem is NLOGSPACE-complete.
\end{myProof}





\noindent{\bf Positive winning for safety and coB\"uchi objectives.} 
We now show that the decision problem for positive winning 
with safety and coB\"uchi objectives for {\sf POMDP} s can be solved in EXPTIME.
We first show with an example that the simple approach of reduction to a 
perfect-information MDP by subset construction and solving the perfect 
information MDP with safety objective for positive winning does not yield 
the desired result.

\begin{example}
Consider the {\sf POMDP}\/ shown in \figurename~\ref{fig:subset-pomdp}: in every state
there exists only one action (which we omit for simplicity). In other words,
we have a partially observable Markov chain. 
States $0$, $1$, and $2$ are safe states and form observation $o_1$,
while state $3$ forms observation $o_2$ (which is not in the safe set). 
The state $0$ in $G$ is positive winning for the safety objective as with 
positive probability the state $2$ is reached and then the state $2$ 
is visited forever.
In contrast, consider the perfect information MDP $G^{{\sf K}}$ obtained from 
$G$ by subset construction (in this case $G^{{\sf K}}$ is a Markov chain).
In $G^{{\sf K}}$ from the state $\{1,2\}$, the possible successors are 
$1,2,$ and $3$, and since the observations are different at $1$ and $2$,
as compared to $3$, the successors of $\{1,2\}$ are $\{1,2\}$ and $\{3\}$. 
The reachable set of states in $G^{{\sf K}}$ from the state $\{0\}$ is shown 
in \figurename~\ref{fig:subset-pomdp}.
In $G^{{\sf K}}$,  the state $\{0\}$ is not positive winning: the state $\{3\}$
is the only recurrent state reachable from $\{0\}$ and hence from the 
state $\{0\}$, with probability~1, the state $\{3\}$ is reached and 
$\{3\}$ is not a safe state. Note that all this holds regardless of the
precise value of nonzero probabilities.
\begin{figure}[t]
 \begin{center}
    \input{figures/subset-pomdp.tex}
    \caption{A {\sf POMDP}\/ $G$ and the perfect information MDP $G^{{\sf K}}$ obtained by subset construction.}
    \label{fig:subset-pomdp}
 \end{center}
\end{figure}
{\nobreak\leavevmode\endof\eopsymbol}\smallskip}\global\def\qed{}
\end{example}

Our result for positive safety and coB\"uchi objectives is based on the computation 
of almost-sure winning states for safety objectives, and on the following lemma.






\begin{lemma}\label{theo:winningK-then-winning}
Let $G=\tuple{L,\Sigma,{\delta},{\cal{O}}}$ be a {\sf POMDP}\/ and let ${\cal T} \subseteq L$ be the set of target states.
If Player~$1$ has an observation-based strategy in $G$ to satisfy $\mathsf{Safe}({\cal T})$ with positive probability
from some state $\l$, then there exists a state $\l'$ such that (a) Player~$1$ has an observation-based strategy 
in $G$ to satisfy $\mathsf{Until}({\cal T},\{\l'\})$ with positive probability from $\l$, and (b) Player~$1$ has an observation-based 
almost-sure winning strategy in $G$ for $\mathsf{Safe}({\cal T})$ from $\l'$.
\end{lemma}

\begin{myProof}
We assume without loss of generality that the non-safe states in $G$ are absorbing.
Assume that Player~$1$ has an observation-based positive winning strategy $\alpha$ in $G$ for the
objective $\mathsf{Safe}({\cal T})$ from~$\l$, and towards a contradiction assume that for all states $\l'$
reachable from $\l$ with positive  probability using $\alpha$ in $G$, Player~$1$ has no observation-based 
almost-sure winning strategy for $\mathsf{Safe}({\cal T})$ from~$\l'$. 
A standard argument shows that from every such state $\l'$,
regardless of the observation-based strategy of Player~$1$, the probability to stay safe
within the next $n$ steps is at most $1 - \eta^n$ where $\eta$ is the least non-zero probability in $G$
and $n$ is the number of states in $G$.
Since under strategy $\alpha$, every reachable state has this property, the probability to stay 
safe within $k\cdot n$ steps is at most $(1 - \eta^n)^k$. 
This value tends to $0$ when $k \to \infty$, 
therefore the probability to stay safe using $\alpha$ from $\l$ is $0$, a contradiction. 
Hence, there exists a state $\l'$ which is almost-sure winning for Player~$1$ (using
observation-based strategy $\alpha$) and such that $\l'$ is reached with positive probability 
from $\l$ while staying in ${\cal T}$ (again using $\alpha$).
\end{myProof}

By Lemma~\ref{theo:winningK-then-winning}, positive winning states can be computed as the
set of states from which Player~$1$ can force with positive probability to reach an almost-sure winning state 
while visiting only safe states. Almost-sure 
winning states can be computed using the following subset construction. 

Given a {\sf POMDP}\/ $G=\tuple{L,\Sigma,{\delta},{\cal{O}}}$ and a set ${\cal T} \subseteq L$ of states, 
the \emph{knowledge-based subset construction} of $G$ is the game of perfect observation
\begin{center}
$G^{{\sf K}} = \tuple{\L, \Sigma, {\delta}^{{\sf K}}}$, 
\end{center}
where $\L = 2^L \backslash \{\emptyset\}$, and for all $s_1, s_2 \in \L$ (in particular $s_2 \neq \emptyset$)
and $\sigma \in \Sigma$, we have $(s_1, \sigma,s_2) \in {\delta}^{{\sf K}}$ iff there exists an observation
$o \in {\cal{O}}$ such that either $s_2 = \mathsf{Post}^G_\sigma(s_1) \cap o \cap {\cal T}$,
or $s_2 = (\mathsf{Post}^G_\sigma(s_1) \cap o) \setminus {\cal T}$. 
We refer to states in $G^{{\sf K}}$ as \emph{cells}.
The following result is established using standard techniques 
(see e.g., Lemma 3.2 and Lemma 3.3 in~\cite{CDHR07}).
and the fact that almost-sure winning and sure winning (sure winning is 
winning with certainty as compared to winning with probability~1 for 
almost-sure winning, see~\cite{CDHR07} for details of sure winning) 
coincide for safety objectives.

\begin{lemma}\label{lem:sure-almost-winning}
Let $G=\tuple{L,\Sigma,{\delta},{\cal{O}}}$ be a {\sf POMDP}\/ and ${\cal T} \subseteq L$ a set of target states.
Let $G^{{\sf K}}$ be the subset construction and $F_{{\cal T}} = \{s \subseteq {\cal T}\}$ the set of safe cells.
Player~$1$ has an almost-sure winning observation-based strategy in $G$ for $\mathsf{Safe}({\cal T})$ from $\l$
if and only if  
Player~$1$ has an almost-sure winning strategy in $G^{{\sf K}}$ for $\mathsf{Safe}(F)$ from cell $\{\l\}$.
\end{lemma}

\begin{remark}
Lemma~\ref{lem:sure-almost-winning} also holds if we replace almost-sure winning
by sure winning, since for safety objectives almost-sure and sure winning 
coincide.
\end{remark}

\begin{comment}
\begin{lemma}\label{theo:winningK-then-winning}
Let $G=\tuple{L,\Sigma,{\delta},{\cal{O}}}$ be a {\sf POMDP} and $G^{{\sf K}}$ the MDP constructed by subset construction.
Let ${\cal T}$ be the set of target observations, and let 
$F =\set{s \subseteq L \mid s \subseteq \gamma(o), o \in {\cal T}}$. 
Let $W$ be the set of cells $s$ in $G^{{\sf K}}$ such that Player~1 has a positive winning strategy 
from $s$ for the objective $\mathsf{Safe}(F)$.
The following assertions hold:
\begin{enumerate}
\item If the initial knowledge for Player~$1$ is a cell in $W$ in $G$, then there is an 
observation-based strategy in $G$ to satisfy $\mathsf{Safe}({\cal T})$ with positive probability.
\item If the initial knowledge for Player~1 is a cell in $2^L \setminus W$, then there is no
observation-based strategy for Player~1 to satisfy $\mathsf{Safe}({\cal T})$ with positive 
probability.
\end{enumerate}
\end{lemma}

\begin{myProof}
We present the proof in two parts.
Without loss of generality, we assume that every state with observations not in ${\cal T}$ is absorbing, and hence
cells in $2^L \setminus F$ are also absorbing.
 
\begin{enumerate}
\item Since $G^{{\sf K}}$ is an MDP of perfect observation, it follows that if there is a 
positive winning strategy for the safety objective $\mathsf{Safe}(F)$, then there is a pure 
memoryless strategy in $G^{{\sf K}}$ that is also positive winning for $\mathsf{Safe}(F)$~\cite{luca-thesis,CJH04}. 
Let $\alpha^{{\sf K}}$ be a pure memoryless positive winning strategy for Player~$1$ 
in $G^{{\sf K}}$ for the objective $\mathsf{Safe}(F)$ from the cells in $W$.
Define $\alpha^o$ a strategy for Player~$1$ in $G$ as follows: 
for every $\rho \in {\sf Prefs}(G)$, let $\alpha^o(\rho) = \alpha^{{\sf K}}(\rho^{{\sf K}})$
where $\rho^{{\sf K}}$ is defined from $\rho= \l_0 \sigma_0 \l_1 \dots \sigma_{n-1} \l_n$ 
by $\rho^{{\sf K}} = s_0 \sigma_0 s_1 \dots \sigma_{n-1} s_n$ 
where $s_i = {\sf K}(\gamma^{-1}(\l_0 \sigma_0 \l_1 \dots \sigma_{i-1} \l_i))$ for each $0 \leq i \leq n$.
Clearly, $\alpha^o$ is a pure observation-based strategy as 
$\gamma^{-1}(\rho) = \gamma^{-1}(\rho')$ implies $\rho^{{\sf K}} = \rho'^{{\sf K}}$.
Since the strategy $\alpha^{{\sf K}}$ is pure memoryless in $G^{{\sf K}}$, the 
strategy $\alpha^o$ is a finite-memory pure strategy with at most exponential
($2^{O(\abs{L})}$) memory.
Once the strategy $\alpha^{{\sf K}}$ is fixed in $G^{{\sf K}}$ we obtain a Markov chain. 
Since $\alpha^{{\sf K}}$ is positive winning, it follows that in the Markov chain 
obtained, from every cell in $W$ a closed recurrent set $C \subseteq W \subseteq F$ 
is reached with positive probability.
Hence if the strategy $\alpha^o$ constructed from $\alpha^{{\sf K}}$ 
is fixed in $G$ and the initial knowledge is 
a cell in $W$, then it ensures the following:
(a)~there exists a subset $O$ of states in $L$ that are labeled by observations in ${\cal T}$,
and once the set $O$ is reached, then the set $O$ is never left (this corresponds to the 
closed recurrent set $C$ in $G^{{\sf K}}$); and
(b)~with positive probability a path is executed that goes through only states labeled by 
observations in ${\cal T}$, and reaches the set $O$.
Hence the strategy $\alpha^o$ is positive winning in $G$, given the initial knowledge 
is a cell in~$W$.


\item Let $\overline{W}=2^L \setminus W$ be the set of cells in $G^{{\sf K}}$ such that there is no 
positive winning strategy for the objective $\mathsf{Safe}(F)$.
Hence from any cell in $\overline{W}$, for any knowledge-based strategy for Player~1 
the following property hold: the play remains in $\overline{W}$ and 
reaches cells in $\overline{W} \setminus F$ with some positive probability 
$\eta>0$ in $2^{\abs{L}}$ steps.
It follows if the initial knowledge for Player~1 in $G$ is a cell in 
$\overline{W}$, then for any observation-based strategy in $G$, 
the probability to reach an observation in ${\cal{O}} \setminus{\cal T}$ in 
$k \cdot 2^{\abs{L}}$ steps is at least $1-(1-\eta')^k$, for some $\eta'>0$.
As $k$ goes to $\infty$, the value of $1-(1-\eta')^k$ goes to~1.
Hence the probability to stay safe in ${\cal T}$ is~0 for any observation-based
Player~1 strategy, with the initial knowledge in $\overline{W}$.
\end{enumerate}
The result follows.
\end{myProof}




In the case of {\sf POMDP} s, given the starting state is a state $\l \in L$, the 
initial knowledge is the cell $\gamma^{-1}(\l)$.
Hence the decision problem for positive winning in {\sf POMDP} s with safety
objectives can be solved by solving the same problem for MDPs with perfect 
observation of exponential size. 
Since positive winning in MDPs of perfect observation with safety objectives 
can be solved in polynomial time~\cite{luca-thesis,CJH04}, 
we obtain an EXPTIME upper bound for {\sf POMDP} s.
\end{comment}








\begin{theorem}\label{thrm_pos_safe} 
Given a {\sf POMDP}\/ $G$ with a safety objective and a starting state $\l$,
the problem of deciding whether there exists a positive winning observation-based 
strategy from $\l$ can be solved in EXPTIME.
\end{theorem}

\begin{myProof}
The almost-sure winning states in $G$ for a safety objective (with observation-based strategy) 
can be computed in exponential time using the subset construction (by Lemma~\ref{lem:sure-almost-winning} and~\cite{CDHR07}).
Then, given the set $W$ of cells that are almost-sure winning in $G^{{\sf K}}$, let ${\cal T}_W = \{\l \in s \mid s \in W \}$ 
be the almost-sure winning states in $G$. We can compute the states from which Player~$1$
can force ${\cal T}_W$ to be reached with positive probability while staying within the safe states
using standard graph analysis algorithms, as in Lemma~\ref{thrm_pos_reach}. Clearly such states
are positive winning in $G$, and by Lemma~\ref{theo:winningK-then-winning} all 
positive winning states in $G$ are obtained in this way. This gives an EXPTIME
algorithm to decide from which states there exists a positive winning observation-based 
strategy for safety objectives.
\end{myProof}

\noindent{\bf Algorithms.}
The complexity bound of Theorem~\ref{thrm_pos_safe} has been established previously in~\cite{GriponS09},
using an extension of the knowledge-based subset construction which is not necessary (where the state space is $L \times 2^L$).
Our proof is simpler and also yield efficient and symbolic algorithms: efficient anti-chain based symbolic 
algorithm for almost-sure winning for safety objectives can be obtained from~\cite{CDHR07}, and positive reachability is 
simple graph reachability. 



\begin{comment}
\noindent{\bf Positive winning for coB\"uchi objectives.} 

We now 
show that we can solve positive winning  for {\sf POMDP} s with coB\"uchi objectives
by iteratively solving for positive winning with reachability 
and safety objectives in {\sf POMDP} s.
Let $G$ be a {\sf POMDP}\/ with a coB\"uchi objective $\mathsf{coB\ddot{u}chi}({\cal T})$, 
where ${\cal T} \subseteq {\cal{O}}$.
We construct the MDP $G^{{\sf K}}$ of perfect observation, and let 
$C=\set{s \subseteq L \mid s \subseteq \gamma(o), o \in {\cal T}}$.
We consider the positive winning for the coB\"uchi objective $\mathsf{coB\ddot{u}chi}(C)$
in $G^{{\sf K}}$. 
The set $W$ of positive winning cells in $G^{{\sf K}}$ is obtained as follows: 
\begin{enumerate}
\item let $W_0=\emptyset$;
\item we obtain $W_{i+1}$ from $W_i$ as follows: 
let $Z_i$ be the set of cells in $G^{{\sf K}}$ such that Player~1 can ensure 
staying safe in $C \cup W_i$ with positive probability, and $W_{i+1}$ is obtained as the 
set of states that can reach $Z_i$ with positive probability.
\end{enumerate}
It follows from above that if the current knowledge is a cell in $W_{i+1}$, then 
either $W_i$ is reached with positive probability or the play eventually only 
visits states in $C$.
It follows from the proof of correctness for positive winning in {\sf POMDP} s with 
safety objective, that if the current knowledge is a cell in $W_{i+1}$,
then there is an observation-based strategy for Player~1 to ensure 
$\mathsf{coB\ddot{u}chi}({\cal T})$. 
Let $W$ be the fixpoint of the iteration, i.e., for some $k$ we have 
$W_{k}= W_{k+1}= W$.
Let $\overline{W}=2^L \setminus W$. 
Then the following assertions hold.
\begin{enumerate}
\item From any cell $\overline{W}$,  Player~1 cannot ensure positive 
probability to stay safe in $C \cup W$.
Otherwise, such a cell would have been included in $Z_{k+1}$ and hence 
it would contradict that $W_k=W_{k+1}$.
Hence for every Player~1 knowledge-based strategy, if the initial knowledge 
is a cell in $\overline{W}$, then the set $(2^L\setminus C) \cap \overline{W}$ is reached 
with probability~1.
It follows that if the current knowledge is a cell in $\overline{W}$, then for any 
observation-based strategy in $G$, observations in the set 
${\cal{O}} \setminus {\cal T}$ is reached with probability~1.

\item From every cell $\overline{W}$, Player~1 cannot ensure to reach $W$ with
positive probability.
Hence for every knowledge-based strategy for Player~1, if the initial knowledge
is a cell in $\overline{W}$, then the play stays safe in $\overline{W}$ with probability~1.
Hence given a knowledge-based strategy for Player~1, from every cell in 
$\overline{W}$, the set $(2^L \setminus C) \cap \overline{W}$ is reached with 
probability~1 and the game stays safe in $\overline{W}$.
It follows that the set $(2^L \setminus C) \cap \overline{W}$ is visited 
infinitely often with probability~1, and this ensures that from $\overline{W}$ 
the coB\"uchi condition is falsified with probability~1.
Hence if the initial knowledge is a cell in $\overline{W}$, then for any 
observation-based strategy in $G$, the coB\"uchi objective 
$\mathsf{coB\ddot{u}chi}({\cal T})$ is falsified with probability~1.
\end{enumerate}
Hence by iteratively solving positive winning in {\sf POMDP} s with reachability 
and safety objectives, the positive winning in {\sf POMDP} s with coB\"uchi 
objectives can be achieved.
Hence we have the following result.
\end{comment}


The positive winning states for a coB\"uchi objective are computed as
the set of almost-sure winning states for safety that can be reached with positive probability.

\begin{theorem}\label{thrm_pos_cobuchi} 
Given a {\sf POMDP}\/ $G$ with a coB\"uchi objective and a starting state $\l$,
the problem of deciding whether there exists a positive winning observation-based strategy from $\l$ 
can be solved in EXPTIME.
\end{theorem}

\begin{myProof}
Let $\mathsf{coB\ddot{u}chi}({\cal T})$ be a coB\"uchi objective in $G = \tuple{L,\Sigma,{\delta},{\cal{O}}}$.
As in the proof of Theorem~\ref{thrm_pos_safe}, we compute in exponential time 
the set ${\cal T}_W$ of almost-sure winning states in $G$ for $\mathsf{Safe}({\cal T})$,
and using Lemma~\ref{thrm_pos_reach} the set $W$ of states from which Player~$1$
is positive winning for $\mathsf{Reach}({\cal T}_W)$. Clearly, all states in $W$ are positive
winning for $\mathsf{coB\ddot{u}chi}({\cal T})$, and $W$ can be computed in EXPTIME. 
We argue that for all states $\l \not \in W$, Player~$1$ is not positive winning
for $\mathsf{coB\ddot{u}chi}({\cal T})$ from $\l$. Note that ${\delta}(\l,\sigma)(\l') = 0$
for all $\l \not \in W$, $\l' \in W$, and $\sigma \in \Sigma$, and thus there are no 
almost-sure winning states for $\mathsf{Safe}({\cal T})$ in $G$ reachable from $L \setminus W$ with positive probability, 
regardless of the strategy of Player~$1$. Therefore, by an argument similar to the proof of 
Lemma~\ref{theo:winningK-then-winning}, for all observation-based strategies for Player~$1$,
from every state $\l \not \in W$, the set $L \setminus {\cal T}$ is reached with probability~$1$
and the event ${\sf B\ddot{u}chi}(L \setminus {\cal T})$ has probability~$1$. The result follows.
\end{myProof}

\section{Lower Bounds for the Qualitative Analysis of {\sf POMDP} s}

In this section we present lower bounds for the qualitative analysis of
{\sf POMDP} s. We first present the lower bounds  for MDPs with 
perfect observation.


\smallskip\noindent{\bf Lower bounds for MDPs with perfect observations.}
In the previous section we argued that for reachability objectives even 
in {\sf POMDP} s the positive winning problem is NLOGSPACE-complete.
For safety objectives and almost-sure winning it is known that an MDP can 
be equivalently considered as a game where Player~2 makes choices of 
the successors from the support of the probability distribution of the 
transition function, and the almost-sure winning set is the same in the MDP and 
the game. Similarly, there is a reduction of games of perfect observations 
to MDPs of perfect observation for almost-sure winning with safety objectives.
The problem of almost-sure winning in games of perfect observation is
alternating reachability and is PTIME-complete~\cite{Beeri,Immerman81},.
It follows that almost-sure winning for safety objectives in MDPs is 
PTIME-complete.
We now show that the almost-sure winning problem for reachability and 
the positive winning problem for safety objectives is PTIME-complete for
MDPs with perfect observation.


\smallskip\noindent{\bf Reduction from the {\sc Circuit-Value-Problem}.}
Let $N=\set{1,2,\ldots,n}$ be a set of AND and OR gates, 
and $I$ be a set of inputs. 
The set of inputs is partitioned into $I_0$ and $I_1$; $I_0$ is the set of
inputs set to~0 (false) and $I_1$ is the set of inputs set to~1 (true).
Every gate receives two inputs and produces one output; 
the inputs of a gate are outputs of another gate or an input from
the set $I$.
The connection graph of the circuit must be acyclic.
Let the gate represented by the node~1 be the output node. 
The {\sc Circuit-Value-Problem} (CVP) is to decide whether the output is~1 or~0. This problem is PTIME-complete.
We present a reduction of CVP to MDPs with perfect observation for 
almost-sure winning with reachability, and positive winning with safety 
objectives.
\begin{enumerate}
\item \emph{Almost-sure reachability.} Given the CVP, we construct the MDP 
of perfect observation as follows:
(a)~the set of states is $N \cup I$;
(b)~the action set is $\Sigma=\set{l,r}$;
(c)~the transition function is as follows: every node in $I$ is absorbing,
and for a state that represents a gate, (i)~if it is an OR gate, then for the 
action $l$ the left input gate is chosen with probability~1, and for the 
action $r$ the right input gate is chosen with probability~1; and 
(ii)~if it is an AND gate, then irrespective of the action, the left and right 
input gate are chosen with probability~$1/2$.
The output of the CVP from node~1 is~1 iff the set $I_1$ is reached from the state~1
in the MDP with probability~1 (i.e., the state~1 is almost-sure winning for the 
reachability objective $\mathsf{Reach}(I_1)$.)

\item \emph{Positive safety.} For positive winning with safety objectives, we 
take the CVP,  apply the same reduction as for almost-sure 
reachability with the following modifications:
every state in $I_0$ remains absorbing and from every state in $I_1$ the next
state is the starting state~1 with probability~1 irrespective of the action.
The set of safety target is the set $I_1 \cup N$. 
If the output of the CVP problem is~1, then from the starting state the set 
$I_1$ is reached with probability~1, and hence the safety objective with the
target $N \cup I_1$ is ensured with probability~1.
If the output of the CVP problem is~0, then from the starting state the set 
$I_0$ is reached with positive probability $\eta>0$ in $n$ steps against 
all strategies. 
Since from every state in $I_1$ the successor state is the state $1$, 
it follows that the probability to reach $I_0$ from the starting state~1 in 
$k\cdot (n+1)$ steps is at least $1-(1-\eta)^k$, and this goes to~1 as 
$k$ goes to $\infty$. 
Hence it follows that from state~1, the answer to the positive winning for
the safety objective $\mathsf{Safe}(N \cup I_1)$ is YES iff the output to the CVP 
is~1.
\end{enumerate}
From the above results it also follows that almost-sure and positive B\"uchi and 
coB\"uchi objectives are PTIME-hard (and PTIME-completeness follows from the 
known polynomial time algorithms for qualitative analysis of MDPs with parity 
objectives~\cite{CJH04,luca-thesis}).

\begin{theorem}
Given an MDP $G$ of perfect observation, the following assertions hold:
(a)~the positive winning problem for reachability objectives is NLOGSPACE-complete, and 
the positive winning problem for safety, B\"uchi, coB\"uchi and parity objectives is PTIME-complete; and 
(b)~the almost-sure winning problem for reachability, safety, B\"uchi, coB\"uchi and parity objectives is PTIME-complete. 
\end{theorem}



\noindent{\bf Lower bounds for {\sf POMDP} s.}
We have already shown that positive winning with reachability objectives
in {\sf POMDP} s is NLOGSPACE-complete.
As in the case of MDPs with perfect observation, for safety objectives and 
almost-sure winning  a {\sf POMDP}\/ can be equivalently considered as a game of 
partial observation where Player~2 makes choices of the successors from the 
support of the probability distribution of the transition function, and 
the almost-sure winning set is the same in the {\sf POMDP}\/ and the game. 
Since the problem of almost-sure winning in games of partial observation with safety
objective is EXPTIME-complete~\cite{BD08}, the EXPTIME-completeness 
result follows.
We now show that almost-sure winning with reachability objectives and positive 
winning with safety objectives is EXPTIME-complete.
Before the result we first present a discussion on polynomial-space 
alternating Turing machines (ATM).


\noindent{\em Discussion.} Let $M$ be a polynomial-space ATM and let $w$ be an input word.
Then, there is an exponential bound on the number of configurations of the machine. 
Hence if $M$ can accept the word $w$, then it can do so within some $k_{\abs{w}}$ steps, 
where $\abs{w}$ is the length of the word $w$, and $k_{\abs{w}}$ is bounded by an exponential in $\abs{w}$. 
We construct an equivalent polynomial-space ATM $M'$ that behaves as $M$ but keeps track (in polynomial space) 
of the number of steps executed by $M$, and given a word $\abs{w}$, 
if the number of steps reaches $k_{\abs{w}}$ without accepting, then the word is rejected.
The machine $M'$ is equivalent to $M$ and reaches the accepting or rejecting states in a number
of steps bounded by an exponential in the length of the input word.
The problem of deciding, given a polynomial-space ATM $M$ and a word $w$, whether $M$ accepts $w$ is 
EXPTIME-complete.


\smallskip\noindent{\bf Reduction from Alternating PSPACE Turing machine.} 
Let $M$ be a polynomial-space ATM such that for every input word $w$,
the accepting or the rejecting state is reached within exponential steps in $\abs{w}$.
A polynomial-time reduction $R_G$ of a polynomial-space ATM $M$ and an input word $w$ to a 
game $G = R_G(M,w)$ of partial observation is given in~\cite{CDHR07} such that 
(a)~there is a special accepting state in $G$, and
(b)~$M$ accepts $w$ iff there is an observation-based strategy for Player~1 in $G$ 
to reach the accepting state with probability~1.
If the above reduction is applied to $M$, then the game structure satisfies the 
following additional properties: there is a special rejecting state that is absorbing, 
and for every observation-based strategy for Player~1, either 
(a)~against all Player~2 strategies the 
accepting state is reached with probability~1; or (b)~there is a pure Player~2 
strategy that reaches the rejecting state with positive probability $\eta>0$ in 
$2^{\abs{L}}$ steps and the accepting or the rejecting state is reached with 
probability~1 in $2^{\abs{L}}$ steps.
We now present the reduction to {\sf POMDP} s:
\begin{enumerate}

\item \emph{Almost-sure winning for reachability.}
Given a polynomial-space ATM $M$ and $w$ an input word, let $G=R_G(M,w)$. We construct a {\sf POMDP}\/ $G'$ from 
$G$ as follows: we only modify the transition function in $G'$ by uniformly choosing over
the successor choices. 
Formally, for a state $\l \in L$ and an action $\sigma \in \Sigma$ 
the probabilistic transition function ${\delta}'$ in $G'$ is as follows:
\[
{\delta}'(\l,\sigma)(\l') = 
\begin{cases}
0 & (\l,\sigma,\l') \not \in {\delta}; \\
1/ \abs{\set{\l_1 \mid (\l,\sigma,\l_1) \in {\delta}}} & (\l,\sigma,\l') \in {\delta}.
\end{cases}
\]
Given an observation-based strategy for Player~1 in $G$, we consider the same
strategy in $G'$: 
(1)~if the strategy reaches the accepting state with probability~1
against all Player~2 strategies in $G$, then the strategy ensures that in $G'$
the accepting state is reached with probability~1; and
(2)~otherwise there is a pure Player~2 strategy $\beta$ in $G$ that ensures the rejecting
state is reached in $2^{\abs{L}}$ steps with probability $\eta>0$, and with 
probability at least $(1/\abs{L})^{2^{\abs{L}}}$ the choices of the successors of strategy $\beta$ 
is chosen in $G'$, and hence the rejecting state is reached with probability at least
$(1/\abs{L})^{2^{\abs{L}}} \cdot \eta>0$. 
It follows that in $G'$ there is an observation-based strategy for almost-sure winning 
the reachability objective with target of the accepting state iff there is such a 
strategy in $G$.
The result follows.

\item \emph{Positive winning for safety.} 
The reduction is same as above. We obtain the {\sf POMDP}\/ $G''$ from the {\sf POMDP}\/ $G'$ above 
by making the following modification: from the state accepting, the {\sf POMDP}\/ goes back to the 
initial state with probability~1.
If there is an observation-based strategy $\alpha$ for Player~1 in $G'$ to reach the 
accepting state, then repeating the strategy $\alpha$ each time the accepting state is 
visited, it can be ensured that the rejecting state is reached with probability~0.
Otherwise, against every observation-based strategy for Player~1, the probability to 
reach  the rejecting state in $k \cdot(2^{\abs{L}}+1)$ steps is at least 
$1-(1-\eta')^k$, where $\eta'=\eta \cdot (1/\abs{L})^{2^{\abs{L}}}>0$ (this is 
because there is a probability to reach the rejecting state with probability at least 
$\eta'$ in $2^{\abs{L}}$ steps, and unless the rejecting state is reached the starting state 
is again reached within $2^{\abs{L}}+1$ steps).
Hence the probability to reach the rejecting state is~1.
It follows that $G'$ is almost-sure winning for the reachability objective with the 
target of the accepting state iff in $G''$ there is an observation-based strategy 
for Player~1 to ensure that the rejecting state is avoided with positive probability.
This completes the proof of correctness of the reduction.
\end{enumerate}

A very brief (two line proof) sketch was presented as the proof of Theorem~1
of~\cite{dA99} to show that positive winning in {\sf POMDP} s with safety objectives
is EXPTIME-hard. 
We were unable to reconstruct the proof: the proof suggested to simulate a 
nondeterministic Turing machine. 
The simulation of a polynomial-space nondeterministic Turing machine only shows 
PSPACE-hardness, and the simulation of a nondeterministic EXPTIME Turing 
machine would have shown NEXPTIME-hardness, and an EXPTIME upper bound is known
for the problem. Our proof presents a different and detailed proof of the 
result of Theorem~1 of~\cite{dA99}.
Hence we have the following theorem, and the results are summarized in Table~\ref{tab1}. 

\begin{theorem}\label{thrm_complexity}
Given a {\sf POMDP}\ $G$, the following assertions hold:
(a)~the positive winning problem for reachability objectives is NLOGSPACE-complete,
the positive winning problem for safety and coB\"uchi objectives is EXPTIME-complete, 
and the positive winning problem for B\"uchi and parity objectives is undecidable; and
(b)~the almost-sure winning problem for reachability, safety and B\"uchi objectives is 
EXPTIME-complete, and the almost-sure winning problem for coB\"uchi and parity objectives is 
undecidable.
\end{theorem}
\begin{myProof}
The results are obtained as follows.
\begin{enumerate}
\item {\em Positive winning.}
The NLOGSPACE-completeness for positive winning with reachability objectives is 
Theorem~\ref{thrm_pos_reach}.
Our reduction from Alternating PSPACE Turing machine shows EXPTIME-hardness for positive 
winning with safety (and hence the lower bound also follows for coB\"uchi objectives), 
and the upper bounds follow from Theorem~\ref{thrm_pos_safe} and Theorem~\ref{thrm_pos_cobuchi}.
The undecidability follows for positive winning for B\"uchi and parity objectives
follows from the result of~\cite{BBG08,GIMBERT:2009:HAL-00403463:3}.

\item {\em Almost-sure winning.} 
It follows from the results of~\cite{CDHR07,BBG08} that the decision 
problems for almost-sure winning for {\sf POMDP} s with reachability,
safety, and B\"uchi objectives can be solved in EXPTIME.
Our reduction from Alternating PSPACE Turing machine shows EXPTIME-hardness for almost-sure
winning with reachability (and hence the lower bound also follows for B\"uchi objectives). 
The lower bound for safety objectives follows from the lower bound for partial information 
games~\cite{CDHR07} and the fact the almost-sure winning for safety coincides 
with almost-sure winning in games.
The undecidability follows for almost-sure winning for coB\"uchi and parity objectives
follows from the result of~\cite{BBG08,GIMBERT:2009:HAL-00403463:3}.
\end{enumerate}
\end{myProof}


\begin{table}
\begin{center}
\begin{tabular}{|c|c|c|}
\hline
             & Positive &  Almost-sure \\
\hline
\,Reachability\, & \,NLOGSPACE-complete (up+lo)\, & EXPTIME-complete (lo)\\ 
\hline
Safety       & EXPTIME-complete (up+lo) &  \,EXPTIME-complete\,~\cite{BD08}\, \\ 
\hline
B\"uchi      & Undecidable~\cite{BBG08} & EXPTIME-complete (lo) \\ 
\hline
coB\"uchi     & EXPTIME-complete (up+lo) & Undecidable~\cite{BBG08} \\ 
\hline
Parity        & Undecidable~\cite{BBG08} & Undecidable~\cite{BBG08} \\ 
\hline
\hline
\end{tabular}
\end{center}
\caption{Computational complexity of {\sf POMDP} s with different classes of 
parity objectives for positive and almost-sure winning. Our contribution of 
upper and lower bounds are indicated as ``up'' and ``lo'' respectively 
in parenthesis.}\label{tab1}
\end{table}

\section{Optimal Memory Bounds for Strategies}
In this section we present optimal bounds on the memory required by 
pure and randomized strategies for positive and almost-sure winning for 
reachability, safety, B\"uchi and coB\"uchi objectives. 



\smallskip\noindent{\bf Bounds for safety objectives.}
First, we consider positive and almost-sure winning with 
safety objectives in {\sf POMDP} s. 
It follows from the correctness argument of Theorem~\ref{thrm_pos_safe} 
that pure strategies 
with exponential memory are sufficient for positive winning with 
safety objectives in {\sf POMDP} s, and the exponential upper bound on memory
of pure strategies for almost-sure winning with safety objectives in {\sf POMDP} s
follows from the reduction to games.
We now present a matching exponential lower bound for randomized strategies.

\begin{lemma}\label{lemm_lower_bound_safety}
There exists a family $(P_n)_{n \in \nat}$ of {\sf POMDP} s 
of size $O(p(n))$ for a polynomial $p$ with a safety 
objective  such that the following assertions hold:
(a)~Player~$1$ has a (pure) almost-sure (and therefore also positive)
winning strategy in each of these {\sf POMDP} s; and 
(b)~there exists a polynomial $q$ such that 
every finite-memory randomized strategy for Player~1 that  is 
positive (or almost-sure) winning 
in $P_n$ has at least $2^{q(n)}$ states.
\end{lemma}


\paragraph{{\bf Preliminary.}}
The set of actions of the {\sf POMDP}\/ $P_n$ is $\Sigma_n \cup \{\#\}$
where $\Sigma_n = \{1, \dots,n\}$. 
The {\sf POMDP}\/ is composed of an initial state $q_0$ and $n$ sub-MDPs $A_i$ with state space $Q_i$, 
each consisting  of a loop over $p_i$ states $q_1^i,\dots,q_{p_i}^i$
where $p_i$ is the $i$-th prime number. 
From each state $q_j^i$ ($1 \leq j < p_i$), every action in $\Sigma_n$ 
leads to the next state $q_{j+1}^i$ with probability $\frac{1}{2}$, and to the initial state $q_0$ 
with probability $\frac{1}{2}$. The action $\#$ is not allowed.
From $q_{p_i}^i$, the action $i$ is not allowed
while the other actions in $\Sigma_n$ lead back the first state $q^i_1$
and to the initial state $q_0$ both with probability $\frac{1}{2}$.
Moreover, the action $\#$ leads back to the initial state (with probability~$1$). 
The disallowed actions lead to a bad state. The states of the $A_i$'s are 
indistinguishable (they have the same observation), while the initial state $q_0$ is visible.
We assume that the state spaces $Q_i$ of the $A_i$'s are disjoint.


\begin{figure}[t]
 \begin{minipage}[b]{.52\linewidth}
 \begin{center}
    \input{figures/exp-POMDP.tex}
   
    \caption{The {\sf POMDP}\/ $P_2$.}
    \label{fig:exp-game}
 \end{center}
 \end{minipage} \hfill 
 \begin{minipage}[b]{.52\linewidth}
 \begin{center}
   \input{figures/exp-POMDP-reach.tex}
  
   \caption{The {\sf POMDP}\/ $P'_2$.}
   \label{fig:exp-POMDP-reach}
 \end{center}
 \end{minipage}
\end{figure}

\paragraph{{\bf {\sf POMDP}\/ family $(P_n)_{n \in\nat}$.}}
The state space of $P_n$ is the disjoint union of $Q_1, \dots, Q_n$ and $\{q_0,\mathsf{Bad}\}$.
The initial state is $q_0$, the final state is $\mathsf{Bad}$. The probabilistic 
transition function is as follows:
\begin{itemize}
\item for all $1 \leq i \leq n$ and $\sigma \in \Sigma_n$, we have
${\delta}(q_0,\sigma)(q^i_1)=\frac{1}{n}$;

\item 
for all $1 \leq i \leq n$, $1 \leq j < p_i$, and $\sigma \in \Sigma_n$, 
$\sigma' \in \Sigma_n \setminus \{i\}$,
we have 
${\delta}(q^i_j,\sigma)(q^i_{j+1})={\delta}(q^i_{j},\sigma)(q_{0})= 
{\delta}(q^i_{p_i},\sigma')(q^i_{1})={\delta}(q^i_{p_i},\sigma')(q_{0})=\frac{1}{2}$;
and 

\item for all $1 \leq i \leq n$ and $1 \leq j < p_i$, we have 
${\delta}(q_0,\#)(\mathsf{Bad})={\delta}(q^i_{j},\#)(\mathsf{Bad})={\delta}(q^i_{p_i},\#)(q_{0})=1$. 
\end{itemize}

The initial state is $q_0$. There are two observations, the state $\{q_0\}$ is 
labelled by observation $o_1$, 
and the other states in $Q_1 \cup \dots \cup Q_n$ (that we call the loops) 
by observation $o_2$.
\figurename~\ref{fig:exp-game} shows the game $P_2$: 
the witness family of POMDPs have similarities with analogous constructions for games~\cite{BCDHR08}.
However the construction of~\cite{BCDHR08} shows lower bounds only for pure strategies and in games, whereas
we present lower bound for randomized strategies and for POMDPs, and hence our proofs are very different.




\paragraph{{\bf Proof of Lemma~\ref{lemm_lower_bound_safety}.}}
After the first transition from the initial state, player~$1$ 
has the following positive winning strategy. Let $p^*_n = \prod_{i=1}^{n} p_i$. 
While the {\sf POMDP}\/ is in the loops (assume that we have seen $j$ times observation $o_2$
consecutively), if $1 \leq j < p^*_n$, then play any action $i$ such that $j \mod p_i \neq 0$
(this is well defined since $p^*_n$ is the lcm of $p_1, \dots, p_n$),
and otherwise play $\#$. It is easy to show that this strategy is winning for 
the safety condition, with probability $1$.

For the second part of the result, assume towards a contradiction 
that there exists a finite-memory randomized strategy $\hat{\alpha}$ 
that is positive winning 
for Player~$1$ and has less than $p^*_n$ states 
(since $p^*_n$ is exponential in $s^*_n = \sum_{i=1}^{n} p_i$, 
the result will follow).
Let $\eta$ be the least positive transition probability described by 
the finite-state strategy $\hat{\alpha}$. 
Consider any history of a play $\rho$ that ends with $o_1$. 
We claim that the following properties hold:
(a)~with probability~$1$ either observation $o_1$ is visited again from $\rho$ or 
the state $\mathsf{Bad}$ is reached; and 
(b)~the state $\mathsf{Bad}$ is reached with a positive probability.
The first property (property~(a)) follows from the fact that for all actions
the loops are left (the state $q_0$ or $\mathsf{Bad}$ is reached) with probability at 
least $\frac{1}{2}$.
We now prove the second property by showing that the state~$\mathsf{Bad}$ is reached with 
probability at least $\Delta_n = \frac{1}{n}\cdot\frac{1}{(2\cdot \eta)^{p^*_n}}$.
To see this, consider the sequence of actions played by strategy $\hat{\alpha}$
after~$\rho$ when only~$o_2$ is observed. Either $\#$ is never played, and then
the action played by $\hat{\alpha}$ after a sequence of $p^*_n$ states leads 
to $\mathsf{Bad}$ (the current state being then $q^i_{p_i}$ for some $1 \leq i \leq n$).
This occurs with probability at least~$\Delta_n$; or~$\#$ is eventually played,
but since $\hat{\alpha}$ has less than $p^*_n$ states, it has to be played
after less than $p^*_n$ steps, which also leads to $\mathsf{Bad}$ with probability at 
least~$\Delta_n$. 
The above two properties that (a)~$o_1 \cup \{\mathsf{Bad}\}$ is reached with probability 
$1$ from $o_1$, 
and (b)~within $p^*_n$ steps after a visit to $o_1$, the state $\mathsf{Bad}$ is reached with
fixed positive probability,
ensures that $\mathsf{Bad}$ is reached with probability~$1$.
Hence $\hat{\alpha}$ is not positive winning.
It follows that randomized strategies that are almost-sure or positive winning in 
{\sf POMDP} s with safety objectives may require exponential memory.



\smallskip\noindent{\bf Bounds for reachability objectives.}
We now argue the memory bounds
for pure and randomized strategies for positive winning with reachability 
objectives.
\begin{enumerate}

\item It follows from the correctness argument of Theorem~\ref{thrm_pos_reach}
that randomized memoryless strategies suffice for positive winning with reachability 
objectives in {\sf POMDP} s.

\item We now argue that for pure strategies, memory of size linear in the number of 
states is sufficient and may be necessary. 
The upper bound follows from the reduction to graph reachability.
Given a {\sf POMDP}\/ $G$, consider the graph $\overline{G}$ constructed from $G$ as 
in the correctness argument for Theorem~\ref{thrm_pos_reach}.
Given the starting state $\l$, if there is path in $\overline{G}$ to the target set 
$T$ obtained from ${\cal T}$, then there is a path $\pi$ of length at most $\abs{L}$. 
The pure strategy for Player~1 in $G$ can play the sequence of actions
of the path $\pi$ to ensure that the target observations ${\cal T}$ 
are reached with positive probability in $G$.
The family of examples to show that pure strategies require linear memory 
can be constructed as follows: we construct a {\sf POMDP}\/ with deterministic
transition function such that there is a unique path (sequence of actions)
of length $O(\abs{L})$ to the target, and any deviation leads to an absorbing 
state, and other than the target state every other state has the same 
observation. In this {\sf POMDP}\/ any pure strategy must remember the exact 
sequence of actions to be played and hence requires $O(\abs{L})$ memory.
\end{enumerate}
It follows from the results of~\cite{BBG08} that for almost-sure winning 
with reachability
objectives in {\sf POMDP} s pure strategies with exponential memory suffice, and 
we now prove an exponential lower bound for randomized strategies.


\begin{lemma}\label{lemm_lower_bound_reachability}
There exists a family $(P_n)_{n \in \nat}$ of {\sf POMDP} s 
of size $O(p(n))$ for a polynomial $p$ with a reachability 
objective  such that the following assertions hold:
(a)~Player~$1$ has an almost-sure 
winning strategy in each of these {\sf POMDP} s; and 
(b)~there exists a polynomial $q$ such that 
every finite-memory randomized strategy for Player~1 that  is 
almost-sure winning 
in $P_n$ has at least $2^{q(n)}$ states.
\end{lemma}




Fix the action set as  $\Sigma = \{\#,{\sf tick}\}$. 
The {\sf POMDP}\/ $P'_n$ is composed of an initial state $q_0$ and $n$ sub-MDPs $H_i$, 
each consisting of a loop over $p_i$ states $q_1^i,\dots,q_{p_i}^i$ where $p_i$ is the $i$-th prime number.
From each state in the loops, the action ${\sf tick}$ can be played and leads to 
the next state in the loop (with probability $1$). The action $\#$ can be played 
in the last state of each loop and leads to the $\mathsf{Goal}$ state. The objective
is to reach $\mathsf{Goal}$ with probability~1. Actions that are not allowed lead to a sink
state from which it is impossible to reach $\mathsf{Goal}$.
There is a unique observation that consists of the whole state space.
\figurename~\ref{fig:exp-POMDP-reach} shows $P'_2$.


\paragraph{{\bf Proof of Lemma~\ref{lemm_lower_bound_reachability}.}}
First we show that Player $1$ has an almost-sure winning 
strategy in $P'_k$ (from $q_0$). 
As there is only one observation,
a strategy for Player $1$ corresponds to a function 
$\alpha: \nat \to \Sigma$.
Consider the strategy $\alpha^*$ as follows:
$\alpha^*(j) = {\sf tick}$ for all $0 \leq j < p^*_k$
and $\alpha^*(j) = \#$ for all $j \geq p^*_k$.
It is easy to check that $\alpha^*$ ensures winning 
with certainty and hence almost-sure winning.

For the second part of the result  assume, towards a contradiction, 
that there exists a finite-memory randomized strategy 
$\hat{\alpha}$ 
that is almost-sure winning and has less than $p^*_k$ states. 
Clearly, 
 $\hat{\alpha}$ cannot play $\#$ before the $(p^*_k+1)$-th round
since one of the subMDPs $H_i$ would 
not be in $q^i_{p_i}$ and therefore Player $1$ would lose with probability at least $\frac{1}{n}$. 
Note that the state reached 
by the strategy automaton defining $\hat{\alpha}$ after $p^*_k$ rounds has necessarily
been visited in a previous round. Since $\hat{\alpha}$ has to play $\#$ eventually to reach $\mathsf{Goal}$,
this means that $\#$ must have been played in some round $j < p^*_k$, 
when at least one of the subgames~$H_i$ was not in location $q^i_{p_i}$, 
so that Player~$1$ would have already lost with probability at least $\frac{1}{n}\cdot \eta$,
where $\eta$ is the least positive probability specified by $\hat{\alpha}$.
This is in contradiction with our assumption that $\hat{\alpha}$ is an almost-sure winning strategy.


\medskip\noindent{\bf Bounds for B\"uchi and coB\"uchi objectives.} 
An exponential upper bound for memory of pure strategies for almost-sure winning of 
B\"uchi objectives follows from the results of~\cite{BBG08}, and the matching lower
bound for randomized strategies follows from our result for reachability 
objectives.
Since positive winning is undecidable for B\"uchi objectives there is no bound 
on memory for pure or randomized strategies for positive winning.
An exponential upper bound for memory of pure strategies for positive winning 
of coB\"uchi objectives follows from the correctness proof of 
Theorem~\ref{thrm_pos_cobuchi} that iteratively combines the positive winning 
strategies for safety and reachability to obtain a positive winning strategy 
for coB\"uchi objective. 
The matching lower bound for randomized strategies follows from our result for 
safety objectives.
Since almost-sure winning is undecidable for coB\"uchi objectives there is no bound 
on memory for pure or randomized strategies for positive winning.
This gives us the following theorem (also summarized in Table~\ref{tab2}), 
which is in contrast to the results for MDPs with perfect observation where 
pure memoryless strategies suffice for almost-sure and positive winning for all 
parity objectives.

\begin{theorem}
The optimal memory bounds for strategies in {\sf POMDP} s are as follows.
\begin{enumerate}
\item Reachability objectives: for positive winning randomized memoryless 
strategies are sufficient, and linear memory is necessary and sufficient for pure 
strategies; and for almost-sure winning exponential memory is necessary and 
sufficient for both pure and randomized strategies.  

\item Safety objectives: for positive winning and almost-sure winning
exponential memory is necessary and sufficient for both pure and 
randomized strategies.  

\item B\"uchi objectives: for almost-sure winning exponential memory is necessary 
and sufficient for both pure and randomized strategies; and there is no bound 
on memory for pure and randomized strategies for positive winning.


\item coB\"uchi objectives: for positive winning exponential memory is 
necessary and sufficient for both pure and randomized strategies; and there 
is no bound on memory for pure and randomized strategies for almost-sure winning.
\end{enumerate}

\end{theorem}



\begin{table}
\begin{center}
\begin{tabular}{|c|c|c|c|c|}
\hline
             & Pure Positive & Randomized Positive   & Pure Almost  & Randomized Almost \\
\hline
Reachability & Linear & Memoryless & Exponential & Exponential \\ 
\hline
Safety       & Exponential & Exponential & Exponential & Exponential \\ 
\hline
B\"uchi       & No Bound & No Bound & Exponential & Exponential \\ 
\hline
coB\"uchi     & Exponential & Exponential & No Bound & No Bound \\ 
\hline
Parity        & No Bound & No Bound & No Bound & No Bound \\ 
\hline
\hline
\end{tabular}
\end{center}
\caption{Optimal memory bounds for pure and randomized strategies for positive and
almost-sure winning.}\label{tab2}
\end{table}


\bibliographystyle{plain}
