{'fraction_non_alphanumeric': 0.049794609758541226, 'fraction_numerical': 0.011121130147279832, 'mean_word_length': 4.205841446453407, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 24, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
POMDPs under Probabilistic Semantics

We consider partially observable Markov decision processes (POMDPs) with limit-average payoff, where a reward value in the interval [0,1] is associated to every transition, and the payoff of an infinite path is the long-run average of the rewards. We consider two types of path constraints: (i) quantitative constraint defines the set of paths where the payoff is at least a given threshold lambda_1 in (0,1]; and (ii) qualitative constraint which is a special case of quantitative constraint with lambda_1=1. We consider the computation of the almost-sure winning set, where the controller needs to ensure that the path constraint is satisfied with probability 1. Our main results for qualitative path constraint are as follows: (i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory controller is undecidable. For quantitative path constraint we show that the problem of deciding the existence of a finite-memory controller is undecidable.


Introduction
Partially observable Markov decision processes (POMDPs). Markov decision processes (MDPs) are standard models for probabilistic systems that exhibit both probabilistic and nondeterministic behavior [10]. MDPs have been used to model and solve control problems for stochastic systems [7,23]: 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. In perfect-observation (or perfectinformation) MDPs (PIMDPs) the controller can ob-serve the current state of the system to choose the next control actions, whereas in partially observable MDPs (POMDPs) the state space is partitioned according to observations that the controller can observe, i.e., given the current state, the controller can only view the observation of the state (the partition the state belongs to), but not the precise state [20]. POMDPs provide the appropriate model to study a wide variety of applications such as in computational biology [5], speech processing [19], image processing [4], robot planning [13,11], reinforcement learning [12], to name a few. POMDPs also subsume many other powerful computational models such as probabilistic finite automata (PFA) [24,21] (since probabilistic finite automata (aka blind POMDPs) are a special case of POMDPs with a single observation).
Limit-average payoff. A payoff function maps every infinite path (infinite sequence of state action pairs) of a POMDP to a real value. The most well-studied payoff in the setting of POMDPs is the limit-average payoff where every state action pair is assigned a realvalued reward in the interval [0, 1] and the payoff of an infinite path is the long-run average of the rewards on the path [7,23]. POMDPs with limit-average payoff provide the theoretical framework to study many important problems of practical relevance, including probabilistic planning and several stochastic optimization problems [11,2,16,17,27].
Expectation vs probabilistic semantics. Traditionally, MDPs with limit-average payoff have been studied with the expectation semantics, where the goal of the controller is to maximize the expected limitaverage payoff. The expected payoff value can be 1 2 when with probability 1 2 the payoff is 1, and with remaining probability the payoff is 0. In many applications of system analysis (such as robot planning and control) the relevant question is the probability measure of the paths that satisfy certain criteria, e.g., whether the probability measure of the paths such that the limit-average payoff is 1 (or the payoff is at least 1 2 ) is at least a given threshold (e.g., see [1,13]). We classify the path constraints for limit-average payoff as follows: (1) quantitative constraint that defines the set of paths with limit-average payoff at least λ 1 , for a threshold λ 1 ∈ (0, 1]; and (2) qualitative constraint is the special case of quantitative constraint that defines the set of paths with limit-average payoff 1 (i.e., the special case with λ 1 = 1). We refer to the problem where the controller must satisfy a path constraint with a probability threshold λ 2 ∈ (0, 1] as the probabilistic semantics. An important special case of probabilistic semantics is the almost-sure semantics, where the probability threshold is 1. The almost-sure semantics is of great importance because there are many applications where the requirement is to know whether the correct behavior arises with probability 1. For instance, when analyzing a randomized embedded scheduler, the relevant question is whether every thread progresses with probability 1. Even in settings where it suffices to satisfy certain specifications with probability λ 2 < 1, the correct choice of λ 2 is a challenging problem, due to the simplifications introduced during modeling. For example, in the analysis of randomized distributed algorithms it is quite common to require correctness with probability 1 (e.g., [22,26]). Besides its importance in practical applications, almost-sure convergence, is a fundamental concept in probability theory, and provide stronger convergence guarantee than convergence in expectation [6].
Previous results. There are several deep undecidability results established for the special case of probabilistic finite automata (PFA) (that immediately imply undecidability for POMDPs). The basic undecidability results are for PFA over finite words: The emptiness problem for PFA under probabilistic semantics is undecidable over finite words [24,21,3]; and it was shown in [16] that even the following approximation version is undecidable: for any fixed 0 < < 1 2 , given a probabilistic automaton and the guarantee that either (a) there is a word accepted with probability at least 1 − ; or (ii) all words are accepted with probability at most ; decide whether it is case (i) or case (ii). The almost-sure problem for probabilistic automata over finite words reduces to the non-emptiness question of universal automata over finite words and is PSPACE-complete. However, another related decision question whether for every > 0 there is a word that is accepted with probability at least 1 − (called the value 1 problem) is undecidable for probabilistic automata over finite words [8]. Also observe that all undecidability results for probabilistic automata over finite words carry over to POMDPs where the controller is restricted to finite-memory strategies. The importance of finite-memory strategies in applications has been established in [9,14,18]. Our contributions. Since under the general probabilistic semantics, the decision problems are undecidable even for PFA, we consider POMDPs with limitaverage payoff under the almost-sure semantics. We present a complete picture of decidability as well as optimal complexity.
(Almost-sure winning for qualitative constraint). We first consider limit-average payoff with qualitative constraint under almost-sure semantics. We show that belief-based strategies are not sufficient (where a belief-based strategy is based on the subset construction that remembers the possible set of current states): we show that there exist POMDPs with limitaverage payoff with qualitative constraint where finitememory almost-sure winning strategy exists but there exists no belief-based almost-sure winning strategy. Our counter-example shows that standard techniques based on subset construction (to construct an exponential size PIMDP) are not adequate to solve the problem. We then show one of our main result that given a POMDP with |S| states and |A| actions, if there is a finite-memory almost-sure winning strategy to satisfy the limit-average payoff with qualitative constraint, then there is an almost-sure winning strategy that uses at most 2 3·|S|+|A| memory. Our exponential memory upper bound is asymptotically optimal, as even for PFA over finite words, exponential memory is required for almost-sure winning (follows from the fact that the shortest witness word for non-emptiness of universal finite automata is at least exponential). We then show that the problem of deciding the existence of a finite-memory almost-sure winning strategy for limit-average payoff with qualitative constraint is EXPTIME-complete for POMDPs. In contrast to our result for finite-memory strategies, we show that deciding the existence of an infinite-memory almost-sure winning strategy for limit-average payoff with qualitative constraint is undecidable for POMDPs.
(Almost-sure winning with quantitative constraint). In contrast to our decidability result under finite-memory strategies for qualitative constraint, we show that the almost-sure winning problem for limit-average payoff with quantitative constraint is undecidable even for finite-memory strategies for POMDPs.
In summary we establish the precise decidability fron-tier for POMDPs with limit-average payoff under probabilistic semantics (see Table 1). For practical purposes, the most prominent question is the problem of finite-memory strategies, and for finite-memory strategies we establish decidability with EXPTIMEcomplete complexity for the important special case of qualitative constraint under almost-sure semantics.

Definitions
We present the definitions of POMDPs, strategies, objectives, and other basic notions required for our results. We follow standard notations from [23,15].
Notations. Given a finite set X, we denote by P(X) the set of subsets of X, i.e., P(X) is the power set of X.
A probability distribution f on X is a function f : X → [0, 1] such that x∈X f (x) = 1, and we denote by D(X) the set of all probability distributions on X. For f ∈ D(X) we denote by Given s, s ∈ S and a ∈ A, we also write δ(s |s, a) for δ(s, a)(s ). A state s is absorbing if for all actions a we have δ(s, a)(s) = 1 (i.e., s is never left from s).

Plays and belief-updates.
A play (or a path) in a POMDP is an infinite sequence (s 0 , a 0 , s 1 , a 1 , s 2 , a 2 , . . .) of states and actions such that for all i ≥ 0 we have δ(s i , a i )(s i+1 ) > 0. We write Ω for the set of all plays. For a finite prefix w = (s 0 , a 0 , s 1 , a 1 , . . . , s n ) we denote by γ(w) = (γ(s 0 ), a 0 , γ(s 1 ), a 1 , . . . , γ(s n )) the observation and action sequence associated with w. For a finite sequence ρ = (o 0 , a 0 , o 1 , a 1 , . . . , o n ) of observations and actions, the belief B(ρ) after the prefix ρ is the set of states in which a finite prefix of a play can be after the sequence ρ of observations and actions, i.e., B(ρ) = {s n = Last(w) | w = (s 0 , a 0 , s 1 , a 1 , . . . , s n ), w is a prefix of a play, and for all 0 ≤ i ≤ n. γ(s i ) = o i }. The belief-updates associated with finite-prefixes are as follows: for prefixes w and w = w·a·s the belief update is defined inductively B(γ(w )) = s1∈B(γ(w)) Supp(δ(s 1 , a)) ∩ γ −1 (γ(s)).

Strategies.
A strategy (or a policy) is a recipe to extend prefixes of plays and is a function σ : (S · A) * · S → D(A) that given a finite history (i.e., a finite prefix of a play) selects a probability distribution over the actions. Since we consider POMDPs, strategies are observation-based, i.e., for all histories w = (s 0 , a 0 , s 1 , a 1 , . . . , a n−1 , s n ) and w = (s 0 , a 0 , s 1 , a 1 , . . . , a n−1 , s n ) such that for all 0 In other words, if the observation sequence is the same, then the strategy cannot distinguish between the prefixes and must play the same. We now present an equivalent definition of observation-based strategies such that the memory of the strategy is explicitly specified, and will be required to present finite-memory strategies. Objectives. An objective in a POMDP G is a measurable set ϕ ⊆ Ω of plays. We first define limit-average payoff (aka mean-payoff) function. Given a POMDP we consider a reward function r : S × A → [0, 1] that maps every state action pair to a real-valued reward in the interval [0, 1]. The LimAvg payoff function maps every play to a real-valued reward that is the long-run average of the rewards of the play. Formally, given a play ρ = (s 0 , a 0 , s 1 , a 1 , s 2 , a 2 , . . .) we have LimAvg(r, ρ) = lim inf n→∞ 1 n · n i=0 r(s i , a i ). When the reward function r is clear from the context, we drop it for simplicity. For a reward function r, we consider two types of limit-average payoff constraints: (i) Qualitative constraint. The qualitative constraint limit-average objective LimAvg =1 defines the set of paths such that the limit-average payoff is 1; i.e., Given a threshold λ 1 ∈ (0, 1), the quantitative constraint limit-average objective LimAvg >λ1 defines the set of paths such that the limit-average payoff is strictly greater than λ 1 ; i.e., LimAvg >λ1 = {ρ | LimAvg(ρ) > λ 1 }.
Probabilistic and almost-sure winning. Given a POMDP, an objective ϕ, and a class C of strategies, we say that: (i) a strategy σ ∈ C is almost-sure winning if P σ (ϕ) = 1; (ii) a strategy σ ∈ C is probabilistic winning, for a threshold λ 2 ∈ (0, 1), if P σ (ϕ) ≥ λ 2 . Theorem 1 (Results for PFA (probabilistic automata over finite words) [21]). The following assertions hold for the class C of all infinite-memory as well as finitememory strategies: (1) the probabilistic winning problem is undecidable for PFA; and (2) the almost-sure winning problem is PSPACE-complete for PFA.
Since PFA are a special case of POMDPs, the undecidability of the probabilistic winning problem for PFA implies the undecidability of the probabilistic winning problem for POMDPs with both qualitative and quantitative constraint limit-average objectives. The almost-sure winning problem is PSPACE-complete for PFAs, and we study the complexity of the almost-sure winning problem for POMDPs with both qualitative and quantitative constraint limit-average objectives, under infinite-memory and finite-memory strategies.
Basic properties of Markov Chains. Since our proofs will use results of Markov chains, we start with some basic results related to Markov chains.
Markov chains and recurrent classes. A Markov chain G = (S, δ) consists of a finite set S of states and a probabilistic transition function δ : S → D(S). Given the Markov chain, we consider the directed graph (S, A recurrent class C ⊆ S of the Markov chain is a bottom strongly connected component (scc) in the graph (S, E) (a bottom scc is an scc with no edges out of the scc). We denote by Rec(G) the set of recurrent classes of the Markov chain, i.e., Rec(G) = {C | C is a recurrent class}. Given a state s and a set U of states, we say that U is reachable from s if there is a path from s to some state in U in the graph (S, E). Given a state s of the Markov chain we denote by Rec(G)(s) ⊆ Rec(G) the subset of the recurrent classes reachable from s in G. A state is recurrent if it belongs to a recurrent class. The following standard properties of reachability and the recurrent classes will be used in our proofs:

Finite-memory strategies with Qualitative Constraint
In this section we show the following three results for finite-memory strategies: (i) in POMDPs with LimAvg =1 objectives belief-based strategies are not sufficient for almost-sure winning; (ii) an exponential upper bound on the memory required by an almostsure winning strategy for LimAvg =1 objectives; and (iii) the decision problem is EXPTIME-complete.
Belief is not sufficient. We now show with an example that there exist POMDPs with LimAvg =1 objectives, where finite-memory randomized almost-sure winning strategies exist, but there exists no beliefbased randomized almost-sure winning strategy (a belief-based strategy only uses memory that relies on the subset construction where the subset denotes the possible current states called belief). We will present the counter-example even for POMDPs with restricted reward function r assigning only Boolean rewards 0 and 1 to the states (does not depend on the action).  Figure 1. All states in U have the same observation. The reward function r assigns the reward 1 to states X, X , Z, Z and 0 to states Y and Y . The belief initially after one-step is the set U = {X, X , Y, Y , Z, Z } since from s 0 all of them are reached with positive probability. The belief is always the set U since every state has an input edge for every action, i.e., if the current belief is U (the set of states that the POMDP is currently in with positive probability is U ), then irrespective of whether a or b is chosen all states of U are reached with positive probability and thus the belief is again U . There are three belief-based strategies: (i) σ 1 that plays always a; (ii) σ 2 that plays always b; or (iii) σ 3 that plays both a and b with positive probability. The Markov chains G σ1 and G σ2 are also shown in Figure 1, and the graph of G σ3 is the same as the POMDP G (with edge labels removed). For all the three strategies, the Markov chains contain the whole set U as the reachable recurrent class, and it follows by Lemma 1 that none of the belief-based strategies σ 1 , σ 2 or σ 3 are almostsure winning for the LimAvg =1 objective. The strategy σ 4 that plays action a and b alternately gives rise to a Markov chain where the recurrent classes do not intersect with Y or Y , and is a finite-memory almost-sure winning strategy for the LimAvg =1 objective.

Strategy complexity
For the rest of the subsection we fix a finite-memory almost-sure winning strategy σ = (σ u , σ n , M, m 0 ) on the POMDP G = (S, A, δ, O, γ, s 0 ) with a reward function r for the objective LimAvg =1 . Our goal is to construct an almost-sure winning strategy for the LimAvg =1 objective with memory size at most Mem * = 2 3·|S| · 2 |A| . We start with a few definitions associated with strategy σ. Intuitively, the action labeled edges of the graph depict the updates of the belief and the functions upon a particular action.
We now define the collapsed strategy for σ. Intuitively we collapse memory elements of σ whenever they agree on all the RecFun, AWFun, and Act functions. The collapsed strategy plays uniformly all the actions from the set given by Act in the collapsed state.
Random variable notation. For all n ≥ 0 we write X n , Y n , W n , R n , A n , L n for the random variables that correspond to the projection of the n th state of the Markov chain G σ on the S component, the belief P(S) component, the AWFun σ component, the RecFun σ component, the Act σ component, and the n th action, respectively.
Run of the Markov chain G σ . A run of the Markov chain G σ is an infinite sequence such that each finite prefix of the run is generated with positive probability on the Markov chain, i.e., for all i ≥ 0, we have In the following lemma we establish important properties of the Markov chain G σ that are essential for our proof.
→ · · · be a run of the Markov chain G σ , then the following assertions hold for all i ≥ 0: Proof. We present the proof of the fifth point, and the other points are straight-forward. For the fifth point consider that W i (X i ) = 1 and R i (X i ) = 1. Then there exists a memory m ∈ M such that (i) AWFun σ (m) = W i , and (ii) RecFun σ (m) = R i . Moreover, the state (X i , m) is a recurrent (since R i (X i ) = 1) and almostsure winning state (since W i (X i ) = 1) in the Markov chain G σ . As L i ∈ Act σ (m) it follows that L i ∈ Supp(σ n (m)), i.e., the action L i is played with positive probability in state X i given memory m, and (X i , m) is in an almost-sure winning recurrent class. By Lemma 1 it follows that the reward r(X i , L i ) must be 1. The desired result follows.
We now introduce the final notion of a collapsedrecurrent state that is required to complete the proof. A state (X, Y, W, R, A) of the Markov chain G σ is collapsed-recurrent, if for all memory elements m ∈ M that were merged to the memory element (Y, W, R, A), the state (X, m) of the Markov chain G σ is recurrent. It will turn out that every recurrent state of the Markov chain G σ is also collapsed-recurrent.
Definition 3. A state (X, Y, W, R, A) of the Markov chain G σ is called collapsed-recurrent iff R(X) = 1.
Note that due to point 4 of Lemma 2 all the states reachable from a collapsed-recurrent state are also collapsed-recurrent. In the following lemma we show that the set of collapsed-recurrent states is reached with probability 1; and the key fact we show is that from every state in G σ a collapsed-recurrent state is reached with positive probability, and then use Property 1 (a) of Markov chains to establish the lemma.  Proof. The initial state of the Markov chain G σ is ({s 0 }, AWFun σ (m 0 ), RecFun σ (m 0 ), Act σ (m 0 )) and as the strategy σ is an almost-sure winning strategy we have that AWFun σ (m 0 )(s 0 ) = 1. It follows from the third point of Lemma 2 that every reachable state (X, Y, W, R, A) in the Markov chain G σ satisfies that W (X) = 1. From the initial state a collapsedrecurrent state is reached with probability 1. It follows that all the recurrent states in the Markov chain G σ are also collapsed-recurrent states. As in all reachable states (X, Y, W, R, A) we have W (X) = 1, by the fifth point of Lemma 2 it follows that every action L played in a collapsed-recurrent state (X, Y, W, R, A) satisfies that the reward r(X, L) = 1. As this true for every reachable recurrent class, the fact that the collapsed strategy is an almost-sure winning strategy for LimAvg =1 objective follows from Lemma 1.
Theorem 2 (Strategy complexity). The following assertions hold: (1) If there exists a finitememory almost-sure winning strategy in the POMDP G = (S, A, δ, O, γ, s 0 ) with reward function r for the LimAvg =1 objective, then there exists a finite-memory almost-sure winning strategy with memory size at most 2 3·|S|+|A| . (2) Finite-memory almost-sure winning strategies for LimAvg =1 objectives in POMDPs in general require exponential memory and belief-based strategies are not sufficient.
Proof. The first point follows from Lemma 4 and the fact that the size of the memory set of the collapsed strategy σ of any finite-memory strategy σ (which is the size of the vertex set of the collapsed graph of σ) is bounded by 2 3·|S|+|A| .

Computational complexity
A naive double-exponential time algorithm would be to enumerate all finite-memory strategies with memory bounded by 2 3·|S|+|A| (by Theorem 2). Our improved exponential-time algorithm consists of two steps: (i) first it constructs a special type of a beliefobservation POMDP G from a POMDP G (and G is exponential in G); and we show that there exists a finite-memory almost-sure winning strategy for the objective LimAvg =1 in G iff there exists a randomized memoryless almost-sure winning strategy in G for the objective LimAvg =1 ; and (ii) then we show how to determine whether there exists a randomized memoryless almost-sure winning strategy in G for the LimAvg =1 objective in polynomial time with respect to the size of G. For a belief-observation POMDP the current belief is always the set of states with current observation.

Construction
of the belief-observation POMDP. Intuitively, the construction of G from G will proceed as follows: if there exists an almost-sure winning finite-memory strategy, then there exists an almost-sure winning collapsed strategy with memory bounded by 2 3·|S|+|A| . This allows us to consider the memory elements M = 2 S × {0, 1} |S| × {0, 1} |S| × 2 A ; and intuitively construct the product of the memory M with the POMDP G. The POMDP G is constructed such that it allows all possible ways the collapsed strategy of a finite-memory almost-sure winning strategy could play. The reward function r in G is obtained from the reward function r in G. In the POMDP G the belief is already included in the state space itself of the POMDP, and the belief represents exactly the set of states in which the POMDP can be with positive probability. Therefore, the POMDP G is a belief-observation POMDP. Since possible memory states of collapsed strategies are part of state space, we only need to consider memoryless strategies in G.
Lemma 5. The POMDP G is a belief-observation POMDP, such that there exists a finite-memory almost-sure winning strategy for the LimAvg =1 objective with the reward function r in the POMDP G iff there exists a memoryless almost-sure winning strategy for the LimAvg =1 objective with the reward function r in the POMDP G.
Almost-sure winning observations. Given a POMDP G = (S, A, δ, O, γ) and an objective ψ, let Almost M (ψ) denote the set of observations o ∈ O, such that there exists a memoryless almost-sure winning strategy to ensure ψ from every state s ∈ γ −1 (o).
Almost-sure winning for LimAvg =1 objectives. Our goal is to compute the set Almost M (LimAvg =1 ) given the belief-observation POMDP G (of our construction of G with product with M ). Let F ⊆ S be the set of states of G where some actions can be played consistently with the collapsed strategy of any finite-memory almost-sure winning strategy. Let G denote the POMDP G restricted to F . We define a subset of states of the belief-observation POMDP G that intuitively correspond to winning collapsedrecurrent states (wcs), i.e., S wcs = {(s, (Y, W, R, A)) | W (s) = 1, R(s) = 1}. Then, we compute the set of observations AW that can ensure to reach S wcs almostsurely in the the POMDP G. We show that the set of observations AW is equal to the set of observations Almost M (LimAvg =1 ) in the POMDP G. Thus the computation reduces to computation of almostsure states for reachability objectives. Finally we show that almost-sure reachability set can be computed in quadratic time for belief-observation POMDPs. The quadratic time algorithm is obtained as follows: we show almost-sure winning observations to ensure to reach a target set T with probability 1 is the greatest fixpoint of a set Y of observations such that playing all actions uniformly that ensures Y is not left, ensures to reach T almost-surely. This characterization gives a nested iterative algorithm that is quadratic time. The EXPTIME-completeness. In this section we first showed that given a POMDP G with a LimAvg =1 objective we can construct an exponential size beliefobservation POMDP G and the computation of the almost-sure winning set for LimAvg =1 objectives is reduced to the computation of the almost-sure winning set for reachability objectives, which we solve in quadratic time in G. This gives us an exponentialtime algorithm to decide (and construct if one ex-  Figure 2: PFA P to a POMDP G ists) the existence of finite-memory almost-sure winning strategies in POMDPs with LimAvg =1 objectives. The EXPTIME-hardness for almost-sure winning can be obtained easily from the result of Reif for two-player partial-observation games with safety objectives [25].
Theorem 3. The following assertions hold: (1) Given a POMDP G with |S| states, |A| actions, and a LimAvg =1 objective, the existence (and construction if one exists) of a finite-memory almost-sure winning strategy can be achieved in 2 O(|S|+|A|) time. (2) The decision problem of given a POMDP and a LimAvg =1 objective whether there exists a finite-memory almostsure winning strategy is EXPTIME-complete.

Remark 2.
We considered observation function that assigns an observation to every state. In general the observation function γ : S → 2 O \ ∅ may assign multiple observations to a single state. In that case we consider the set of observations as O = 2 O \ ∅ and consider the mapping that assigns to every state an observation from O and then apply our results.

Finite-memory strategies with Quantitative Constraint
We will show that the problem of deciding whether there exists a finite-memory (as well as an infinitememory) almost-sure winning strategy for the objective LimAvg > 1 2 is undecidable. We present a reduction from the standard undecidable problem for probabilistic finite automata (PFA). A PFA P = (S, A, δ, F, s 0 ) is a special case of a POMDP G = (S, A, δ, O, γ, s 0 ) with a single observation O = {o} such that for all states s ∈ S we have γ(s) = o. Moreover, the PFA proceeds for only finitely many steps, and has a set F of desired final states. The strict emptiness problem asks for the existence of a strategy w (a finite word over the alphabet A) such that the measure of the runs ending in the desired final states F is strictly greater than 1 2 ; and the strict emptiness problem for PFA is undecidable [21]. 1 2 k < ∞. By Borel-Cantelli lemma [6, Theorem 6.1, page 47] we have that the probability that bad is visited infinitely often is 0.
(Almost-sure LimAvg =1 implies value 1). We prove the converse. Consider that the PFA P does not satisfy the value 1 problem, i.e., there exists a constant c > 0 such that for all w ∈ A * we have that the probability that w is accepted in P is at most 1 − c < 1. We will show that there is no almost-sure winning strategy. Assume towards contradiction that there exists an infinite-memory almost-sure winning strategy σ in the POMDP G ; and the infinite word corresponding to σ must play infinitely many sequences of #'s to ensure LimAvg =1 . Let X i be the random variable for the rewards for the i-th sequence of #'s. Then we have that X i = 1 with probability at most 1 − c and 0 otherwise. The expected LimAvg payoff is then at most: E(lim inf n→∞ 1 n n i=0 X i ). Since X i 's are nonnegative measurable function, by Fatou's lemma [6, Theorem 3.5, page 16] It follows that E σ (LimAvg) ≤ 1 − c. Note that if the strategy σ was almost-sure winning for the objective LimAvg =1 (i.e., P σ (LimAvg =1 ) = 1), then the expectation of the LimAvg payoff would also be 1 (i.e., E σ (LimAvg) = 1). Therefore we have reached a contradiction to the fact that the strategy σ is almost-sure winning for the objective LimAvg =1 . Theorem 5. The problem whether there exists an infinite-memory almost-sure winning strategy in a POMDP with the objective LimAvg =1 is undecidable.