Paper deep dive
Solving Robust POMDPs with Omega-regular Objectives via Partially Observable Stochastic Games
Durgam Latha, Dion Reji, S. Akshay, Djordje Zikelic, Shankaranarayanan Krishna
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 8/27/2026, 4:23:49 AM
Summary
This paper establishes a semantic equivalence between (s,a)-rectangular Robust Partially Observable Markov Decision Processes (RPOMDPs) with polytopic uncertainty sets and Partially Observable Stochastic Games (POSGs) under omega-regular objectives. The authors prove that these problems are polynomial-time reducible to each other, allowing the derivation of new computational complexity bounds for solving RPOMDPs and Robust MDPs (RMDPs) with objectives such as reachability, safety, Büchi, and co-Büchi. The work covers various winning conditions including Sure, Almost Sure, Limit Sure, and Quantitative winning.
Entities (14)
Relation Signals (8)
Robust POMDP → isequivalentto → Partially Observable Stochastic Game
confidence 98% · we show for the first time that reductions can be constructed in both directions, establishing the semantic equivalence between (s,a)-rectangular RPOMDPs with polytopic uncertainty sets and POSGs.
Dorđe Žikelić → affiliatedwith → Nanyang Technological University
confidence 95% · Đorđe Žikelić Affiliation: Nanyang Technological University
Durgam Latha → affiliatedwith → Indian Institute of Technology Bombay
confidence 95% · Durgam Latha ... Affiliation: Indian Institute of Technology Bombay
Shankaranarayanan Krishna → affiliatedwith → Indian Institute of Technology Bombay
confidence 95% · Shankaranarayanan Krishna Affiliation: Indian Institute of Technology Bombay
Robust POMDP → hasuncertaintysettype → Polytopic Uncertainty Set
confidence 95% · for (s,a)-rectangular RPOMDPs with polytopic uncertainty sets
Omega-regular Objective → includes → Linear Temporal Logic
confidence 90% · general omega-regular objectives, which subsume ... linear temporal logic (LTL) objectives
Omega-regular Objective → includes → Reachability
confidence 90% · general omega-regular objectives, which subsume a broad class of objectives such as reachability
Omega-regular Objective → →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Robust POMDPs (RPOMDPs) generalize classical POMDPs to the setting where exact transition probabilities are not known -- rather, they are only known to belong to some uncertainty set of values. In this work, we study the problem of solving RPOMDPs with general omega-regular objectives, which subsume a broad class of objectives such as reachability, safety, and linear temporal logic (LTL) objectives. We show that, for (s,a)-rectangular RPOMDPs with polytopic uncertainty sets, the problem of solving RPOMDPs under omega-regular objectives can be reduced to solving partially observable stochastic games (POSGs) under omega-regular objectives. Moreover, we show for the first time that reductions can be constructed in both directions, establishing the semantic equivalence between (s,a)-rectangular RPOMDPs with polytopic uncertainty sets and POSGs. This allows us to derive a range of new computational complexity results, including both upper and lower complexity bounds, on solving RPOMDPs with different omega-regular objectives. As a corollary, we also derive new computational complexity results for RMDPs.
Tags
Links
- Source: https://arxiv.org/abs/2608.24986v1
- Canonical: https://arxiv.org/abs/2608.24986v1
Trouble viewing inline? Open PDF directly →
Full Text
207,375 characters extracted from source content.
Expand or collapse full text
Solving Robust POMDPs with ω-regular Objectives via Partially Observable Stochastic Games Durgam Latha Dion Reji S. Akshay Affiliation: Indian Institute of Technology Bombay Affiliation: Mumbai, India Đorđe Žikelić Affiliation: Nanyang Technological University Affiliation: Singapore, Singapore Shankaranarayanan Krishna Affiliation: Indian Institute of Technology Bombay Affiliation: Mumbai, India Abstract Robust POMDPs (RPOMDPs) generalize classical POMDPs to the setting where exact transition probabilities are not known – rather, they are only known to belong to some uncertainty set of values. In this work, we study the problem of solving RPOMDPs with general ω-regular objectives, which subsume a broad class of objectives such as reachability, safety, and linear temporal logic (LTL) objectives. We show that, for (s,a)(s,a)-rectangular RPOMDPs with polytopic uncertainty sets, the problem of solving RPOMDPs under ω-regular objectives can be reduced to solving partially observable stochastic games (POSGs) under ω-regular objectives. Moreover, we show for the first time that reductions can be constructed in both directions, establishing the semantic equivalence between (s,a)(s,a)-rectangular RPOMDPs with polytopic uncertainty sets and POSGs. This allows us to derive a range of new computational complexity results, including both upper and lower complexity bounds, on solving RPOMDPs with different ω-regular objectives. As a corollary, we also derive new computational complexity results for RMDPs. 1 Introduction Partially observable Markov decision processes (POMDPs) are a standard model for sequential decision making under uncertainty and imperfect state observability (Kaelbling et al., 1998). The problem of solving a POMDP is concerned with computing a strategy (or policy) that maximizes the expected payoff or the probability of satisfying some objective. However, classical algorithms assume that transition probabilities are exactly known, which is not always a realistic assumption. In practice, transition probabilities are usually inferred from data and as such their estimates come with a level of uncertainty (Chatterjee et al., 2024). In the fully observable setting, this challenge is addressed through robust MDPs (RMDPs) (Nilim and Ghaoui, 2003; Iyengar, 2005), which generalize classical MDPs by assuming that transition probabilities belong to some uncertainty sets of possible values, rather than being exactly given. Robust POMDPs (RPOMDPs) (Osogami, 2015) provide a robust generalization of POMDPs. Recent years have seen significant advances in algorithmic approaches to solving RMDPs and RPOMDPs (Nilim and Ghaoui, 2003; Iyengar, 2005; Wiesemann et al., 2013; Kaufman and Schaefer, 2013; Tamar et al., 2014; Ghavamzadeh et al., 2016; Ho et al., 2021; Asadi et al., 2026a; Tewari and Bartlett, 2007; Grand-Clément and Petrik, 2023; Goyal and Grand-Clément, 2023; Wang et al., 2023; Chatterjee et al., 2024; Meggendorfer et al., 2025; Osogami, 2015; Chamie and Mostafa, 2018; Suilen et al., 2020; Nakao et al., 2021; Cubuktepe et al., 2021; Galesloot et al., 2025a; Galesloot et al., 2025b; Krale et al., 2025). However, reward objectives do not consider logical correctness properties that are particularly important in safety-critical applications. For instance, in self-driving cars, the reach-avoid correctness property is concerned with reaching some target region while avoiding the unsafe obstacles (Summers and Lygeros, 2010). The stability correctness property requires the agent to eventually reach and stay within some target region ad infinitum (Khalil and Grizzle, 2002). These are both classical examples of logical correctness properties in control and robotics applications, which are not defined in terms of reward objectives. In formal methods, logical correctness properties are formally defined via logics such as linear temporal logic (LTL) (Pnueli, 1977), or more generally ω-regular specifications (Clarke et al., 2018), which subsumes most logical correctness properties appearing in control and robotics applications (Kress-Gazit et al., 2009). While recent years have seen significant advances in solving RMDPs and RPOMDPs with reward objectives, the literature on logical correctness objectives remains limited. Even the literature on RMDPs with ω-regular objectives either makes significant assumptions on uncertainty sets such as interval MDPs (Chatterjee et al., 2008; Sen et al., 2006), or is restricted to probability 11 or limit-sure satisfaction of ω-regular specifications (Asadi et al., 2026b). Our Contributions. In this work, we consider the problem of solving RMDPs and RPOMDPs with ω-regular objectives, with a focus on computational complexity aspects. As common in the literature on solving R(PO)MDPs, we consider RPOMDPs with (s,a)(s,a)-rectangular and polytopic uncertainty sets. These assumptions are quite general and subsume types of uncertainty sets considered in the existing literature, such as intervals (Givan et al., 2000) or L1L^1-uncertainty sets (Ho et al., 2021). Our approach is based on the following fundamental novel result – we formally prove that the problem of solving RPOMDPs with ω-regular objectives is equivalent to the problem of solving partially observable stochastic games (POSGs) (Hansen et al., 2004) with ω-regular objectives. That is, we show that the two problems can be reduced to each other in polynomial-time and thus any known algorithm and computational complexity result for solving one problem readily applies to the other problem. The key novelty of our result lies in establishing the equivalence of the two models. Previous work has shown that, under reward objectives, the problem of solving R(PO)MDPs can be reduced to the problem of solving (PO)SGs (Chatterjee et al., 2024; Grand-Clément et al., 2023; Bovy et al., 2024). However, in this work, we consider ω-regular objectives rather than reward objectives. Moreover, we show that the two models can be reduced to each other, hence are equivalent, and the reduction from (PO)SGs to R(PO)MDPs turns out to be much more technically challenging. To the best of our knowledge, this is the first time that a stochastic game model has been formally polynomial-time reduced to a robust MDP model. Since the problem of solving POSGs under ω-regular objectives has received more attention (Chatterjee et al., 2013) compared to RPOMDPs, our equivalence result allows us to derive a plethora of new computational complexity results on solving RPOMDPs that were previously unknown. Our results are summarized in Table 1. We derive results for several variants of the ω-regular objective satisfaction problem: (1) Sure Winning, where the objective needs to be satisfied for every RPOMDP run, (2) Almost Sure Winning, where the objective needs to be satisfied with probability 1, (3) Limit Sure Winning, where the objective needs to be satisfied with probability 1−ϵ1-ε for every ϵ>0ε>0, and (4) Quantitative Winning, where the objective needs to be satisfied with at least some given probability p∈[0,1]p∈[0,1]. Moreover, we derive complexity bounds both under the one-sided partial observability setting (that we call 1s-RPOMDPs) where only the agent has partial observability but the environment has full observability of the state, and the two-sided partial observability setting (which we refer to as RPOMDPs) where both the agent and the environment only have partial observability of the state. In addition, as a direct corollary of our equivalence result under full observability, we derive new complexity bounds for RMDPs with ω-regular objectives under the Quantitative Winning setting that were previously unknown, see Table 1. Thus, our work significantly advances the state of the art in solving R(PO)MDPs under ω-regular objectives and provides a complete picture of the complexity landscape for different variants of the problem. Our contributions can be summarized as follows: 1. Equivalence of RPOMDPs and POSGs. We formally prove, for the first time, that the problems of solving RPOMDPs and POSGs under ω-regular objectives are equivalent, i.e. polynomial-time reducible to each other. No previous work has considered reduction from a stochastic game model to a robust MDP model. 2. New complexity results for R(PO)MDPs. We derive new computational complexity results for RPOMDPs under ω-regular objectives, see Table 1. As a corollary, we also derive new complexity results for RMDPs. Sure Winning (Table 1) Almost Sure Winning(Table 3) RMDP 1s RPOMDP RPOMDP RMDP 1s RPOMDP RPOMDP Safe Linear-time EXPTIME-c EXPTIME-c Linear-time EXPTIME-c EXPTIME-c Reach Linear-time EXPTIME-c EXPTIME-c Linear-time EXPTIME-c Open Büchi Quad-time EXPTIME-c EXPTIME-c Quad-time EXPTIME-c Open co-Büchi Quad-time EXPTIME-c EXPTIME-c Quad-time Undecidable Undecidable ω-regular NP ∩ coNP EXPTIME-c EXPTIME-c NP ∩ coNP Undecidable Undecidable Limit Sure Winning (Table 4) Quantitative Winning(Table 5) RMDP 1s RPOMDP RPOMDP RMDP 1s RPOMDP RPOMDP Safe Linear-time EXPTIME-c EXPTIME-c NP ∩ coNP Undecidable Undecidable Reach Linear-time Undecidable Undecidable NP ∩ coNP Undecidable Undecidable Büchi Quad-time Undecidable Undecidable NP ∩ coNP Undecidable Undecidable co-Büchi Quad-time Undecidable Undecidable NP ∩ coNP Undecidable Undecidable ω-regular NP ∩ coNP Undecidable Undecidable NP ∩ coNP Undecidable Undecidable Table 1: Summary of complexity results that follow from our equivalence of RPOMDPs and POSGs under ω-regular objectives. We show results both for general ω-regular objectives as well as for special instances of objectives (reachability, safety, Büchi, co-Büchi) for which more efficient algorithms are known. The ’-c’ suffix denotes completeness, otherwise shown results denote upper complexity bounds. The red colored entries are our novel results that were previously unknown and that follow from our equivalence result with POSGs (Chatterjee et al., 2013). The table considers RMDPs (full observability for both the agent and the environment), 1s-RPOMDPs (partial observability for the agent only), and RPOMDPs (partial observability for both). The blue colored entries remain open problems since the decidability and complexity of solving POSGs under almost sure winning reachability and Büchi objectives is a well-known open problem (Chatterjee et al., 2013). The table numbers correspond to the tables in (Chatterjee et al., 2013) from which the respective complexity results on POSGs were obtained. Related Work. Recent years have seen significant advances in algorithmic approaches to solving RMDPs under reward objectives, with efficient algorithms being proposed for expected discounted-sum reward and long-run average reward, as discussed above. These works assume knowledge of the RMDP model and provide guarantees on the correctness of their results. In addition, reinforcement learning algorithms for solving RMDPs in a model-free setting but without guarantees on the correctness of results have also been proposed (Roy et al., 2017; Tessler et al., 2019; Wang and Zou, 2021; Wang and Zou, 2022; Wang et al., 2024). Algorithmic approaches for solving RPOMDPs under reward objectives were considered in (Osogami, 2015; Chamie and Mostafa, 2018; Suilen et al., 2020; Nakao et al., 2021; Cubuktepe et al., 2021; Galesloot et al., 2025a; Galesloot et al., 2025b; Krale et al., 2025). See (Suilen et al., 2024) for a recent survey. We study R(PO)MDPs under ω-regular objectives, which have received much less attention. To the best of our knowledge, no existing work considers solving RPOMDPs with ω-regular objectives. Literature on RMDPs with ω-regular objectives either makes significant assumptions on the structure of uncertainty sets such as interval MDPs (Chatterjee et al., 2008; Sen et al., 2006), or is restricted to probability 11 or limit-sure satisfaction of ω-regular specifications (Asadi et al., 2026b) where the two objectives are shown to have the same value, but without exact complexity bounds that we establish. The one-sided POSG notion we consider is from (Chatterjee et al., 2013) where observations are on states; Horák et al. (2023) considers a notion of one sided stochastic games where observations are on transitions. The existence of a reduction from R(PO)MDPs to (PO)SGs under reward objectives has been observed in prior work (Nilim and Ghaoui, 2003; Grand-Clément et al., 2023). The work (Chatterjee et al., 2024) formalizes the reduction from RMDPs to turn-based stochastic games under both expected discounted-sum and long-run average objectives. The work (Bovy et al., 2024) formalizes the reduction from RPOMDPs to POSGs under discounted-sum objectives. However, none of these works consider ω-regular objectives. Moreover, we for the first time establish a polynomial-time reduction in the opposite direction – from (PO)SGs to R(PO)MDPs – under ω-regular objectives. 2 Model Definition and Preliminaries For a set X, we denote by Δ(X) (X) the set of all probability distributions over X and by 2X2^X the set of all subsets of X. For x∈Xx∈ X, Dirac(x)∈Δ(X)Dirac(x)∈ (X) is the Dirac distribution assigning probability 11 to x. For a sequence b=b0,b1,b2,⋯,bnb=b_0,b_1,b_2,·s,b_n, we write last(b)=bnlast(b)=b_n. For x=(x1,x2,⋯xk)x=(x_1,x_2,·s x_k), x(i)x(i) denotes the element at i-th index. Let ℕN represent the set of natural numbers. RPOMDPs. A Robust POMDP (RPOMDP) is a tuple (S,A,,,,,,s0)(S,A,P,O_ a,O_ e,Z_ a,Z_ e,s_0), where S and A are finite sets of states and actions, s0∈Ss_0∈ S is the initial state, and ⊆(S×A→Δ(S))P (S× A→ (S)), called the uncertainty set, is a subset of all functions from S×AS× A to Δ(S) (S). ,O_ a,O_ e respectively are finite sets of observations for the agent and environment, :S→,:S→Z_ a:S _ a,Z_ e:S _ e are observation functions mapping states to observations. A robust MDP (RMDP) arises when both the agent and the environment have full observability: for ⋆∈a,e ∈\a,e\, ⋆=os⋆∣s∈SO_ =\o _s s∈ S\ with (s)=osaZ_ a(s)=o^a_s and (s)=oseZ_ e(s)=o^e_s. A one-sided RPOMDP has partial observability for the agent but full for the environment, i.e. =os∣s∈SO_ e=\o_s s∈ S\ with (s)=osZ_ e(s)=o_s. Assumptions: (s,a)(s,a)-rectangularity and Polytopic Uncertainty Sets. As is common in the algorithmic study of RMDPs and uncertain POMDPs (Nilim and Ghaoui, 2003; Iyengar, 2005; Bovy, 2023), we restrict our attention to RPOMDPs with (s,a)(s,a)-rectangular uncertainty sets. That is, we assume that the uncertainty set is of the form =∏(s,a)∈S×AP(s,a)P= _(s,a)∈ S× AP(s,a) with each P(s,a)⊆Δ(S)P(s,a) (S), meaning that the environment can choose transition probabilities independently across state-action pairs. Moreover, we assume that each P(s,a)P(s,a) is a polytope with a finite vertex set Vs,aV_s,a. We take every Vs,aV_s,a to be given explicitly as part of the input. Accordingly, all model sizes and linear-time claims are measured with respect to these explicit vertex lists. A point in P(s,a)P(s,a) is a distribution over S, see Figure 1(a). Standard examples include L1L^1 and interval uncertainty sets (Ho et al., 2021; Givan et al., 2000). In the rest of the paper, RPOMDPs refer to (s,a)(s,a)-rectangular polytopic RPOMDPs. Semantics of RPOMDPs. Informally, the semantics of RPOMDPs are defined as follows. The process begins in state s0s_0 with observations ((s0),(s0))(Z_ a(s_0),Z_ e(s_0)). At each step t, an agent chooses an action ata_t; the agent does not know the exact state sts_t, but only the agent observation ota=(st)o^a_t=Z_ a(s_t). In response, using its observation history and ata_t, the adversarial environment selects a complete transition assignment Pt∈P_t ; the transition from the actual state uses its component Pt(st,at)∈P(st,at)P_t(s_t,a_t)∈ P(s_t,a_t). The environment observes only ote=(st)o^e_t=Z_ e(s_t). The next state st+1s_t+1 is sampled from Pt(st,at)P_t(s_t,a_t), the agent observes (st+1)Z_ a(s_t+1) and the process continues. This process is formalized via agent and environment strategies. Following the terminology of (Bovy et al., 2024), our semantics model dynamic uncertainty where the environment may select a new probability assignment at each time step. A history is a finite sequence ht=s0,(o0a,o0e),s1,…,st,(ota,ote)∈(S×)∗h_t=s_0,(o^a_0,o^e_0),s_1,…,s_t,(o^a_t,o^e_t)∈(S×O_ a×O_ e) . An agent (resp., environment) observation history for hth_t is a sequence ohta=o0a,…,ota∈()∗×(resp., ohte=o0e,…,ote∈()∗×).oh^a_t=o^a_0,…,o^a_t∈(O_ a)^*×O_ a(resp., oh^e_t=o^e_0,…,o^e_t∈(O_ e)^*×O_ e). Let a OH_a and e OH_e denote the sets of agent and environment observation histories. An agent and environment strategy are mappings σ:a→⋃o∈∏s:(s)=oΔ(A),π:e×A→,σ: OH_a→ _o _ a _s:\,Z_ a(s)=o (A), π: OH_e× A , such that σ(oh)∈∏s:(s)=last(oh)Δ(A)σ(oh)∈ _s:\,Z_ a(s)=last(oh) (A). Given a RPOMDP ℳM, let Σℳ _M and Πℳ _M denote all agent and environment strategies. Note that our strategies are “action invisible” since they map observation histories which do not record actions. A strategy is finite-memory if it can be implemented by a finite-state transducer that reads the player’s observation history and outputs the required assignment. It is memoryless if one memory state suffices; strategies not restricted to finite memory are called infinite-memory strategies. A pair of strategies (σ,π)∈Σℳ×Πℳ(σ,π)∈ _M× _M induces a play ρ=s0,a0,s1,a1,⋯∈(S×A)ωρ=s_0,a_0,s_1,a_1,…∈(S× A)^ω starting from s0s_0. At time t, let αt=σ(ohta) _t=σ(oh^a_t) and Pt=π(ohte,at)P_t=π(oh^e_t,a_t) be the assignments selected from the players’ observation histories. The action ata_t is sampled according to the distribution αt(st) _t(s_t). The next state satisfies Pr(st+1∣ht,at)=Pt(st,at)(st+1) (s_t+1 h_t,a_t)=P_t(s_t,a_t)(s_t+1). Let ℳ Plays_M denote the set of all plays in ℳM. Given an initial state s0s_0, each pair of strategies (σ,π)∈Σℳ×Πℳ(σ,π)∈ _M× _M induces a probability measure ℙs0σ,π(⋅)P_s_0^σ,π(·) over the set ℳ Plays_M (Billingsley, 2017). We write ℳσ,π Plays_M^σ,π for the set of supported plays: those plays for which every finite prefix has positive probability under (σ,π)(σ,π). ω-regular Objectives. A logical objective in an RPOMDP ℳM is a measurable set W⊆ℳW Plays_M. We consider ω-regular objectives (Clarke et al., 2018), specified via a parity automaton. Standard examples are reachability (visit a target state at least once), safety (avoid a bad state forever), Büchi (visit a target state infinitely often), and co-Büchi (visit a bad state only finitely often). It is a classical result in formal methods that every ω-regular objective can be represented via a parity automaton (Thomas, 1997). We assume we have already taken the product of the RPOMDP and the parity automaton, and that the RPOMDP is equipped with a priority function p:S→0,1,…,d,d∈ℕp:S→\0,1,…,d\,d assigning a priority to each state. The ω-regular objective is then the set of plays in which the minimum priority that is visited infinitely often is even, i.e. Parityℳ(p)=ρ∈ℳ|minp(s):s∈Inf(ρ) is evenParity_M\! (p )= \ρ∈ Plays_M | \p(s):s (ρ)\ is even \. Here Inf(ρ)Inf(ρ) is the set of states that occur infinitely often in ρ. Partially Observable Stochastic Games (POSGs). A turn-based, two-player (, max, min) POSG Chatterjee et al. (2013) is a tuple =(S,S,A,A,δ,s0,,,,),G=(S_ max,S_ min,A_ max,A_ min,δ,s_0,O_ max,O_ min,Z_ max,Z_ min), where S_ max and S_ min are the sets of max- and min-states, respectively. Write S=S∪S^G=S_ max∪ S_ min, with initial state s0∈Ss_0∈ S^G. The action sets of the two players are A_ max and A_ min, and we write A=A∪A^G=A_ max∪ A_ min. The transition function is δ:(S×A)∪(S×A)→Δ(S).δ:(S_ max× A_ max)∪(S_ min× A_ min)→ (S^G). Observations are given by sets ,O_ max,O_ min and functions :S→Z_ max:S^G _ max, :S→Z_ min:S^G _ min for two players. A POSG is alternating control (ac-POSG) if δ(s,a)∈Δ(S)δ(s,a)∈ (S_ min) for every (s,a)∈S×A(s,a)∈ S_ max× A_ max and δ(s,a)∈Δ(S)δ(s,a)∈ (S_ max) for every (s,a)∈S×A(s,a)∈ S_ min× A_ min. Throughout, ac-POSGs start in a max-state, s0∈Ss_0∈ S_ max; otherwise, a fresh deterministic initial max-state can be prepended. A history of G is a sequence ht=s0,(o01,o02),s1,…,st,(ot1,ot2)h_t=s_0,(o^1_0,o^2_0),s_1,…,s_t,(o^1_t,o^2_t) in (S×)∗(S^G×O_ max×O_ min)^* such that for all 0≤i≤t0≤ i≤ t, oi1=(si),oi2=(si).o^1_i=Z_ max(s_i),o^2_i=Z_ min(s_i). Moreover, for every 0≤i<t0≤ i<t, there is an action a∈Aa∈ A_ max if si∈Ss_i∈ S_ max, or a∈Aa∈ A_ min if si∈Ss_i∈ S_ min, such that δ(si,a)(si+1)>0δ(s_i,a)(s_i+1)>0. For ⋆∈, ∈\ max, min\, if hth_t ends in an S⋆S_ -state, its ⋆ -observation history is the sequence of that player’s observations oh⋆=o0⋆,…,ot⋆oh =o _0,…,o _t. We write ⋆ OH_ ^G for the set of all such histories. A ⋆ -strategy, for ⋆∈, ∈\ max, min\, maps each observation history as follows: σ⋆:⋆→⋃o∈⋆∏s∈S⋆:⋆(s)=oΔ(A⋆), _ : OH_ ^G→ _o _ _s∈ S_ :\,Z_ (s)=o (A_ ), such that σ⋆(oh)∈∏s∈S⋆:⋆(s)=last(oh)Δ(A⋆). _ (oh)∈ _s∈ S_ :\,Z_ (s)=last(oh) (A_ ). Thus the strategy sees only ohoh; the game subsequently evaluates the component of the selected assignment belonging to its current state. We write σ and π for the max- and min-strategies, respectively. Note that these are referred to as action-invisible strategies in the literature Chatterjee et al. (2013). Plays induced by (σ,π)(σ,π) are defined analogously to RPOMDP plays. Plays_G denotes the set of all plays. Probability measures of plays, objectives W⊆W Plays_G as well as the value Val(W)Val_G(W) are defined in a similar manner to RPOMDPs. Let Σ _G and Π _G denote the sets of all max- and min-strategies, respectively. Problem. Given an RPOMDP ℳM with an ω-regular objective W, its value and (its value under a fixed agent strategy σ) are defined as Valℳ(W)=supσ∈Σℳinfπ∈Πℳℙs0σ,π(W)Val_M(W)= _σ∈ _M _π∈ _MP_s_0^σ,π(W) and (Valℳσ(W)=infπ∈Πℳℙs0σ,π(W)Val^σ_M(W)= _π∈ _MP_s_0^σ,π(W)), respectively. We consider the four classical ω-regular analysis problems: • Almost-sure analysis asks whether there exists an agent strategy σ such that Valℳσ(W)=1Val^σ_M(W)=1. • Limit-sure analysis asks whether, for every ϵ>0ε>0, there exists an agent strategy σϵ _ε such that Valℳσϵ(W)≥1−ϵVal _ε_M(W)≥ 1-ε, equivalently, whether Valℳ(W)=1Val_M(W)=1. • Sure analysis asks whether there exists an agent strategy σ such that ℳσ,π⊆W Plays^σ,π_M W for every environment strategy π. • Quantitative analysis asks, for a given probability threshold p∈[0,1]p∈[0,1], if Valℳ(W)≥pVal_M(W)≥ p. The computational analysis problems above have been investigated for POSGs (Chatterjee et al., 2013). 3 Equivalence with Partially Observable Stochastic Games (ac-POSG) This section presents the main result of the paper. We provide reductions between RPOMDPs and alternating control POSGs for each problem above. Throughout, we make the standard assumption that every action in a player’s action alphabet is enabled at every state owned by that player. An action is effective at a state if the construction explicitly specifies its transition there, and an effective edge is a positive-probability transition under an effective action. We only display the effective actions and edges; every omitted state-action pair is implicitly completed by an absorbing outcome losing for its owner. This completion does not affect the analysis problems below. Both reductions are linear in the model size (measured in the number of states, effective actions and transitions). s1s_1s2s_2s3s_3aap1p_1r1r_1aap2p_2q2q_2r2r_2aar3r_3p3p_3b,1b,1b,1b,1b,1b,1 s1s_1s2s_2s3s_3(s1,a)(s_1,a)(s2,a)(s_2,a)(s3,a)(s_3,a)(s1,b)(s_1,b)(s2,b)(s_2,b)(s3,b)(s_3,b)aabbaabbaabbv11v_11v12v_12v21v_21v22v_22v23v_23v31v_31v32v_32(1,0,0)(1,0,0)(0,1,0)(0,1,0)(0,0,1)(0,0,1) Figure 1: (a) RPOMDP ℳM with states s1,s2,s3s_1,s_2,s_3 and actions a,ba,b. Each transition arrow consists of two parts, the first denotes an action (a or b) whereas the second denotes the probability of moving to a state upon taking that action (e.g. p1p_1 is the probability of moving to s2s_2 upon taking action a in s1s_1). The uncertainty set of the RPOMDP is defined by specifying the vertex set of the uncertainty polytope for each state-action pair. We let Vs1,a=v11,v12V_s_1,a=\v_11,v_12\ and (0,p1,r1)∈P(s1,a)(0,p_1,r_1)∈ P(s_1,a). Vs2,a=v21V_s_2,a=\v_21,v22v_22,v23v_23\ and (p2,q2,r2)∈P(s2,a)(p_2,q_2,r_2)∈ P(s_2,a). Vs3,a=v31,v32V_s_3,a=\v_31,v_32\ and (p3,0,r3)∈P(s3,a)(p_3,0,r_3)∈ P(s_3,a). Note that on b, all transitions are deterministic, so Vs1,b=(1,0,0)V_s_1,b=\(1,0,0)\, Vs2,b=(0,1,0)V_s_2,b=\(0,1,0)\ and Vs3,b=(0,0,1)V_s_3,b=\(0,0,1)\. (b) The ac-POSG constructed from the RPOMDP, circular and rectangular states represent max-player and min-player states, respectively. The action set of the max-player is the same as the action set in the RPOMDP on the left, namely a,b\a,b\. Min-player states are all combinations of state-action pairs in the RPOMDP on the left. The effective actions at each such state are the vertices of the corresponding uncertainty polytope. For instance, at (s1,a)(s_1,a) these are v11v_11 and v12v_12 from Vs1,aV_s_1,a; randomizing with probabilities (α1,α2)( _1, _2) mimics the point α1v11+α2v12 _1v_11+ _2v_12 in P(s1,a)P(s_1,a). We omit the remaining completed actions and the effective edges from (s2,a)(s_2,a) and (s3,a)(s_3,a) for clarity. 3.1 Reduction from RPOMDPs to ac-POSGs Our reduction from RPOMDPs to ac-POSGs draws insight from and generalizes the reduction from RMDPs to stochastic games that was presented in (Chatterjee et al., 2024). In this work, we generalize this reduction to the setting with partial observability. In what follows, given a polytopic RPOMDP ℳ=(S,A,,,,,,s0)M=(S,A,P,O_ a,O_ e,Z_ a,Z_ e,s_0) with any of the objectives defined in Section 2, we outline our construction of the equivalent ac-POSG =(S,S,A,A,δ,s0,,,,)G=(S_ max^G,S_ min^G,A_ max^G,A_ min^G,δ^G,s_0^G,O_ max^G,O_ min^G,Z_ max^G,Z_ min^G) and the corresponding objective. The formal construction is deferred to Appendix A. POSG Construction. The POSG G is defined as follows. Intuitively, the ac-POSG models the interaction between the agent and the environment in the original RPOMDP, where the max-player corresponds to the agent, the min-player to the environment, and the two players alternate in moves: States: max-player states S=S_ max^G=S are the states of the original RPOMDP, min-player states S_ min^G are state–action pairs (s,a)∈S×A(s,a)∈ S× A, and the initial state is s0=s0∈Ss_0^G=s_0∈ S_ max^G. Actions: the max-player’s actions are those of the RPOMDP, A=A_ max^G=A. At min-state (s,a)(s,a) the effective actions are the vertices Vs,aV_s,a, and the global min-action alphabet is A=⋃(s,a)∈S×AVs,aA_ min^G= _(s,a)∈ S× AV_s,a. Observations: =O_ max^G=O_ a and =O_ min^G=O_ e, with (s)=((s,a))=(s)Z_ max^G(s)=Z_ max^G((s,a))=Z_ a(s) and (s)=((s,a))=(s)Z_ min^G(s)=Z_ min^G((s,a))=Z_ e(s). Transitions: from max-state s under action a, the POSG moves deterministically to the min-state (s,a)(s,a), i.e. δ(s,a)=Dirac((s,a))δ^G(s,a)=Dirac((s,a)); from min-state s′=(s,a)s =(s,a) under an effective action v∈Vs,av∈ V_s,a, δ(s′,v)=vδ^G(s ,v)=v is the distribution over S_ max^G specified by the vertex v of the uncertainty polytope P(s,a)P(s,a). Randomizing over effective min-actions therefore produces every distribution in P(s,a)P(s,a). The constructed POSG is linear in the size of the RPOMDP and the number of vertices of the uncertainty polytopes. Figure 1(b) shows an example of our construction. Parity Objectives: The ω-regular objective in the ac-POSG G is specified by the priority function p′:S→0,1,…,dp :S^G→\0,1,…,d\ defined via p′(s′)=p(s)p (s )=p(s) for any s′∈Ss ∈ S^G, where s is the state component of s′s (s′=s =s or s′=(s,a)s =(s,a)) and p is the priority function of ℳM. Theorem 3.1 (Proof in Appendix A.4). Let ℳM be a RPOMDP and G the induced ac-POSG. Then Valℳ(W)=Val(W′)Val_M(W)=Val_G(W ) for any ω-regular objective W in ℳM and corresponding objective W′W in G. Consequently, sure, almost-sure, limit-sure, and quantitative analysis of any objective above on ℳM is inter-reducible in linear time, and therefore in polynomial time, with the corresponding analysis on G, under the explicit vertex representation fixed in Section 2. 3.2 Reduction from ac-POSGs to RPOMDPs Key Challenge and Our Solution. Reduction from ac-POSGs to RPOMDPs turns out to be much more challenging due to the following subtle reason. Given an ac-POSG, if the max-player in a state s chooses action a, the min-player gets to see the observation (s′)Z_ min(s ) where δ(s,a)(s′)>0δ(s,a)(s )>0 before choosing its own action. On the contrary, in an RPOMDP, after the agent chooses an action a at a state s, the environment at (s,a)(s,a) commits to a polytope P(s,a)P(s,a) immediately, with nothing observed in between. Thus, at a first glance, it seems that the min-player in ac-POSGs has more power compared to the environment in RPOMDPs. Somewhat surprisingly, we show that this is not the case and that it is still possible to construct a reduction from ac-POSGs to RPOMDPs. This observation motivates us to construct a two-step reduction. The first step of the reduction reduces ac-POSGs to an intermediate model which we call pre-min-transformed POSG, which resolves this semantic discrepancy. The second step then reduces a pre-min-transformed POSG to an RPOMDP. 3.2.1 Step 1: Reduction from ac-POSGs to Pre-min-transformed POSGs The pre-min transformation inserts, before every min-state s∈Ss∈ S_ min, a fresh dummy max-state dsd_s whose sole effective action leads deterministically to s, and whose observations to both players are copies of the observations of s. Neither player gains strategic power: the max-player has nothing to choose at dsd_s (every other globally enabled action takes the max-losing default transition), while the min-player sees the same information at s as in G, the observation at dsd_s is determined by the observation at s and so reveals nothing new. The following construction formalizes this intuition. Pre-min-transformed POSG. Let =(S,S,A,A,δ,s0,,,,)G=(S_ max,S_ min,A_ max,A_ min,δ,s_0,O_ max,O_ min,Z_ max,Z_ min) be an ac-POSG, D=ds∣s∈SD=\d_s s∈ S_ min\ be the set of dummy states , and †=ox†∣x∈O =\o _x x _ max\ and #=ox#∣x∈O^\#=\o^\#_x x _ min\ be copies of observations for both players. The corresponding pre-min- transformed POSG ′=(S′,S′,A′,A′,δ′,s0,′,′,′,′)G =(S_ max ,S_ min ,A_ max ,A_ min ,δ ,s_0,O_ max ,O_ min ,Z_ max ,Z_ min ) is defined via: • States. S′=S∪DS_ max =S_ max∪ D and S′=S_ min =S_ min, with initial state s0s_0. • Actions. A′=A∪⊤A_ max =A_ max∪\ \ and A′=A_ min =A_ min, with all respective actions enabled throughout. The effective max-actions are A_ max at original max-states and the fresh action ⊤ at dummy states. • Observations. ′=∪†O_ max =\ O_ max∪O and ′=∪#O_ min =O_ min∪O^\#, with ′(s)=(s)Z_ max (s)=Z_ max(s) and ′(s)=(s)Z_ min (s)=Z_ min(s) for all s∈S∪Ss∈ S_ max∪ S_ min, while ′(ds)=o(s)†Z_ max (d_s)=o _Z_ max(s) and ′(ds)=o(s)#Z_ min (d_s)=o^\#_Z_ min(s) for all ds∈Dd_s∈ D are the newly introduced observation copies. • Transition function. (i) For s1∈Ss_1∈ S_ max, a1∈Aa_1∈ A_ max, and s2∈Ss_2∈ S_ min such that δ(s1,a1)(s2)>0δ(s_1,a_1)(s_2)>0, the pre-min-transformed POSG transitions to the min-player copy ds2d_s_2 rather than to the min-player state, i.e. δ′(s1,a1)(ds2)=δ(s1,a1)(s2)δ (s_1,a_1)(d_s_2)=δ(s_1,a_1)(s_2). (i) For s2∈Ss_2∈ S_ min and a2∈Aa_2∈ A_ min, the transition function is the same as in the original ac-POSG, i.e. δ′(s2,a2)=δ(s2,a2)δ (s_2,a_2)=δ(s_2,a_2). (i) For the newly introduced copy states ds∈Dd_s∈ D and action ⊤ , we define δ′(ds,⊤)=Dirac(s)δ (d_s, )=Dirac(s). Pre-min-transformed POSG objective. Plays of G and ′G are related by a bijection Γ:→′ : Plays_G→ Plays_G . Since G is alternating control, every h=s0,a0,s1,a1,⋯∈h=s_0,a_0,s_1,a_1,…∈ Plays_G has s2k∈Ss_2k∈ S_ max and s2k+1∈Ss_2k+1∈ S_ min, and Γ inserts the pair (ds2k+1,⊤)(d_s_2k+1, ) between every S_ max-step and the following S_ min-step. Observation histories lift the same way via Γ,Γ _O max, _O min. Strategies in ,′G,G are functions of observation histories. We lift them between the two games as follows. For ⋆∈, ∈\ max, min\, Φ⋆ _ takes a G-strategy σ to the ′G -strategy that, given a ′G -observation history oh′oh ending in non-dummy state, strips the inserted observations and queries σ at the underlying G-history: Φ⋆(σ)(oh′)=σ((ΓO⋆)−1(oh′)) _ (σ)(oh )=σ(( _O )^-1(oh )); for ending at dummy states Φ(σ) _ max(σ) plays ⊤ deterministically. The reverse Ψ⋆ _ goes the other way: Ψ⋆(σ′)(oh)=σ′(ΓO⋆(oh)) _ (σ )(oh)=σ ( _O (oh)). The pairs are mutual inverses, Φ⋆=(Ψ⋆)−1 _ =( _ )^-1, which helps us lift objectives across to ′G . ∙ Parity objective. Let p:S∪S→0,1,…,dp:S_ max∪ S_ min→\0,1,…,d\ be the priority function for G. Define p′:S′∪S′→0,1,…,dp :S_ max ∪ S_ min →\0,1,…,d\ by p′(s)=p(s)p (s)=p(s) for s∈S∪Ss∈ S_ max∪ S_ min and p′(ds)=p(s)p (d_s)=p(s) for ds∈Dd_s∈ D. Size and memory preservation under Pre- min. It is easy to see that |′|=(||)|G |=O(|G|) and the construction runs in linear time. Moreover, |ΓO⋆(oh)|| _O (oh)| (|ΓO⋆)−1(oh′)|| _O )^-1(oh )|) is linear in |oh||oh| (|oh′||oh |). Finally, the lifting maps Φ⋆,Ψ⋆ _ , _ preserve memory class exactly: memoryless, finite-memory and infinite-memory regimes correspond exactly between G and ′G . See details in Appendix B.3.1. Lemma 3.2 (Equivalence between G and ′G , Appendix B.4). Let G be an ac-POSG and ′G its Pre- min transformation. The play map Γ and the strategy maps Φ⋆,Ψ⋆ _ , _ (⋆∈, ∈\ max, min\) satisfy the following: for every priority function p on G, every ω-regular objective W in G and the lifted objective W′W in ′G and every ρ∈,σ∈Σ,π∈Πρ∈ Plays_G,σ∈ _G,π∈ _G: (I, obj.) ρ∈W⇔Γ(ρ)∈W′;ρ∈ W\! \! (ρ)∈ W ; \,\,\, (I, plays) Γ(σ,π)=′Φ(σ),Φ(π); ( Plays_G^σ,π)= Plays_G _ max(σ), _ min(π); (I, prob.) ℙσ,π(W)=ℙ′Φ(σ),Φ(π)(W′);P_G^σ,π(W)=P_G _ max(σ), _ min(π)(W ); \! (IV, val.) Val(W)=Val′(W′)Val_G(W)=Val_G (W ). Consequently, sure, almost-sure, limit-sure, and quantitative analysis of any objective above on G is inter-reducible in linear time with the corresponding analysis on ′G . s1s_1s2s_2t1t_1t2t_2aabbaaxxyyxx s1s_1s2s_2dt1d_t_1dt2d_t_2t1t_1t2t_2aabbaa⊤ ⊤ xxxxyy (dt2,⊤)P(d_t_2, )(dt1,⊤)P(d_t_1, )(s1,a)P(s_1,a)(s1,b)P(s_1,b)(s2,a)P(s_2,a)s1s_1s2s_2dt1d_t_1dt2d_t_2aabbaa⊤ ⊤ Figure 2: (a) A POSG G. max-states s1,s2s_1,s_2 are circles, while min-states t1,t2t_1,t_2 are rectangles. (b) The Pre- min transformed game ′G with dashed circles representing new dummy states- dt1,dt2d_t_1,d_t_2 and dashed arrows represent the ⊤ -action. (c) The reduced RPOMDP ℜ() R(G) with green dotted circles represent uncertainty sets P(s,a)P(s,a). P(s1,a)P(s_1,a) is a singleton consisting of the distribution δ(s1,a)δ(s_1,a), likewise for P(s1,b)P(s_1,b) and P(s2,a)P(s_2,a). P(dt1,⊤)P(d_t_1, ) is also a singleton δ′(dt1,x)\δ (d_t_1,x)\. P(dt2,⊤)P(d_t_2, ) is the polytope with two vertices δ′(dt2,x),δ′(dt2,y)\δ (d_t_2,x),δ (d_t_2,y)\. 3.2.2 Step 2: Reduction from Pre-min-transformed POSGs to RPOMDPs We translate a Pre-min-transformed POSG ′G into a value-equivalent RPOMDP ℜ() R\! (G ) by eliminating the min-player’s states and folding the min-player’s choices into polytope choices for the RPOMDP environment. In ′G , every play has the periodic structure s1→a1ds2→⊤s2→a2s3→a3ds4→⊤s4⋯,s_1 a_1d_s_2 s_2 a_2s_3 a_3d_s_4 s_4·s, in which S∪DS_ max∪ D states alternate with S_ min-states. The key observation is that the min-player’s only role is to pick an action a∈Aa∈ A_ min at each S_ min-state s, and this choice deterministically fixes a transition distribution δ′(s,a)∈Δ(S)δ (s,a)∈ (S_ max). This is precisely the role of the environment in an RPOMDP: given a state and an action, it selects a distribution from the uncertainty set. We exploit this correspondence by collapsing each S_ min-state s into the dummy state dsd_s that immediately precedes it: the polytope P(ds,⊤)P(d_s, ) has as its vertices, the distributions δ′(s,a)δ (s,a), one per min-action a∈Aa∈ A_ min. Picking a point in this polytope is a convex combination ∑aαaδ′(s,a) _a _a\,δ (s,a), where αa _a is the distribution value induced by − min-action a at s. The RPOMDP environment at (ds,⊤)(d_s, ) therefore has exactly the choices available to the min-player at s in ′G . The following construction formalizes this intuition. RPOMDP construction. Given a Pre-min-transformed POSG ′=(S∪D,S,A∪⊤,A,δ′,s0,∪†,∪#,′,′)G =(S_ max∪ D,S_ min,A_ max∪\ \,A_ min,δ ,s_0,O_ max ,O_ min ^\#,Z_ max ,Z_ min ), the corresponding RPOMDP ℜ()=(Sℜ,Aℜ,ℜ,ℜ,ℜ,ℜ,ℜ,s0ℜ) R\! (G )=(S_ R,A_ R,P_ R,O_ a R,O_ e R,Z_ a R,Z_ e R,s_0 R) is defined as follows: • States. Sℜ=S∪DS_ R=S_ max∪ D, with initial state s0ℜ=s0s_0 R=s_0. • Actions. Aℜ=A∪⊤A_ R=A_ max∪\ \, with every action enabled at every RPOMDP state. The construction lists A_ max as effective at original max-states and ⊤ at dummy states. • Uncertainty set. ℜ=∏(s,a)∈Sℜ×AℜP(s,a)P_ R= _(s,a)∈ S_ R× A_ RP(s,a). The polytopes have vertex sets Vs,a=δ′(s,a)V_s,a=\δ (s,a)\ if s,a∈S×As,a∈ S_ max× A_ max, Vs,a=δ′(s′,a′)∣a′∈AV_s,a=\δ (s ,a ) a ∈ A_ min\ if s=ds′,a=⊤s=d_s ,\ a= . • Observations. ℜ=∪†O_ a R=O_ max and ℜ=∪#O_ e R=O_ min ^\#, with ℜ(s′)=′(s′)Z_ a R(s )=Z_ max (s ) and ℜ(s′)=′(s′)Z_ e R(s )=Z_ min (s ) for all s′∈Sℜs ∈ S_ R. RPOMDP objectives. We first relate plays of ′G and ℜ() R\! (G ). For ρ′∈′ρ ∈ Plays_G , Λ:′→ℜ() : Plays_G → Plays_ R\! (G ) removes every S_ min-state and every A_ min-action from ρ′ρ . The map Λ is many-to-one: ′G -plays that agree on S∪DS_ max∪ D states and A∪⊤A_ max∪\ \ actions but differ in the A_ min-action chosen at S_ min-states map to the same ℜ() R\! (G )-play. Its set-valued inverse Λ−1(ρℜ) ^-1(ρ R) recovers the pre-image by re-introducing an arbitrary A_ min-action consistent with the realised next state. Observation histories lift via Λ,Λ _O max, _O min: the agent map Λ _O max is a bijection between ′ OH_ max^G and ℜ() OH_ a R\! (G ), while the environment map Λ _O min is a bijection onto the co-domain of environment histories ending at a dummy state. Strategies in ′G and ℜ() R\! (G ) are functions of observation histories. We lift strategies between the two models as follows. Ω:Σ′→Σℜ() _ max: _G → _ R\! (G ) converts a ′G - max-strategy σ′σ into an agent strategy. Given an agent observation history ohℜoh R, the new strategy first lifts ohℜoh R to its ′G -counterpart (Λ)−1(ohℜ)( _O max)^-1(oh R) and queries σ′σ there: Ω(σ′)(ohℜ)=σ′((Λ)−1(ohℜ)) _ max(σ )(oh R)=σ \! (( _O max)^-1(oh R) ). Ω:Π′→Πℜ() _ min: _G → _ R\! (G ) converts a ′G - min-strategy π′π into an environment strategy. At a dummy state ds′d_s under ⊤ , with environment history ohℜoh R ending in #O^\#, write π′((Λ)−1(ohℜ))(s′)(a)=αaπ \! (( _O min)^-1(oh R) )(s )(a)= _a for the randomised min-action a at s′s ; then Ω(π′) _ min(π ) selects the convex combination ∑a∈Aαa⋅δ′(s′,a)∈P(ds′,⊤) _a∈ A_ min _a·δ (s ,a)∈ P(d_s , ). At non-dummy state-action pairs, the polytope is a singleton, and Ω(π′) _ min(π ) picks its unique element. The reverse maps Ξ:Σℜ()→Σ′ _ max: _ R\! (G )→ _G and Ξ:Πℜ()→Π′ _ min: _ R\! (G )→ _G are defined analogously: Ξ(σℜ)(oh′)=σℜ(Λ(oh′)) _ max(σ R)(oh )=σ R( _O max(oh )); the environment map is defined analogously from the convex coefficients of the selected point. The formal strategy maps are given in the Appendix. ∙ Parity objective. Let p′p be the priority function for ′G . Define the priority function for ℜ() R\! (G ), pℜ:Sℜ→0,1,…,dp R:S_ R→\0,1,…,d\ by pℜ(s′)=p′(s′)p R(s )=p (s ) for all s′∈Sℜs ∈ S_ R. Size and memory preservation under RPOMDP construction. It is easy to see that |ℜ()|=(|′|)| R\! (G )|=O(|G |) and the construction runs in linear time. Moreover, observation histories on the two sides are linear in each other. The lifting maps Ω⋆,Ξ⋆ _ , _ preserve memory class exactly: memoryless, finite-memory, and infinite-memory regimes correspond exactly between ′G and ℜ() R\! (G ) (Appendix C.3.1). Lemma 3.3 (Equivalence between ′G and ℜ() R\! (G ), Proof in Appendix C.4). Let ′G be a Pre-min-transformed POSG and ℜ() R\! (G ) its RPOMDP reduction. The play map Λ and the strategy maps Ω⋆,Ξ⋆ _ , _ (⋆∈, ∈\ max, min\) satisfy the following: for every priority function p′p on ′G , every ω-regular objective W′W in ′G with the lifted objective WℜW R in ℜ() R\! (G ) and for every ρ′∈′ρ ∈ Plays_G , σ′∈Σ′σ ∈ _G and π′∈Π′π ∈ _G : (I, obj.) ρ′∈W′⇔Λ(ρ′)∈Wℜ;ρ ∈ W \! \! (ρ )∈ W R; (I, plays) Λ(′σ′,π′)=ℜ()Ω(σ′),Ω(π′) ( Plays_G ^σ ,π )= Plays_ R\! (G ) _ max(σ ), _ min(π ); (I, prob.) ℙ′σ′,π′(W′)=ℙℜ()Ω(σ′),Ω(π′)(Wℜ)P_G ^σ ,π (W )=P_ R\! (G ) _ max(σ ), _ min(π )(W R); (IV, val.) Val′(W′)=Valℜ()(Wℜ)Val_G (W )=Val_ R\! (G )(W R) Consequently, sure, almost-sure, limit-sure, and quantitative analysis of any objective defined above on ′G is inter-reducible in linear time with the corresponding analysis on ℜ() R\! (G ). Proof outline. The four clauses are proved in sequence, each using the previous one. (1) holds because Λ leaves the underlying S∪DS_ max∪ D-state sequence unchanged: target states are visited at exactly the same positions, and pℜp R is just the restriction of p′p to SℜS_ R, so the only states removed from ρ′ρ are S_ min-states whose priority by construction equals that of the preceding dummy state – which does not change the lim inf used in the parity condition. (2): Take ρ′∈′σ′,π′ρ ∈ Plays_G ^σ ,π and check, step by step, that Λ(ρ′) (ρ ) could have been produced by the strategy pair (Ω(σ′),Ω(π′))( _ max(σ ), _ min(π )) in ℜ() R\! (G ). At each S_ max-state, the singleton uncertainty set forces the unique transition; at each dummy state, the convex combination ∑aαaδ′(s,a) _a _aδ (s,a) chosen by Ω(π′) _ min(π ) is exactly the next-state distribution induced by π′π at s. Conversely, every play in ℜ()Ω(σ′),Ω(π′) Plays_ R\! (G ) _ max(σ ), _ min(π ) has a ′G -pre-image in Λ−1 ^-1 obtained by drawing, at each dummy step, a min-action according to the coefficients (αa)( _a). (3) is a cylinder-set induction on history length with three cases (S_ max-extension, dummy-state extension, and S→S_ min→ S_ max traversal): in each case the probability of the next step in ℜ() R\! (G ) reduces to the corresponding ′G -probability, with the deterministic ⊤ -transition contributing 11 and the polytope coefficients matching the min-action distribution. (4) first applies (3) in both mapping directions to show equality of the inner infima for each fixed agent strategy, and then takes the outer supremum; only agent maps need to be bijective. The “consequently” is immediate: quantitative and limit-sure analysis follow from clause (4); almost-sure follows from (3) by taking the infimum over π′π on each side and matching witnesses through Ω and Ξ ; and sure analysis follows from (2) and (1) since a strategy keeping all ′G -plays inside W′W corresponds via Ω to a strategy keeping all ℜ() R\! (G )-plays inside WℜW R, and conversely via Ξ . Thus from the above and from Lemmas 3.3 and 3.2, we conclude: Theorem 3.4 (Equivalence of G and ℜ() R\! (G )). Let G be an ac-POSG and ℜ() R\! (G ) be the constructed RPOMDP as in Section 3.2. The sure, almost-sure, limit-sure, and quantitative analysis of any ω-regular objective on G is inter-reducible in linear time with the corresponding analysis on ℜ() R\! (G ). Complexity Results. A corollary of the reductions in Sections 3.1 and 3.2 is that, under (s,a)(s,a)-rectangularity, Polytopic RPOMDPs are equivalent to finite ac-POSGs for any ω-regular objective. Our proofs show this for action-invisible strategies, where agent and environment strategies cannot observe the agent’s chosen actions in their respective observation histories. Thanks to the bidirectional equivalence, RPOMDPs inherit both upper and lower complexity bounds from POSGs for \sure, almost-sure, limit-sure, quantitative\ winning under ω-regular objectives, see (Chatterjee et al., 2013) for a survey. Table 1 summarizes these results. 4 Conclusion We studied RPOMDPs under ω-regular objectives, and showed that solving them is equivalent to solving ac-POSGs under ω-regular objectives. We do this by establishing polynomial-time reductions in both directions. Exploiting this equivalence, we derived several new computational complexity results for both RPOMDPs and RMDPs, and provided a complete picture of the complexity landscape of the problem under action invisible strategies. Our results apply to R(PO)MDPs with (s,a)(s,a)-rectangular and polytopic uncertainty sets. Interesting future work would be studying computational complexity bounds under more general settings. References Asadi et al. (2026a) A. Asadi, K. Chatterjee, E. K. Goharshady, M. Karrabi, A. Montaseri, and C. Pagano Strongly polynomial time complexity of policy iteration for l∞_ $∞$ robust mdps. CoRR abs/2601.23229. External Links: Link, Document, 2601.23229 Cited by: §1. Asadi et al. (2026b) A. Asadi, K. Chatterjee, E. K. Goharshady, M. Karrabi, and A. Shafiee Qualitative analysis of ω-regular objectives on robust mdps. In Fortieth AAAI Conference on Artificial Intelligence, Thirty-Eighth Conference on Innovative Applications of Artificial Intelligence, Sixteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2026, Singapore, January 20-27, 2026, p. 36137–36145. External Links: Link, Document Cited by: §1, §1. Billingsley (2017) P. Billingsley Probability and measure. John Wiley & Sons. Cited by: §2. Bovy et al. (2024) E. M. Bovy, M. Suilen, S. Junges, and N. Jansen Imprecise probabilities meet partial observability: game semantics for robust pomdps. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, p. 6697–6706. External Links: Link Cited by: §1, §1, §2. Bovy (2023) E. M. Bovy The underlying belief model of uncertain partially observable markov decision processes. Master’s Thesis, Radboud University. Cited by: §2. Chamie and Mostafa (2018) M. E. Chamie and H. Mostafa Robust action selection in partially observable markov decision processes with model uncertainty. In 57th IEEE Conference on Decision and Control, CDC 2018, Miami, FL, USA, December 17-19, 2018, p. 5586–5591. External Links: Link, Document Cited by: §1, §1. Chatterjee et al. (2013) K. Chatterjee, L. Doyen, and T. A. Henzinger A survey of partial-observation stochastic parity games. Formal Methods Syst. Des. 43 (2), p. 268–284. External Links: Link, Document Cited by: Table 1, Table 1, §1, §1, §2, §2, §2, §3.2.2. Chatterjee et al. (2024) K. Chatterjee, E. K. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic Solving long-run average reward robust mdps via stochastic games. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, p. 6707–6715. External Links: Link Cited by: §1, §1, §1, §1, §3.1. Chatterjee et al. (2008) K. Chatterjee, K. Sen, and T. A. Henzinger Model-checking omega-regular properties of interval markov chains. In Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, p. 302–317. External Links: Link, Document Cited by: §1, §1. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem (Eds.) (2018) E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem (Eds.) Handbook of model checking. Springer. External Links: Link, Document, ISBN 978-3-319-10574-1 Cited by: §1, §2. Cubuktepe et al. (2021) M. Cubuktepe, N. Jansen, S. Junges, A. Marandi, M. Suilen, and U. Topcu Robust finite-state controllers for uncertain pomdps. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, p. 11792–11800. External Links: Link, Document Cited by: §1, §1. Galesloot et al. (2025a) M. F. L. Galesloot, R. Andriushchenko, M. Ceska, S. Junges, and N. Jansen Robust finite-memory policy gradients for hidden-model pomdps. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2025, Montreal, Canada, August 16-22, 2025, p. 8518–8526. External Links: Link, Document Cited by: §1, §1. Galesloot et al. (2025b) M. F. L. Galesloot, M. Suilen, T. D. Simão, S. Carr, M. T. J. Spaan, U. Topcu, and N. Jansen Pessimistic iterative planning with rnns for robust pomdps. In ECAI 2025 - 28th European Conference on Artificial Intelligence, 25-30 October 2025, Bologna, Italy - Including 14th Conference on Prestigious Applications of Intelligent Systems (PAIS 2025), p. 4823–4831. External Links: Link, Document Cited by: §1, §1. Ghavamzadeh et al. (2016) M. Ghavamzadeh, M. Petrik, and Y. Chow Safe policy improvement by minimizing robust baseline regret. In Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, p. 2298–2306. External Links: Link Cited by: §1. Givan et al. (2000) R. Givan, S. M. Leach, and T. L. Dean Bounded-parameter markov decision processes. Artif. Intell. 122 (1-2), p. 71–109. External Links: Link, Document Cited by: §1, §2. Goyal and Grand-Clément (2023) V. Goyal and J. Grand-Clément Robust markov decision processes: beyond rectangularity. Math. Oper. Res. 48 (1), p. 203–226. External Links: Link, Document Cited by: §1. Grand-Clément et al. (2023) J. Grand-Clément, M. Petrik, and N. Vieille Beyond discounted returns: robust markov decision processes with average and blackwell optimality. CoRR abs/2312.03618. External Links: Link, Document, 2312.03618 Cited by: §1, §1. Grand-Clément and Petrik (2023) J. Grand-Clément and M. Petrik Reducing blackwell and average optimality to discounted mdps via the blackwell discount factor. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, External Links: Link Cited by: §1. Hansen et al. (2004) E. A. Hansen, D. S. Bernstein, and S. Zilberstein Dynamic programming for partially observable stochastic games. In Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California, USA, p. 709–715. External Links: Link Cited by: §1. Ho et al. (2021) C. P. Ho, M. Petrik, and W. Wiesemann Partial policy iteration for l1-robust markov decision processes. J. Mach. Learn. Res. 22, p. 275:1–275:46. External Links: Link Cited by: §1, §1, §2. Horák et al. (2023) K. Horák, B. Bošanskỳ, V. Kovařík, and C. Kiekintveld Solving zero-sum one-sided partially observable stochastic games. Artificial Intelligence 316, p. 103838. Cited by: §1. Iyengar (2005) G. N. Iyengar Robust dynamic programming. Math. Oper. Res. 30 (2), p. 257–280. External Links: Link, Document Cited by: §1, §1, §2. Kaelbling et al. (1998) L. P. Kaelbling, M. L. Littman, and A. R. Cassandra Planning and acting in partially observable stochastic domains. Artif. Intell. 101 (1-2), p. 99–134. External Links: Link, Document Cited by: §1. Kaufman and Schaefer (2013) D. L. Kaufman and A. J. Schaefer Robust modified policy iteration. INFORMS J. Comput. 25 (3), p. 396–410. External Links: Link, Document Cited by: §1. Khalil and Grizzle (2002) H. K. Khalil and J. W. Grizzle Nonlinear systems. Vol. 3, Prentice hall Upper Saddle River, NJ. Cited by: §1. Krale et al. (2025) M. Krale, E. M. Bovy, M. F. L. Galesloot, T. D. Simão, and N. Jansen On evaluating policies for robust POMDPs. In Eighteenth European Workshop on Reinforcement Learning, External Links: Link Cited by: §1, §1. Kress-Gazit et al. (2009) H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robotics 25 (6), p. 1370–1381. External Links: Link, Document Cited by: §1. Meggendorfer et al. (2025) T. Meggendorfer, M. Weininger, and P. Wienhöft Solving robust markov decision processes: generic, reliable, efficient. In Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence, Fifteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2025, Philadelphia, PA, USA, February 25 - March 4, 2025, p. 26631–26641. External Links: Link, Document Cited by: §1. Nakao et al. (2021) H. Nakao, R. Jiang, and S. Shen Distributionally robust partially observable markov decision process with moment-based ambiguity. SIAM J. Optim. 31 (1), p. 461–488. External Links: Link, Document Cited by: §1, §1. Nilim and Ghaoui (2003) A. Nilim and L. E. Ghaoui Robustness in markov decision problems with uncertain transition matrices. In Advances in Neural Information Processing Systems 16 [Neural Information Processing Systems, NIPS 2003, December 8-13, 2003, Vancouver and Whistler, British Columbia, Canada], p. 839–846. External Links: Link Cited by: §1, §1, §1, §2. Osogami (2015) T. Osogami Robust partially observable markov decision process. In Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015, p. 106–115. External Links: Link Cited by: §1, §1, §1. Pnueli (1977) A. Pnueli The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, p. 46–57. External Links: Link, Document Cited by: §1. Roy et al. (2017) A. Roy, H. Xu, and S. Pokutta Reinforcement learning under model mismatch. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, p. 3043–3052. External Links: Link Cited by: §1. Sen et al. (2006) K. Sen, M. Viswanathan, and G. Agha Model-checking markov chains in the presence of uncertainties. In Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings, p. 394–410. External Links: Link, Document Cited by: §1, §1. Suilen et al. (2024) M. Suilen, T. Badings, E. M. Bovy, D. Parker, and N. Jansen Robust markov decision processes: A place where AI and formal methods meet. In Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I, p. 126–154. External Links: Link, Document Cited by: §1. Suilen et al. (2020) M. Suilen, N. Jansen, M. Cubuktepe, and U. Topcu Robust policy synthesis for uncertain pomdps via convex optimization. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, p. 4113–4120. External Links: Link, Document Cited by: §1, §1. Summers and Lygeros (2010) S. Summers and J. Lygeros Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Autom. 46 (12), p. 1951–1961. External Links: Link, Document Cited by: §1. Tamar et al. (2014) A. Tamar, S. Mannor, and H. Xu Scaling up robust mdps using function approximation. In Proceedings of the 31th International Conference on Machine Learning, ICML 2014, Beijing, China, 21-26 June 2014, p. 181–189. External Links: Link Cited by: §1. Tessler et al. (2019) C. Tessler, Y. Efroni, and S. Mannor Action robust reinforcement learning and applications in continuous control. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, p. 6215–6224. External Links: Link Cited by: §1. Tewari and Bartlett (2007) A. Tewari and P. L. Bartlett Bounded parameter markov decision processes with average reward criterion. In Learning Theory, 20th Annual Conference on Learning Theory, COLT 2007, San Diego, CA, USA, June 13-15, 2007, Proceedings, p. 263–277. External Links: Link, Document Cited by: §1. Thomas (1997) W. Thomas Languages, automata, and logic. In Handbook of Formal Languages, Volume 3: Beyond Words, p. 389–455. External Links: Link, Document Cited by: §2. Wang et al. (2023) Y. Wang, A. Velasquez, G. K. Atia, A. Prater-Bennette, and S. Zou Robust average-reward markov decision processes. In Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, p. 15215–15223. External Links: Link, Document Cited by: §1. Wang et al. (2024) Y. Wang, A. Velasquez, G. K. Atia, A. Prater-Bennette, and S. Zou Robust average-reward reinforcement learning. J. Artif. Intell. Res. 80, p. 719–803. External Links: Link, Document Cited by: §1. Wang and Zou (2021) Y. Wang and S. Zou Online robust reinforcement learning with model uncertainty. In Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual, p. 7193–7206. External Links: Link Cited by: §1. Wang and Zou (2022) Y. Wang and S. Zou Policy gradient method for robust reinforcement learning. In International Conference on Machine Learning, ICML 2022, 17-23 July 2022, Baltimore, Maryland, USA, p. 23484–23526. External Links: Link Cited by: §1. Wiesemann et al. (2013) W. Wiesemann, D. Kuhn, and B. Rustem Robust markov decision processes. Math. Oper. Res. 38 (1), p. 153–183. External Links: Link, Document Cited by: §1. Appendix Table of Contents • Section A Conversion of RPOMDP ℳM to POSG G – Section A.1 Mapping of plays, observation histories and strategies from ℳM to G – Section A.2 Lifting objectives from ℳM to G – Section A.3 Value Preservation between ℳM to G – Section A.4 Proof of Theorem 3.1 • Section B ac-POSG G to Pre-min transformed POSG ′G – Section B.1 Mapping of plays, observation histories and strategies from G to ′G – Section B.2 Lifting objectives from G to ′G – Section B.3 Value Preservation between G to ′G – Section B.3.1 Size and memory preservation between G and ′G – Section B.4 Proof of Lemma 3.2 • Section C Constructing an RPOMDP from a Pre- min-transformed POSG – Section C.1 Mapping of plays, observation histories and strategies from ′G to ℜ() R\! (G ) – Section C.2 Lifting objectives from ′G to ℜ() R\! (G ) – Section C.3 Value Preservation between ′G to ℜ() R\! (G ) – Section C.3.1 Size and memory preservation between ′G and ℜ() R\! (G ) – Section C.4 Proof of Lemma 3.3 As in the main text, all actions are formally enabled at all states. When a construction displays only effective actions, omitted actions are implicitly completed by an absorbing outcome losing for their owner. We suppress these dominated transitions and carry out the mappings on the displayed effective actions. For the max-player, assigning positive probability to an omitted action can only decrease the probability of satisfying the objective, so that probability can be reassigned to an effective action. Dually, an omitted min-action reaches a max-winning outcome and therefore cannot improve the min-player’s strategy. Thus both players may be restricted to effective actions without changing the value or the sure, almost-sure, limit-sure, and quantitative winning sets. This argument applies because all objectives considered here are represented as parity objectives and the completion outcomes are absorbing wins or losses; an arbitrary action-sensitive objective would first need to be encoded in the state space. Appendix A Reduction of RPOMDPs to POSGs Definition: Let ℳ=(S,A,,,,,,s0)M=(S,A,P,O_ a,O_ e,Z_ a,Z_ e,s_0) be a polytopic RPOMDP. We define the POSG induced by ℳM as =(S,S,A,A,δ,s0,,,,)G=(S_ max^G,S_ min^G,A_ max^G,A_ min^G,δ^G,s_0^G,O_ max^G,O_ min^G,Z_ max^G,Z_ min^G). For each (s,a)∈S×A(s,a)∈ S× A, let Vs,aV_s,a denote the set of vertices of the local uncertainty polytope P(s,a)P(s,a). • States: S=S_ max^G=S and S=S×AS_ min^G=S× A. Let S=S∪S^G=S_ max^G∪ S_ min^G. • Actions: A=A_ max^G=A and A=⋃(s,a)∈S×AVs,aA_ min^G= _(s,a)∈ S× AV_s,a. At min-state (s,a)(s,a) the effective actions are Vs,aV_s,a; all remaining min-actions use the implicit min-losing transition. Let A=A∪A^G=A_ max^G∪ A_ min^G. • Transition function δ:(S×A)∪(S×A)→Δ(S)δ^G:(S_ max^G× A_ max^G)∪(S_ min^G× A_ min^G)→ (S^G) is defined as follows: – For max-player having state-action pairs (s,a)∈S×A(s,a)∈ S_ max^G× A_ max^G, the transition function is given as Dirac distribution with probability mass on state (s,a)∈S(s,a)∈ S_ min^G δ(s,a)(s′)=1if s′=(s,a)0otherwiseδ^G(s,a)(s )= cases1&if s =(s,a)\\ 0&otherwise cases – For an effective min-action v∈Vs,av∈ V_s,a at (s,a)∈S(s,a)∈ S_ min^G, the transition function is the probability distribution over S_ max^G given by δ((s,a),v)(s′)=v(s′)wheres′∈Sandv(s′)denotes thes′th entry inv0otherwiseδ^G((s,a),v)(s )= casesv(s )&where~s ∈ S_ max^G~and~v(s )~denotes the~s th entry in~v\\ 0&otherwise cases Every other globally enabled min-action follows the default max-winning transition and is suppressed from the display. • Initial state: s0=s0∈Ss_0^G=s_0∈ S_ max^G. • Observation functions: Z_ max^G and Z_ min^G are functions from states S^G to O_ max^G and O_ min^G respectively. – For s∈Ss∈ S_ max^G, (s)=(s)Z_ max^G(s)=Z_ a(s) – For (s,a)∈S(s,a)∈ S_ min^G, ((s,a))=(s)Z_ max^G((s,a))=Z_ a(s) – For s∈Ss∈ S_ max^G, (s)=(s)Z_ min^G(s)=Z_ e(s) – For (s,a)∈S(s,a)∈ S_ min^G, ((s,a))=(s)Z_ min^G((s,a))=Z_ e(s) An effective play in G has the form ρ=s0,a0,s1,a1,…∈ρ=s_0,a_0,s_1,a_1,…∈ Plays_G, where for every k≥0k≥ 0, s2k∈Ss_2k∈ S_ max^G, a2k∈Aa_2k∈ A_ max^G, s2k+1=(s2k,a2k)∈Ss_2k+1=(s_2k,a_2k)∈ S_ min^G, and a2k+1∈Vs2k,a2ka_2k+1∈ V_s_2k,a_2k. Non-matching min-actions take the implicit min-losing transition. At step t, the history is ht=s0,(o01,o02),s1,…,st,(ot1,ot2)h_t=s_0,(o^1_0,o^2_0),s_1,…,s_t,(o^1_t,o^2_t), where oi1=(si)o^1_i=Z_ max^G(s_i) and oi2=(si)o^2_i=Z_ min^G(s_i). A.1 Mapping Plays, Observation Histories and Strategies from ℳM to G In this section, we establish a formal mapping between the plays, observation histories and strategies of the RPOMDP ℳM and the POSG G. Mapping on Plays: • Define a mapping Θ:ℳ→2 : Plays_M→ 2 Plays_G as follows. Let ρ=s0,a0,s1,a1,⋯∈ℳρ=s_0,a_0,s_1,a_1,·s∈ Plays_M. Then Θ(ρ) (ρ) is the set of all plays ρ′=s0′,a0′,s1′,a1′,s2′,a2′,⋯∈ρ =s _0,a _0,s _1,a _1,s _2,a _2,·s∈ Plays_G is given index-wise, ∀k≥0:∀ k≥ 0: s2k′=sk,a2k′=ak,s2k+1′=(s2k′,a2k′)=(sk,ak),a2k+1′=v∈Vsk,aks _2k=s_k,a _2k=a_k,s _2k+1=(s _2k,a _2k)=(s_k,a_k),a _2k+1=v∈ V_s_k,a_k (arbitrary v). Thus, Θ(ρ) (ρ) consists of all plays in G obtained by resolving each transition in ρ using an arbitrary choice of vertex from the uncertainty set at each step. For X⊆ℳ,Θ(X)=⋃ρ∈XΘ(ρ)X Plays_M, (X)= _ρ∈ X (ρ). • Define Υ:→ℳ : Plays_G→ Plays_M as follows. Let ρ′=s0′,a0′,s1′,a1′,s2′,a2′,⋯ρ =s _0,a _0,s _1,a _1,s _2,a _2,·s be a play in G. Then Υ(ρ′)=ρ=s0,a0,s1,a1,⋯∈ℳ (ρ )=ρ=s_0,a_0,s_1,a_1,·s∈ Plays_M is given index-wise by si=s2i′s_i=s _2i and ai=a2i′a_i=a _2i for every i≥0i≥ 0. The map Υ is many-to-one. For Y⊆Y Plays_G, define Υ(Y)=Υ(ρ′)∣ρ′∈Y (Y)=\ (ρ ) ρ ∈ Y\; for X⊆ℳX Plays_M, define its preimage Υ−1(X)=ρ′∈∣Υ(ρ′)∈X ^-1(X)=\ρ ∈ Plays_G (ρ )∈ X\. Mapping on Observation Histories: a,e OH_a, OH_e denote the set of agent and environment observation histories respectively in RPOMDP ℳM. , OH^G_ max, OH^G_ min denote observation histories of , max, min players respectively in POSG G. 1. Define Θa:a→ _a: OH_a→ OH_ max^G. For agent observation history oha=o0,o1⋯,ot∈aoh^a=o_0,o_1·s,o_t∈ OH_a, the mapping is given by Θa(oha)=oh=o0′,o1′,⋯,o2t′ _a(oh^a)=oh max=o _0,o _1,·s,o _2t is given index-wise, ∀ 0≤k≤t−1,o2k′=o2k+1′=ok,o2t′=ot∀\>0≤ k≤ t-1,o _2k=o _2k+1=o_k,o _2t=o_t. 2. Define Υa:→a _a: OH_ max^G→ OH_a. For max-player observation history oh=o0,o1,⋯,ot−1,otoh max=o_0,o_1,·s,o_t-1,o_t, the mapping is given by Υa(oh)=oha=o0′,o1′,⋯,ot/2′ _a(oh max)=oh^a=o _0,o _1,·s,o _t/2 is given index-wise, ∀0≤i≤t/2,oi′=o2i\>∀ 0≤ i≤ t/2,\>\>o _i=o_2i. 3. Define Θe:e→ _e: OH_e→ OH_ min^G. Let ohe=o0,o1,⋯,ot∈eoh^e=o_0,o_1,·s,o_t∈ OH_e. The function is given by Θe(ohe)=oh=o0′,o1′,⋯,o2t′,o2t+1′ _e(oh^e)=oh min=o _0,o _1,·s,o _2t,o _2t+1 is given index-wise, ∀0≤k≤t,o2k′=o2k+1′=ok∀ 0≤ k≤ t,o _2k=o _2k+1=o_k. 4. Define Υe:→e _e: OH_ min^G→ OH_e. Let oh=o0,o1,⋯,ot∈oh min=o_0,o_1,·s,o_t∈ OH_ min^G. The function is given by Υe(oh)=ohe=o0′,o1′,⋯,o(t−1)/2′ _e(oh min)=oh^e=o _0,o _1,·s,o _(t-1)/2 is given index-wise, ∀0≤i≤(t−1)/2,oi′=o2i∀ 0≤ i≤(t-1)/2,\>\>o _i=o_2i. Lemma A.1. Let ⋆∈a,e ∈\a,e\. Θ⋆ _ and Υ⋆ _ are inverses of each other. Proof. 1. For all oh=o1,o1,o2,o2,⋯,ot−1,ot−1,ot∈oh=o_1,o_1,o_2,o_2,·s,o_t-1,o_t-1,o_t∈ OH^G_ max, Θa(Υa(oh))=Θa(o1,o2,⋯,ot−1,ot)=o1,o1,o2,o2,⋯,ot−1,ot−1,ot=oh _a( _a(oh))= _a(o_1,o_2,·s,o_t-1,o_t)=o_1,o_1,o_2,o_2,·s,o_t-1,o_t-1,o_t=oh 2. For all oh=o1,o2,⋯,ot−1,ot∈aoh=o_1,o_2,·s,o_t-1,o_t∈ OH_a, Υa(Θa(oh))=Υa(o1,o1,o2,o2,⋯,ot−1,ot−1,ot)=o1,o2,⋯,ot−1,ot=oh _a( _a(oh))= _a(o_1,o_1,o_2,o_2,·s,o_t-1,o_t-1,o_t)=o_1,o_2,·s,o_t-1,o_t=oh 3. For all oh=o1,o1,o2,o2,⋯,ot−1,ot−1,ot,ot∈oh=o_1,o_1,o_2,o_2,·s,o_t-1,o_t-1,o_t,o_t∈ OH^G_ min, Θe(Υe(oh))=Θe(o1,o2,⋯,ot−1,ot)=o1,o1,o2,o2,⋯,ot−1,ot−1,ot,ot=oh _e( _e(oh))= _e(o_1,o_2,·s,o_t-1,o_t)=o_1,o_1,o_2,o_2,·s,o_t-1,o_t-1,o_t,o_t=oh 4. For all oh=o1,o2,⋯,ot−1,ot∈eoh=o_1,o_2,·s,o_t-1,o_t∈ OH_e, Υe(Θe(oh))=Υe(o1,o1,o2,o2,⋯,ot−1,ot−1,ot,ot)=o1,o2,⋯,ot−1,ot=oh _e( _e(oh))= _e(o_1,o_1,o_2,o_2,·s,o_t-1,o_t-1,o_t,o_t)=o_1,o_2,·s,o_t-1,o_t=oh ∎ Mapping of Strategies For each (s,a)∈S×A(s,a)∈ S× A, define the barycenter map s,a:Δ(Vs,a)→P(s,a),s,a(λ)=∑v∈Vs,aλ(v)v. bar_s,a: (V_s,a)→ P(s,a), bar_s,a(λ)= _v∈ V_s,aλ(v)v. For each P∈P(s,a)P∈ P(s,a), choose coefficients αs,aP∈Δ(Vs,a)α^P_s,a∈ (V_s,a) such that s,a(αs,aP)=P bar_s,a(α^P_s,a)=P. Such coefficients need not be unique; fix one choice for every P once and for all. We identify Δ(Vs,a) (V_s,a) with distributions over A_ min^G supported on Vs,aV_s,a. Also fix an arbitrary reference distribution Ps,a0∈P(s,a)P^0_s,a∈ P(s,a) for every (s,a)∈S×A(s,a)∈ S× A. 1. The agent strategy σ∈Σℳσ∈ _M for RPOMDP ℳM is given by σ:a→⋃o∈∏s:(s)=oΔ(A)σ: OH_a→ _o _ a _s:\,Z_ a(s)=o (A) 2. The environment strategy π∈Πℳπ∈ _M for RPOMDP ℳM is given by π:e×A→.π: OH_e× A . 3. The max-player strategy σ′∈Σσ ∈ _G for POSG G from the reduction is given by σ′:→⋃o∈∏s∈S:(s)=oΔ(A)σ : OH_ max^G→ _o _ max^G _s∈ S_ max^G:\,Z_ max^G(s)=o (A_ max^G) (recall that max and min states alternate) 4. The min-player strategy π′∈Ππ ∈ _G for POSG G from the reduction is given by π′:→⋃o∈∏s∈S:(s)=oΔ(A)π : OH_ min^G→ _o _ min^G _s∈ S_ min^G:\,Z_ min^G(s)=o (A_ min^G) (recall that max and min states alternate) Define the mappings • ℭa:Σℳ→Σ C_a: _M→ _G. For all σ∈Σℳσ∈ _M and oh∈oh∈ OH_ max^G, ℭa(σ)(oh)=σ(Υa(oh)). C_a(σ)(oh)=σ( _a(oh)). • a:Σ→Σℳ D_a: _G→ _M. For all σ′∈Σσ ∈ _G and oh∈aoh∈ OH_a, a(σ′)(oh)=σ′(Θa(oh)). D_a(σ )(oh)=σ ( _a(oh)). • ℭe:Πℳ→Π C_e: _M→ _G. For all π∈Πℳπ∈ _M, oh∈oh∈ OH_ min^G, and (s,a)∈S(s,a)∈ S_ min^G with ((s,a))=last(oh)Z_ min^G((s,a))=last(oh), use the component notation above. ℭe(π)(oh)((s,a))=αs,aπ(Υe(oh),a)(s,a). C_e(π)(oh)((s,a))=α^π( _e(oh),a)(s,a)_s,a. • e:Π→Πℳ D_e: _G→ _M. For all π′∈Ππ ∈ _G, oh∈eoh∈ OH_e, and a∈Aa∈ A, define the complete assignment e(π′)(oh,a)∈ D_e(π )(oh,a) componentwise as follows. e(π′)(oh,a)(x,b)=x,a(π′(Θe(oh))((x,a)))if b=a and (x)=last(oh),Px,b0otherwise. D_e(π )(oh,a)(x,b)= cases bar_x,a\! (π ( _e(oh))((x,a)) )&if b=a and Z_ e(x)=last(oh),\\ P^0_x,b&otherwise. cases Hence every component belongs to its corresponding local uncertainty set. Remark A.2. For every π∈Πℳπ∈ _M, oh∈oh∈ OH_ min^G, and compatible (s,a)(s,a), π(Υe(oh),a)(s,a)=s,a(ℭe(π)(oh)((s,a))).π( _e(oh),a)(s,a)= bar_s,a\! ( C_e(π)(oh)((s,a)) ). Lemma A.3. The agent maps ℭa C_a and a D_a are mutual inverses. The environment maps satisfy, at every compatible ohoh, s, and a, e(ℭe(π))(oh,a)(s,a) D_e( C_e(π))(oh,a)(s,a) =π(oh,a)(s,a), =π(oh,a)(s,a), s,a(ℭe(e(π′))(oh)((s,a))) bar_s,a\! ( C_e( D_e(π ))(oh)((s,a)) ) =s,a(π′(oh)((s,a))). = bar_s,a\! (π (oh)((s,a)) ). Thus both compositions preserve the next-state distribution. Proof. The agent identities follow from Lemma A.1. The environment identities follow from s,a(αs,aP)=P bar_s,a(α^P_s,a)=P and the two history identities in Lemma A.1. ∎ A.2 Lifting Objectives Let W be a parity objective in RPOMDP ℳM given by the priority function p:S→0,1,⋯,d,d∈ℕp:S→\0,1,·s,d\,\ d . Then, the lifted objective in POSG G, W′⊆W Plays^G is given the priority function p:S∪S→0,1,⋯,dp^G:S_ max^G∪ S_ min^G→\0,1,·s,d\ defined as p(s)=p(s)if s∈Sp(s′)if s=(s′,a)∈Sp^G(s)= casesp(s)&if s∈ S_ max^G\\ p(s )&if s=(s ,a)∈ S_ min^G\\ cases Lemma A.4. Let W be parity objective in RPOMDP ℳM given by the priority function p and let W′W be the lifted objective in POSG G. Then, ρ∈W⇔Θ(ρ)⊆W′ρ∈ W (ρ) W Proof. We have W=Parityℳ(p)W=Parity_M\! (p ) and W′=Parity(p)W =Parity_G\! (p^G ) where p^G is defined as above. Any play ρ=s0,a0,s1,a1,⋯∈ℳρ=s_0,a_0,s_1,a_1,·s∈ Plays_M has parity sequence: p(ρ)=p0,p1,p2,⋯p(ρ)=p_0,p_1,p_2,·s such that pi=p(si)p_i=p(s_i). Any play in Θ(ρ) (ρ) is of the form ρ′=s0,a0,(s0,a0),a0′,s1,⋯ρ =s_0,a_0,(s_0,a_0),a _0,s_1,·s with parity sequence p(ρ′)=p0,p0,p1,p1,⋯p^G(ρ )=p_0,p_0,p_1,p_1,·s, since p(si)=p((si,ai))=p(si)p^G(s_i)=p^G((s_i,a_i))=p(s_i). Due to repeating values lim infi→∞ _i→∞ of the sequence do not change, then lim infi→∞(p(ρ))=lim infi→∞(p(ρ′)) _i→∞(p(ρ))= _i→∞(p^G(ρ )). Thus, ρ∈W⟹ρ′∈W′⇔Θ(ρ)⊆W′ρ∈ W ρ ∈ W (ρ) W . The reverse direction follows similarly. ∎ A.3 Value Preservation Lemma A.5. The strategy maps preserve the induced probability measure in both directions. In particular, ℙℳσ,π(W) _M^σ,π(W) =ℙℭa(σ),ℭe(π)(W′) =P_G C_a(σ), C_e(π)(W ) for all σ∈Σℳ, π∈Πℳ, all $σ∈ _ M$, $π∈ _M$, ℙσ′,π′(W′) _G^σ ,π (W ) =ℙℳa(σ′),e(π′)(W) =P_M D_a(σ ), D_e(π )(W) for all σ′∈Σ, π′∈Π, all $σ ∈ _G$, $π ∈ _G$, where W⊆ℳW Plays_M is a parity objective of ℳM and W′=Θ(W)W = (W) is the corresponding objective in G. Proof. For a history h, let Cyl(h)Cyl(h) denote the set of all runs having h as a prefix. Since the probability measure over runs is uniquely determined by its values on cylinder sets, it suffices to show that corresponding cylinder sets have the same probability. Let HℳH_M(resp. H_G) denote the set of histories in RPOMDP ℳM (resp. POSG G). Define the mapping Θh:Hℳ→2H _h:H_M→ 2^H_G as follows: Let h=s0,(o0a,o0e),s1,…st,(ota,ote)∈Hℳh=s_0,(o^a_0,o^e_0),s_1,… s_t,(o^a_t,o^e_t)∈ H_M. Then Θh(h) _h(h) is the set of all histories h′=s0′,(o0max,o0min),s1′,…s2t′,(o2tmax,o2tmin)h =s _0,(o^max_0,o^min_0),s _1,… s _2t,(o^max_2t,o^min_2t) is given index-wise, ∀k≥0:∀ k≥ 0: s2k′=sk,s2k+1′=(sk,ak)s _2k=s_k,s _2k+1=(s_k,a_k) where ak∈Aa_k∈ A_ max^G and ∀i≥0∀ i≥ 0 oimax=(si′),oimin=(si′)o^max_i=Z_ max^G(s _i),o^min_i=Z_ min^G(s _i). Thus, Θh(h) _h(h) consists of all histories in G obtained by resolving each transition in h using an arbitrary choice of action from A_ max^G at each step. We show that for a finite history h in W, there exists corresponding set of histories H′=Θh(h)H = _h(h) in W′W such that ℙℳσ,π(Cyl(h))=∑h′∈H′ℙℭa(σ),ℭe(π)(Cyl(h′))P_M^σ,π(Cyl(h))= _h ∈ H P_G C_a(σ), C_e(π)(Cyl(h )) The proof follows induction on the length of h with base condition h=s0h=s_0 and H′=s0H =\s_0\ with values ℙℳσ,π(Cyl(h))=∑h′∈H′ℙℭa(σ),ℭe(π)(Cyl(h′))=1P_M^σ,π(Cyl(h))= _h ∈ H P_G C_a(σ), C_e(π)(Cyl(h ))=1. For induction, let h=h1,s1,(o1,o1′)h=h_1,s_1,(o_1,o _1) where o1=(s1),o1′=(s1)o_1=Z_ a(s_1),o _1=Z_ e(s_1) and h1h_1 ending in state s with observations history pair (o,o′)(o,o ). Let H1′=Θh(h1)H _1= _h(h_1). A history h′∈H′h ∈ H is of the form h′=h1′,(s,a),(o,o′),s1,(o1,o1′)h =h _1,(s,a),(o,o ),s_1,(o_1,o _1) where h1′∈H1′,a∈Ah _1∈ H _1,\>a∈ A(an arbitrary action a). Let oha,oheoh^a,oh^e be the agent and environment observations histories for history h1h_1. Let ohoh max be max player observation history for all histories h1′∈H1′h _1∈ H _1. Then oha=Υa(oh)oh^a= _a(oh max). Let ohoh min be min player observation history for h1′,(s,a),(o,o′)h _1,(s,a),(o,o ) where h′∈H1′h ∈ H _1. Then ohe=Υe(oh)oh^e= _e(oh min). For a given σ′∈Σ,π′∈Πσ ∈ _G,π ∈ _G in history h′h , the transition probability from s to (s,a)(s,a) is given by σ′(oh)(s)(a)σ (oh max)(s)(a) and the transition probability from (s,a)(s,a) to s1s_1 is given by all the transitions on the vertices v∈Vs,av∈ V_s,a i.e., (∑v∈Vs,aπ′(oh)((s,a))(v)⋅v(s1)) ( _v∈ V_s,aπ (oh min)((s,a))(v)· v(s_1) ). ∑h′∈H′ _h ∈ H ℙℭa(σ),ℭe(π)(Cyl(h′)) _G C_a(σ), C_e(π)(Cyl(h )) =∑h′∈H′(ℙℭa(σ),ℭe(π)(Cyl(h1′))×ℭa(σ)(oh)(s)(a)×(∑v∈Vs,aℭe(π)(oh)((s,a))(v)⋅v(s1))) = _h ∈ H (P_G C_a(σ), C_e(π)(Cyl(h_1 ))× C_a(σ)(oh max)(s)(a)× ( _v∈ V_s,a C_e(π)(oh min)((s,a))(v)· v(s_1) ) ) =∑h′∈H1′ℙℭa(σ),ℭe(π)(Cyl(h1′))×∑a∈A(ℭa(σ)(oh)(s)(a)×(∑v∈Vs,aℭe(π)(oh)((s,a))(v)⋅v(s1))) = _h ∈ H _1P_G C_a(σ), C_e(π)(Cyl(h_1 ))× _a∈ A ( C_a(σ)(oh max)(s)(a)× ( _v∈ V_s,a C_e(π)(oh min)((s,a))(v)· v(s_1) ) ) By induction hypothesis, ∑h′∈H1′ℙℭa(σ),ℭe(π)(Cyl(h1′))=ℙℳσ,π(Cyl(h1)) _h ∈ H _1P_G C_a(σ), C_e(π)(Cyl(h _1))=P_M^σ,π(Cyl(h_1)). From definition of ℭa C_a, ℭa(σ)(oh)(s)(a)=σ(Υa(oh))(s)(a)=σ(oha)(s)(a) C_a(σ)(oh max)(s)(a)=σ( _a(oh max))(s)(a)=σ(oh^a)(s)(a). From remark A.2, (∑v∈Vs,aℭe(π)(oh)((s,a))(v)⋅v(s1))=π(Υe(oh),a)(s,a)(s1)=π(ohe,a)(s,a)(s1) ( _v∈ V_s,a C_e(π)(oh min)((s,a))(v)· v(s_1) )=π( _e(oh min),a)(s,a)(s_1)=π(oh^e,a)(s,a)(s_1). So, ∑h′∈H′ℙℭa(σ),ℭe(π)(Cyl(h′)) _h ∈ H P_G C_a(σ), C_e(π)(Cyl(h )) =ℙℳσ,π(Cyl(h1))×∑a∈A(σ(oha)(s)(a)×π(ohe,a)(s,a)(s1)) =P_M^σ,π(Cyl(h_1))× _a∈ A (σ(oh^a)(s)(a)×π(oh^e,a)(s,a)(s_1) ) =ℙℳσ,π(Cyl(h)) =P_M^σ,π(Cyl(h)) The converse cylinder identity follows by the same induction, replacing the vertex distribution by its barycenter. The second identity of Lemma A.3 shows that this replacement preserves every next-state probability. Equality on all cylinders yields both asserted measure equalities and hence both objective-probability equalities. ∎ Lemma A.6. Let W⊆ℳW Plays_M be a parity objective of ℳM and let W′=Θ(W)W = (W) be the corresponding objective in G. Then, Valℳ(W)=Val(W′).Val_M(W)=Val_G(W ). Proof. For fixed σ∈Σℳσ∈ _M, set qℳ(σ)=infπ∈Πℳℙℳσ,π(W),q(σ′)=infπ′∈Πℙσ′,π′(W′).q_M(σ)= _π∈ _MP_M^σ,π(W), q_G(σ )= _π ∈ _GP_G^σ ,π (W ). The first equality in Lemma A.5 gives q(ℭa(σ))≤qℳ(σ)q_G( C_a(σ))≤ q_M(σ), because every π∈Πℳπ∈ _M has the image ℭe(π)∈Π C_e(π)∈ _G. Conversely, for every π′∈Ππ ∈ _G, the second equality in Lemma A.5 and a(ℭa(σ))=σ D_a( C_a(σ))=σ give ℙℭa(σ),π′(W′)=ℙℳσ,e(π′)(W),P_G C_a(σ),π (W )=P_M^σ, D_e(π )(W), hence qℳ(σ)≤q(ℭa(σ))q_M(σ)≤ q_G( C_a(σ)). Therefore qℳ(σ)=q(ℭa(σ))for every σ∈Σℳ.q_M(σ)=q_G( C_a(σ)) every $σ∈ _ M$. Finally, ℭa C_a is a bijection by Lemma A.3, so taking the outer supremum yields Valℳ(W) _M(W) =supσ∈Σℳqℳ(σ)=supσ∈Σℳq(ℭa(σ)) = _σ∈ _Mq_M(σ)= _σ∈ _Mq_G( C_a(σ)) =supσ′∈Σq(σ′)=Val(W′). = _σ ∈ _Gq_G(σ )=Val_G(W ). ∎ Lemma A.7. For mapped strategies, projection preserves the supported plays in both directions: Υ(ℭa(σ),ℭe(π)) \! ( Plays C_a(σ), C_e(π)_G ) =ℳσ,π, = Plays^σ,π_M, Υ(σ′,π′) \! ( Plays^σ ,π _G ) =ℳa(σ′),e(π′). = Plays D_a(σ ), D_e(π )_M. Proof. We prove the first equality by induction on finite effective prefixes; the second follows by the same argument using the reverse maps. The initial prefixes coincide. Suppose corresponding prefixes end in the RPOMDP state s and the POSG max-state s. Their agent observation histories correspond under Θa _a and Υa _a, and ℭa(σ)(Θa(oha))(s)=σ(oha)(s). C_a(σ)( _a(oh^a))(s)=σ(oh^a)(s). Consequently, an action a has positive probability after one prefix exactly when it has positive probability after the other. The POSG then moves deterministically to (s,a)(s,a). At the min-state (s,a)(s,a), let λ=ℭe(π)(Θe(ohe))((s,a))λ= C_e(π)( _e(oh^e))((s,a)) and P=π(ohe,a)(s,a)=s,a(λ)P=π(oh^e,a)(s,a)= bar_s,a(λ). For every successor s′s , nonnegativity gives P(s′)>0⟺λ(v)v(s′)>0 for some v∈Vs,a.P(s )>0 λ(v)v(s )>0 for some v∈ V_s,a. Thus an RPOMDP extension to s′s is supported exactly when some POSG extension through an effective vertex v to s′s is supported. This proves the induction step and the first projected-prefix equality. For arbitrary σ′,π′σ ,π , replace λ by π′(oh)((s,a))π (oh)((s,a)) and use the barycenter identity in Lemma A.3; the same induction proves the second equality. Finally, an infinite play is supported exactly when all its finite prefixes are supported, yielding both displayed play-set equalities. ∎ Lemma A.8 (Sure winning analysis). Let W⊆ℳW Plays_M be a parity objective of ℳM and W′=Υ−1(W)=Θ(W)W = ^-1(W)= (W) its lifted objective in G. The preimage Υ−1 ^-1 was defined in Appendix A.1. For σ∈Σℳσ∈ _M, let σ′=ℭa(σ)σ = C_a(σ). Then, σ is sure winning for W⇔σ′ is sure winning for W′.σ is sure winning for W σ is sure winning for W . Proof. Suppose first that σ is sure winning and take arbitrary π′∈Ππ ∈ _G. By Lemma A.7, Υ(σ′,π′)=ℳσ,e(π′)⊆W, \! ( Plays^σ ,π _G )= Plays^σ, D_e(π )_M W, so σ′,π′⊆Υ−1(W)=W′ Plays^σ ,π _G ^-1(W)=W . Conversely, suppose that σ′σ is sure winning and take arbitrary π∈Πℳπ∈ _M. The first equality in Lemma A.7 gives Υ(σ′,ℭe(π))=ℳσ,π ( Plays^σ , C_e(π)_G)= Plays^σ,π_M; since the game plays lie in W′W , their projections lie in W. ∎ Lemma A.9 (Almost-sure analysis). Let W⊆ℳW Plays_M be a parity objective of ℳM and W′=Θ(W)W = (W) its lifted objective in G. For σ∈Σℳσ∈ _M, let σ′=ℭa(σ)σ = C_a(σ). Then, σ is almost-sure winning for W⇔σ′ is almost-sure winning for W′.σ is almost-sure winning for W σ is almost-sure winning for W . Proof. The fixed-strategy equality established in the proof of Lemma A.6 gives infπ∈Πℳℙℳσ,π(W)=infπ′∈Πℙσ′,π′(W′). _π∈ _MP_M^σ,π(W)= _π ∈ _GP_G^σ ,π (W ). One side equals 11 if and only if the other does. ∎ Lemma A.10 (Limit-sure Analysis). Let W⊆ℳW Plays_M be a parity objective of ℳM and W′=Θ(W)W = (W) is the corresponding objective in G. Then, W is limit-sure winning⇔W′ is limit-sure winningW is limit-sure winning W is limit-sure winning Proof. Follows directly from lemma A.6. ∎ Lemma A.11 (Quantitative Analysis). Let W⊆ℳW Plays_M be a parity objective of ℳM and W′=Θ(W)W = (W) is the corresponding objective in G. Then, for k∈(0,1)k∈(0,1) Valℳ(W)≥k⇔Val(W′)≥kVal_M(W)≥ k _G(W )≥ k Proof. Follows directly from lemma A.6. ∎ A.4 Proof of Theorem 3.1 Proof. Because parity subsumes all ω-regular objectives, from Lemma A.6, Valℳ(W)=Val(W′)Val_M(W)=Val_G(W ) for any ω-regular objective W in ℳM and its lifted objective W′W in G. The “consequently” statement follows from lemmas A.8, A.9, A.10, and A.11. ∎ Appendix B The Pre- min-transformation from ac-POSG G to ′G In this section, we begin with the transformation from G to ′G . Consider any alternating control POSG G. In G the max-player selects an action from a max-state and the output is immediately a min-state (and vice versa). To make the subsequent RPOMDP construction cleaner, we first insert a dummy max-state dsd_s before every min-state s∈Ss∈ S_ min, so that the max-player always acts twice in a row before the min-player acts. The max-action at a dummy state is always the fixed action ⊤ with a deterministic transition to the corresponding min-state; it therefore carries no strategic content. Definition B.1 (Pre- min transformation). Given an alternating control POSG =(S,S,A,A,δ,s0,,,,)G=(S_ max,S_ min,A_ max,A_ min,δ,s_0,O_ max,O_ min,Z_ max,Z_ min), the Pre- min transformation of G is the POSG ′=(S′,S′,A′,A′,δ′,s0,′,′,′,′)G =(S_ max ,S_ min ,A_ max ,A_ min ,δ ,s_0,O_ max ,O_ min ,Z_ max ,Z_ min ) where: • State spaces: S′=S∪ds∣s∈S⏟D,S′=S,S_ max \;=\;S_ max\;∪\; \\,d_s s∈ S_ min\,\_D, S_ min \;=\;S_ min, where D is a set of fresh dummy max-states, one for each min-state. • Actions: A′=A∪⊤,A′=A,A_ max \;=\;A_ max\;∪\;\ \, A_ min \;=\;A_ min, where ⊤∉A ∉ A_ max is fresh. All actions in A′A_ max are enabled at every max-state; A_ max is effective at original max-states and ⊤ is effective at dummy states. • Transition function δ′δ : – For s1∈Ss_1∈ S_ max, a1∈Aa_1∈ A_ max, and s2∈Ss_2∈ S_ min: δ′(s1,a1)(ds2)=δ(s1,a1)(s2)δ (s_1,a_1)(d_s_2)=δ(s_1,a_1)(s_2). – For s2∈Ss_2∈ S_ min and a2∈Aa_2∈ A_ min: δ′(s2,a2)=δ(s2,a2)δ (s_2,a_2)=δ(s_2,a_2). – For ds∈Dd_s∈ D and action ⊤ : δ′(ds,⊤)=Dirac(s)δ (d_s, )=Dirac(s). – Every other max state-action pair follows the implicit max-losing transition. • Observations: ′=∪ox†∣x∈⏟†,′=∪ox#∣x∈⏟#.O_ max \;=\;O_ max\;∪\; \\,o _x x _ max\,\_O , _ min \;=\;O_ min\;∪\; \\,o^\#_x x _ min\,\_O^\#. • Observation functions: – ∀s∈S∪S∀ s∈ S_ max∪ S_ min: ′(s)=(s)Z_ max (s)=Z_ max(s) and ′(s)=(s)Z_ min (s)=Z_ min(s). – ∀ds∈D∀ d_s∈ D: ′(ds)=o(s)†Z_ max (d_s)=o _Z_ max(s) and ′(ds)=o(s)#Z_ min (d_s)=o^\#_Z_ min(s). B.1 Mapping plays, observation histories and strategies from G to ′G Mapping on plays. We define a map Γ:→′ : Plays_G→ Plays_G . Let h=s0,a0,s1,a1,s2,a2,⋯∈h=s_0,a_0,s_1,a_1,s_2,a_2,…∈ Plays_G. Since G is alternating control, even-indexed states lie in S_ max and odd-indexed states lie in S_ min. We set Γ(h)=h′=s0′,a0′,s1′,a1′,⋯ (h)=h =s _0,a _0,s _1,a _1,·s index-wise as: For k≥0k≥ 0, s3k′ s _3k =s2k =s_2k a3k′ a _3k =a2k =a_2k s3k+1′ s _3k+1 =ds2k+1 =d_s_2k+1 a3k+1′ a _3k+1 =⊤ = s3k+2′ s _3k+2 =s2k+1 =s_2k+1 a3k+2′ a _3k+2 =a2k+1 =a_2k+1 For X⊆X Plays_G, define Γ(X)=Γ(ρ)∣ρ∈X (X)=\ (ρ) ρ∈ X\. Observation B.2. By construction of ′G , Γ(h)∈′ (h)∈ Plays_G for every h∈h∈ Plays_G, so Γ is well-defined. Observation B.3. Every play h′=s1,a1,s2,a2,⋯∈′h =s_1,a_1,s_2,a_2,·s∈ Plays_G satisfies, for each k≥0k≥ 0: s3k+1∈S,a3k+1∈A,s3k+2∈D,a3k+2=⊤,s3k+3∈S,a3k+3∈As_3k+1∈ S_ max, a_3k+1∈ A_ max, s_3k+2∈ D, a_3k+2= , s_3k+3∈ S_ min, a_3k+3∈ A_ min Lemma B.4. Let h′∈′h ∈ Plays_G and let h be obtained by removing all occurrences of states in D and the action ⊤ from h′h . Then h∈h∈ Plays_G and Γ(h)=h′ (h)=h . Lemma B.5. The map Γ:→′ : Plays_G→ Plays_G is a bijection. Mapping on observation histories. We extend Γ to observation histories. For the max-player, define Γ:→′ _O max: OH^G_ max→ OH^G _ max as follows. Let oh=x0,y0,…,xn−1,yn−1,xn∈oh=x_0,y_0,…,x_n-1,y_n-1,x_n∈ OH^G_ max. Then Γ(oh)=x0,z0,y0,x1,z1,y1,…,xn−1,zn−1,yn−1,xn _O max(oh)=x_0,z_0,y_0,x_1,z_1,y_1,…,x_n-1,z_n-1,y_n-1,x_n where each zi=oyi†z_i=o _y_i. Since Γ(oh) _O max(oh) cannot end with a o†o -observation by construction, the map is not surjective. We nevertheless define an inverse (Γ)−1:′→( _O max)^-1: OH^G _ max→ OH^G_ max by removing all occurrences of observations in †O . We define Γ _O min and (Γ)−1( _O min)^-1 for the min-player analogously. Lemma B.6. Let ⋆∈, ∈\ max, min\. For all oh∈⋆oh∈ OH^G_ , (Γ⋆)−1(Γ⋆(oh))=oh( _O )^-1( _O (oh))=oh. Lemma B.7. Let ⋆∈, ∈\ max, min\ and let o⋆∈†o if ⋆= = max and o⋆∈#o ^\# otherwise. For all oh′=(oh1′,o)∈⋆′oh =(oh _1,o)∈ OH^G _ , Γ⋆((Γ⋆)−1(oh1′,o))=oh′if o≠o⋆,oh1′otherwise. _O \! (( _O )^-1(oh _1,o) )= casesoh &if o≠ o ,\\ oh _1&otherwise. cases Mapping of strategies. As in the main text, each player selects a complete prescription based only on its observation history. Thus, for ⋆∈, ∈\ max, min\, a strategy in G has type σ⋆:⋆→⋃o∈⋆∏s∈S⋆:⋆(s)=oΔ(A⋆), _ : OH_ ^G→ _o _ _s∈ S_ :\,Z_ (s)=o (A_ ), and the corresponding strategies in ′G use the same direct product with S′,S′,A′,A′S_ max ,S_ min ,A_ max ,A_ min . The expressions below evaluate the selected assignment at a compatible state; that state is not an input to the strategy. We define the following four maps lifting strategies between G and ′G : 1. Φ:Σ→Σ′ _ max: _G→ _G : for each σ∈Σσ∈ _G, oh′∈′oh ∈ OH^G _ max and ∀s∈S∪D∀ s∈ S_ max∪ D such that ′(s)=last(oh′)=last((Γ)−1(oh′))Z_ max (s)=last(oh )=last(( _O max)^-1(oh )), then Φ(σ)(oh′)(s)=σ((Γ)−1(oh′))(s) _ max(σ)(oh )(s)=σ (( _O max)^-1(oh ) )(s) If ′(s)=last(oh′)∈†Z_ max (s)=last(oh ) , then Φ(σ)(oh′)(s)=Dirac(⊤) _ max(σ)(oh )(s)=Dirac( ) 2. Φ:Π→Π′ _ min: _G→ _G : for each π∈Ππ∈ _G, oh′∈′oh ∈ OH^G _ min and ∀s∈S∀ s∈ S_ min such that ′(s)=last(oh′)Z_ min (s)=last(oh ), then Φ(π)(oh′)(s)=π((Γ)−1(oh′))(s) _ min(π)(oh )(s)=π\! (( _O min)^-1(oh ) )(s) 3. Ψ:Σ′→Σ _ max: _G → _G: for each σ′∈Σ′σ ∈ _G , oh∈oh∈ OH^G_ max and ∀s∈S∀ s∈ S_ max such that (s)=last(oh)Z_ max(s)=last(oh), then Ψ(σ′)(oh)(s)=σ′(Γ(oh))(s). _ max(σ )(oh)(s)=σ \! ( _O max(oh) )(s). 4. Ψ:Π′→Π _ min: _G → _G: for each π′∈Π′π ∈ _G , oh∈oh∈ OH_ min^G and ∀s∈S∀ s∈ S_ min such that (s)=last(oh)Z_ min(s)=last(oh), then Ψ(π′)(oh)(s)=π′(Γ(oh))(s). _ min(π )(oh)(s)=π \! ( _O min(oh) )(s). Lemma B.8. For ⋆∈, ∈\ max, min\, Φ⋆ _ and Ψ⋆ _ are inverses of each other: Φ⋆=(Ψ⋆)−1 _ =( _ )^-1 and Ψ⋆=(Φ⋆)−1 _ =( _ )^-1. Proof. Without loss of generality, let ⋆= = min. We first show Ψ(Φ(π))(oh)(s)=π(oh)(s) _ min( _ min(π))(oh)(s)=π(oh)(s) for all π∈Ππ∈ _G, oh∈oh∈ OH_ min^G and s∈Ss∈ S_ min such that (s)=last(oh)Z_ min(s)=last(oh). Ψ(Φ(π))(oh)(s) _ min( _ min(π))(oh)(s) =Φ(π)(Γ(oh))(s) = _ min(π)\! ( _O min(oh) )(s) by definition of Ψ definition of _ min =π((Γ)−1(Γ(oh)))(s) =π\! (( _O min)^-1\! ( _O min(oh) ) )(s) by definition of Φ definition of _ min =π(oh)(s) =π(oh)(s) by Lemma B.6. Conversely, for all π′∈Π′π ∈ _G , oh′∈′oh ∈ OH_ min^G and s∈Ss∈ S_ min such that ′(s)=last(oh′)Z_ min (s)=last(oh ): Φ(Ψ(π′))(oh′)(s) _ min( _ min(π ))(oh )(s) =Ψ(π′)((Γ)−1(oh′))(s) = _ min(π )\! (( _O min)^-1(oh ) )(s) by definition of Φ definition of _ min =π′(Γ((Γ)−1(oh′)))(s) =π \! ( _O min\! (( _O min)^-1(oh ) ) )(s) by definition of Ψ definition of _ min =π′(oh′)(s) =π (oh )(s) by Lemma B.7 and last(oh′)∉#last(oh ) ^\#. ∎ B.2 Lifting objectives from G to ′G Let p:S∪S→0,1,…,dp:S_ max∪ S_ min→\0,1,…,d\ be the priority function for G. Define p′:S′∪S′→0,1,…,dp :S_ max ∪ S_ min →\0,1,…,d\ by p′(s)=p(s)p (s)=p(s) for s∈S∪Ss∈ S_ max∪ S_ min and p′(ds)=p(s)p (d_s)=p(s) for ds∈Dd_s∈ D. Lemma B.9. Let G, ′G , p, and p′p be as above, and let ρ∈ρ∈ Plays_G. Then ρ∈Parity(p)⇔Γ(ρ)∈Parity′(p′).ρ _G\! (p ) (ρ) _G \! (p ). Proof. The play Γ(ρ) (ρ) visits every dummy state ds∈Dd_s∈ D exactly once between visiting s∈Ss∈ S_ max and s∈Ss∈ S_ min; p′(ds)=p(s)p (d_s)=p(s), so no new priority value is introduced. The sequence of priorities seen along Γ(ρ) (ρ) is therefore a repetition of the sequence seen along ρ (each value appears twice in a row at the dummy-state interleaving), which does not change the lim inf . Hence Γ(ρ) (ρ) satisfies the parity condition with respect to p′p if and only if ρ satisfies it with respect to p. ∎ B.3 Value Preservation Lemma B.10. The strategy maps preserve objective probabilities in both directions: ℙσ,π(W) _G^σ,π(W) =ℙ′Φ(σ),Φ(π)(W′), =P_G _ max(σ), _ min(π)(W ), for all σ∈Σ, π∈Π, all $σ∈ _ G$, $π∈ _G$, ℙ′σ′,π′(W′) _G ^σ ,π (W ) =ℙΨ(σ′),Ψ(π′)(W), =P_G _ max(σ ), _ min(π )(W), for all σ′∈Σ′, π′∈Π′, all $σ ∈ _G $, $π ∈ _G $, where W⊆W Plays_G is a parity objective of G and W′=Γ(W)W = (W) is its corresponding objective in ′G . Proof. Let ρ∈Wρ∈ W be a play of G and let ρ′=Γ(ρ)∈W′ρ = (ρ)∈ W . It suffices to show that for every finite history h in W the corresponding history h′h (constructed index-wise exactly as Γ constructs ρ′ρ from ρ, but truncated to end at the same state as h) satisfies ℙσ,π(Cyl(h))=ℙ′Φ(σ),Φ(π)(Cyl(h′)).P_G^σ,π(Cyl\! (h ))=P_G _ max(σ), _ min(π)(Cyl\! (h )). Since the probability measure over plays is uniquely determined by its values on cylinder sets, this suffices. The proof proceeds by induction on |h||h|. The base case h=s0h=s_0 holds trivially since h′=s0h =s_0 and both cylinders have probability 11. For the inductive step, write h=h1,sh=h_1,s and distinguish two cases. Case 1: s∈Ss∈ S_ max. Then last(h1)∈Slast(h_1)∈ S_ min. By construction, h′=h1′,sh =h _1,s where h1′h _1 is the prefix corresponding to h1h_1 and oh1′=′(h1′)oh_1 =Z_ min (h_1 ). Let oh1=(h1)oh_1=Z_ min(h_1) and s1=last(h1′)s_1=last(h _1). ℙ′Φ(σ),Φ(π)(Cyl(h′)) _G _ max(σ), _ min(π)(Cyl\! (h )) =ℙ′Φ(σ),Φ(π)(Cyl(h1′))×∑a∈A(Φ(π)(oh1′)(s1)(a)×δ′(s1,a)(s)). =P_G _ max(σ), _ min(π)(Cyl\! (h _1 ))× _a∈ A_ min ( _ min(π)(oh _1)(s_1)(a)×δ (s_1,a)(s) ). By the induction hypothesis, ℙ′Φ(σ),Φ(π)(Cyl(h1′))=ℙσ,π(Cyl(h1))P_G _ max(σ), _ min(π)(Cyl\! (h _1 ))=P_G^σ,π(Cyl\! (h_1 )). For a∈A:a∈ A_ min: By definition of Φ _ min, oh1′=(Γ)−1(oh1)oh _1=( _O min)^-1(oh_1) we have Φ(π)(oh1′)(s1)(a)=π(oh1)(s1)(a) _ min(π)(oh _1)(s_1)(a)=π(oh_1)(s_1)(a) and last(h1)=last(h1′)=s1last(h_1)=last(h _1)=s_1 by construction and δ′=δ =δ on S×AS_ min× A_ min we have δ′(s1,a)(s)=δ(s1,a)(s)δ (s_1,a)(s)=δ(s_1,a)(s). Hence ℙ′Φ(σ),Φ(π)(Cyl(h′)) _G _ max(σ), _ min(π)(Cyl\! (h )) =ℙσ,π(Cyl(h1))×∑a∈A(π(oh1)(s1)(a)×δ(s1,a)(s)) =P_G^σ,π(Cyl\! (h_1 ))× _a∈ A_ min (π(oh_1)(s_1)(a)×δ(s_1,a)(s) ) =ℙσ,π(Cyl(h)) =P_G^σ,π(Cyl\! (h )) Case 2: s∈Ss∈ S_ min. Then last(h1)∈Slast(h_1)∈ S_ max. By construction, h′=h1′,ds,sh =h _1,d_s,s, so (h′)=oh1′,o†,oZ_ max(h )=oh _1,o _o,o where o=(s)o=Z_ max(s) and oh1′=′(h1′)oh _1=Z_ max (h _1) . Let oh1=(h1)oh_1=Z_ max(h_1) and s1=last(h1′)=last(h1)s_1=last(h _1)=last(h_1). ℙ′Φ(σ),Φ(π)(Cyl(h′)) _G _ max(σ), _ min(π)(Cyl\! (h )) =ℙ′Φ(σ),Φ(π)(Cyl(h1′)) =P_G _ max(σ), _ min(π)(Cyl\! (h _1 )) ×∑a∈A(Φ(σ)(oh1′)(s1)(a)×δ′(s1,a)(ds)) × _a∈ A_ max ( _ max(σ)(oh _1)(s_1)(a)×δ (s_1,a)(d_s) ) ×Φ(σ)(oh1′,o†)(ds)(⊤)×δ′(ds,⊤)(s). × _ max(σ)(oh _1,o _o)(d_s)( )×δ (d_s, )(s). By the induction hypothesis the ℙ′Φ(σ),Φ(π)(Cyl(h1′))=ℙσ,π(Cyl(h1))P_G _ max(σ), _ min(π)(Cyl\! (h _1 ))=P_G^σ,π(Cyl\! (h_1 )). For a∈Aa∈ A_ max: By definition of Φ _ max, oh1=(Γ)−1(oh1′)oh_1=( _O max)^-1(oh _1) Φ(σ)(oh1′)(s1)(a)=σ(oh1)(s1)(a) _ max(σ)(oh _1)(s_1)(a)=σ(oh_1)(s_1)(a) and By construction of ′G , δ′(s1,a)(ds)=δ(s1,a)(s)δ (s_1,a)(d_s)=δ(s_1,a)(s). Since ⊤ is the sole effective action at any dummy state, Φ(σ)(oh1′,o†)(ds)(⊤)=1 _ max(σ)(oh _1,o _o)(d_s)( )=1. Finally, δ′(ds,⊤)(s)=1δ (d_s, )(s)=1 by construction of ′G . Hence ℙ′Φ(σ),Φ(π)(Cyl(h′)) _G _ max(σ), _ min(π)(Cyl\! (h )) =ℙσ,π(Cyl(h1))×∑a∈A(σ(oh1)(s1)(a)×δ(s1,a)(s))×1×1 =P_G^σ,π(Cyl\! (h_1 ))× _a∈ A_ max (σ(oh_1)(s_1)(a)×δ(s_1,a)(s) )× 1× 1 =ℙσ,π(Cyl(h)) =P_G^σ,π(Cyl\! (h )) The symmetric direction (replacing Φ⋆ _ by Ψ⋆=(Φ⋆)−1 _ =( _ )^-1) follows by an identical argument. ∎ We now state the main correctness theorem for Pre- min transformation. Lemma B.11. Let G be any alternating control POSG and ′G its Pre- min transformation. Let W⊆W Plays_G be parity objective and W′=Γ(W)W = (W) its corresponding objective in ′G . Then Val(W)=Val′(W′).Val_G(W)=Val_G (W ). Proof. For fixed σ∈Σσ∈ _G, set q(σ)=infπ∈Πℙσ,π(W),q′(σ′)=infπ′∈Π′ℙ′σ′,π′(W′).q_G(σ)= _π∈ _GP_G^σ,π(W), q_G (σ )= _π ∈ _G P_G ^σ ,π (W ). The first equality in Lemma B.10 gives q′(Φ(σ))≤q(σ)q_G ( _ max(σ))≤ q_G(σ) because every π∈Ππ∈ _G has an image Φ(π)∈Π′ _ min(π)∈ _G . Conversely, for every π′∈Π′π ∈ _G , the second equality there and Ψ(Φ(σ))=σ _ max( _ max(σ))=σ give ℙ′Φ(σ),π′(W′)=ℙσ,Ψ(π′)(W),P_G _ max(σ),π (W )=P_G^σ, _ min(π )(W), so q(σ)≤q′(Φ(σ))q_G(σ)≤ q_G ( _ max(σ)). Hence the two fixed-strategy infima are equal. Since Φ _ max is a bijection by Lemma B.8, taking the outer supremum yields Val(W) _G(W) =supσ∈Σq(σ)=supσ∈Σq′(Φ(σ)) = _σ∈ _Gq_G(σ)= _σ∈ _Gq_G ( _ max(σ)) =supσ′∈Σ′q′(σ′)=Val′(W′). = _σ ∈ _G q_G (σ )=Val_G (W ). ∎ Corollary B.12. Let G be any alternating control POSG and ′G its Pre- min transformation. Let p- a priority function for G. Then Val(Parity(p))=Val′(Parity′(p′)).Val_G\! (Parity_G\! (p ) )=Val_G \! (Parity_G \! (p ) ). Proof. Follows directly from lemma B.11 together with Lemma B.9. ∎ Lemma B.13. For any σ∈Σσ∈ _G and π∈Ππ∈ _G: Γ(σ,π)=′Φ(σ),Φ(π). ( Plays^σ,π_G )\;=\; Plays _ max(σ),\, _ min(π)_G . where σ,π(resp.′σ′,π′) Plays^σ,π_G(resp. Plays^σ ,π _G ) denote the set of plays in (resp.′)G(resp.G ) under the pair of strategies σ,π(resp.σ′,π′)σ,π(resp.σ ,π ). Proof. Let ρ′∈Γ(σ,π)ρ ∈ ( Plays^σ,π_G). Then there exists ρ∈σ,πρ∈ Plays^σ,π_G with Γ(ρ)=ρ′ (ρ)=ρ . Write ρ=s0,a0,s1,a1,…ρ=s_0,a_0,s_1,a_1,… and ρ′=s0,a0,ds1,⊤,s1,a1,…ρ =s_0,a_0,d_s_1, ,s_1,a_1,… as constructed by Γ . We verify ρ′ρ is consistent with (Φ(σ),Φ(π))( _ max(σ), _ min(π)). • At each max-state sk∈S (k is even)s_k∈ S_ max (k is even): The max-player observation history in ′G at state sks_k is ohk′=Γ(ohk)oh _k= _O max(oh_k), where ohoh is the max-player observation history of ρ at sks_k. By definition of Φ _ max: Φ(σ)(ohk′)(sk) _ max(σ)(oh _k)(s_k) =σ((Γ)−1(ohk′))(sk) =σ\! (( _O max)^-1(oh _k) )(s_k) =σ(ohk)(sk) =σ(oh_k)(s_k) from Lemma B.6 Because ρ∈σ,πρ∈ Plays^σ,π_G, action aka_k is in the support of σ(ohk)(sk)σ(oh_k)(s_k), and hence also in the support of Φ(σ)(ohk′)(sk) _ max(σ)(oh _k)(s_k). The max-transition in ′G sends (sk,ak)(s_k,a_k) to dsk+1d_s_k+1 with probability δ′(sk,ak)(dsk+1)=δ(sk,ak)(sk+1)δ (s_k,a_k)(d_s_k+1)=δ(s_k,a_k)(s_k+1), matching the transition used in ρ. • At each dummy state ds2k+1∈Dd_s_2k+1∈ D: By definition of Φ _ max, the strategy assigns Dirac(⊤)Dirac( ) to the sole effective action; all other globally enabled actions are max-losing defaults. Moreover, δ′(ds2k+1,⊤)(s2k+1)=1δ (d_s_2k+1, )(s_2k+1)=1. • At each min-state sk∈Ss_k∈ S_ min (k is odd): The min-player observation history in ′G at sks_k is oh′=Γ(oh)oh = _O min(oh), where ohoh is the min-player observation history of ρ at state sks_k. By definition of Φ _ min: Φ(π)(oh′)(sk) _ min(π)(oh )(s_k) =π((Γ)−1(oh′))(sk) =π\! (( _O min)^-1(oh ) )(s_k) =π(oh)(sk) =π(oh)(s_k) from lemma B.6 Because ρ∈σ,πρ∈ Plays^σ,π_G, action aka_k is in the support of π(oh)(sk)π(oh)(s_k), hence action aka_k is also in the support of Φ(π)(oh′)(sk) _ min(π)(oh )(s_k). Thus ρ′∈′Φ(σ),Φ(π)ρ ∈ Plays _ max(σ), _ min(π)_G , hence Γ(σ,π)⊆′Φ(σ),Φ(π) ( Plays^σ,π_G ) Plays _ max(σ),\, _ min(π)_G . Since Γ:→′ : Plays_G→ Plays_G is a bijection (Lemma B.5), every ρ′∈′Φ(σ),Φ(π)ρ ∈ Plays _ max(σ), _ min(π)_G has a unique pre-image ρ=Γ−1(ρ′)ρ= ^-1(ρ ) obtained by removing all dummy states and ⊤ -actions. By the same step-by-step argument with (Γ)−1( _O max)^-1, (Γ)−1( _O min)^-1 in place of Γ _O max, Γ _O min, and using Ψ⋆=(Φ⋆)−1 _ =( _ )^-1 in place of Φ⋆ _ , the play ρ is consistent with (σ,π)(σ,π), hence ′Φ(σ),Φ(π)⊆Γ(σ,π) Plays _ max(σ),\, _ min(π)_G ( Plays^σ,π_G ) . ∎ Lemma B.14 (Sure Winning). Let W⊆W Plays_G be a parity objective of G and W′=Γ(W)W = (W) be its lifted objective in ′G . Let σ∈Σσ∈ _G and σ′=Φ(σ)σ = _ max(σ). Then, σ is sure winning for W⇔σ′ is sure winning for W′$σ$ is sure winning for W $σ $ is sure winning for W Proof. We will show that ∀π∈Π:σ,π⊆W⇔∀π′∈Π′:′σ′,π′⊆W′∀π∈ _G:\> Plays^σ,π_G W ∀π ∈ _G :\> Plays^σ ,π _G W For forward direction, let σ∈Σσ∈ _G be sure winning for W. Then, ∀π∈Π:σ,π⊆W∀π∈ _G:\> Plays^σ,π_G W. From lemma B.9, for any ρ∈σ,π,ρ∈W⇔Γ(ρ)⊆W′ρ∈ Plays^σ,π_G,ρ∈ W (ρ) W . Since ρ is arbitrary, we have Γ(σ,π)⊆W′ ( Plays^σ,π_G) W . For any π′∈Π′π ∈ _G : Due to bijection of Φ,Ψ,∃π _ min, _ min,∃π such that π′=Φ(π)π = _ min(π). Then, from lemma B.13 and B.8 ′σ′,π′=Γ(Ψ(σ′),Ψ(π′))=Γ(Ψ(Φ(σ)),Ψ(Φ(π)))=Γ(σ,π)⊆W′ Plays^σ ,π _G \>=\> ( Plays _ max(σ ), _ min(π )_G)= ( Plays _ max( _ max(σ)), _ min( _ min(π))_G)= ( Plays^σ,π_G)\> \>W The reverse direction can be proven similarly using inverse mappings Ψ,Ψ _ max, _ min. ∎ Lemma B.15 (Almost-sure Winning). Let W⊆W Plays_G be a parity objective of G and W′=Γ(W)W = (W) be lifted objective in ′G . Let σ∈Σσ∈ _G and σ′=Φ(σ)σ = _ max(σ). Then, σ is almost-sure winning for W⇔σ′ is almost-sure winning for W′$σ$ is almost-sure winning for W $σ $ is almost-sure winning for W Proof. The fixed-strategy equality established in the proof of Lemma B.11 is infπ∈Πℙσ,π(W)=infπ′∈Π′ℙ′σ′,π′(W′). _π∈ _GP_G^σ,π(W)= _π ∈ _G P_G ^σ ,π (W ). Hence one side equals 11 if and only if the other does. ∎ Lemma B.16 (Limit-Sure Winning). Let W⊆W Plays_G be a parity objective of G and W′=Γ(W)W = (W) is the corresponding objective in ′G . Then, W is limit-sure⇔W′ is limit-sureW is limit-sure W is limit-sure Proof. Follows directly from lemma B.11. ∎ Lemma B.17 (Quantitative Analysis). Let W⊆W Plays_G be a parity objective of G and W′=Γ(W)W = (W) is the corresponding objective in ′G . Then, for k∈(0,1)k∈(0,1) Val(W)≥k⇔Val′(W′)≥kVal_G(W)≥ k _G (W )≥ k Proof. Follows directly from lemma B.11. ∎ B.3.1 Size and Memory Preservation of the reduction Lemma B.18. Let G be an alternating-control POSG and ′G its Pre- min transformation. The maps Γ:→′ : Plays_G→ Plays_G , ΓO,ΓO _O max, _O min on observation histories, and Φ⋆,Ψ⋆=(Φ⋆)−1 _ , _ =( _ )^-1 (⋆∈, ∈\ max, min\) on strategies satisfy the following. Exact counts use the displayed transitions; the implicit sink completion has constant descriptive overhead. Let S′=S′∪S′S =S_ max ∪ S_ min and A′=A′∪A′A =A_ max ∪ A_ min . 1. (size) |S′|=|S|+|S||S |=|S_G|+|S_ min|, |A′|=|A|+1|A |=|A_G|+1, |′|=2|||O_ max |=2|O_ max|, |′|=2|||O_ min |=2|O_ min|, and |δ′|=|δ|+|S||δ |=|δ|+|S_ min|. In particular, |′|=(||)|G |=O(|G|) and the construction runs in linear time. 2. (history length) For every oh∈⋆oh∈ OH^G_ , |ΓO⋆(oh)|=⌈3|oh|−12⌉| _O (oh)|= 3|oh|-12 and for every oh′∈⋆′oh ∈ OH^G _ , |(ΓO⋆)−1(oh′)|≤|oh′||( _O )^-1(oh )|≤|oh |. Observation histories on the two sides are linear in each other. 3. (memory) The lifting maps Φ⋆,Ψ⋆ _ , _ preserve memory class exactly: memoryless, finite-memory and infinite-memory regimes correspond exactly between G and ′G . Proof. Clause (1). Direct from the construction. The state space gains one fresh dummy state per S_ min-state, so |S′|=|S|+2|S|=|S|+|S||S |=|S_ max|+2|S_ min|=|S_G|+|S_ min|. The action set gains the single fresh action ⊤ , so |A′|=|A|+1|A |=|A_G|+1. The observation alphabets are ′=∪ox†∣x∈O_ max =O_ max∪\o _x x _ max\ and ′=∪ox#∣x∈O_ min =O_ min∪\o^\#_x x _ min\, which doubles each cardinality. The transition function δ′δ agrees with δ on every (s,a)∈S×A(s,a)∈ S_ min× A_ min, and on each (s,a)∈S×A(s,a)∈ S_ max× A_ max replaces the target s2∈Ss_2∈ S_ min by ds2∈Dd_s_2∈ D – giving the same number of edges as δ – and additionally contributes the deterministic edge δ′(ds,⊤)=Dirac(s)δ (d_s, )=Dirac(s) for every ds∈Dd_s∈ D, of which there are |S||S_ min|. Hence |δ′|=|δ|+|S||δ |=|δ|+|S_ min|. Each component is therefore a constant or unit-additive perturbation of the corresponding component in G, so |′|=(||)|G |=O(|G|) and ′G is computed from G in linear time. Clause (2). Let ⋆= = max and let oh=o0,o1,…,o2n∈⋆oh=o_0,o_1,…,o_2n∈ OH^G_ , so that |oh|=2n+1|oh|=2n+1. By construction, ΓO⋆(oh)=o0,z1,o1,o2,z3,o3,…,o2n−2,z2n−1,o2n−1,o2n, _O (oh)=o_0,z_1,o_1,o_2,z_3,o_3,…,o_2n-2,z_2n-1,o_2n-1,o_2n, where z2k+1z_2k+1 is the appropriately tagged copy of o2k+1o_2k+1 (z2k+1=o2k+1†z_2k+1=o _o_2k+1) one tagged observation is inserted between every pair of consecutive original observations. Hence |ΓO⋆(oh)|=(2n+1)+n=3n+1=3|oh|−12| _O (oh)|=(2n+1)+n=3n+1= 3|oh|-12 Let ⋆= = min and let oh=o0,o1,…,o2n+1∈⋆oh=o_0,o_1,…,o_2n+1∈ OH^G_ , so that |oh|=2n+2|oh|=2n+2. By construction, ΓO⋆(oh)=o0,z1,o1,o2,z3,o3,…,o2n−2,z2n−1,o2n−1,o2n,,z2n+1,o2n+1 _O (oh)=o_0,z_1,o_1,o_2,z_3,o_3,…,o_2n-2,z_2n-1,o_2n-1,o_2n,,z_2n+1,o_2n+1 where z2k+1z_2k+1 is the appropriately tagged copy of o2k+1o_2k+1 (z2k+1=o2k+1#z_2k+1=o^\#_o_2k+1) one tagged observation is inserted between every pair of consecutive original observations. Hence |ΓO⋆(oh)|=(2n+2)+n+1=3n+3=3|oh|2.| _O (oh)|=(2n+2)+n+1=3n+3= 3|oh|2. From above values, for ⋆∈, ∈\ max, min\, |ΓO⋆(oh)|=⌈3|oh|−12⌉| _O(oh)|= 3|oh|-12 For the reverse direction, (ΓO⋆)−1( _O )^-1 acts on oh′∈⋆′oh ∈ OH^G _ by deleting observations in †O for ⋆= = max and in #O^\# for ⋆= = min. Deletion only shortens the sequence, so |(ΓO⋆)−1(oh′)|≤|oh′||( _O )^-1(oh )|≤|oh |. Combining the two bounds, observation histories on the two sides are within a factor of 32 32 in length. Clause (3). Fix ⋆∈, ∈\ max, min\ and let a finite-memory strategy be realized by a transducer M=(Q,q0,u,g)M=(Q,q_0,u,g), where u updates the memory state from observations and g outputs the complete state-indexed action assignment prescribed by the strategy. For the forward map Φ⋆ _ , run M on (ΓO⋆)−1(oh′)( _O )^-1(oh ). This can be done online with the same memory set Q: an inserted observation in †O or #O^\# is skipped, while every original observation is processed exactly as in M. At an original player state, the output is the assignment produced by g; at a dummy max-state, the output assigns Dirac(⊤)Dirac( ) to every compatible dummy state. Thus the resulting transducer realizes Φ⋆ _ and uses exactly the memory states in Q. Conversely, let M′M realize a strategy in ′G . To realize Ψ⋆ _ in G, run M′M on the virtual history ΓO⋆(oh) _O (oh). Each inserted observation is determined by the adjacent original observation, so the corresponding finite block can be fed to M′M as soon as that original observation is read; no additional persistent memory is required. The output at an original state is then precisely M′M ’s output after reading ΓO⋆(oh) _O (oh). Lemmas B.6 and B.7 show that these simulations realize the stated strategy maps. Therefore both maps preserve the number of memory states. In particular, one-state memoryless strategies, finite-memory strategies, and unrestricted infinite-memory strategies correspond in both directions. ∎ B.4 Proof of Lemma 3.2 Proof. Because parity objective subsumes all ω-regular objectives, from lemma B.11, Val(W)=Val′(W′)Val_G(W)=Val_G (W ) for any ω-regular objective W in G and its corresponding objective W′W in ′G . The “consequently” statement follows from lemmas B.14, B.15, B.16, and B.17. ∎ Appendix C Constructing an RPOMDP from a Pre- min Transformed POSG Let ′G be the Pre- min transformation of an alternating control POSG G as constructed in definition B.1. In ′G , every play has the periodic structure s1→a1ds2→⊤s2→a2s3→a3ds4→⊤s4⋯s_1\; a_1\;d_s_2\; \;s_2\; a_2\;s_3\; a_3\;d_s_4\; \;s_4\;·s where max-states and dummy states in S∪DS_ max∪ D alternate with S_ min-states. The key observation is that the min-player’s choice of action a∈Aa∈ A_ min at a S_ min-state s determines the next transition distribution δ′(s,a)∈Δ(S)δ (s,a)∈ (S_ max). This is exactly the role of the environment in an RPOMDP: given a state and an action, it selects a distribution from the uncertainty set. We exploit this to define a polytopic RPOMDP ℜ() R\! (G ) whose states are the max-states and dummy states of ′G , and whose uncertainty set at each dummy state under action ⊤ is the polytope whose vertices are the transition distributions corresponding to the min-player’s available actions. Definition C.1 (RPOMDP reduction of a Pre- min transformed POSG). Let ′=(S∪D,S,A∪⊤,A,δ′,s0,∪†,∪#,′,′)G =(S_ max∪ D,S_ min,A_ max∪\ \,A_ min,δ ,s_0,O_ max ,O_ min ^\#,Z_ max ,Z_ min ) be a Pre- min transformed POSG. We define the associated RPOMDP as ℜ()=(Sℜ,Aℜ,ℜ,ℜ,ℜ,ℜ,ℜ,s0ℜ), R\! (G )=(S_ R,\;A_ R,\;P_ R,\;O_ a R,\;O_ e R,\;Z_ a R,\;Z_ e R,\;s_0 R), where: • (State space) Sℜ=S∪DS_ R=S_ max∪ D. • (Actions) Aℜ=A∪⊤A_ R=A_ max∪\ \, with every action enabled at every state. The effective pairs are (s,a)∈S×A(s,a)∈ S_ max× A_ max and (ds,⊤)(d_s, ); all other pairs use the default max-losing singleton transition. • (Uncertainty set) ℜ=∏(s,a)∈Sℜ×AℜP(s,a)P_ R= _(s,a)∈ S_ R× A_ RP(s,a), where the non-default polytopes are: – For (s,a)∈S×A(s,a)∈ S_ max× A_ max or s=ds′∈Ds=d_s ∈ D and a=⊤a= , define Vs,a=δ′(s,a)if s∈S,a∈A,δ′(s′,a′)|a′∈Aif s=ds′,a=⊤,s′∈S.V_s,a= cases\δ (s,a)\&if s∈ S_ max,\ a∈ A_ max,\\ \\,δ (s ,a )\; |\;a ∈ A_ min\, \&if s=d_s ,\ a= ,\ s ∈ S_ min. cases For these pairs, P(s,a)=conv(Vs,a),P(s,a)=conv(V_s,a), where conv(Vs,a)conv(V_s,a) denotes the convex hull of Vs,aV_s,a. Every remaining pair uses the implicit max-losing singleton. • (Agent observations) ℜ=∪†O_ a R=O_ max . • (Environment observations) ℜ=∪#O_ e R=O_ min ^\#. • (Agent observation function) ℜ:Sℜ→ℜZ_ a R:S_ R _ a R with ℜ(s′)=′(s′)Z_ a R(s )=Z_ max (s ) for s′∈Sℜs ∈ S_ R. • (Environment observation function) ℜ:Sℜ→ℜZ_ e R:S_ R _ e R with ℜ(s′)=′(s′)Z_ e R(s )=Z_ min (s ) for s′∈Sℜs ∈ S_ R. • (Initial state) s0ℜ=s0s_0 R=s_0. Remark C.2. The vertex set Vds,⊤=δ′(s,a)∣a∈AV_d_s, =\δ (s,a) a∈ A_ min\ of the polytope P(ds,⊤)P(d_s, ) encodes all min-actions at s∈Ss∈ S_ min: each vertex corresponds to the distribution induced by a min-action. The environment in ℜ() R\! (G ) selects any convex combination of these vertices, which corresponds to the min-player in ′G playing a randomized distribution over actions at state s. At non-dummy states s′∈Ss ∈ S_ max, the uncertainty set is a singleton, so the environment has no real choice there. This makes ℜ() R\! (G ) a polytopic (s,a)(s,a)-rectangular RPOMDP. C.1 Mapping plays, observation histories, strategies from ′G to ℜ() R\! (G ) Mapping on plays. Because the uncertainty set at dummy states is polytopic (not a singleton), different plays in ′G that agree on all S∪DS_ max∪ D states and A∪⊤A_ max∪\ \ actions but differ in the min-action chosen at S_ min-states will map to the same play in ℜ() R\! (G ). We therefore define Λ:′→ℜ() : Plays_G → Plays_ R\! (G ) and its set-valued inverse Λ−1:ℜ()→2′ ^-1: Plays_ R\! (G )→ 2 Plays_G . Let ρ′∈′ρ ∈ Plays_G be of the form ρ′=s1,a1,s2,a2,s3,a3,…ρ =s_1,a_1,s_2,a_2,s_3,a_3,… where by construction of ′G , for all k≥0k≥ 0: s3k+1∈S,s3k+2∈D,s3k+3∈S,a3k+1∈A,a3k+2=⊤,a3k+3∈A.s_3k+1∈ S_ max, s_3k+2∈ D, s_3k+3∈ S_ min, a_3k+1∈ A_ max, a_3k+2= , a_3k+3∈ A_ min. We define Λ(ρ′)=ρℜ (ρ )=ρ R where ρℜ=t1,b1,t2,b2,…∈ℜ()ρ R=t_1,b_1,t_2,b_2,…∈ Plays_ R\! (G ) is given index-wise, for all k≥0k≥ 0, by: t2k+1 t_2k+1 =s3k+1∈S, =s_3k+1∈ S_ max, b2k+1 b_2k+1 =a3k+1∈A, =a_3k+1∈ A_ max, t2k+2 t_2k+2 =s3k+2∈D, =s_3k+2∈ D, b2k+2 b_2k+2 =⊤. = . That is, we remove all occurrences of S_ min-states and A_ min-actions from ρ′ρ . Set-valued inverse. Define Λ−1:ℜ()→2′ ^-1: Plays_ R\! (G )→ 2 Plays_G as follows. Let ρℜ=t1,b1,t2,b2,…∈ℜ()ρ R=t_1,b_1,t_2,b_2,…∈ Plays_ R\! (G ) where for all k≥0k≥ 0: t2k+1∈St_2k+1∈ S_ max, t2k+2∈Dt_2k+2∈ D, b2k+1∈Ab_2k+1∈ A_ max, b2k+2=⊤b_2k+2= . Then Λ−1(ρℜ) ^-1(ρ R) is the set of all plays ρ′=s1,a1,s2,a2,s3,a3,…∈′ρ =s_1,a_1,s_2,a_2,s_3,a_3,…∈ Plays_G such that for all k≥0k≥ 0: s3k+1 s_3k+1 =t2k+1, =t_2k+1, a3k+1 a_3k+1 =b2k+1, =b_2k+1, s3k+2 s_3k+2 =t2k+2, =t_2k+2, a3k+2 a_3k+2 =⊤, = , s3k+3 s_3k+3 =s such that t2k+2=ds∈D, =s such that t_2k+2=d_s∈ D, a3k+3 a_3k+3 ∈A (arbitrary action subject to δ′(s3k+3,a3k+3)(s3k+4)>0). ∈ A_ min (arbitrary action subject to δ (s_3k+3,a_3k+3)(s_3k+4)>0). Thus Λ−1(ρℜ) ^-1(ρ R) consists of all plays in ′G obtained by resolving each transition at a dummy state using an arbitrary min-action. In particular, Λ(ρ′)=ρℜ (ρ )=ρ R for every ρ′∈Λ−1(ρℜ)ρ ∈ ^-1(ρ R), i.e. Λ is many-to-one. Mapping on observation histories. We extend Λ to observation histories exactly as before. Let oh=o1,o2,o3,…,on∈′oh=o_1,o_2,o_3,…,o_n∈ OH_ max^G . We define Λ:′→ℜ() _O max: OH_ max^G → OH_ a R\! (G ) by Λ(oh)=ohℜ _O max(oh)=oh R where ohℜ=o~1,o~2,o~3,…oh R= o_1, o_2, o_3,… is given index-wise, for all k≥0k≥ 0 such that indices exist, by: o~2k+1 o_2k+1 =o3k+1, =o_3k+1, o~2k+2 o_2k+2 =o3k+2. =o_3k+2. Observations o3k+3o_3k+3 of S_ min-states are removed. The map Λ _O max is a bijection with inverse (Λ)−1:ℜ()→′( _O max)^-1: OH_ a R\! (G )→ OH_ max^G defined, for ohℜ=o~1,o~2,…,o~m∈ℜ()oh R= o_1, o_2,…, o_m∈ OH_ a R\! (G ) (o~2k+1∈,o~2k+2∈o† o_2k+1 _ max, o_2k+2∈ o for k≥0k≥ 0), by (Λ)−1(ohℜ)=oh=o1,o2,…,ok( _O max)^-1(oh R)=oh=o_1,o_2,…,o_k where for all k≥0k≥ 0: o3k+1 o_3k+1 =o~2k+1, = o_2k+1, o3k+2 o_3k+2 =o~2k+2, = o_2k+2, o3k+3 o_3k+3 =x such that o~2k+2=ox†, =x such that o_2k+2=o _x, ok o_k =o~m = o_m We extend this to the min-player. We define Λ:′→^ℜ() _O min: OH_ min^G → OH_ e R\! (G ), where ^ℜ()⊆ℜ() OH_ e R\! (G ) OH_ e R\! (G ) is the set of environment observation histories of ℜ() R\! (G ) ending in an observation of a state in D, i.e, ^ℜ()=ohℜ∈ℜ()∣last(ohℜ)∈# OH_ e R\! (G )=\oh R∈ OH_ e R\! (G ) (oh R) ^\#\. For oh=o1,o2,…,on∈′oh=o_1,o_2,…,o_n∈ OH_ min^G , Λ(oh)=o~1,o~2,… _O min(oh)= o_1, o_2,… is defined index-wise for all k≥0k≥ 0 by: o~2k+1 o_2k+1 =o3k+1, =o_3k+1, o~2k+2 o_2k+2 =o3k+2. =o_3k+2. Since last(oh)∈last(oh) _ min, the mapped history ends in #O^\# and hence lies in ^ℜ() OH_ e R\! (G ). Its inverse (Λ)−1:^ℜ()→′( _O min)^-1: OH_ e R\! (G )→ OH_ min^G is defined for ohℜ=o~1,o~2,…,o~m∈^ℜ()oh R= o_1, o_2,…, o_m∈ OH_ e R\! (G ) by (Λ)−1(ohℜ)=o1,o2,…,om+m/2( _O min)^-1(oh R)=o_1,o_2,…,o_m+m/2 where for all k≥0k≥ 0: o3k+1 o_3k+1 =o~2k+1, = o_2k+1, o3k+2 o_3k+2 =o~2k+2, = o_2k+2, o3k+3 o_3k+3 =x such that o~2k+2=ox#, =x such that o_2k+2=o^\#_x, om+m/2 o_m+m/2 =x such that o~m=ox#. =x such that o_m=o^\#_x. Lemma C.3. For all ohℜ∈ℜ()oh R∈ OH_ a R\! (G ), Λ((Λ)−1(ohℜ))=ohℜ _O max\! (( _O max)^-1(oh R) )=oh R; and for all oh′∈′oh ∈ OH_ max^G , (Λ)−1(Λ(oh′))=oh′( _O max)^-1\! ( _O max(oh ) )=oh . Lemma C.4. For all ohℜ∈^ℜ()oh R∈ OH_ e R\! (G ), Λ((Λ)−1(ohℜ))=ohℜ _O min\! (( _O min)^-1(oh R) )=oh R; and for all oh′∈′oh ∈ OH_ min^G , (Λ)−1(Λ(oh′))=oh′( _O min)^-1\! ( _O min(oh ) )=oh . Mapping of strategies. Recall from section 2 and the definition of RPOMDP that: • A player strategy in ′G maps its observation history to state-indexed distributions over its global action alphabet, as in the main text. • An agent strategy σℜ∈Σℜ()σ R∈ _ R\! (G ) maps each observation history to state-indexed distributions over AℜA_ R. • An environment strategy πℜ∈Πℜ()π R∈ _ R\! (G ) has type πℜ:ℜ()×Aℜ→ℜπ R: OH_ e R\! (G )× A_ R _ R and hence selects a complete transition assignment. Since ℜP_ R is (s,a)(s,a)-rectangular and polytopic, the environment strategy πℜ∈Πℜ()π R∈ _ R\! (G ) at a dummy state ds∈Dd_s∈ D under action ⊤ picks a distribution πℜ(ohℜ,⊤)(ds,⊤)∈P(ds,⊤)π R(oh R, )(d_s, )∈ P(d_s, ), which by Definition C.1 is a convex combination of the vertices Vds,⊤=δ′(s,a)∣a∈AV_d_s, =\δ (s,a) a∈ A_ min\. We write this as πℜ(ohℜ,⊤)(ds,⊤)=∑a∈Aαa⋅δ′(s,a),αa≥0,∑a∈Aαa=1.π R(oh R, )(d_s, )= _a∈ A_ min _a·δ (s,a), _a≥ 0,\; _a∈ A_ min _a=1. For every s∈Ss∈ S_ min, define s′:Δ(A)→P(ds,⊤),s′(λ)=∑a∈Aλ(a)δ′(s,a). bar^G _s: (A_ min)→ P(d_s, ), bar^G _s(λ)= _a∈ A_ minλ(a)δ (s,a). For each P∈P(ds,⊤)P∈ P(d_s, ), choose βsP∈Δ(A) _s^P∈ (A_ min) such that s′(βsP)=P bar^G _s( _s^P)=P. The coefficients may be nonunique; fix one such βsP _s^P for every P. For a complete assignment P∈ℜP _ R, fix a reference element Px,b0∈P(x,b)P^0_x,b∈ P(x,b) for every (x,b)∈Sℜ×Aℜ(x,b)∈ S_ R× A_ R. We define the following four maps lifting strategies between ′G and ℜ() R\! (G ): 1. Ω:Σ′→Σℜ() _ max: _G → _ R\! (G ): for each σ′∈Σ′σ ∈ _G , ohℜ∈ℜ()oh R∈ OH_ a R\! (G ) and ∀s∈Sℜ=S∪D∀ s∈ S_ R=S_ max∪ D such that ℜ(s)=last(ohℜ)Z_ a R(s)=last(oh R), Ω(σ′)(ohℜ)(s)=σ′((Λ)−1(ohℜ))(s) _ max(σ )(oh R)(s)=σ \! (( _O max)^-1(oh R) )(s) 2. Ω:Π′→Πℜ() _ min: _G → _ R\! (G ): for each π′∈Π′π ∈ _G , ohℜ∈ℜ()oh R∈ OH_ e R\! (G ), and b∈Aℜb∈ A_ R, define the complete assignment Ω(π′)(ohℜ,b)∈ℜ _ min(π )(oh R,b) _ R by Ω(π′)(ohℜ,b)(x,c)=s′(π′((Λ)−1(ohℜ))(s))if x=ds,b=c=⊤,ℜ(x)=last(ohℜ),δ′(x,b)if x∈S,b=c∈A,ℜ(x)=last(ohℜ),Px,c0otherwise. _ min(π )(oh R,b)(x,c)= cases bar^G _s\! (π \! (( _O min)^-1(oh R) )(s) )& array[]lif x=d_s,\ b=c= ,\\[-2.0pt] Z_ e R(x)=last(oh R), array\\ δ (x,b)& array[]lif x∈ S_ max,\ b=c∈ A_ max,\\[-2.0pt] Z_ e R(x)=last(oh R), array\\ P^0_x,c&otherwise. cases 3. Ξ:Σℜ()→Σ′ _ max: _ R\! (G )→ _G : for each σℜ∈Σℜ()σ R∈ _ R\! (G ), oh′∈′oh ∈ OH_ max^G and ∀s∈S∪D∀ s∈ S_ max∪ D such that ′(s)=last(oh′)Z_ max (s)=last(oh ) , Ξ(σℜ)(oh′)(s)=σℜ(Λ(oh′))(s). _ max(σ R)(oh )(s)=σ R\! ( _O max(oh ) )(s). 4. Ξ:Πℜ()→Π′ _ min: _ R\! (G )→ _G : for each πℜ∈Πℜ()π R∈ _ R\! (G ), oh′∈′oh ∈ OH_ min^G and ∀s′∈S∀ s ∈ S_ min with ′(s′)=last(oh′)Z_ min (s )=last(oh ), define Ξ(πℜ)(oh′)(s′)=βs′πℜ(Λ(oh′),⊤)(ds′,⊤). _ min(π R)(oh )(s )= _s ^π R( _O min(oh ), )(d_s , ). Remark C.5. By definition of Ξ _ min, for all πℜ∈Πℜ()π R∈ _ R\! (G ), oh′∈′oh ∈ OH_ min^G , and ds′∈Dd_s ∈ D, πℜ(Λ(oh′),⊤)(ds′,⊤)=s′(Ξ(πℜ)(oh′)(s′)).π R( _O min(oh ), )(d_s , )= bar^G _s \! ( _ min(π R)(oh )(s ) ). Lemma C.6. The agent maps Ω _ max and Ξ _ max are mutual inverses. For every compatible dummy history and state, the environment maps satisfy Ω(Ξ(πℜ))(ohℜ,⊤)(ds,⊤) _ min( _ min(π R))(oh R, )(d_s, ) =πℜ(ohℜ,⊤)(ds,⊤), =π R(oh R, )(d_s, ), s′(Ξ(Ω(π′))(oh′)(s)) bar^G _s\! ( _ min( _ min(π ))(oh )(s) ) =s′(π′(oh′)(s)). = bar^G _s\! (π (oh )(s) ). Thus the environment compositions preserve transition distributions. Proof. The agent identities follow immediately from Lemmas C.3 and the definitions of Ω,Ξ _ max, _ max. The environment identities follow from s′(βsP)=P bar^G _s( _s^P)=P and Lemma C.4. At non-dummy states the uncertainty set is a singleton. ∎ C.2 Lifting objectives from ′G to ℜ() R\! (G ) Define pℜ:Sℜ→0,1,…,d,d∈ℕp R:S_ R→\0,1,…,d\,d by pℜ(s′)=p′(s′)p R(s )=p (s ) for s′∈Sℜs ∈ S_ R where p′p is priority function for ′G . Lemma C.7. Let ′G , ℜ() R\! (G ), p′p , and pℜp R be as above, and let ρ′∈′ρ ∈ Plays_G . Then ρ′∈Parity′(p′)⇔Λ(ρ′)∈Parityℜ()(pℜ).ρ _G \! (p ) (ρ ) _ R\! (G )\! (p R ). Proof. By construction of pℜp R, every state s′∈Ss ∈ S_ max in Λ(ρ′) (ρ ) carries priority pℜ(s′)=p′(s′)p R(s )=p (s ), and every dummy state ds∈Dd_s∈ D carries priority pℜ(ds)=p′(ds)p R(d_s)=p (d_s). The S_ min-states of ρ′ρ are removed by Λ ; since by definition of p′p the priority of each s∈Ss∈ S_ min equals that of the preceding dummy state dsd_s, no lim inf -relevant priority value is lost. Hence the parity condition is preserved. ∎ C.3 Value Preservation between ′G and ℜ() R\! (G ) Lemma C.8. The strategy maps preserve objective probabilities in both directions: ℙ′σ′,π′(W′) _G ^σ ,π (W ) =ℙℜ()Ω(σ′),Ω(π′)(Wℜ), =P_ R\! (G ) _ max(σ ), _ min(π )(W R), ℙℜ()σℜ,πℜ(Wℜ) _ R\! (G )^σ R,π R(W R) =ℙ′Ξ(σℜ),Ξ(πℜ)(W′), =P_G _ max(σ R), _ min(π R)(W ), for all strategies of the indicated types, where W′⊆′W Plays_G is parity objective in ′G and Wℜ=Λ(W′)W R= (W ) is the corresponding objective in ℜ() R\! (G ). Proof. Since the probability measure over plays is uniquely determined by its values on cylinder sets, it suffices to show that for every finite history h′h in W′W ending at a state in S∪DS_ max∪ D, there exists a corresponding history hℜh R in WℜW R such that ℙ′σ′,π′(Cyl(h′))=ℙℜ()Ω(σ′),Ω(π′)(Cyl(hℜ)).P_G ^σ ,π (Cyl\! (h ))=P_ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R )). We map each such h′h to hℜh R similar to Λ maps the corresponding plays (dropping S_ min-states). The proof proceeds by induction on the length of h′h . Base case. h′=s0h =s_0. Then hℜ=s0ℜ=s0h R=s_0 R=s_0 and both cylinders have probability 11. Inductive step. We distinguish three cases based on how h′h is extended. Case 1: h′h is of the form h1′,dsh _1,d_s where ds∈Dd_s∈ D. Then last(h1′)∈Slast(h _1)∈ S_ max and hℜ=h1ℜ,dsh R=h R_1,d_s where h1ℜh R_1 corresponds to h1′h _1 by induction. Let ohaℜ=ℜ(h1ℜ)oh R_a=Z_ a R(h R_1). Since last(h1ℜ)=s1∈Slast(h R_1)=s_1∈ S_ max, the uncertainty set for a∈Aa∈ A_ max, P(s1,a)P(s_1,a) is a singleton δ′(s1,a)\δ (s_1,a)\. Then ℙℜ()Ω(σ′),Ω(π′)(Cyl(hℜ)) _ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R )) =ℙℜ()Ω(σ′),Ω(π′)(Cyl(h1ℜ))×∑a∈A(Ω(σ′)(ohaℜ)(s1)(a)×δ′(s1,a)(ds)). =P_ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R_1 ))× _a∈ A_ max ( _ max(σ )(oh R_a)(s_1)(a)×δ (s_1,a)(d_s) ). By the induction hypothesis, ℙℜ()Ω(σ′),Ω(π′)(Cyl(h1ℜ))=ℙ′σ′,π′(Cyl(h1′))P_ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R_1 ))=P_G ^σ ,π (Cyl\! (h _1 )). Since last(ohaℜ)∈last(oh R_a) _ max and (Λ)−1(ohaℜ)=′(h1′)( _O max)^-1(oh R_a)=Z_ max (h _1), we have Ω(σ′)(ohaℜ)(s1)(a)=σ′(′(h1′))(s1)(a) _ max(σ )(oh R_a)(s_1)(a)=σ (Z_ max (h _1))(s_1)(a). The singleton uncertainty set means the environment contributes the unique element δ′(s1,a)δ (s_1,a) evaluated for transition to dsd_s. Hence ℙℜ()Ω(σ′),Ω(π′)(Cyl(hℜ)) _ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R )) =ℙ′σ′,π′(Cyl(h1′))×∑a∈A(σ′(′(h1′))(s1)(a)×δ′(s1,a)(ds)) =P_G ^σ ,π (Cyl\! (h _1 ))× _a∈ A_ max (σ (Z_ max (h _1))(s_1)(a)×δ (s_1,a)(d_s) ) =ℙ′σ′,π′(Cyl(h′)) =P_G ^σ ,π (Cyl\! (h )) Case 2: h′h is of the form h1′,sh _1,s where s∈Ss∈ S_ min and last(h1′)=ds∈Dlast(h _1)=d_s∈ D. The sole effective action from dsd_s is ⊤ and the transition δ′(ds,⊤)=Dirac(s)δ (d_s, )=Dirac(s) is deterministic. The corresponding prefix in ℜ() R\! (G ) is hℜ=h1ℜh R=h R_1 (unchanged, since the S_ min-state s is removed by Λ ). Since the ⊤ step at dsd_s is deterministic (probability 11) in both ′G and ℜ() R\! (G ), and the S_ min-state s is not present in ℜ() R\! (G ), we have immediately ℙℜ()Ω(σ′),Ω(π′)(Cyl(hℜ))=ℙ′σ′,π′(Cyl(h′))P_ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R ))=P_G ^σ ,π (Cyl\! (h )) Case 3: h′h is of the form h1′,s,s′h _1,s,s where last(h1′)=ds∈Dlast(h _1)=d_s∈ D, s∈Ss∈ S_ min, and s′∈Ss ∈ S_ max. Then hℜ=h1ℜ,s′h R=h R_1,s where h1ℜh R_1 corresponds to h1′h _1. Let ohaℜ=ℜ(h1ℜ)oh R_a=Z_ a R(h R_1) and oheℜ=ℜ(h1ℜ)oh R_e=Z_ e R(h R_1). Since last(h1ℜ)=ds∈Dlast(h R_1)=d_s∈ D, we have last(oheℜ)∈#last(oh R_e) ^\#. The environment in ℜ() R\! (G ) selects a distribution from P(ds,⊤)P(d_s, ); the mapped agent plays the sole effective action ⊤ with probability 11. ℙℜ()Ω(σ′),Ω(π′)(Cyl(hℜ)) _ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R )) =ℙℜ()Ω(σ′),Ω(π′)(Cyl(h1ℜ))×Ω(σ′)(ohaℜ)(ds)(⊤) =P_ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R_1 ))× _ max(σ )(oh R_a)(d_s)( ) ×Ω(π′)(oheℜ,⊤)(ds,⊤)(s′) × _ min(π )(oh R_e, )(d_s, )(s ) where we use the fact that the distribution selected by the environment at (ds,⊤)(d_s, ) is evaluated at s′s . By definition of Ω _ min, Ω(π′)(oheℜ,⊤)(ds,⊤)=∑a′∈Aπ′((Λ)−1(oheℜ))(s)(a′)⋅δ′(s,a′). _ min(π )(oh R_e, )(d_s, )= _a ∈ A_ minπ \! (( _O min)^-1(oh R_e) )(s)(a )·δ (s,a ). Evaluating at s′s : Ω(π′)(oheℜ,⊤)(ds,⊤)(s′)=∑a′∈Aπ′((Λ)−1(oheℜ))(s)(a′)⋅δ′(s,a′)(s′). _ min(π )(oh R_e, )(d_s, )(s )= _a ∈ A_ minπ \! (( _O min)^-1(oh R_e) )(s)(a )·δ (s,a )(s ). Since (Λ)−1(oheℜ)=′(h1′,s)( _O min)^-1(oh R_e)=Z_ min (h _1,s), this equals ∑a′∈Aπ′(′(h1′,s))(s)(a′)⋅δ′(s,a′)(s′) _a ∈ A_ minπ (Z_ min (h _1,s))(s)(a )·δ (s,a )(s ). Also, Ω(σ′)(ohaℜ)(ds)(⊤)=1 _ max(σ )(oh R_a)(d_s)( )=1 since ⊤ is the sole effective action at dummy states. By the induction hypothesis applied to h1′h _1, ℙℜ()Ω(σ′),Ω(π′)(Cyl(hℜ)) _ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R )) =ℙ′σ′,π′(Cyl(h1′))×∑a′∈Aπ′(′(h1′,s))(s)(a′)⋅δ′(s,a′)(s′). =P_G ^σ ,π (Cyl\! (h _1 ))× _a ∈ A_ minπ (Z_ min (h _1,s))(s)(a )·δ (s,a )(s ). On the other hand, in ′G , from history h1′h _1 ending at dsd_s, the max-player plays ⊤ (probability 11), reaching s deterministically, after which the min-player at s chooses action a′∈Aa ∈ A_ min with probability π′(′(h1′))(s)(a′)π (Z_ min (h _1))(s)(a ), reaching s′s with probability δ′(s,a′)(s′)δ (s,a )(s ). Therefore, summing over all min actions in ′G : ℙ′σ′,π′(Cyl(h′)) _G ^σ ,π (Cyl\! (h )) =ℙ′σ′,π′(Cyl(h1′))×1×∑a′∈Aπ′(′(h1′,s))(s)(a′)⋅δ′(s,a′)(s′). =P_G ^σ ,π (Cyl\! (h _1 ))× 1× _a ∈ A_ minπ (Z_ min (h _1,s))(s)(a )·δ (s,a )(s ). These two expressions agree, so ℙℜ()Ω(σ′),Ω(π′)(Cyl(hℜ))=ℙ′σ′,π′(Cyl(h′))P_ R\! (G ) _ max(σ ), _ min(π )(Cyl\! (h R ))=P_G ^σ ,π (Cyl\! (h )). For the converse mapping, repeat the cylinder induction with Ξ _ max and Ξ _ min. At a dummy state, the first environment identity in Lemma C.6 ensures that the selected action mixture has barycenter exactly πℜ(ohℜ,⊤)(ds,⊤)π R(oh R, )(d_s, ). Thus every cylinder probability, and consequently the probability of the parity objective, is preserved in the reverse direction as well. ∎ We now state the main equivalence theorem for the RPOMDP reduction. Lemma C.9. Let ′G be a Pre- min transformed POSG and ℜ() R\! (G ) its RPOMDP reduction. Let W′⊆′W Plays_G be parity objective and Wℜ=Λ(W′)W R= (W ) its corresponding objective in ℜ() R\! (G ). Then Val′(W′)=Valℜ()(Wℜ).Val_G (W )=Val_ R\! (G )(W R). Proof. For fixed σ′∈Σ′σ ∈ _G , write q′(σ′)=infπ′∈Π′ℙ′σ′,π′(W′),qℜ()(σℜ)=infπℜ∈Πℜ()ℙℜ()σℜ,πℜ(Wℜ).q_G (σ )= _π ∈ _G P_G ^σ ,π (W ), q_ R\! (G )(σ R)= _π R∈ _ R\! (G )P_ R\! (G )^σ R,π R(W R). The first equality in Lemma C.8 gives qℜ()(Ω(σ′))≤q′(σ′)q_ R\! (G )( _ max(σ ))≤ q_G (σ ). Conversely, for every πℜ∈Πℜ()π R∈ _ R\! (G ), the second equality there and Ξ(Ω(σ′))=σ′ _ max( _ max(σ ))=σ give ℙℜ()Ω(σ′),πℜ(Wℜ)=ℙ′σ′,Ξ(πℜ)(W′),P_ R\! (G ) _ max(σ ),π R(W R)=P_G ^σ , _ min(π R)(W ), so q′(σ′)≤qℜ()(Ω(σ′))q_G (σ )≤ q_ R\! (G )( _ max(σ )). Hence the two fixed-strategy infima are equal. Since Ω _ max is a bijection by Lemma C.6, Val′(W′) _G (W ) =supσ′∈Σ′q′(σ′)=supσ′∈Σ′qℜ()(Ω(σ′)) = _σ ∈ _G q_G (σ )= _σ ∈ _G q_ R\! (G )( _ max(σ )) =supσℜ∈Σℜ()qℜ()(σℜ)=Valℜ()(Wℜ). = _σ R∈ _ R\! (G )q_ R\! (G )(σ R)=Val_ R\! (G )(W R). ∎ Corollary C.10. Let ′G be a Pre- min transformed POSG and ℜ() R\! (G ) its RPOMDP reduction. Let p′p a priority function for ′G . Then Val′(Parity′(p′))=Valℜ()(Parityℜ()(pℜ)).Val_G \! (Parity_G \! (p ) )=Val_ R\! (G )\! (Parity_ R\! (G )\! (p R ) ). Proof. Follows directly from lemma C.9 together with lemma C.7. ∎ Lemma C.11. Projected supported plays are preserved in both mapping directions: Λ(′σ′,π′) \! ( Plays^σ ,π _G ) =ℜ()Ω(σ′),Ω(π′), = Plays _ max(σ ), _ min(π )_ R\! (G ), Λ(′Ξ(σℜ),Ξ(πℜ)) \! ( Plays _ max(σ R), _ min(π R)_G ) =ℜ()σℜ,πℜ. = Plays^σ R,π R_ R\! (G ). Proof. We prove both equalities by induction on corresponding finite prefixes. The initial prefixes consist of s0s_0 on both sides. Suppose first that corresponding prefixes under (σ′,π′)(σ ,π ) end at an original max-state s∈Ss∈ S_ max. Their agent observation histories correspond under Λ _O max, and the definition of Ω _ max gives Ω(σ′)(Λ(oh′))(s)=σ′(oh′)(s). _ max(σ )( _O max(oh ))(s)=σ (oh )(s). Thus the same max-actions have positive probability. For every such action a, the RPOMDP uncertainty set at (s,a)(s,a) is the singleton δ′(s,a)\δ (s,a)\, so a dummy state dtd_t is a supported successor in ℜ() R\! (G ) exactly when it is a supported successor in ′G . Now suppose the corresponding prefixes end at dtd_t. In ′G , the effective action ⊤ leads deterministically to t∈St∈ S_ min, after which the min-player uses λ=π′(oht′)(t)∈Δ(A)λ=π (oh _t)(t)∈ (A_ min). In ℜ() R\! (G ), the mapped environment selects t′(λ) bar^G _t(λ) at (dt,⊤)(d_t, ). Hence, for every successor s′∈Ss ∈ S_ max, t′(λ)(s′)>0⟺λ(a)δ′(t,a)(s′)>0 for some a∈A, bar^G _t(λ)(s )>0 λ(a)δ (t,a)(s )>0 for some a∈ A_ min, because all summands are nonnegative. Therefore an extension from dtd_t to s′s is supported in ℜ() R\! (G ) exactly when an extension from dtd_t through t and some supported min-action a to s′s is supported in ′G . This proves the induction step for the first equality. For the reverse direction, agent-action supports agree by the definition of Ξ _ max. At a dummy state use λ=Ξ(πℜ)(oh′)(t)λ= _ min(π R)(oh )(t). The first identity in Lemma C.6 gives t′(λ)=πℜ(Λ(oh′),⊤)(dt,⊤) bar^G _t(λ)=π R( _O min(oh ), )(d_t, ), so the same nonnegativity argument proves the reverse induction step. Finally, an infinite play is supported exactly when all its finite prefixes are supported. Applying Λ to the resulting prefix correspondences yields both displayed equalities. ∎ Lemma C.12. Let W′⊆′W Plays_G be a parity objective of ′G and Wℜ=Λ(W′)W R= (W ) its lifted objective in ℜ() R\! (G ). Let σ∈Σ′σ∈ _G and σℜ=Ω(σ)σ R= _ max(σ). Then σ is sure winning for W′⇔σℜ is sure winning for Wℜ.$σ$ is sure winning for $W $ $σ R$ is sure winning for $W R$. Proof. Suppose σ is sure winning and take arbitrary πℜ∈Πℜ()π R∈ _ R\! (G ). The second equality of Lemma C.11 gives ℜσℜ,πℜ()=Λ(′σ,Ξ(πℜ))⊆Wℜ. Plays^σ R,π R_ R\! (G )= \! ( Plays^σ, _ min(π R)_G ) W R. Conversely, suppose σℜσ R is sure winning and take arbitrary π′∈Π′π ∈ _G . The first equality gives Λ(′σ,π′)=ℜσℜ,Ω(π′)()⊆Wℜ ( Plays^σ,π _G )= Plays^σ R, _ min(π )_ R\! (G ) W R. Lemma C.7 then implies ′σ,π′⊆W′ Plays^σ,π _G W . ∎ Lemma C.13 (Almost-sure Winning). Let W′⊆′W Plays_G be a parity objective of ′G and Wℜ=Λ(W′)W R= (W ) its lifted objective in ℜ() R\! (G ). Let σ∈Σ′σ∈ _G and σℜ=Ω(σ)σ R= _ max(σ). Then, σ is almost-sure winning for W′⇔σℜ is almost-sure winning for Wℜ.$σ$ is almost-sure winning for $W $ $σ R$ is almost-sure winning for $W R$. Proof. The fixed-strategy equality proved in Lemma C.9 is infπ′∈Π′ℙ′σ,π′(W′)=infπℜ∈Πℜ()ℙℜ()σℜ,πℜ(Wℜ). _π ∈ _G P_G ^σ,π (W )= _π R∈ _ R\! (G )P_ R\! (G )^σ R,π R(W R). Hence one side equals 11 if and only if the other does. ∎ Lemma C.14 (Limit-Sure Winning). Let W′⊆′W Plays_G be a parity objective of ′G and Wℜ=Λ(W′)W R= (W ) is the corresponding objective in ℜ() R\! (G ). Then, W′ is limit-sure⇔Wℜ is limit-sureW is limit-sure W R is limit-sure Proof. Follows directly from lemma C.9. ∎ Lemma C.15 (Quantitative Analysis). Let W′⊆′W Plays_G be a parity objective of ′G and Wℜ=Λ(W′)W R= (W ) is the corresponding objective in ℜ() R\! (G ). Then, for k∈(0,1)k∈(0,1) Val′(W′)≥k⇔Valℜ()(Wℜ)≥kVal_G (W )≥ k _ R\! (G )(W R)≥ k Proof. Follows directly from lemma C.9. ∎ C.3.1 Size and memory preservation between ′G and ℜ() R\! (G ) Lemma C.16 (Size and memory preservation under RPOMDP reduction). Let ′G be a Pre-min-transformed POSG and ℜ() R\! (G ) its RPOMDP reduction. The maps Λ:′→ℜ() : Plays_G → Plays_ R\! (G ), Λ,Λ _O max, _O min on observation histories, and Ω⋆,Ξ⋆ _ , _ (⋆∈, ∈\ max, min\) on strategies satisfy the following. 1. (size) |Sℜ|=|S|+|S||S_ R|=|S_ max|+|S_ min|, |Aℜ|=|A|+1|A_ R|=|A_ max|+1, the total vertex count of ℜP_ R is at most |S||A|+|S||A||S_ min|\,|A_ min|+|S_ max|\,|A_ max|, and observation alphabets are inherited unchanged from ′G . In particular, |ℜ()|=(|′|)| R\! (G )|=O(|G |) and the construction runs in linear time. 2. (history length) For every oh′∈′oh ∈ OH_ max^G , |Λ(oh′)|=⌈2|oh′|+13⌉| _O max(oh )|= 2|oh |+13 , and for every ohℜ∈ℜ()oh R∈ OH_ a R\! (G ), |(Λ)−1(ohℜ)|=|ohℜ|+⌊|ohℜ|/2⌋|( _O max)^-1(oh R)|=|oh R|+ |oh R|/2 . The same bounds hold for Λ _O min on ′ OH_ min^G and ^ℜ() OH_ e R\! (G ). Observation histories on the two sides are linear in each other. 3. (memory) The lifting maps Ω⋆,Ξ⋆ _ , _ preserve memory class exactly: memoryless, finite-memory and infinite-memory regimes correspond exactly between ′G and ℜ() R\! (G ). Proof. Clause (1). Direct from the construction. The state space deletes the min-states S_ min retaining only S∪DS_ max∪ D, so |Sℜ|=|S|+|S||S_ R|=|S_ max|+|S_ min|. The action set deletes the min-actions retaining only A∪⊤A_ max∪\ \, so |Aℜ|=|A|+1|A_ R|=|A_ max|+1. The observation alphabets are ℜ=∪ox†∣x∈=′O_ max R=O_ max∪\o _x x _ max\=O_ max and ℜ=∪ox#∣x∈=′O_ min R=O_ min∪\o^\#_x x _ min\=O_ min , which have the same cardinalities as in ′G . For every (s,a)∈S×A(s,a)∈ S_ max× A_ max, the non-default vertex set Vs,aV_s,a is the singleton δ′(s,a)\δ (s,a)\. For each (ds,⊤)(d_s, ), the vertex list consists of δ′(s,a)δ (s,a) for all a∈Aa∈ A_ min. Hence the construction lists at most |S||A|+|S||A||S_ max|\,|A_ max|+|S_ min|\,|A_ min| generators; all other globally enabled pairs share one default max-losing rule. Each component is therefore a constant or unit-additive perturbation of the corresponding component in ′G , so |ℜ()|=(|′|)| R\! (G )|=O(|G |) and ℜ() R\! (G ) is computed from ′G in linear time. Clause (2). Let oh′=o0,z1,o1,o2,z3,o3,⋯,o2n−2,z2n−1,o2n−1,o2n∈′oh =o_0,z_1,o_1,o_2,z_3,o_3,·s,o_2n-2,z_2n-1,o_2n-1,o_2n∈ OH^G _ max ending in max state, so that |oh′|=3n+1|oh |=3n+1. By construction, ΛO(oh′)=o0,z1,⋯,o2n, _O max(oh )=o_0,z_1,·s,o_2n, where o2k+1o_2k+1 are removed for every 3 states. Hence |ΛO(oh′)|=2n+1=2|oh′|+13.| _O max(oh )|=2n+1= 2|oh |+13. Let oh′=o0,z1,o1,o2,z3,o3,⋯,o2n−2,z2n−1,o2n−1,o2n,z2n+1∈′oh =o_0,z_1,o_1,o_2,z_3,o_3,·s,o_2n-2,z_2n-1,o_2n-1,o_2n,z_2n+1∈ OH^G _ max ending in dummy state, so that |oh′|=3n+2|oh |=3n+2. By construction, ΛO(oh′)=o0,z1,⋯,o2n,z2n+1 _O max(oh )=o_0,z_1,·s,o_2n,z_2n+1 where o2k+1o_2k+1 are removed for every 3 states. Hence |ΛO(oh′)|=2n+2=2|oh′|+23.| _O max(oh )|=2n+2= 2|oh |+23. From above values, For every oh′∈′oh ∈ OH_ max^G , |Λ(oh′)|=⌈2|oh′|+13⌉| _O max(oh )|= 2|oh |+13 Let oh=o0,z1,⋯,o2n∈aℜ()oh=o_0,z_1,·s,o_2n∈ OH R\! (G )_a ending in S_ max state, so that |oh|=2n+1|oh|=2n+1. By construction, (ΛO)−1(oh)=o0,z1,o1,o2,z3,o3,⋯,o2n−2,z2n−1,o2n−1,o2n( _O max)^-1(oh)=o_0,z_1,o_1,o_2,z_3,o_3,·s,o_2n-2,z_2n-1,o_2n-1,o_2n where o2k+1o_2k+1 are added deterministically from z2k+1z_2k+1 for every 2 states. Hence |(ΛO)−1(oh)|=3n+1=3|oh|−12=|oh|+|oh|−12.|( _O max)^-1(oh)|=3n+1= 3|oh|-12=|oh|+ |oh|-12. Let oh=o0,z1,⋯,o2n,z2n+1∈aℜ()oh=o_0,z_1,·s,o_2n,z_2n+1∈ OH R\! (G )_a ending in dummy state, so that |oh|=2n+2|oh|=2n+2. By construction, (ΛO)−1(oh)=o0,z1,o1,o2,z3,o3,⋯,o2n−2,z2n−1,o2n−1,o2n,z2n+1( _O max)^-1(oh)=o_0,z_1,o_1,o_2,z_3,o_3,·s,o_2n-2,z_2n-1,o_2n-1,o_2n,z_2n+1 where o2k+1o_2k+1 are added from z2k+1z_2k+1 for every 2 states. Hence |(ΛO)−1(oh)|=3n+2=3|oh|2−1=|oh|+|oh|−22.|( _O max)^-1(oh)|=3n+2= 3|oh|2-1=|oh|+ |oh|-22. Thus, for every oh∈ℜ()oh∈ OH_ a R\! (G ), |(Λ)−1(oh)|=|oh|+⌊|oh|−12⌋|( _O max)^-1(oh)|=|oh|+ |oh|-12 . The environment-history bounds follow identically. Clause (3). Fix a player and let its strategy be realized by a transducer M=(Q,q0,u,g)M=(Q,q_0,u,g) over that player’s observation alphabet. The history maps Λ _O max and Λ _O min delete each S_ min-observation, while their inverses reinsert it. The deleted observation is determined by the preceding tagged dummy observation: ox†o _x or ox#o^\#_x uniquely determines x. Consequently, both contraction and expansion can be performed online without adding persistent memory states. For Ω _ max, run the transducer for σ′σ on the expanded history (Λ)−1(ohℜ)( _O max)^-1(oh R) and use its state-indexed action assignment unchanged. For Ω _ min, run the transducer for π′π on (Λ)−1(ohℜ)( _O min)^-1(oh R) and apply s′ bar^G _s to the output distribution at a compatible dummy state; at a non-dummy state the required transition assignment is the unique element of the singleton uncertainty set. These are output transformations and require no additional memory. Conversely, Ξ _ max runs the transducer for σℜσ R on the contracted history Λ(oh′) _O max(oh ). The map Ξ _ min runs the transducer for πℜπ R on Λ(oh′) _O min(oh ) and applies the fixed coefficient choice βsP _s^P to the selected polytope point. Again, contraction and the output transformation leave the memory set Q unchanged. The history identities in Lemmas C.3 and C.4 show that these transducers realize the four stated strategy maps. Thus each map preserves the number of memory states. In particular, memoryless, finite-memory, and unrestricted infinite-memory strategies correspond in both directions. ∎ C.4 Proof of Lemma 3.3 Proof. Because parity objective subsumes all ω-regular objectives, from lemma C.9, Val′(W′)=Valℜ()(Wℜ)Val_G (W )=Val_ R\! (G )(W R) for any ω-regular objective W′W in ′G and its corresponding objective WℜW R in ℜ() R\! (G ). The “consequently” statement follows from lemmas C.12, C.13, C.14, and C.15. ∎