Paper deep dive
Quantitative Analysis of $ω$-Regular Robust MDPs
Ali Asadi, Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Alipasha Montaseri, Ali Shafiee
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 8/29/2026, 3:42:35 AM
Summary
This paper addresses the quantitative analysis of Robust Markov Decision Processes (RMDPs) with linearly defined uncertainty sets and parity objectives. The authors prove that both agent and environment have pure memoryless optimal policies. They present a polynomial-time algorithm for quantitative parity on linearly defined robust Markov chains (RMCs) using linear programming, which serves as a subroutine in a policy-iteration algorithm for RMDPs. Experiments show the approach scales better than explicit reductions to stochastic games on benchmarks with high branching factors.
Entities (8)
Relation Signals (6)
Robust Markov Decision Process → supports → Parity Objective
confidence 95% · We consider (s,a)-rectangular RMDPs with linearly defined uncertainty sets and study parity objectives
Agent → hasoptimalpolicytype → Memoryless Policy
confidence 94% · we show that both the agent and the environment admit pure memoryless optimal policies.
Environment → hasoptimalpolicytype → Memoryless Policy
confidence 94% · we show that both the agent and the environment admit pure memoryless optimal policies.
Policy Iteration Algorithm → uses → Linear Program
confidence 93% · use it as a subroutine in a policy-iteration algorithm for RMDPs... For reachability objectives, we formulate a polynomial-size linear program.
Linearly Defined Uncertainty Set → enables → polynomial-time algorithm
confidence 92% · we give a polynomial-time algorithm for quantitative parity on linearly defined robust Markov chains
Robust Markov Chain → issubclassof → Robust Markov Decision Process
confidence 90% · We first consider robust Markov chains (RMCs), i.e., RMDPs in which the agent has a single action.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Robust Markov Decision Processes (RMDPs) generalize classical MDPs by allowing uncertainty in transition probabilities and optimizing against their worst-case realization. We consider $(s,a)$-rectangular RMDPs with \emph{linearly defined} uncertainty sets and study parity objectives, which are a canonical representation of $\omega$-regular objectives. An uncertainty set is linearly defined if it is described by linear inequalities over the transition distribution together with auxiliary variables, which capture the standard $L_1$ and $L_\infty$ balls as well as general polytopic uncertainty sets. The quantitative value is the supremum, over all agent policies, of the satisfaction probability guaranteed against the adversarial environment. Previous work studied the qualitative analysis, namely the almost-sure (resp. positive) problem that asks whether a single agent policy guarantees satisfaction with probability one (resp. positive probability) against every environment policy. In this work, we solve the exact quantitative problem. Our contributions are threefold. First, we show that both the agent and the environment admit pure memoryless optimal policies. Second, we give a polynomial-time algorithm for quantitative parity on linearly defined robust Markov chains and use it as a subroutine in a policy-iteration algorithm for RMDPs. The algorithm combines quantitative one-step improvements with qualitative almost-sure improvements. Finally, we report experiments comparing our approach with the explicit reduction to stochastic games.
Tags
Links
- Source: https://arxiv.org/abs/2608.25968v1
- Canonical: https://arxiv.org/abs/2608.25968v1
Trouble viewing inline? Open PDF directly →
Full Text
180,512 characters extracted from source content.
Expand or collapse full text
Quantitative Analysis of ω-Regular Robust MDPs Ali Asadi Krishnendu Chatterjee Ehsan Kafshdar Goharshady Mehrdad Karrabi Alipasha Montaseri Ali Shafiee Abstract Robust Markov Decision Processes (RMDPs) generalize classical MDPs by allowing uncertainty in transition probabilities and optimizing against their worst-case realization. We consider (s,a)(s,a)-rectangular RMDPs with linearly defined uncertainty sets and study parity objectives, which are a canonical representation of ω-regular objectives. An uncertainty set is linearly defined if it is described by linear inequalities over the transition distribution together with auxiliary variables, which captures the standard L1L_1 and L∞L_∞ balls as well as general polytopic uncertainty sets. The quantitative value is the supremum, over all agent policies, of the satisfaction probability guaranteed against the adversarial environment. Previous work studied the qualitative analysis, namely the almost-sure (resp. positive) problem that asks whether a single agent policy guarantees satisfaction with probability one (resp. positive probability) against every environment policy. In this work, we solve the exact quantitative problem. Our contributions are threefold. First, we show that both the agent and the environment admit pure memoryless optimal policies. Second, we give a polynomial-time algorithm for quantitative parity on linearly defined robust Markov chains and use it as a subroutine in a policy-iteration algorithm for RMDPs. The algorithm combines quantitative one-step improvements with qualitative almost-sure improvements. Finally, we report experiments comparing our approach with the explicit reduction to stochastic games. 1Institute of Science and Technology Austria ali.asadi@ist.ac.at, krichnendu.chatterjee@ist.ac.at, ehsan.goharshady@ist.ac.at, mehrdad.karrabi@ist.ac.at, alipasha.montaseri@ist.ac.at, ali.shafiee@ist.ac.at 1 Introduction Robust MDPs. Markov Decision Processes (MDPs) are a fundamental framework for reasoning, decision making, and stochastic planning (Puterman 1994). In a classical MDP, an agent chooses actions and the next state is determined stochastically according to a known transition function. However, transition probabilities are often estimated from data, and the exact transition function is therefore not known. Robust Markov Decision Processes (RMDPs) address this issue by associating every state-action pair with an uncertainty set of possible transition distributions (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann et al. 2013). After observing the action of the agent, an adversarial environment chooses a distribution from the corresponding uncertainty set, and the goal of the agent is to optimize against all such choices. This setting is known as (s,a)(s,a)-rectangular uncertainty. In this work, we consider linearly defined uncertainty sets, i.e. sets described by rational linear inequalities over the transition distribution together with auxiliary variables that are existentially quantified. The auxiliary variables keep the description succinct: the standard L1L_1 and L∞L_∞ balls around a nominal transition distribution are linearly defined with linearly many inequalities, whereas an L1L_1 ball has exponentially many facets in the transition probabilities alone. Since every uncertainty set lies in the probability simplex, linearly defined sets are precisely the convex polytopes, so this model subsumes general polytopic uncertainty sets while admitting far more succinct descriptions. Parity and ω-Regular Objectives. Most of the RMDP literature considers quantitative objectives such as discounted sum or long-run average reward. These objectives provide performance guarantees, but they do not express the logical correctness requirements that arise in safety-critical systems, e.g., an autonomous system is required to avoid unsafe configurations, eventually complete a task, or repeatedly provide a service. Such reachability, safety, and liveness requirements are naturally expressed by ω-regular objectives. Parity objectives are a canonical representation of this class. An ω-regular objective can be represented by a finite deterministic parity automaton. Combining this automaton with an RMDP yields a product RMDP with a parity objective (Baier and Katoen 2008). Hence, RMDPs with parity objectives provide a flexible and broad framework for the analysis of probabilistic systems with logical objectives. Quantitative Analysis. Given an RMDP and a logical objective, the value of a state is the maximal satisfaction probability guaranteed by the agent against every environment choice. Qualitative analysis considers two questions. The almost-sure (resp. positive) problem asks whether there exists an agent policy that guarantees satisfaction with probability one (resp. greater than zero) against every environment choice. However, these qualitative analyses do not distinguish among policies when no almost-sure guarantee exists. Hence, quantitative analysis is important for finding optimal policies and computing the values. The work of Asadi et al. (2026b) gives algorithms for the positive and almost-sure problems: polynomial time for reachability and safety objectives, and quasi-polynomial time and polynomial space for all parity objectives. However, the quantitative analysis remains open. Contributions. We solve the quantitative parity problem for RMDPs with linearly defined uncertainty sets. Our contributions are threefold. 1. We first consider robust Markov chains (RMCs), i.e., RMDPs in which the agent has a single action. For reachability objectives, we formulate a polynomial-size linear program. We then combine this formulation with an analysis of recurrent components to solve parity objectives, which yields a polynomial-time algorithm for the quantitative parity problem. 2. We then present a policy-iteration algorithm for RMDPs. We establish that both the agent and the environment admit stationary memoryless optimal policies. Each iteration evaluates the RMC induced by the current agent policy and applies either a quantitative one-step improvement or a qualitative almost-sure improvement. We show that the algorithm terminates with the exact value vector and optimal agent and environment policies. 3. Finally, we implement our algorithms for reachability and parity objectives under L1L_1 and L∞L_∞ uncertainty. We compare our approach with the explicit reduction to a turn-based stochastic game. Our approach scales substantially better on the Garnet and Inventory benchmarks, whose branching factor grows with the instance size, whereas the explicit reduction is faster on the Frozen Lake benchmark, which has a small branching factor. Related Work. Our policy-iteration algorithm is, in spirit, close to the strategy-improvement method for stochastic parity and Rabin games (Chatterjee and Henzinger 2006a; Chatterjee and Henzinger 2006b), but in our robust setting the environment ranges over a continuum of distributions in an uncertainty polytope rather than over the finitely many vertices of a stochastic game. Our improvement therefore works directly with the linearly defined uncertainty sets (through the value classes, tight actions, and tight faces of Section 4) and never constructs the exponentially larger game. The closest prior work on logical objectives for RMDPs is Asadi et al. (2026b), which solves the positive and almost-sure problems using uncertainty-set oracles. Our qualitative improvement step invokes their almost-sure parity procedure as a sub-routine, whereas the exact quantitative problem we solve here remained open. An extended discussion of related work is deferred to Appendix A. 2 Preliminaries and Model Description Notation. For any finite set A we use Δ(A) (A) and 2A2^A to denote the set of all distributions over A and the power-set of A respectively. We use [n][n] as shorthand for 0,…,n\0,…,n\. MDPs and MCs. A Markov decision process (MDP) is a tuple M=(,,δ)M=(S,A,δ) where S is a finite set of states, A is a finite set of actions and δ:×→Δ()δ ×A→ (S) specifies the transition probabilities. A Markov chain (MC) is an MDP whose action set is a singleton, i.e. ||=1|A|=1. The semantics of MDPs are defined by policies. An agent policy is σ:(×)∗×→Δ()σ (S×A)^*×S→ (A) that maps a history of states and actions to a distribution over actions. Given such a policy a token is placed on an initial state s0∈s_0 and at the i-th step, the agent draws an action ai∼σ(s0,a0,…,si−1,ai−1,si)a_i σ(s_0,a_0,…,s_i-1,a_i-1,s_i) and the next state si+1s_i+1 is sampled from δ(si,ai)δ(s_i,a_i). Fixing an initial state s0s_0, the cylinder construction of (Baier and Katoen 2008) generates a probability distribution Prs0σ ^σ_s_0 over infinite paths in the MDP. The semantics of MCs are defined analogously, but since there is no choice of actions, the next state is sampled directly from the transition probabilities. RMDPs and RMCs. Robust Markov Decision Processes (RMDPs) extend MDPs by allowing uncertainty in the transition probabiliaties. Formally, an RMDP is a tuple ℳ=(,,)M=(S,A,P) where S and A are as before, but :×→2Δ()P ×A→ 2 (S) maps each state-action pair to a set of possible transition distributions, called the uncertainty set. A Robust Markov Chain (RMC) is an RMDP where ||=1|A|=1, hence an RMC ℛR is defined by a pair (,)(S,P). The semantics of RMDPs are defined by a pair of policies: an agent policy σ as before, and an environment policy τ:(×)∗×(×)→Δ()τ (S×A)^*×(S×A)→ (S) that maps a history of states and actions to a distribution over next states where for every history h∈(×)∗h∈(S×A)^* and (si,ai)∈×(s_i,a_i) ×A, it holds that τ(h,si,ai)∈(si,ai)τ(h,s_i,a_i) (s_i,a_i). As with MDPs, fixing an initial state s0s_0 and a policy profile (σ,τ)(σ,τ) in an RMDP ℳM induces a probability distribution Prσ,τ ^σ,τ over infinite paths in ℳM. The semantics of RMCs are defined analogously. Policies. An agent policy σ is deterministic if it maps every history to a single action and memoryless if it only depends on the current state, i.e. σ(h,s)=σ(h′,s)σ(h,s)=σ(h ,s) for all histories h,h′h,h and state s∈s . A positional policy is both deterministic and memoryless. Conventionally, we assume positional policies are →S functions. We denote the set of all agent policies by Σ and the set of all environment policies by Γ . Fixing a positional policy σ in an RMDP ℳM, induces an RMC ℳσM^σ where the only available action at each state s is σ(s)σ(s) and the uncertainty set is defined as σ(s)=(s,σ(s))P^σ(s)=P(s,σ(s)). Remark 1. This work is concerned with (s,a)(s,a)-rectangular RMDPs whose semantics are defined above: the environment observes the action taken by the agent and then chooses a distribution from the corresponding uncertainty set. Objectives and Values. An objective φ is a measurable set of infinite paths in ℳM. Given an agent policy σ and an environment policy τ, we denote by Prℳ,sσ,τ[φ] ^σ,τ_M,s[ ] the probability that a path starting from state s satisfies the objective φ . The value of an objective φ in an RMDP ℳM from s is sℳ(φ)=supσ∈Σinfτ∈ΓPrsσ,τ[φ]. v^M_s( )= _σ∈ _τ∈ ^σ,τ_s[ ]. Values are defined analogously for RMCs. We focus on parity objectives. A parity objective (C) Parity(C) is defined with respect to a coloring function C:→[d]C →[d]. Particularly, (C) Parity(C) is defined as the set of all infinite paths π such that the maximum color that appears infinitely often in π is even, i.e. (C)=π∈ω∣maxC(s)∣s∈(π) is even, Parity(C)=\π ^ω \C(s) s∈ Inf(π)\ ~is~ even\, where (π) Inf(π) denotes the set of states that occur infinitely often in π. It is a classical result that every ω-regular objective, including reachability, safety and liveness, can be reduced to a parity objective (Baier and Katoen 2008). Model Assumption. A linearly defined uncertainty set (s,a)P(s,a) is the projection of a polyhedron onto the probability coordinates, i.e. there exist a matrix A and a vector b, of dimensions compatible with k auxiliary variables, where: (s,a)=x∈Δ()|∃y∈ℝk:A[xy]≤b.P(s,a)= \x∈ (S)\; |\;∃ y ^k A bmatrixx\\ y bmatrix≤ b \. Note that the auxiliary variables y are existentially quantified, so a linearly defined set need not be cut out by linear inequalities over x alone. This is strictly more expressive in terms of succinctness: an L1L_1 ball around a nominal distribution is linearly defined using only O(||)O(|S|) inequalities and auxiliary variables, whereas over x alone it has exponentially many facets (see Appendix B). Finally, since (s,a)⊆Δ()P(s,a) (S) is bounded, every linearly defined uncertainty set is a convex polytope. Throughout this paper, we assume that every uncertainty set is linearly defined. This assumption is satisfied by the standard L1L_1 and L∞L_∞ balls (See Appendix B), as well as by the more general polytopic uncertainty sets. Problem Statement. The main problem statement in this paper is summarized as follows: Given a linearly defined RMDP ℳM and a parity objective (C) Parity(C), the quantitative parity problem asks to compute the value sℳ((C)) v^M_s( Parity(C)) for every state s∈s . In Section 3, we present an algorithm for solving the quantitative parity problem in RMCs that runs in polynomial time. We will than use the RMC algorithm as a sub-procedure to solve the quantitative parity problem in RMDPs in Section 4. 3 Quantitative RMC Analysis Sub-Procedure We present a polynomial-time algorithm for solving the quantitative safety and parity objectives in linearly defined RMCs ℛ=(,)R=(S,P) where the environment’s goal is to minimize the probability that the objective is satisfied. This is then used in the algorithm for solving RMDPs as a sub-procedure. In what follows, we first consider the case of safety objectives (Section 3.1) and present an LP-based algorithm for solving them. We then use the method for solving safety objectives and present a solution for the quantitative parity problem (Section 3.2). 3.1 Safety Given a set ⊆T , the safety objective () Safe(T) is the set of infinite paths that never leave T. The environment is adversarial and minimizes the probability of remaining safe, so the value at a state s is sℛ(())=infτPrsτ[()] v^R_s( Safe(T))= _τ ^τ_s[ Safe(T)]. We compute this value for every s with a single linear program, exploiting the duality of safety and reachability together with the flow-like characterization of reachability probabilities. Pre-Processing. We first dispose of the states whose safety value is 00 or 11. We use the polynomial-time method of (Asadi et al. 2026b) to compute the sets =0S^=0 and =1S^=1 of states with safety value 00 and 11, respectively. Our pre-processing step makes all states in =0∪=1S^=0 ^=1 absorbing. This leaves the states ?=∖(=0∪=1)S^?=S (S^=0 ^=1), whose values are to be computed. Flow-like Characterization. Fix a source state s0∈?s_0 ^? and picture injecting one unit of probability mass there. As the play unfolds, this mass is routed through the state space along the transition probabilities until it is absorbed in =0∪=1S^=0 ^=1. The adversarial environment moves this mass so as to minimize the amount absorbed in =1S^=1 and maximize the amount absorbed in =0S^=0. Recording, for each state s, the expected number of visits xsx_s, and for each edge (s,s′)(s,s ) the expected number of traversals fs,s′f_s,s , these quantities behave exactly like a conserved flow. They satisfy the following linear properties, which we later assemble into the LP: • Non-negativity. No state is visited and no edge is traversed a negative number of times: ≡⋀s∈?,s′∈(xs≥0∧fs,s′≥0). NNeg\;≡\; _s ^?,\,s (x_s≥ 0\; \;f_s,s ≥ 0 ). • Conservation. The expected number of visits to a state equals the mass injected there plus the total flow entering it, which is Kirchhoff’s conservation law: ≡⋀s∈?(xs= 1[s=s0]+∑s′∈?fs′,s). Cons\;≡\; _s ^? (x_s\;=\;1[\,s=s_0\,]\;+\; _s ^?f_s ,s ). • Splitting. Each visit to a state is followed by exactly one outgoing edge, so the visits to a state are split among its outgoing flow: ≡⋀s∈?(∑s′∈fs,s′=xs). Split\;≡\; _s ^? ( _s f_s,s \;=\;x_s ). • Admissibility. The proportions in which the flow leaves a state form a distribution s/xs f_s/x_s, where s=(fs,s′)s′∈ f_s=(f_s,s )_s , that the environment is allowed to pick, i.e. s/xs∈(s) f_s/x_s (s). This membership is, at face value, nonlinear: it divides the flow variables by the visit variable. However, by the Assumption (s)=p:Asp≤bsP(s)=\p:A_s\,p≤ b_s\, so the constraint reads As(s/xs)≤bsA_s( f_s/x_s)≤ b_s; multiplying both sides by xs≥0x_s≥ 0 preserves the inequality and clears the denominator, yielding the equivalent linear constraint ≡⋀s∈?(Ass≤xsbs). Adm\;≡\; _s ^? (A_s\, f_s\;≤\;x_s\,b_s ). This is jointly linear in the flow variables s f_s and the visit variable xsx_s, since AsA_s and bsb_s are constants. Since =1S^=1 is absorbing, the probability of reaching =1S^=1 from s0s_0 is simply the total flow that crosses into =1S^=1. Hence, the environment minimises ∑s∈?w∈=1fs,w _ subarraycs ^?\\ w ^=1 subarrayf_s,w, which is therefore the objective of the LP. The following lemma (proved in Appendix C) formalises the above discussion and establishes the correctness of the LP: Lemma 2. Given a linearly defined RMC ℛR, initial state s0∈?s_0 ^? and with safe set ⊆T , let ∗ v^* be the solution to the following linear program: minx,f _x,\,f ∑s∈?,w∈=1fs,w _ subarraycs ^?,\,w ^=1 subarrayf_s,w (⋆ ) s.t. .t. ∧, NNeg\, \, Cons\, \, Split\, \, Adm, then s0ℛ(())=∗ v^R_s_0( Safe(T))= v^*. Building on this, we obtain that the safety values of an RMC, together with optimal environment policies, can be computed in polynomial time. Theorem 3. Given a linearly defined RMC ℛR with safety objective () Safe(T), for each fixed s, the value sℛ(()) v^R_s( Safe(T)), together with a positional environment policy that attains it, can be computed in time polynomial in the size of ℛR. 3.2 Parity In this section, we solve the quantitative parity problem by reducing it to a safety computation. Recall that the environment is adversarial and minimizes the probability of satisfying (C) Parity(C). We first show a polynomial-time algorithm that computes the set WoddW_odd of states lying in an end-component whose dominant color is odd implying that the environment can violate (C) Parity(C) with probability 11. We then show that the parity value at any state equals the value of (∖Wodd) Safe(S W_odd), i.e., the environment’s goal is to minimize the probability of not reaching WoddW_odd. This value is then computed by the safety variant of the LP of Section 3.1. Almost-Sure Violation of Parity. We compute the set WoddW_odd of states lying in an end-component from which the environment can violate (C) Parity(C) with probability 11. We note that the algorithm of (Asadi et al. 2026b) can be used to compute this qualitative information too, however, their method requires super-polynomial time in the worst case, while our goal is to provide a polynomial-time algorithm. We first define the notion of maximal end-components (MECs) in RMCs, which are the analogue of MECs in MDPs: Definition 4. For a set U⊆U and a state s∈Us∈ U, let U(s)=p∈(s):(p)⊆UP_U(s)=\\,p (s)\;:\; supp(p) U\,\ be the set of distributions at s with which the environment can keep the play inside U. A set U⊆U is an end-component (EC) of an RMC ℛR if the following conditions hold: 1. For every state s∈Us∈ U, we have U(s)≠∅P_U(s)≠ . 2. The graph induced by UP_U on U is strongly connected. Furthermore, U is a maximal EC (MEC) if there is no end-component U′⊆U such that U⊂U′U⊂ U . Intuitively, whenever the play enters a (maximal) EC, the environment can ensure that the play remains in the end-component forever. The environment’s goal would then be to reach an end-component in which the parity objective can be violated almost-surely. The MecDecomp procedure in Algorithm 4 of Appendix D takes an RMC ℛR as input and returns its MECs in polynomial time. The algorithm is based on the standard algorithm for computing MECs in MDPs (Chatterjee and Henzinger 2014), and utilizes the polytopic structure of the uncertainty sets. Algorithm 1 illustrates the OddEC procedure which utilizes MecDecomp to compute the set WoddW_odd as the union of those ECs where the environment can almost-surely violate (C) Parity(C) in them. Since the play can be confined to a MEC and visits all of its states infinitely often, the dominant color the environment can enforce in a MEC is its highest color mim_i: if mim_i is odd, the environment stays in the MEC forever and makes the dominant color odd, so the whole MEC violates the objective and is added to WoddW_odd; otherwise the environment must avoid the even color mim_i becoming dominant, so we discard the states of color mim_i and recurse on the rest. Algorithm 1 (B) OddEC(B) 0: A subset B⊆B ; the top-level call uses B=B=S. 0: Union of ECs in B whose dominant color is odd. 1: M1,…,Mk←(B)M_1,…,M_k← MecDecomp(B) 2: W←∅W← 3: for i=1,…,ki=1,…,k do 4: mi←maxs∈MiC(s)m_i← _s∈ M_iC(s) 5: if mim_i is odd then W←W∪MiW← W∪ M_i 6: else W←W∪(Mi∖C−1(mi))W← W∪ OddEC(M_i C^-1(m_i)) 7: end for 8: return W The following lemma (proved in Appendix E) establishes the correctness and complexity of the OddEC procedure. Lemma 5. OddEC computes WoddW_odd in polynomial time. Quantitative Satisfaction of Parity. Having computed WoddW_odd, we reduce the quantitative parity problem to the safety computation of Section 3.1. From any state in WoddW_odd the environment violates (C) Parity(C) almost-surely, and, conversely, under every environment policy, almost every play settles in an EC. So, under every environment policy, the probability of violating (C) Parity(C) is at most the probability of reaching WoddW_odd, and the environment attains it by playing optimally for reachability of WoddW_odd and then enforcing an odd dominant color. The following lemma establishes this reduction, and is proved in Appendix E. Lemma 6. Given a linearly defined RMC ℛ=(,)R=(S,P) it holds that sℛ((C))=sℛ((∖Wodd)) v^R_s( Parity(C))= v^R_s ( Safe(S W_odd) ). The right-hand side is exactly the value computed by the LP (⋆)( ) of Section 3.1, instantiated with unsafe set U=WoddU=W_odd. This yields the parity values, and optimal positional environment policies, in polynomial time: Theorem 7. Given a linearly defined RMC ℛR with parity objective (C) Parity(C), for all s∈s the value sℛ((C)) v^R_s( Parity(C)), together with a positional environment policy that attains it, can be computed in time polynomial in the size of ℛR. 4 Quantitative Analysis of ω-Regular RMDPs Algorithm 2 presents our policy-iteration algorithm for the quantitative parity problem on linearly defined RMDPs. The algorithm ranges over positional agent policies and, in each iteration, tries to improve the current policy by calling the Improve procedure of Algorithm 3. Throughout this section we fix an RMDP ℳM and a parity objective (C) Parity(C). In what follows we describe the algorithm and its ingredients, and state its correctness and complexity guarantees. The proofs are deferred to Appendix G. Positional Determinacy. Before diving into the algorithm, we establish that for parity objectives, positional optimal policies exist for both the agent and the environment. Fixing a positional agent policy σ induces the RMC ℳσM^σ whose only action at each state s is σ(s)σ(s) and whose uncertainty set is σ(s)=(s,σ(s))P^σ(s)=P(s,σ(s)); we write σ v^σ for its value vector, sσ=infτPrsσ,τ[φ] v^σ_s= _τ ^σ,τ_s[ ]. Our analysis rests on the following determinacy result, which is where polytopic properties of the uncertainty sets are used. Proposition 8. Let ℳM be a linearly defined RMDP with parity objective φ=(C) = Parity(C). There exists a positional agent policy σ∗σ and a positional environment policy τ∗τ where infτPrsσ∗,τ[φ]=supσPrsσ,τ∗[φ]=sℳ(φ) _τ ^σ ,τ_s[ ]= _σ ^σ,τ _s[ ]= v^M_s( ) for every s. The proof uses the reduction introduced in (Chatterjee et al. 2024) to reduce ℳM to a finite turn-based stochastic parity game in which the environment’s choice is replaced by an adversarial choice of a corner of the uncertainty set. The reduction is value-preserving and maps positional strategies of the game back to positional policies of ℳM, so positional determinacy of stochastic games implies the proposition. The number of corners, and hence the size of the game, may however be exponential, so this route requires exponential space; our policy iteration algorithm below instead runs in polynomial space. Combined with the polynomial-time RMC solver of Section 3, Proposition 8 also settles the complexity of the decision problem. Corollary 9. Given a linearly defined RMDP ℳM, a state s∈s and a rational λ∈[0,1]λ∈[0,1], the problem of deciding whether sℳ(φ)≥λ v^M_s( )≥λ is (i) in ∩NP and (i) at least as hard as the analogous problem in turn-based stochastic parity games. Hardness implies that a polynomial-time algorithm here would also solve turn-based stochastic parity games, a long-standing open problem. Policy Iteration. The policy iteration algorithm PI (Algorithm 2) starts from an arbitrary positional agent policy and iteratively calls the Improve procedure (Algorithm 3) to improve it. Once the policy can not be improved further, the algorithm returns it together with its value vector. To this end, the main technical ingredient of the algorithm lies in the Improve procedure, explained next. Policy Improvement. The Improve procedure (Algorithm 3) takes as input a positional agent policy σ, computes its value vector σ v^σ (using the method of Section 3), and then tries to improve σ in one of the following two ways: • Quantitative improvement: A quantitative improvement is possible when for some state s an action a exists such that its worst-case one-step value ν(s,a)=minp∈(s,a)p⋅σν(s,a)= _p (s,a)p· v^σ strictly exceeds the current value sσ v^σ_s. In this case, the agent switches to such an action a for every state s where an improvement is possible and returns the new policy (Lines 2–9 of Algorithm 3). The following lemma shows that the resulting policy is strictly better than σ: Lemma 10. Let σ′=(ℳ,σ)σ = Improve(M,σ) be obtained by a quantitative improvement. Then sσ′≥sσ v^σ _s≥ v^σ_s for all s∈s , and sσ′>sσ v^σ _s> v^σ_s for some s∈s . • Qualitative improvement: If a quantitative improvement is not available, the algorithm checks whether a qualitative improvement is possible. To this end, the algorithm iterates over the value classes of σ v^σ: Value Classes, Tight Actions, Tight Faces. For r∈[0,1]r∈[0,1], the value class σ(r)=s∈∣sσ=r VC^σ(r)=\s v^σ_s=r\ is the set of states of value r under σ. There are at most |||S| non-empty value classes. An action a∈a is tight at s (with respect to σ v^σ) if ν(s,a)=sσν(s,a)= v^σ_s; we write σ(s)A v^σ(s) for the set of tight actions at s, and call σ(s,a)P v^σ(s,a) the tight face at (s,a)(s,a) when a is tight at s. If a is tight at s then every p∈(s,a)p (s,a) satisfies p⋅σ≥sσp· v^σ≥ v^σ_s; if a is not tight at s and no action improves at s, then minpp⋅σ<sσ _pp· v^σ< v^σ_s. For every value class Ur=σ(r)U_r= VC^σ(r), the algorithm will then construct an RMDP ℳrM_r together with a coloring CrC_r defined as follows: (i) the states of ℳrM_r are those of UrU_r together with a fresh terminal state ⊥ , (i) the agent’s actions are its tight actions, (i) the uncertainty sets of ℳrM_r are the tight faces of ℳM inside UrU_r and the singleton δ⊥\ _ \ (dirac distribution over ⊥ ) outside UrU_r, and (iv) the coloring CrC_r is the same as C inside UrU_r and assigns a fresh dominating odd color to ⊥ . The algorithm then calls the almost-sure parity procedure of (Asadi et al. 2026b) on (ℳr,(Cr))(M_r, Parity(C_r)) to compute the set Wr⊆UrW_r U_r as the set of state where the agent can guarantee (Cr) Parity(C_r)’s satisfaction with probability 1 together with its corresponding optimal policy σr _r (lines 10–15). If Wr≠∅W_r≠ , then the agent can improve its policy by switching to σr _r on WrW_r. The following lemma shows that the resulting policy is strictly better than σ: Lemma 11. Let σ′=(ℳ,σ)σ = Improve(M,σ) be obtained by a qualitative improvement, i.e. a quantitative improvement is not possible and W:=⋃r<1Wr≠∅W:= _r<1W_r≠ . Then sσ′≥sσ v^σ _s≥ v^σ_s for all s∈s , and sσ′>sσ v^σ _s> v^σ_s for all s∈Ws∈ W. Intuitively, Lemma 11 follows by the fact that if the environment tries to keep the run inside UrU_r, then the agent can guarantee (Cr) Parity(C_r) with probability 1, and if the environment tries to escape UrU_r, then the agent can guarantee a value strictly larger than r by the definition of tight faces. The full proof is given in Appendix G. Algorithm 2 (ℳ) PI(M) 0: Linearly Defined RMDP ℳM, coloring C 0: optimal agent policy σ∗σ^* and value vector ℳ(φ) v^M( ) 1: pick an arbitrary positional policy σ 2: repeat 3: σold←σ _old←σ 4: σ←(ℳ,σold)σ← Improve(M, _old) 5: until σ=σoldσ= _old 6: return σ and σ v^σ Algorithm 3 (ℳ,σ) Improve(M,σ) 0: RMDP ℳM, coloring C, agent policy σ 0: policy σ′σ with σ′=σ =σ or σ′⪈σ v^σ v^σ 1: σ←SolveRMC(ℳσ,(C)) v^σ← SolveRMC(M^σ, Parity(C)) ⊳ Section 3 2: for each (s,a)∈×(s,a) ×A do 3: ν(s,a)←minp∈(s,a)p⋅σν(s,a)← _p (s,a)p· v^σ ⊳ one linear program 4: end for 5: I←s∈∣maxa∈ν(s,a)>sσI←\\,s _a ν(s,a)> v^σ_s\,\ 6: if I≠∅I≠ then 7: σ′(s)←argmaxa∈ν(s,a)if s∈I,σ(s)otherwise.σ (s)← cases _a ν(s,a)&if s∈ I,\\ σ(s)&otherwise. cases 8: return σ′σ 9: end if 10: W←∅W← 11: for each value r<1r<1 of σ v^σ with Ur=σ(r)≠∅U_r= VC^σ(r)≠ do 12: Construct ℳrM_r and coloring CrC_r from ν 13: (Wr,σr)←AlmostSureParity(ℳr,(Cr))(W_r, _r)← AlmostSureParity(M_r, Parity(C_r)) 14: W←W∪WrW← W∪ W_r 15: end for 16: if W≠∅W≠ then 17: σ′(s)←σr(s)if s∈Wr for some r,σ(s)otherwise.σ (s)← cases _r(s)&if s∈ W_r for some r,\\ σ(s)&otherwise. cases 18: return σ′σ 19: end if 20: return σ Correctness and Complexity. It follows directly from Lemma 10 and Lemma 11 that every call to Improve either returns a strictly better policy or the same policy, in which case a fixpoint is reached. Hence, the policy is indeed improved in every iteration of PI. Since there are only finitely many positional policies, the algorithm must terminate. The following theorem establishes the correctness and complexity of the algorithm: Theorem 12. Given a linearly defined RMDP ℳM and a parity objective φ : • (ℳ) PI(M) terminates after at most |||||A|^|S| calls to Improve. • (ℳ) PI(M) returns an optimal positional agent policy σ∗σ^* together with the value vector ℳ(φ) v^M( ). • (ℳ) PI(M) runs in polynomial space. The polynomial space requirement is specifically important because the reduction in the proof of Proposition 8 explodes the state-space exponentially. 5 Experimental Results Figure 1: Solve time as a function of the number of states N, with one benchmark per column and one uncertainty norm per row: L1L_1 (a–c) and L∞L_∞ (d–f). Blue solid lines show our algorithm and red dashed lines the baseline; within each color, dark circles mark the reachability objective and light triangles the parity objective (Frozen Lake is reachability-only). Each point is the mean over 1010 random seeds, with error bars and shaded bands giving one standard deviation. The dotted horizontal line is the 120s timeout, and a × marks a timed-out. We implemented our proposed method and conducted a series of experiments to evaluate its performance. The experiments were designed to assess the effectiveness and applicability of our approach for quantitative analysis of both general parity objectives and the special class of reachability objectives. We compare our method against the technique that reduces the RMDP into a stochastic game (as in Appendix F) and solves it using the policy iteration algorithm of (Chatterjee and Henzinger 2006a). The experiments are designed to answer the following research questions: • RQ1: How does our method perform in terms of computational efficiency compared to the baseline approach? • RQ2: How does our method scale with increasing problem size and complexity? • RQ3: What are the limitations of our method, and in what scenarios does it outperform the baseline approach? Experimental Setup. We implemented our approach and the baseline method in Python, and used them to compute the quantitative value of the benchmarks explained next. All experiments were conducted on a machine with an Intel Core Ultra 5 225U processor and 16GB of RAM. We used a timeout of 120 seconds for each experiment. Benchmarks. We conducted experiments on three classes of benchmarks, where the branching factor m denotes the number of possible successors of a state under a fixed action. Garnet and Inventory Management support both objectives, while Frozen Lake supports only reachability. In all cases, the uncertainty sets are L∞L_∞ or L1L_1 balls around the nominal distributions. The benchmarks are summarized as follows (full details are given in Appendix H): • Garnet (adapted from (Archibald et al. 1995)) is a family of randomly generated MDPs. The state-space consists of N states partitioned into k subsets, G0,…,GkG_0,…,G_k. Every state has three available actions, each leading to m=⌈N⌉m= N possible successors. Taking an action from a state in G0G_0 will either lead to a state in G0G_0 or to a state in one of the other subsets, while taking an action from a state in GiG_i for i>0i>0 will lead to a state in GiG_i. The transition probabilities are drawn uniformly at random from the probability simplex. As a reachability objective, each one of the subsets is considered to have a target and an trap state; the goal is to reach the target state of some subset. As a parity objective, each state is assigned a random color and the goal is to satisfy the respective parity condition. • Inventory Management (adapted from (Iyengar 2005)) models a warehouse with capacity N whose state is the stock level. At each step the agent orders new units against an uncertain demand. Specifically, the agent will choose to buy a∈0,…,amaxa∈\0,…,a_ \ new units and the demand d is drawn uniformly from 0,…,dmax\0,…,d_ \. The state will then transition from s to s+a−ds+a-d; if the demand exceeds the available stock (d>s+ad>s+a), or the delivery pushes the stock over the capacity (s+a−d>Ns+a-d>N), the run instead ends in one of two absorbing failure states. We fix dmax=⌈N⌉d_ = N and amax=⌈0.75dmax⌉a_ = 0.75\,d_ . Once the stock reaches a threshold T, a larger order option becomes available. The reachability objective is to reach a stock level above a threshold, while the parity objective is to keep the stock level above a threshold infinitely often. • Frozen Lake (Brockman et al. 2016) is the classic grid world where the agent walks on a k×k× k grid from the top-left cell toward the bottom-right. Each move proceeds in the intended direction or in one of the two perpendicular ones with probability 13 13 each, and a random 20%20\% of the cells are holes, which are absorbing failures. Results. Figure 1 reports the solve times of both algorithms against the state-space size, on a log–log scale; every configuration is grown until each algorithm, in turn, exceeds the 120120-second timeout, marked by a ×. The returned values of both approaches were checked to match on all benchmarks. The picture cleanly separates two regimes, governed by the branching factor m. On Garnet and Inventory Management, where m grows with the instance size, our algorithm scales substantially better than the baseline, across both norms and both objectives (panels a, b, d, e). The baseline’s cost is driven by the number of extreme points of the uncertainty set, which grows rapidly with m: it already exceeds the timeout at a few hundred states, whereas our algorithm keeps solving an order of magnitude larger instances (up to n≈1200n≈ 1200 on Inventory). At the largest sizes where the baseline still completes, our algorithm is faster by roughly one to two orders of magnitude, and this gap widens as the instances grow. Consistent with the extra work of the parity decomposition, parity (light curves) is somewhat more expensive than reachability (dark curves) for both algorithms, so the baseline times out slightly earlier on parity than on reachability. Frozen Lake is the opposite regime (panels c, f). Here the branching factor is fixed at m≤3m≤ 3, so each uncertainty set has only a handful of extreme points and the reduced stochastic game stays close in size to the original RMDP. The baseline therefore has the advantage: it is roughly an order of magnitude faster than our algorithm at matched sizes and scales to far larger grids (beyond n≈104n≈ 10^4), while the overhead of our linear-programming inner solver dominates. These results answer our research questions directly. Our method is the more efficient choice (RQ1) and scales to markedly larger instances (RQ2) precisely when the branching factor m is large, since its per-iteration cost is polynomial in the size of the RMDP rather than in the number of extreme points of the uncertainty sets. Its limitation (RQ3) shows up when m is small: when the uncertainty sets have few extreme points, the reduction to a stochastic game produces a compact game that the baseline solves faster. Finally, we note that the number of iterations both in our approach and the baseline is observed to be smaller than the theoretical worst-case bound, which is exponential in the number of states. This is consistent with the known behavior of policy iteration on stochastic games, where the number of iterations is often observed to be polynomial in practice, despite the worst-case exponential bound. This suggests that the practical performance of our algorithms may be significantly better than the theoretical worst-case analysis would suggest (See Appendix H for details). 6 Conclusion and Future Works In this paper, we study the quantitative parity problem for (s,a)(s,a)-rectangular RMDPs with linearly defined uncertainty sets. We give a polynomial-time algorithm for robust Markov chains, casting robust safety as a linear program over occupation measures and reducing parity to safety through a maximal-end-component analysis, and use it as a subroutine in a policy-iteration algorithm for RMDPs that combines quantitative one-step improvements with qualitative almost-sure improvements, runs in polynomial space, and computes the exact values together with optimal positional policies for both the agent and the environment. The decision problem for linearly defined RMDPs is in ∩NP and as hard as turn-based stochastic parity games. An interesting future question is whether the exact value is computable in polynomial time. Other promising directions are to extend beyond linearly defined sets to nonlinear convex uncertainty, such as ellipsoidal or divergence-based balls, to relax (s,a)(s,a)-rectangularity, and to study the learning setting in which the uncertainty sets are estimated from samples. References Archibald et al. (1995) T. W. Archibald, K. I. McKinnon, and L. C. Thomas On the generation of markov decision processes. Journal of the Operational Research Society 46 (3), p. 354–361. Cited by: 1st item. 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∞L_∞ robust mdps. In Conference on Learning Theory (COLT), Proceedings of Machine Learning Research. Cited by: Appendix A. 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 AAAI, p. 36137–36145. Cited by: Appendix A, §C.2, §C.5, §1, §1, §3.1, §3.2, 2nd item, Remark 42. Baier and Katoen (2008) C. Baier and J. Katoen Principles of model checking. MIT Press. Cited by: Appendix A, Appendix G, §1, §2, §2. Behzadian et al. (2021) B. Behzadian, M. Petrik, and C. P. Ho Fast algorithms for L∞L_∞-constrained s-rectangular robust mdps. Advances in Neural Information Processing Systems 34, p. 25982–25992. Cited by: Appendix A. Bozkurt et al. (2020) A. K. Bozkurt, Y. Wang, M. M. Zavlanos, and M. Pajic Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In 2020 IEEE International Conference on Robotics and Automation (ICRA), p. 10349–10355. Cited by: Appendix A. Brockman et al. (2016) G. Brockman, V. Cheung, L. Pettersson, J. Schneider, J. Schulman, J. Tang, and W. Zaremba OpenAI Gym. Note: arXiv:1606.01540 External Links: 1606.01540 Cited by: 3rd item. Chatterjee et al. (2024) K. Chatterjee, E. K. Goharshady, M. Karrabi, P. Novotný, and Đ. Žikelić Solving long-run average reward robust MDPs via stochastic games. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, p. 6707–6715. External Links: Document Cited by: Appendix A, §4. Chatterjee and Henzinger (2014) K. Chatterjee and M. Henzinger Efficient and dynamic algorithms for alternating büchi games and maximal end-component decomposition. Journal of the ACM 61 (3), p. 15:1–15:40. External Links: Document Cited by: §3.2. Chatterjee and Henzinger (2006a) K. Chatterjee and T. A. Henzinger Strategy improvement and randomized subexponential algorithms for stochastic parity games. In STACS 2006 – 23rd Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, Vol. 3884, p. 512–523. Cited by: Appendix A, §F.5, §1, §5. Chatterjee and Henzinger (2006b) K. Chatterjee and T. A. Henzinger Strategy improvement for stochastic rabin and streett games. In CONCUR 2006 – Concurrency Theory, Lecture Notes in Computer Science, Vol. 4137, p. 375–389. Cited by: Appendix A, §1. Chatterjee and Henzinger (2012) K. Chatterjee and T. A. Henzinger A survey of stochastic ω-regular games. Journal of Computer and System Sciences 78 (2), p. 394–413. Cited by: Appendix A, §F.4, §F.5. 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. Cited by: Appendix A. Hahn et al. (2019) E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak Omega-regular objectives in model-free reinforcement learning. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, Vol. 11427, p. 395–412. Cited by: Appendix A. Ho et al. (2021) C. P. Ho, M. Petrik, and W. Wiesemann Partial policy iteration for l1-robust markov decision processes. Journal of Machine Learning Research 22 (275), p. 1–46. Cited by: Appendix A. Iyengar (2005) G. N. Iyengar Robust dynamic programming. Mathematics of Operations Research 30 (2), p. 257–280. Cited by: Appendix A, §1, 2nd item. Kaufman and Schaefer (2013) D. L. Kaufman and A. J. Schaefer Robust modified policy iteration. INFORMS J. Comput. 25 (3), p. 396–410. Cited by: Appendix A. Moos et al. (2022) J. Moos, K. Hansel, H. Abdulsamad, S. Stark, D. Clever, and J. Peters Robust reinforcement learning: a review of foundations and recent advances. Machine Learning and Knowledge Extraction 4 (1), p. 276–315. Cited by: Appendix A. Nilim and El Ghaoui (2005) A. Nilim and L. El Ghaoui Robust control of markov decision processes with uncertain transition matrices. Operations Research 53 (5), p. 780–798. Cited by: Appendix A, §1. Parys (2019) P. Parys Parity games: zielonka’s algorithm in quasi-polynomial time. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 138, p. 10:1–10:13. Cited by: Appendix A. Pinto et al. (2017) L. Pinto, J. Davidson, R. Sukthankar, and A. Gupta Robust adversarial reinforcement learning. In Proceedings of the 34th International Conference on Machine Learning (ICML), Proceedings of Machine Learning Research, Vol. 70, p. 2817–2826. Cited by: Appendix A. Puterman (1994) M. L. Puterman Markov decision processes: discrete stochastic dynamic programming. Wiley Series in Probability and Statistics, Wiley. Cited by: §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. arXiv preprint arXiv:2411.11451. Cited by: Appendix A. 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), Lecture Notes in Computer Science, Vol. 4539, p. 263–277. Cited by: Appendix A. Wang et al. (2023) Y. Wang, A. Velasquez, G. K. Atia, A. Prater-Bennette, and S. Zou Robust average-reward markov decision processes. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 37, p. 15215–15223. Cited by: Appendix A. Wang and Zou (2021) Y. Wang and S. Zou Online robust reinforcement learning with model uncertainty. In Advances in Neural Information Processing Systems (NeurIPS), Vol. 34. Cited by: Appendix A. Wiesemann et al. (2013) W. Wiesemann, D. Kuhn, and B. Rustem Robust markov decision processes. Mathematics of Operations Research 38 (1), p. 153–183. Cited by: Appendix A, §1. Wolff et al. (2012) E. M. Wolff, U. Topcu, and R. M. Murray Robust control of uncertain markov decision processes with temporal logic specifications. In 2012 IEEE 51st IEEE Conference on Decision and Control (CDC), p. 3372–3379. External Links: Document Cited by: Appendix A. Zielonka (1998) W. Zielonka Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200 (1-2), p. 135–183. Cited by: Appendix A. Appendix A Related Work Robust MDPs. RMDPs were introduced for sequential decision making under uncertain transition probabilities, with the foundational works of (Iyengar 2005; Nilim and El Ghaoui 2005) establishing robust dynamic programming for rectangular uncertainty. We refer to Suilen et al. (2024) for a recent survey. Subsequent works studied general robust policy-iteration methods (Wiesemann et al. 2013; Kaufman and Schaefer 2013), as well as faster algorithms for specific uncertainty classes such as L1L_1 and L∞L_∞ (Ho et al. 2021; Behzadian et al. 2021). Recent works study exact computation and the complexity of policy iteration for discounted RMDPs (Asadi et al. 2026a), while others consider the average-reward and bounded-parameter settings (Wang et al. 2023; Chatterjee et al. 2024; Tewari and Bartlett 2007; Givan et al. 2000). All of these results consider quantitative objectives such as discounted-sum, average reward, and finite horizon, whereas our focus is logical objectives. Parity Objectives and Strategy Improvement. Parity objectives and their quantitative analysis have been studied extensively for MDPs and two-player stochastic games. We refer to Baier and Katoen (2008); Chatterjee and Henzinger (2012) for an overview, and to Zielonka (1998); Parys (2019) for algorithms solving parity games. Our policy-iteration algorithm is, in spirit, close to the strategy-improvement paradigm for stochastic parity and Rabin games (Chatterjee and Henzinger 2006a; Chatterjee and Henzinger 2006b), which likewise iterates over positional strategies and alternates value improvements with qualitative sub-computations. The essential difference is that in our robust setting the environment ranges over a continuum of distributions in an uncertainty polytope rather than over the finitely many vertices of a stochastic game. Our improvement therefore works directly with the linearly defined uncertainty sets, through the value classes, tight actions, and tight faces of Section 4, and never constructs the exponentially larger game. Logical Objectives on Uncertain MDPs. The closest prior work considers temporal-logic control of uncertain MDPs under a constant-support assumption and approximates satisfaction probabilities using value iteration (Wolff et al. 2012). Asadi et al. (2026b) remove structural assumptions and solve the positive and almost-sure reachability and parity problems using uncertainty-set oracles. Our qualitative improvement step invokes their almost-sure parity procedure as a sub-routine, whereas the exact quantitative problem we solve here remained open. Reinforcement Learning. RMDPs are the model underlying robust reinforcement learning, where the goal is to learn policies that hedge against misspecification of the transition model. Adversarial and model-uncertainty formulations optimize the worst-case return over an uncertainty set (Pinto et al. 2017; Wang and Zou 2021), and we refer to Moos et al. (2022) for a survey. This line targets quantitative reward objectives, whereas we compute exact values of ω-regular objectives. Orthogonally, a body of work learns policies for ω-regular and temporal-logic objectives in the non-robust setting, typically by reducing the objective to a reachability reward on a product with an automaton (Hahn et al. 2019; Bozkurt et al. 2020). Our setting combines the two axes: exact quantitative analysis of ω-regular objectives against adversarial transition uncertainty. Appendix B Linear Descriptions of L∞L_∞ and L1L_1 Uncertainty Sets Recall the Assumption of Section 3: the uncertainty set of each state s is a polytope (s)=p∈Δ():Asp≤bsP(s)=\p∈ (S):A_s\,p≤ b_s\. Here we show that the two most common uncertainty models, the L∞L_∞ and L1L_1 balls around a nominal distribution, fit this form (the L1L_1 case after introducing auxiliary variables). Fix a state s with nominal distribution p^s∈Δ() p_s∈ (S) and radius δs≥0 _s≥ 0; write p^s,s′ p_s,s for the nominal probability of the successor s′s . L∞L_∞ ball. The set (s)=p∈Δ():‖p−p^s‖∞≤δsP(s)= \\,p∈ (S):\|p- p_s\|_∞≤ _s\, \ is cut out, with no auxiliary variables, by the box constraints −δs≤ps′−p^s,s′≤δsfor every s′∈,- _s\;≤\;p_s - p_s,s \;≤\; _s every s , i.e. ps′≤p^s,s′+δsp_s ≤ p_s,s + _s and −ps′≤δs−p^s,s′-p_s ≤ _s- p_s,s . Stacking these 2||2|S| inequalities gives As=[I−I]A_s= [ smallmatrixI\\ -I smallmatrix ] and bs=[p^s+δs−p^s+δs]b_s= [ smallmatrix p_s+ _s1\\ - p_s+ _s1 smallmatrix ], so (s)=p∈Δ():Asp≤bsP(s)=\p∈ (S):A_s\,p≤ b_s\ exactly as in the Assumption. L1L_1 ball. The set (s)=p∈Δ():‖p−p^s‖1≤δs=p∈Δ():∑s′∈|ps′−p^s,s′|≤δsP(s)= \\,p∈ (S):\|p- p_s\|_1≤ _s\, \= \\,p∈ (S): _s |p_s - p_s,s |≤ _s\, \ has, in general, exponentially many facets, but it becomes linear after introducing one auxiliary variable ys′y_s per successor to model |ps′−p^s,s′||p_s - p_s,s |: ys′≥ps′−p^s,s′,ys′≥p^s,s′−ps′,(s′∈),∑s′∈ys′≤δs.y_s ≥ p_s - p_s,s , y_s ≥ p_s,s -p_s , (s ), _s y_s ≤ _s. At an optimum each ys′y_s equals |ps′−p^s,s′||p_s - p_s,s |, so the projection onto the p-coordinates of the polytope defined by these 2||+12|S|+1 inequalities (over the 2||2|S| variables (p,y)(p,y)) is exactly the L1L_1 ball. Writing the constraints as As[py]≤bsA_s [ smallmatrixp\\ y smallmatrix ]≤ b_s presents (s)P(s) as the projection of a polytope, using only a linear number of auxiliary variables and inequalities. Extending the LP to auxiliary variables. The L1L_1 description uses auxiliary variables, so (s)P(s) is a projected polytope rather than the plain form p:Asp≤bs\p:A_sp≤ b_s\. The program (⋆)( ) and its correctness extend to this case without change. Indeed, the linearisation of Lemma 16 rewrites the admissibility constraint p∈(s)p (s), with p=s/xsp= f_s/x_s, by multiplying through by xs≥0x_s≥ 0; applying the same scaling to the auxiliary variables (replacing y by y′=xsy =x_s\,y) turns As[py]≤bsA_s [ smallmatrixp\\ y smallmatrix ]≤ b_s into the linear constraint As[sy′]≤xsbsA_s [ smallmatrix f_s\\ y smallmatrix ]≤ x_s\,b_s over the flow and (scaled) auxiliary variables. Thus, for L∞L_∞, L1L_1, and general (possibly projected) polytopes alike, the value sℛ(()) v^R_s( Safe(T)) is computed by a single polynomial-size linear program, and Lemma 2 applies uniformly. Appendix C Proofs of Lemma 2 and Theorem 3 Throughout this section we fix a linearly defined RMC ℛ=(,)R=(S,P) with, for every s∈s , (s)=p∈Δ():Asp≤bsP(s)=\p∈ (S):A_s\,p≤ b_s\, a safe set ⊆T , and an initial state s0s_0. A positional environment policy is a map τ:→Δ()τ → (S) with τ(s)∈(s)τ(s) (s) for all s; we write ps,s′τ=τ(s)(s′)p^τ_s,s =τ(s)(s ) for its one-step probabilities. Since an RMC has a single action, the safety value from Section 3.1 is sℛ(())=infτPrsτ[()], v^R_s( Safe(T))= _τ ^τ_s[ Safe(T)], the infimum ranging over all environment policies. The preprocessing computes the sets =1=s∈:sℛ(())=1,=0=s∈:sℛ(())=0,?=∖(=0∪=1),S^=1=\\,s : v^R_s( Safe(T))=1\,\, ^=0=\\,s : v^R_s( Safe(T))=0\,\, ^?=S (S^=0 ^=1), and makes the states of =0∪=1S^=0 ^=1 absorbing sinks. Every unsafe state (outside T) has safety value 00, so ∖⊆=0S ^=0 and hence ?⊆S^? . We prove that for s0∈?s_0 ^? the optimum of (⋆)( ) equals s0ℛ(()) v^R_s_0( Safe(T)); for s0∈=1s_0 ^=1 (resp. =0S^=0) the value is 11 (resp. 00) by definition. A reachability objective (T) Reach(T) specifies the set of all runs that reach a state in T eventually, i.e. (T)=π∈ω|∃i:πi∈T Reach(T)=\π ^ω|∃ i: _i∈ T\ C.1 Occupation Measures Definition 13 (Expected visits and flows). Fix a positional environment policy τ. For s,s′∈s,s , the expected number of visits to s and the expected flow along (s,s′)(s,s ), both from s0s_0, are xsτ=∑t=0∞Prs0τ[st=s],fs,s′τ=∑t=0∞Prs0τ[st=s,st+1=s′].x_s^τ= _t=0^∞ ^τ_s_0[s_t=s], f_s,s ^τ= _t=0^∞ ^τ_s_0[s_t=s,\,s_t+1=s ]. By the Markov property of a positional τ, Prs0τ[st=s,st+1=s′]=ps,s′τPrs0τ[st=s] ^τ_s_0[s_t=s,\,s_t+1=s ]=p^τ_s,s \, ^τ_s_0[s_t=s]; summing over t gives the factorisation fs,s′τ=xsτps,s′τ,hence∑s′∈fs,s′τ=xsτwhenever xsτ<∞.f_s,s ^τ=x_s^τ\,p_s,s ^τ, _s f_s,s ^τ=x_s^τ x_s^τ<∞. (1) Whenever xsτ<∞x_s^τ<∞ for all s∈?s ^?, conditioning on the state at time t−1t-1 and summing gives Cons, and Split is the second identity in (1); together with NNeg (immediate) the pair (xτ,fτ)(x^τ,f^τ) then satisfies the constraints of (⋆)( ) by Lemma 16. Moreover, since =1S^=1 is absorbing, a play crosses from ?S^? into =1S^=1 at most once and exactly when it reaches =1S^=1, so the objective of (⋆)( ) evaluated at this occupation is ∑s∈?,w∈=1fs,wτ=Prs0τ[(=1)]. _s ^?,\,w ^=1f_s,w^τ= ^τ_s_0[ Reach(S^=1)]. (2) C.2 Correctness of the Preprocessing Lemma 14 (Qualitative preprocessing). The sets =1S^=1 and =0S^=0 are computable in polynomial time, and making states in =0S^=0 unsafe absorbing and states in =1S^=1 safe absorbing does not change the safety value of any state in ?S^?. Proof. The qualitative sets =1S^=1 and =0S^=0 are computable in polynomial time by (Asadi et al. 2026b). From a state of =1S^=1 the play is safe under every policy, and from a state of =0S^=0 some policy is unsafe almost surely; making these states absorbing therefore only relabels play that has already committed to value 11 or 00, and does not change any safety value. ∎ Lemma 15. Let τ⋆τ be a positional environment policy attaining s0ℛ(()) v^R_s_0( Safe(T)). Then from s0∈?s_0 ^? the play reaches =0∪=1S^=0 ^=1 almost surely; consequently xsτ⋆<∞x_s^τ <∞ for every s∈?s ^?, and under τ⋆τ a play is safe if and only if it reaches =1S^=1, so that Prs0τ⋆[()]=Prs0τ⋆[(=1)] ^τ _s_0[ Safe(T)]= ^τ _s_0[ Reach(S^=1)]. Proof. Suppose the induced Markov chain has a BSCC B reachable from s0s_0 with B⊆?B ^?. Since ?⊆S^? and B is a BSCC, the play from any u∈Bu∈ B stays in B⊆B forever and is therefore safe with probability 11. Fix such a u. As u∈?u ^?, we have uℛ(())<1 v^R_u( Safe(T))<1, so some policy τ′τ is unsafe from u with positive probability. Consider the policy that follows τ⋆τ until u is first visited and then switches to τ′τ . Since =0∪=1S^=0 ^=1 is absorbing, u is reached from s0s_0 with some probability q>0q>0 along a path inside ?⊆S^? , and under τ⋆τ these are exactly the safe plays that visit u; replacing their safe continuation by τ′τ hence lowers the safety probability from s0s_0 strictly below Prs0τ⋆[()] ^τ _s_0[ Safe(T)], contradicting the optimality of τ⋆τ at s0s_0. Hence every BSCC reachable from s0s_0 meets =0∪=1S^=0 ^=1, so the play reaches =0∪=1S^=0 ^=1 almost surely, the hitting time τ has finite expectation, and xsτ⋆≤s0τ⋆[τ]<∞x_s^τ ^τ _s_0[τ]<∞ for every s∈?s ^?. Finally, once absorbed in =1S^=1 the play is safe, whereas from =0S^=0 the optimal τ⋆τ is unsafe almost surely; hence, under τ⋆τ , being safe coincides with reaching =1S^=1, giving Prs0τ⋆[()]=Prs0τ⋆[(=1)] ^τ _s_0[ Safe(T)]= ^τ _s_0[ Reach(S^=1)]. ∎ C.3 Linearization of the Uncertainty Lemma 16. Fix s∈?s ^?, a scalar xs≥0x_s≥ 0, and a vector s=(fs,s′)s′∈ f_s=(f_s,s )_s . The constraints s≥0 f_s≥ 0, ∑s′∈fs,s′=xs _s f_s,s =x_s, and Ass≤xsbsA_s\, f_s≤ x_s\,b_s hold if and only if there exists p∈(s)p (s) with s=xsp f_s=x_s\,p. Proof. (⇐ ) Given p∈(s)p (s) with s=xsp f_s=x_s\,p: non-negativity and ∑s′fs,s′=xs∑s′ps′=xs _s f_s,s =x_s _s p_s =x_s follow from p∈Δ()p∈ (S), and multiplying Asp≤bsA_s\,p≤ b_s by xs≥0x_s≥ 0 gives Ass≤xsbsA_s\, f_s≤ x_s\,b_s. (⇒ ) If xs>0x_s>0, set p=s/xsp= f_s/x_s. Then p≥0p≥ 0, ∑s′ps′=1 _s p_s =1, so p∈Δ()p∈ (S); dividing Ass≤xsbsA_s\, f_s≤ x_s\,b_s by xsx_s gives Asp≤bsA_s\,p≤ b_s, hence p∈(s)p (s) and s=xsp f_s=x_s\,p. If xs=0x_s=0, then s≥0 f_s≥ 0 and ∑s′fs,s′=0 _s f_s,s =0 force s=0=xsp f_s=0=x_s\,p for any p∈(s)p (s), and (s)≠∅P(s)≠ . ∎ In particular, ∧ Split NNeg Adm at a state s∈?s ^? holds exactly when the outgoing flow is s=xsp f_s=x_s\,p for some admissible distribution p∈(s)p (s). C.4 Proof of Lemma 2 Proof of Lemma 2. Fix s0∈?s_0 ^?. We show that the optimum of (⋆)( ) equals s0ℛ(()) v^R_s_0( Safe(T)), via two inequalities. The optimum is at most the value. Let τ⋆τ be an optimal positional policy; by Lemma 15 it has finite occupation. By (1) and Lemma 16, the occupation (xτ⋆,fτ⋆)(x^τ ,f^τ ) satisfies ∧ NNeg Cons Split Adm, so it is feasible for (⋆)( ). By (2) and Lemma 15, its objective is Prs0τ⋆[(=1)]=Prs0τ⋆[()]=s0ℛ(()) ^τ _s_0[ Reach(S^=1)]= ^τ _s_0[ Safe(T)]= v^R_s_0( Safe(T)). Since (⋆)( ) minimises, its optimum is at most the value. The value is at most the optimum. Let (x⋆,f⋆)(x ,f ) be any feasible solution of (⋆)( ). Define a positional environment policy τ∘τ by τ∘(s)=s⋆/xs⋆if s∈? and xs⋆>0,p†∈(s) (arbitrary)otherwise.τ (s)= cases f _s/x _s&if s ^? and x _s>0,\\ p (s) (arbitrary)&otherwise. cases By Lemma 16, τ∘(s)∈(s)τ (s) (s), so τ∘τ is a valid positional policy, and xs⋆ps,s′τ∘=fs,s′⋆x _s\,p^τ _s,s =f _s,s for all s∈?s ^? (both sides vanish when xs⋆=0x _s=0, as then s⋆=0 f _s=0). We show xsτ∘≤xs⋆x^τ _s≤ x _s for every s∈?s ^? by proving xsτ∘,N≤xs⋆x^τ ,N_s≤ x _s for the truncated occupation xsτ∘,N=∑t=0NPrs0τ∘[st=s]x^τ ,N_s= _t=0^N ^τ _s_0[s_t=s], by induction on N. For N=0N=0, xsτ∘,0=[s=s0]≤xs⋆x^τ ,0_s=1[s=s_0]≤ x _s by Cons and f⋆≥0f ≥ 0; and the inductive step uses xs′⋆ps′,sτ∘=fs′,s⋆x _s p^τ _s ,s=f _s ,s and Cons, xsτ∘,N=[s=s0]+∑s′∈?xs′τ∘,N−1ps′,sτ∘≤[s=s0]+∑s′∈?fs′,s⋆=xs⋆.x^τ ,N_s=1[s=s_0]+ _s ^?x^τ ,N-1_s \,p^τ _s ,s 1[s=s_0]+ _s ^?f _s ,s=x _s. Letting N→∞N→∞ gives xsτ∘≤xs⋆<∞x^τ _s≤ x _s<∞; in particular τ∘τ has finite occupation, so it reaches =0∪=1S^=0 ^=1 almost surely from s0s_0. Using (2), xsτ∘≤xs⋆x^τ _s≤ x _s, and xs⋆ps,wτ∘=fs,w⋆x _sp^τ _s,w=f _s,w, Prs0τ∘[(=1)]=∑s∈?w∈=1xsτ∘ps,wτ∘≤∑s∈?w∈=1xs⋆ps,wτ∘=∑s∈?w∈=1fs,w⋆. ^τ _s_0[ Reach(S^=1)]= _ subarraycs ^?\\ w ^=1 subarrayx^τ _s\,p^τ _s,w≤ _ subarraycs ^?\\ w ^=1 subarrayx _s\,p^τ _s,w= _ subarraycs ^?\\ w ^=1 subarrayf _s,w. (3) It remains to bound the safety value by Prs0τ∘[(=1)] ^τ _s_0[ Reach(S^=1)]. Consider the policy τ τ that follows τ∘τ until the play first reaches =0∪=1S^=0 ^=1 (which happens almost surely), then, from a state of =1S^=1, plays to stay safe (possible, since safety value 11 means safe under every policy), and from a state of =0S^=0, plays an unsafe-almost-surely continuation (possible, since safety value 00). Then a τ τ-play is safe exactly when it is absorbed in =1S^=1, so s0ℛ(())≤Prs0τ^[()]=Prs0τ∘[(=1)]≤∑s∈?w∈=1fs,w⋆, v^R_s_0( Safe(T))\;≤\; τ_s_0[ Safe(T)]\;=\; ^τ _s_0[ Reach(S^=1)]\;≤\; _ subarraycs ^?\\ w ^=1 subarrayf _s,w, using (3). As this holds for every feasible solution, the value is at most the optimum of (⋆)( ). Combining the two inequalities, the optimum of (⋆)( ) equals s0ℛ(()) v^R_s_0( Safe(T)). ∎ C.5 Proof of Theorem 3 Proof of Theorem 3. The sets =1,=0S^=1,S^=0 are computable in polynomial time (Asadi et al. 2026b). The program (⋆)( ) has O(||2)O(|S|^2) variables and, by the Assumption, a number of constraints polynomial in the encoding of ℛR, and linear programs of polynomial size are solvable in polynomial time. States in =1S^=1 and =0S^=0 have known safety values 11 and 00; for the remaining states, solving (⋆)( ) once per source s0∈?s_0 ^? yields all values sℛ(()) v^R_s( Safe(T)) and, corresponding optimal positional policies, all in polynomial time. ∎ Appendix D MecDecomp Procedure for Computing MEC Decompositions of RMCs Throughout, fix an RMC ℛ=(,)R=(S,P) with linearly defined uncertainty. We recall the notion of maximal end-component from Definition 4 and give the MecDecomp procedure that computes them; its correctness is established in Theorem 18. Internal transitions. For a set B⊆B and a state s∈Bs∈ B, let B(s)=p∈(s):(p)⊆BP_B(s)\;=\;\\,p (s)\;:\; supp(p) B\,\ be the set of admissible distributions at s whose support stays inside B, i.e. the one-step choices with which the environment can keep the play within B. We say B is closed if B(s)≠∅P_B(s)≠ for every s∈Bs∈ B; equivalently, from every state of B the environment has at least one distribution that does not leave B. The internal transition graph of B is the directed graph GB=(B,EB)G_B=(B,E_B) whose edges record the transitions the environment can take while remaining in B, EB=(s,s′)∈B×B:∃p∈B(s),ps′>0.E_B\;=\;\\,(s,s )∈ B× B\;:\;∃\,p _B(s),\ p_s >0\,\. This is exactly the notation of Definition 4: the end-components of ℛR are the non-empty closed sets B whose internal transition graph GBG_B is strongly connected, and a maximal end-component (MEC) is an end-component that is not strictly contained in another. Algorithm. Algorithm 4 computes the MEC decomposition of ℛR. Following the standard MDP procedure, it repeatedly closes a candidate set B by discarding every state from which the environment cannot avoid leaving B, and then splits the closed set into the strongly connected components of GBG_B, recursing on each proper component. Both operations reduce to polynomially many linear-programming queries against the description of P. Algorithm 4 (B) MecDecomp(B): MEC decomposition of an RMC 0: A subset B⊆B of an RMC ℛR with linearly defined uncertainty; the top-level call uses B=B=S. 0: The set of MECs contained in B. 1: repeat 2: ←s∈B:B(s)=∅ Leak←\\,s∈ B\;:\;P_B(s)= \,\ 3: B←B∖B← B Leak 4: until =∅ Leak= 5: if B=∅B= then 6: return ∅ 7: end if 8: Compute the edge set EBE_B and the SCCs C1,…,CkC_1,…,C_k of GBG_B 9: if k=1k=1 then 10: return B\B\ B is a MEC 11: end if 12: ←∅ Result← 13: for i=1,…,ki=1,…,k do 14: ←∪(Ci) Result← Result∪ MecDecomp(C_i) 15: end for 16: return Result LP primitives. The two operations on P are realised as linear programs: • Closure test B(s)≠∅P_B(s)≠ . Add the equalities ps′=0p_s =0 for every s′∉Bs ∉ B to the linear description Asp≤bsA_s\,p≤ b_s of (s)P(s) and test feasibility over the simplex; the set B(s)P_B(s) is non-empty iff this program is feasible. • Edges of GBG_B. For each ordered pair (s,s′)∈B×B(s,s )∈ B× B, maximise ps′p_s subject to p∈B(s)p _B(s); the edge (s,s′)(s,s ) belongs to EBE_B iff the optimum is strictly positive. The strongly connected components of GBG_B are then computed by Tarjan’s algorithm in time linear in |B|+|EB||B|+|E_B|. Lemma 17. The maximal end-components of ℛR are pairwise disjoint. Proof. Let M1,M2M_1,M_2 be MECs with a common state s∈M1∩M2s∈ M_1∩ M_2; we show that M1∪M2M_1∪ M_2 is an end-component, which, since two distinct MECs cannot contain one another, strictly contains M1M_1 and contradicts its maximality. For closure, take any s′∈M1∪M2s ∈ M_1∪ M_2, say s′∈Mis ∈ M_i. As MiM_i is closed, Mi(s′)≠∅P_M_i(s )≠ ; and since Mi⊆M1∪M2M_i M_1∪ M_2, a distribution supported in MiM_i is also supported in M1∪M2M_1∪ M_2, so Mi(s′)⊆M1∪M2(s′)P_M_i(s ) _M_1∪ M_2(s ) and the latter is non-empty. For strong connectivity of GM1∪M2G_M_1∪ M_2, note that relaxing the support constraint from ⊆Mi M_i to ⊆M1∪M2 M_1∪ M_2 only adds edges, so GMiG_M_i is a subgraph of GM1∪M2G_M_1∪ M_2 restricted to MiM_i; hence each MiM_i is internally strongly connected in GM1∪M2G_M_1∪ M_2, and the shared state s links the two parts, making M1∪M2M_1∪ M_2 strongly connected. Thus M1∪M2M_1∪ M_2 is an end-component. ∎ Theorem 18. Algorithm 4 returns the set of maximal end-components of ℛR, using O(||3)O(|S|^3) linear-programming queries each of size polynomial in the encoding of ℛR, and hence runs in polynomial time. Moreover, a single invocation (B) MecDecomp(B), excluding the work of its recursive calls, performs O(|B|2)O(|B|^2) linear-programming queries. Proof. We first argue correctness and then bound the number of LP queries. Both parts rely on the invariant that at every call (B) MecDecomp(B), every MEC of ℛR that intersects B is contained in B. The invariant holds for the top-level call with B=B=S, since every MEC intersects S and is contained in it. Closure preserves end-components. The closure loop removes a state s from B only when B(s)=∅P_B(s)= . Let E be any end-component with E⊆BE B and s∈Es∈ E. Since E is closed, E(s)≠∅P_E(s)≠ , and E(s)⊆B(s)P_E(s) _B(s) because E⊆BE B; hence B(s)≠∅P_B(s)≠ and s is not removed. Therefore every end-component contained in B survives the closure loop. Let B⋆B be the closed set obtained when the loop terminates. Every end-component lies in a single SCC of GB⋆G_B . For an end-component E⊆B⋆E B , the support condition (p)⊆E supp(p) E is stronger than (p)⊆B⋆ supp(p) B , so GEG_E is a subgraph of GB⋆G_B restricted to E. Hence E is strongly connected inside GB⋆G_B and is contained in a single strongly connected component. Base case: one SCC. Suppose GB⋆G_B is strongly connected (a single SCC). Then B⋆B is non-empty, closed, and strongly connected, so it is an end-component. By Lemma 17 it lies in a unique MEC M of ℛR; since M intersects B, the invariant gives M⊆BM B, and M survives the closure loop, so M⊆B⋆M B . Combined with B⋆⊆MB M (as B⋆B is an end-component contained in the MEC M), we get B⋆=MB =M. Thus the algorithm correctly returns the single MEC B⋆\B \. Recursive case: several SCCs. If GB⋆G_B has SCCs C1,…,CkC_1,…,C_k with k≥2k≥ 2, then by the previous paragraph every end-component inside B⋆B lies in some CiC_i, and the algorithm recurses on each CiC_i. The invariant is maintained for each recursive call: any MEC M intersecting CiC_i also intersects B, so M⊆BM B by the parent invariant, M⊆B⋆M B by closure, and M⊆CiM C_i since it lies in a single SCC. By induction on the recursion, the calls collectively return exactly the MECs of ℛR contained in B; for the top-level call B=B=S this is the full MEC decomposition. Complexity. A single call, excluding its recursive calls, performs O(|B|2)O(|B|^2) LP queries: the closure loop runs at most |B||B| rounds, each testing the |B||B| feasibility programs B(s)≠∅P_B(s)≠ , and building GBG_B uses one maximisation LP per ordered pair in B×B× B; the SCC computation is linear in |B|+|EB||B|+|E_B| and uses no LPs. This is the second claim of the statement. We bound the total by counting the recursion level by level. There are at most |||S| levels, because each child CiC_i is a proper subset of its parent: Ci⊆B⋆⊆BC_i B B, and recursion happens only when B⋆B splits into k≥2k≥ 2 SCCs. The sets processed at any fixed level are pairwise disjoint, since the children of a node are the pairwise-disjoint SCCs of B⋆B and children of distinct nodes stay inside the disjoint sets of their parents. Hence each level costs at most ∑B at that levelO(|B|2)≤O((∑B|B|)2)=O(||2) _B at that levelO(|B|^2)≤ O ( ( _B|B| )^2 )=O(|S|^2) LP queries, and the at most |||S| levels cost O(||3)O(|S|^3) in total. Each query is a linear program of size polynomial in the encoding of ℛR and is solvable in polynomial time, so the whole algorithm runs in polynomial time. ∎ Appendix E Proofs of Lemmas 5 and 6 Throughout this section we fix a linearly defined RMC ℛ=(,)R=(S,P), a coloring C:→[d]C →[d], and an initial state s0s_0. Recall from Section 3.2 that a play π violates (C) Parity(C) exactly when its dominant color maxC(s):s∈(π) \C(s):s∈ Inf(π)\ is odd, and write Wodd=()W_odd= OddEC(S) for the output of Algorithm 1; the internal transition graph GBG_B and the restricted uncertainty sets BP_B are those of Appendix D. The proofs rest on two properties of WoddW_odd: the environment can confine a play to it while forcing an odd dominant color (Lemma 19), and every violating play must reach it (Lemma 20). Lemma 19 (Confinement). Every end-component E of ℛR whose dominant color maxs∈EC(s) _s∈ EC(s) is odd satisfies E⊆WoddE W_odd. Moreover, there is a positional environment policy τstay _stay under which WoddW_odd is closed and, from every s∈Wodds∈ W_odd, the dominant color visited infinitely often is odd almost surely. Proof. First part. We show E⊆WoddE W_odd by induction on the recursion depth of the call (B) OddEC(B) that first has E⊆BE B (the top-level call has B=⊇EB=S E). Since E is an end-component contained in B and MECs are maximal, E is contained in some MEC MiM_i of B computed by (B) MecDecomp(B). Let mi=maxs∈MiC(s)m_i= _s∈ M_iC(s). If mim_i is odd, the algorithm adds MiM_i to its output, so E⊆Mi⊆WoddE M_i W_odd. If mim_i is even, then, as E⊆MiE M_i, its dominant color satisfies maxs∈EC(s)≤mi _s∈ EC(s)≤ m_i; being odd it cannot equal the even mim_i, so maxs∈EC(s)<mi _s∈ EC(s)<m_i and no state of E has color mim_i. Hence E∩Ui=∅E∩ U_i= for Ui=s∈Mi:C(s)=miU_i=\s∈ M_i:C(s)=m_i\, i.e. E⊆Mi∖UiE M_i U_i, and the algorithm recurses on Mi∖UiM_i U_i at strictly greater depth; the inductive hypothesis gives E⊆WoddE W_odd. Second part. Each set added to the output is a MEC MiM_i (of some subset B) with odd dominant color mim_i; such an MiM_i is an end-component of ℛR, since every s∈Mis∈ M_i admits p∈Mi(s)⊆(s)p _M_i(s) (s) with (p)⊆Mi supp(p) M_i. Fix any such MiM_i. Its internal transition graph GMiG_M_i is strongly connected, and for each s∈Mis∈ M_i the convexity of (s)P(s) lets us average the distributions witnessing the outgoing GMiG_M_i-edges of s into a single τstay(s)∈(s) _stay(s) (s) with (τstay(s))⊆Mi supp( _stay(s)) M_i that covers all GMiG_M_i-successors of s. Under τstay _stay the set MiM_i is thus closed and strongly connected, hence a single BSCC, so a play started anywhere in MiM_i visits every state of MiM_i infinitely often almost surely; its dominant color is therefore mim_i, which is odd. As WoddW_odd is the disjoint union of these MECs, defining τstay _stay componentwise makes WoddW_odd closed with the stated property. ∎ Lemma 20 (Reaching WoddW_odd). For every positional environment policy τ, Prs0τ[¬(C)]≤Prs0τ[(Wodd)]. ^τ_s_0[ \, Parity(C)]\;≤\; ^τ_s_0[ Reach(W_odd)]. Proof. Fix a positional τ. The Markov chain it induces from s0s_0 reaches a bottom strongly connected component (BSCC) almost surely. Any such BSCC C is closed under τ and strongly connected, and each s∈Cs∈ C has τ(s)∈(s)τ(s) (s) with (τ(s))⊆C supp(τ(s)) C, so C is an end-component of ℛR. On the event ¬(C) \, Parity(C) the play visits exactly the states of its BSCC infinitely often, i.e. (π)=C Inf(π)=C, and its dominant color maxs∈CC(s) _s∈ CC(s) is odd; by Lemma 19 this forces C⊆WoddC W_odd, so the play reaches WoddW_odd. Hence ¬(C)⊆(Wodd) \, Parity(C) Reach(W_odd) up to a null set, giving the inequality. ∎ Proof of Lemma 5. By the first part of Lemma 19, the output Wodd=()W_odd= OddEC(S) contains every end-component with an odd dominant color; conversely, by construction it is a union of MECs MiM_i with odd dominant color mim_i, each an end-component of ℛR. Thus WoddW_odd is exactly the set of states lying in an end-component whose dominant color is odd, and by the second part of the lemma the environment forces an odd dominant color almost surely from every state of WoddW_odd via τstay _stay, so each such state has parity value 00, as required. For the complexity, we count the LP queries of the top-level call () OddEC(S) level by level, over the two nested recursions of OddEC and MecDecomp at once. This is the right way to account for them: OddEC calls MecDecomp afresh at every node of its own recursion, so composing the two bounds as black boxes (O(|B|3)O(|B|^3) queries per MEC decomposition, times an OddEC recursion of depth Ω(||) (|S|)) would give only O(||4)O(|S|^4). But the cubic factor of Theorem 18 is not the cost of one MEC decomposition: a single invocation of (B) MecDecomp(B) costs only O(|B|2)O(|B|^2) queries, the extra factor |||S| being itself the number of levels of MecDecomp’s recursion. Counting the levels of the two recursions together therefore adds these factors instead of multiplying them. So consider the combined recursion, whose nodes are all the invocations of MecDecomp made during () OddEC(S), each labelled by the set B it is invoked on. A node (B) MecDecomp(B) has as children either the invocations (C1),…,(Ck) MecDecomp(C_1),…, MecDecomp(C_k) on the SCCs of B⋆B , or, if (B) MecDecomp(B) returns a single MEC M=B⋆M=B whose dominant colour m is even, the single invocation (M∖C−1(m)) MecDecomp(M C^-1(m)) made by the recursive call of line 6 of Algorithm 1. This covers every invocation of MecDecomp, since each MEC MiM_i processed by OddEC is returned by exactly one node, the one with B⋆=MiB =M_i. There are at most |||S| levels, because a child’s set is a proper subset of its parent’s: Ci⊊B⋆⊆BC_i B B as B⋆B splits into k≥2k≥ 2 SCCs, and M∖C−1(m)⊊M⊆BM C^-1(m) M B as the maximal-colour states of M are removed before recursing. The sets at any fixed level are pairwise disjoint, because siblings are disjoint — they are distinct SCCs of B⋆B in the first case, and there is only one child in the second — and children of distinct nodes stay inside the disjoint sets of their parents. Hence each level costs at most O(||2)O(|S|^2) LP queries by the per-invocation bound of Theorem 18, and O(||3)O(|S|^3) queries suffice in total. The remaining work of OddEC — computing each mim_i, testing its parity, and forming Mi∖C−1(mi)M_i C^-1(m_i) and the union W — is O(|B|)O(|B|) per node, hence O(||)O(|S|) per level and O(||2)O(|S|^2) in total. Each LP query has size polynomial in the encoding of ℛR, so WoddW_odd is computed in polynomial time. ∎ Proof of Lemma 6. Write R=supτPrs0τ[(Wodd)]R= _τ ^τ_s_0[ Reach(W_odd)] for the maximal probability of reaching WoddW_odd. Since the environment minimizes the probability of (C) Parity(C), s0ℛ((C))=infτPrs0τ[(C)]=1−supτPrs0τ[¬(C)], v^R_s_0( Parity(C))= _τ ^τ_s_0[ Parity(C)]=1- _τ ^τ_s_0[ \, Parity(C)], and this value is attained by a positional environment policy, so the last supremum may be restricted to positional policies. Indeed, the parity problem in a linearly defined RMC reduces to a parity problem in an MDP controlled by the environment: at each state s let the actions be the (finitely many) vertices of the polytope (s)P(s), each with the transition distribution of the corresponding corner. Every environment policy of the RMC is a policy of this MDP whose one-step choice p∈(s)p (s) is a convex combination of vertex actions, and conversely; the two induce the same distributions over plays, so the parity values coincide. Since parity MDPs attain their optimal values by positional policies mapping each state to a single action, the environment has a positional optimal policy that selects one vertex of (s)P(s) at each state. We show the resulting supremum equals R. Upper bound. For every positional τ, Lemma 20 gives Prs0τ[¬(C)]≤Prs0τ[(Wodd)]≤R ^τ_s_0[ \, Parity(C)]≤ ^τ_s_0[ Reach(W_odd)]≤ R. Lower bound. Applying Theorem 3 to the safe set ∖WoddS W_odd (equivalently, to the unsafe set WoddW_odd) yields a positional environment policy τreach _reach attaining Prs0τreach[(Wodd)]=R _reach_s_0[ Reach(W_odd)]=R. Define the positional policy τ⋆(s)=τstay(s)s∈Wodd,τreach(s)s∉Wodd,τ (s)= cases _stay(s)&s∈ W_odd,\\ _reach(s)&s∉ W_odd, cases with τstay _stay from Lemma 19. Since τ⋆τ agrees with τreach _reach until WoddW_odd is first hit, it reaches WoddW_odd with probability R; and once inside, WoddW_odd is closed under τstay _stay and the dominant color is odd almost surely, so (Wodd) Reach(W_odd) implies ¬(C) \, Parity(C) under τ⋆τ . Hence Prs0τ⋆[¬(C)]≥Prs0τ⋆[(Wodd)]=R ^τ _s_0[ \, Parity(C)]≥ ^τ _s_0[ Reach(W_odd)]=R. Combining the two bounds, supτPrs0τ[¬(C)]=R _τ ^τ_s_0[ \, Parity(C)]=R, so, using the safety–reachability duality with unsafe set U=WoddU=W_odd, s0ℛ((C))=1−R=s0ℛ((∖Wodd)).∎ v^R_s_0( Parity(C))=1-R= v^R_s_0 ( Safe(S W_odd) ). Proof of Theorem 7. By Lemma 5, WoddW_odd is computable in polynomial time. By Lemma 6 the parity value at every state equals the safety value of (∖Wodd) Safe(S W_odd), which, together with an optimal positional environment policy, is computed in polynomial time by Theorem 3. The policy τ⋆τ built in the proof of Lemma 6 (reaching WoddW_odd optimally and then applying τstay _stay) is a corresponding optimal positional environment policy for (C) Parity(C). ∎ Appendix F Proof of Proposition 8 and Corollary 9 This appendix proves Proposition 8: every linearly defined RMDP satisfies the positional-determinacy condition of Proposition 8. The argument reduces a linearly defined RMDP ℳM to a finite turn-based stochastic parity game G (the vertex game of ℳM) in which the environment’s choice of a distribution from an uncertainty polytope is replaced by an adversarial choice of a vertex (corner) of that polytope followed by a probabilistic step. The reduction is value-preserving and carries positional strategies of G back to positional policies of ℳM; since turn-based stochastic parity games are positionally determined, so is ℳM. Specialising to the single-action case yields the reduction of a linearly defined RMC to an MDP used in Sections 3 and 3.2. Throughout we fix a linearly defined RMDP ℳ=(,,)M=(S,A,P) and a coloring C:→[d]C →[d], and write φ=(C) = Parity(C). F.1 Vertices of the Uncertainty Polytopes For a state-action pair (s,a)(s,a) the uncertainty set (s,a)=p∈Δ():As,ap≤bs,aP(s,a)=\p∈ (S):A_s,a\,p≤ b_s,a\ is a bounded polytope (it is contained in the simplex Δ() (S)). Let ((s,a)) Vert(P(s,a)) denote its finite set of vertices (extreme points). The Minkowski–Weyl theorem for polytopes gives the following standard fact, on which the whole reduction rests. Lemma 21 (Vertex representation). Each polytope (s,a)P(s,a) has finitely many vertices, and (s,a)=∑q∈((s,a))λq:λq≥0,∑qλq=1,P(s,a)\;=\; \\, _q∈ Vert(P(s,a)) _q\,q\;:\; _q≥ 0,\ _q _q=1\, \, i.e. every admissible distribution p∈(s,a)p (s,a) is a convex combination of vertices of (s,a)P(s,a). Since a convex combination of distributions is again a distribution, each vertex q∈((s,a))q∈ Vert(P(s,a)) is itself a distribution over S, and it is the extreme-point distribution the environment may commit to. Lemma 21 is the only place where polytopicity is used: it is what makes the environment’s continuous choice reducible to a finite one. F.2 The Vertex Game We build a turn-based stochastic parity game =(V,V◇,V□,V○,E,C)G=(V,V_ ,V_ ,V_ ,E,C_G) with three kinds of vertices: • Agent vertices V◇=vs:s∈V_ =\\,v_s:s \,\, one per state, owned by the agent (the maximiser); • Environment vertices V□=vs,a:s∈,a∈V_ =\\,v_s,a:s ,\ a \,\, one per state-action pair, owned by the environment (the minimiser); • Probabilistic vertices V○=vs,a,q:s∈,a∈,q∈((s,a))V_ =\\,v_s,a,q:s ,\ a ,\ q∈ Vert(P(s,a))\,\, one per chosen vertex of an uncertainty polytope. The moves are as follows. From an agent vertex vsv_s the agent chooses an action a∈a and moves to the environment vertex vs,av_s,a. From an environment vertex vs,av_s,a the environment chooses a vertex q∈((s,a))q∈ Vert(P(s,a)) and moves to the probabilistic vertex vs,a,qv_s,a,q. From a probabilistic vertex vs,a,qv_s,a,q the next vertex is sampled: the game moves to the agent vertex vs′v_s with probability q(s′)q(s ) for each s′∈s . Thus E=(vs,vs,a):a∈∪(vs,a,vs,a,q):q∈((s,a))∪(vs,a,q,vs′):q(s′)>0.E\;=\;\\,(v_s,v_s,a):a \,\∪\\,(v_s,a,v_s,a,q):q∈ Vert(P(s,a))\,\∪\\,(v_s,a,q,v_s ):q(s )>0\,\. The coloring C_G assigns to each agent vertex the color of its state, C(vs)=C(s)C_G(v_s)=C(s), and to every environment and probabilistic vertex the least color 00, which is even and dominated by every color of [d][d]: C(vs)=C(s),C(vs,a)=C(vs,a,q)=0.C_G(v_s)=C(s), C_G(v_s,a)=C_G(v_s,a,q)=0. A play of G satisfies the parity objective iff the largest color occurring infinitely often is even. The game is finite: it has ||+||||+∑s,a|((s,a))||S|+|S||A|+ _s,a| Vert(P(s,a))| vertices. F.3 Correspondence of Plays and Strategies Every play of G from vs0v_s_0 has the form vs0vs0,a0vs0,a0,q0vs1vs1,a1vs1,a1,q1vs2⋯,v_s_0\,v_s_0,a_0\,v_s_0,a_0,q_0\,v_s_1\,v_s_1,a_1\,v_s_1,a_1,q_1\,v_s_2·s, alternating one agent vertex, one environment vertex and one probabilistic vertex per round. Deleting the environment and probabilistic vertices yields the projected path ρ(π)=s0s1s2⋯∈ωρ(π)=s_0s_1s_2·s ^ω, an infinite path of ℳM. The projection ρ is a colour-faithful correspondence. Lemma 22 (Play projection). For every play π of G, the maximal color occurring infinitely often in π equals the maximal color occurring infinitely often in ρ(π)ρ(π). Consequently π satisfies (C) Parity(C_G) iff ρ(π)ρ(π) satisfies (C) Parity(C). Proof. Each round of π contributes exactly one agent vertex vsiv_s_i with color C(si)C(s_i) and two auxiliary vertices with color 00. Hence the multiset of colors seen infinitely often in π is that of ρ(π)ρ(π) together with the color 00 (seen infinitely often, as the play is infinite). Since 00 is the least color, it never changes the maximum, so the maximal recurring color of π equals that of ρ(π)ρ(π). The parity condition depends only on this maximum. ∎ We now match strategies. A (behavioural) agent strategy in G chooses, given the history ending at an agent vertex vsv_s, a distribution over actions; a positional (pure memoryless) agent strategy is a map →S . These are literally the agent policies of ℳM, with positional strategies corresponding to positional agent policies. For the environment, at an environment vertex vs,av_s,a a behavioural strategy chooses a distribution over the vertices ((s,a)) Vert(P(s,a)); the induced one-step distribution over successor states s′s is ∑qλqq(s′) _q _q\,q(s ), i.e. the convex combination ∑qλqq∈(s,a) _q _q\,q (s,a) by Lemma 21. The next lemma records that these convex combinations range over exactly (s,a)P(s,a), so environment strategies of G and environment policies of ℳM realise precisely the same one-step distributions. Lemma 23 (Environment moves). Fix (s,a)(s,a). The set of one-step distributions over S that the environment can realise at vs,av_s,a in G, namely ∑qλqq:λ∈Δ(((s,a)))\ _q _q\,q:λ∈ ( Vert(P(s,a)))\, equals (s,a)P(s,a). In particular, a pure choice of a single vertex q realises the distribution q, and every distribution p∈(s,a)p (s,a) is realised by some (possibly randomised) choice. Proof. Every convex combination of vertices lies in (s,a)P(s,a) because the polytope is convex; conversely, by Lemma 21 every p∈(s,a)p (s,a) is such a convex combination. Committing to a single vertex q (i.e. λq=1 _q=1) realises q itself. ∎ Given a strategy profile in G and its counterpart in ℳM realising the same one-step distributions at every vertex, the two induce, via the cylinder construction, the same probability distribution over projected paths; combined with Lemma 22 this yields value preservation. Lemma 24 (Value preservation). For every s∈s , the value of G at vsv_s for the objective (C) Parity(C_G) equals sℳ(φ) v^M_s( ). Moreover, for a fixed positional agent policy σ (resp. positional environment policy τ) the value of the corresponding one-player game equals infτ′Prsσ,τ′[φ] _τ ^σ,τ _s[ ] (resp. supσ′Prsσ′,τ[φ] _σ ^σ ,τ_s[ ]). Proof. Fix any agent strategy and environment strategy in G. By Lemma 23 there are an agent policy and an environment policy of ℳM that at every state (resp. state-action pair) reproduce the same one-step distribution over successors, and conversely every pair of policies of ℳM arises this way. Because the one-step distributions agree at every vertex, the two induced measures assign equal probability to every cylinder of projected paths, so Pr of the event π:ρ(π)⊧(C)\π:ρ(π) Parity(C)\ in G equals Prsσ,τ[φ] ^σ,τ_s[ ] in ℳM; by Lemma 22 the former equals the probability of (C) Parity(C_G). Taking sup over agent strategies and inf over environment strategies on both sides gives val(vs)=supσinfτPrsσ,τ[φ]=sℳ(φ)val_G(v_s)= _σ _τ ^σ,τ_s[ ]= v^M_s( ). The one-player statements follow by fixing the corresponding player’s strategy to the positional policy and repeating the argument. ∎ F.4 Proof of Proposition 8 Proof of Proposition 8. Turn-based stochastic games with a parity objective are positionally (pure-memoryless) determined: both players have optimal pure memoryless strategies, and the game has a value satisfying supσinfτ=infτsupσ _σ _τ= _τ _σ (Chatterjee and Henzinger 2012). Apply this to the vertex game G of ℳM. Let σ σ and τ τ be optimal pure memoryless strategies of the agent and the environment in G. Map them back to ℳM. The strategy σ σ selects, at each agent vertex vsv_s, a single action σ∗(s)∈σ (s) ; this is a positional agent policy of ℳM. The strategy τ τ selects, at each environment vertex vs,av_s,a, a single vertex qs,a∈((s,a))q_s,a∈ Vert(P(s,a)); setting τ∗(s,a)=qs,a∈(s,a)τ (s,a)=q_s,a (s,a) (a vertex distribution) gives a positional environment policy of ℳM. By Lemma 23 these choices realise exactly the same one-step distributions in ℳM as σ^,τ σ, τ do in G, so by Lemma 24 they are value preserving. Optimality of σ σ in G means that against every environment strategy it secures at least the game value, which by Lemma 24 is sℳ(φ) v^M_s( ); translating through the strategy correspondence, infτPrsσ∗,τ[φ]=sℳ(φ) _τ ^σ ,τ_s[ ]= v^M_s( ) for all s. Symmetrically, optimality of τ τ gives supσPrsσ,τ∗[φ]=sℳ(φ) _σ ^σ,τ _s[ ]= v^M_s( ) for all s. Hence infτPrsσ∗,τ[φ]=sℳ(φ)=supσPrsσ,τ∗[φ]for all s∈, _τ ^σ ,τ_s[ ]\;=\; v^M_s( )\;=\; _σ ^σ,τ _s[ ] all s , with σ∗σ and τ∗τ positional, which is exactly the positional-determinacy condition. In particular the two orders of optimization coincide, so ℳM is determined. This proves Proposition 8. ∎ F.5 Proof of Corollary 9 Throughout this subsection, RMDP-Parity denotes the decision problem of Corollary 9: given a linearly defined RMDP ℳ=(,,)M=(S,A,P), a coloring C:→[d]C →[d], a state s∈s and a rational threshold λ∈[0,1]λ∈[0,1] written in binary, decide whether sℳ((C))≥λ v^M_s( Parity(C))≥λ. Analogously, SG-Parity denotes the problem of deciding, for a finite turn-based stochastic parity game ℋH with rational transition probabilities, a vertex v of ℋH and a rational λ∈[0,1]λ∈[0,1], whether valℋ(v)≥λval_H(v)≥λ. We write ‖ℳ‖\|M\| for the bit-size of the encoding of ℳM, and recall from the preliminaries that each uncertainty set is presented as (s,a)=x∈Δ()|∃y∈ℝk:As,a[xy]≤bs,a,P(s,a)= \x∈ (S)\; |\;∃ y ^k A_s,a bmatrixx\\ y bmatrix≤ b_s,a \, where we assume without loss of generality that the simplex constraints defining Δ() (S) are among the rows of As,a[x;y]≤bs,aA_s,a\,[x;y]≤ b_s,a. The two assertions of Corollary 9 are proved separately in Lemma 26 and Lemma 27 below. Membership in ∩NP . The certificates we use are positional policies. For the agent a positional policy is a map →S and is trivially of size O(||log||)O(|S| |A|). For the environment a positional policy must name a distribution inside each uncertainty set, so we first record that the distributions selected by the optimal environment policy constructed in the proof of Proposition 8 (vertices of the uncertainty polytopes) admit a compact encoding, even though the number of such vertices may be exponential (Remark 29). Lemma 25 (Vertices admit compact encodings). Let (s,a)P(s,a) be a linearly defined uncertainty set. Then every q∈((s,a))q∈ Vert(P(s,a)) is a rational vector of bit-size polynomial in ‖ℳ‖\|M\|. Moreover, given a rational vector q∈ℚq ^S, one can decide in time polynomial in ‖ℳ‖\|M\| and the bit-size of q whether q∈(s,a)q (s,a). Proof. Write As,a=[Ax∣Ay]A_s,a=[A^x A^y] according to the split of the variables into x and y, and let Q=(x,y):Axx+Ayy≤bs,aQ=\(x,y):A^xx+A^yy≤ b_s,a\, so that (s,a)P(s,a) is the projection of Q onto the x-coordinates. By the Fourier–Motzkin projection lemma, (s,a)=x∈ℝ:(μ⊤Ax)x≤μ⊤bs,a for all μ∈K,P(s,a)=\\,x ^S\;:\;(μ A^x)\,x≤μ b_s,a\ for all μ∈ K\,\, where K=μ≥0:μ⊤Ay=0K=\μ≥ 0:μ A^y=0\ is the projection cone of Q, and it suffices to range over the finitely many extreme rays of K. Each extreme ray of K is a basic solution of a rational system whose size is bounded by ‖ℳ‖\|M\|, hence, by Cramer’s rule, is a rational vector of bit-size polynomial in ‖ℳ‖\|M\|; consequently each inequality (μ⊤Ax)x≤μ⊤bs,a(μ A^x)x≤μ b_s,a in the above description has bit-size polynomial in ‖ℳ‖\|M\|, although there may be exponentially many of them. Now let q be a vertex of (s,a)P(s,a). Since (s,a)⊆Δ()P(s,a) (S) is a polytope of dimension at most |||S|, the vertex q is the unique solution of a subsystem of |||S| linearly independent inequalities of the above description taken with equality. Applying Cramer’s rule once more to this subsystem, whose entries are of bit-size polynomial in ‖ℳ‖\|M\|, shows that q is rational of bit-size polynomial in ‖ℳ‖\|M\|. For the second claim, q∈(s,a)q (s,a) holds iff the linear system Ayy≤bs,a−AxqA^yy≤ b_s,a-A^xq in the unknown y is feasible, which is an LP feasibility test on rational data of size polynomial in ‖ℳ‖\|M\| and the size of q, and is therefore decidable in polynomial time. ∎ Lemma 26. RMDP-Parity∈∩ RMDP-Parity . Proof. We show that both RMDP-Parity and its complement are in NP. Membership in NP. The certificate is a positional agent policy σ:→σ , of size polynomial in ‖ℳ‖\|M\|. The verifier constructs the induced RMC ℳσ=(,σ)M^σ=(S,P^σ) with σ(s)=(s,σ(s))P^σ(s)=P(s,σ(s)); this is again linearly defined, is obtained from ℳM by discarding the uncertainty sets of the unselected actions, and hence is computable in polynomial time. By Theorem 7 the verifier then computes sσ=infτPrsσ,τ[φ] v^σ_s= _τ ^σ,τ_s[ ] in time polynomial in ‖ℳ‖\|M\|; in particular sσ v^σ_s is a rational of bit-size polynomial in ‖ℳ‖\|M\|, being the output of a polynomial-time computation, so the verifier can compare it with λ exactly in polynomial time. It accepts iff sσ≥λ v^σ_s≥λ. Soundness: for every positional agent policy σ we have sσ≤supσ′infτPrsσ′,τ[φ]=sℳ(φ) v^σ_s≤ _σ _τ ^σ ,τ_s[ ]= v^M_s( ), so an accepting certificate witnesses sℳ(φ)≥λ v^M_s( )≥λ. Completeness: if sℳ(φ)≥λ v^M_s( )≥λ, then the positional policy σ∗σ of Proposition 8 satisfies sσ∗=sℳ(φ)≥λ v^σ _s= v^M_s( )≥λ and is accepted. Membership in coNP. We give an NP procedure for the complement, i.e. for deciding sℳ(φ)<λ v^M_s( )<λ. The certificate is a positional environment policy τ, presented as a table of rational distributions τ(s,a)∈(s,a)τ(s,a) (s,a) for all (s,a)∈×(s,a) ×A; the verifier first checks τ(s,a)∈(s,a)τ(s,a) (s,a) for every pair, which by Lemma 25 takes polynomial time, and rejects the certificate otherwise. Fixing τ leaves the MDP ℳτ=(,,δ)M^τ=(S,A,δ) with δ(s,a)=τ(s,a)δ(s,a)=τ(s,a), whose transition probabilities are exactly the entries of the certificate and whose size is therefore polynomial in the size of the certificate. Since agent policies of ℳM played against the fixed τ are precisely the policies of ℳτM^τ, we have supσPrsσ,τ[φ]=sℳτ((C)) _σ ^σ,τ_s[ ]= v^M^τ_s( Parity(C)). The quantitative parity problem on MDPs is solvable in polynomial time (Chatterjee and Henzinger 2012): one computes the maximal end-component decomposition, retains those end-components in which the agent can enforce an even dominant colour, and solves a maximal reachability LP for their union; in particular the value is a rational of bit-size polynomial in the size of ℳτM^τ. The verifier computes this value and accepts iff it is smaller than λ. Soundness: for every positional environment policy τ we have supσPrsσ,τ[φ]≥supσinfτ′Prsσ,τ′[φ]=sℳ(φ) _σ ^σ,τ_s[ ]≥ _σ _τ ^σ,τ _s[ ]= v^M_s( ), so an accepting certificate witnesses sℳ(φ)<λ v^M_s( )<λ. Completeness: if sℳ(φ)<λ v^M_s( )<λ, take the positional environment policy τ∗τ constructed in the proof of Proposition 8. It satisfies supσPrsσ,τ∗[φ]=sℳ(φ)<λ _σ ^σ,τ _s[ ]= v^M_s( )<λ and, crucially, it selects at each pair (s,a)(s,a) a vertex qs,a∈((s,a))q_s,a∈ Vert(P(s,a)); by Lemma 25 each qs,aq_s,a is rational of bit-size polynomial in ‖ℳ‖\|M\|, so τ∗τ is a certificate of polynomial size and is accepted. ∎ We stress that neither direction materialises the vertex game G: the NP verifier runs the polynomial-time LP-based RMC solver of Section 3 on the compact facet description, and the coNP verifier only ever writes down one vertex per state-action pair rather than all of them. Hardness. For the lower bound we exhibit the converse of the vertex-game construction: stochastic games are a special case of linearly defined RMDPs, in which the environment’s uncertainty set is the convex hull of the Dirac distributions on the available successors. Lemma 27. SG-Parity reduces to RMDP-Parity in polynomial time. Hence RMDP-Parity is at least as hard as SG-Parity. Proof. Let ℋ=(V,V◇,V□,V○,E,Cℋ)H=(V,V_ ,V_ ,V_ ,E,C_H) be a turn-based stochastic parity game with a rational transition distribution pv∈Δ(V)p_v∈ (V) at every v∈V○v∈ V_ , together with a vertex v0v_0 and a rational λ. We build a linearly defined RMDP ℳℋ=(V,,)M_H=(V,A,P) with =a1,…,amA=\a_1,…,a_m\, where m is the maximum out-degree in ℋH, and coloring C=CℋC=C_H, as follows. Fix for each vertex v an enumeration v1,…,vdeg(v)v^1,…,v (v) of its successors. • For v∈V◇v∈ V_ (an agent vertex) and i≤deg(v)i≤ (v), put (v,ai)=δviP(v,a_i)=\ _v^i\, the singleton containing the Dirac distribution on the i-th successor. • For v∈V□v∈ V_ (an environment vertex), put (v,ai)=convδv1,…,δvdeg(v)=p∈Δ(V):p(u)=0 for all u with (v,u)∉EP(v,a_i)=conv\ _v^1,…, _v (v)\=\p∈ (V):p(u)=0 for all u with (v,u)∉ E\ for every i. • For v∈V○v∈ V_ (a probabilistic vertex), put (v,ai)=pvP(v,a_i)=\p_v\ for every i. For v∈V◇v∈ V_ and i>deg(v)i> (v) we set (v,ai)=(v,a1)P(v,a_i)=P(v,a_1), so that the action set is uniform and no action is spurious. Every uncertainty set above is cut out by linear equalities and the simplex constraints, hence is linearly defined without auxiliary variables, and ℳℋM_H is computable from ℋH in polynomial time. It remains to show vℳℋ((C))=valℋ(v) v^M_H_v( Parity(C))=val_H(v) for every v∈Vv∈ V, from which the reduction follows by asking RMDP-Parity about ℳℋM_H, v0v_0 and λ. Consider the vertex game G of ℳℋM_H constructed above. For v∈V□v∈ V_ the distributions δv1,…,δvdeg(v) _v^1,…, _v (v) are distinct unit vectors and therefore affinely independent, so each of them is an extreme point of their convex hull and no other point is: ((v,ai))=δv1,…,δvdeg(v) Vert(P(v,a_i))=\ _v^1,…, _v (v)\. For v∈V◇∪V○v∈ V_ ∪ V_ the uncertainty sets are singletons and thus have a single vertex. Hence in G: at v∈V◇v∈ V_ the agent chooses one of the successors of v and the play proceeds deterministically to it; at v∈V□v∈ V_ the agent has no meaningful choice, the environment chooses a vertex δvi _v^i, and the play proceeds deterministically to viv^i; at v∈V○v∈ V_ neither player has a choice and the next vertex is sampled from pvp_v. Thus G is exactly ℋH with every edge subdivided by at most two auxiliary vertices of colour 00, and with a dummy choice inserted at the vertices of V□∪V○V_ ∪ V_ . Since 00 is dominated by every colour of [d][d], the argument of Lemma 22 applies verbatim: the maximal colour occurring infinitely often along a play of G equals that of the corresponding play of ℋH, and the strategy correspondence of Lemma 24 maps strategies of the two games to one another while preserving the induced distributions over projected paths. Consequently val(v)=valℋ(v)val_G(v)=val_H(v), and by Lemma 24 applied to ℳℋM_H we get vℳℋ((C))=val(v)=valℋ(v) v^M_H_v( Parity(C))=val_G(v)=val_H(v), as required. ∎ Lemma 26 and Lemma 27 together prove Corollary 9. Two consequences are worth recording. First, since no polynomial-time algorithm for SG-Parity is known (the best known bounds are randomised sub-exponential (Chatterjee and Henzinger 2006a)) a polynomial-time algorithm for the quantitative parity problem on linearly defined RMDPs would resolve a long-standing open problem; this is the sense in which the exponential iteration bound of Theorem 12 is not an artefact of our analysis. Second, membership in ∩NP implies that RMDP-Parity is not NP-hard unless =NP=coNP, so the source of hardness is not NP-hardness but the same “∩NP barrier” as for stochastic games. Remark 28 (The RMC specialisation). When ||=1|A|=1 the agent has no choice and the agent vertices merge with the (unique) environment vertices, so G becomes a one-player stochastic game controlled by the environment, i.e. an MDP whose actions at state s are the vertices ((s)) Vert(P(s)) and whose transition under vertex q is q itself. Every environment policy of the RMC is a policy of this MDP whose one-step choice is a convex combination of vertex actions, and conversely, so the two induce the same distributions over plays and the parity values coincide (Lemma 24). Since parity MDPs admit optimal positional policies, the environment has a positional optimal policy selecting one vertex of (s)P(s) at each state. This is precisely the reduction invoked in the proof of Lemma 6 and in Section 3.2. Remark 29 (Size of the reduction). The vertex game G is value-equivalent to ℳM and could in principle be solved directly by a stochastic-game (resp. MDP) parity solver, computing ℳ(φ) v^M( ) exactly. However its size is governed by ∑s,a|((s,a))| _s,a| Vert(P(s,a))|, and a polytope described by polynomially many facets in dimension |||S| can have |((s,a))|| Vert(P(s,a))| exponential in |||S| (for instance the L1L_1 ball, whose vertex count grows with |||S|). Thus G may be exponentially larger than ℳM, and even writing it down need not be possible in polynomial space. This is exactly the inefficiency that motivates the polynomial time and space, LP-based algorithms of Section 3 and Section 4, which operate on the compact facet description of the polytopes rather than on their vertices. Appendix G Proofs of Section 4 This appendix provides the proofs of the results of Section 4. Throughout we use the notation and standing objects of that section: the linearly defined RMDP ℳ=(,,)M=(S,A,P), the coloring C and objective φ=(C) = Parity(C), the induced RMC ℳσM^σ and its value vector σ v^σ, the value classes σ(r) VC^σ(r), the one-step optima ν(s,a)=minp∈(s,a)p⋅σν(s,a)= _p (s,a)p· v^σ, tight actions σ(s)A v^σ(s), tight faces σ(s,a)P v^σ(s,a), the improvable set I, and the trap value-class RMDPs ℳrM_r over Ur∪⊥U_r∪\ \ (where the agent is restricted to tight actions, the environment to tight faces, and all mass leaving UrU_r is collapsed onto the losing sink ⊥ by the linear map κr _r) together with their colorings CrC_r, almost-sure regions Wr=ℳr((Cr))∩UrW_r= AS_M_r( Parity(C_r))∩ U_r and positional almost-sure winning policies σr _r on WrW_r. Recall that σr(s)∈σ(s) _r(s) v^σ(s) for every s∈Wrs∈ W_r by construction, since ℳrM_r offers no other actions. We use freely the fact, established in Section 4, that p⋅=sp· u= u_s for every tight action a∈A(s)a∈ A u(s) and every p in the tight face (s,a)P u(s,a), the support property of WrW_r recorded in Lemma 37 below, and the elementary facts about one-step minima: since each uncertainty set is a nonempty compact polytope and p↦p⋅p p· u is linear, every infimum infp∈(s,a)p⋅ _p (s,a)p· u is attained, and the set of minimisers is the nonempty face of (s,a)P(s,a) obtained by adjoining the single linear inequality p⋅≤ν(s,a)p· u≤ _ u(s,a), whose vertices are vertices of (s,a)P(s,a). In particular every argmin below is nonempty, and so is every uncertainty set of ℳrM_r, being the image of a nonempty set under κr _r. Hence, every ℳrM_r is a legitimate linearly defined RMDP and Proposition 8 applies to it. Markov-chain preliminaries. When both policies are positional the pair (σ,τ)(σ,τ) induces a finite Markov chain over S with transition matrix P(s,t)=τ(s,σ(s))(t)P(s,t)=τ(s,σ(s))(t). We use the standard theory of finite Markov chains (Baier and Katoen 2008): with probability 11 the play eventually enters a closed recurrent class ℛRC and visits all its states infinitely often, so (π)=ℛ Inf(π)=RC almost surely conditioned on entering ℛRC. Call ℛRC even if maxC(ℛ) C(RC) is even and odd otherwise; conditioned on entering ℛRC, the play satisfies φ with probability 11 if ℛRC is even and 00 if it is odd. Hence, writing ◊ℛ for the event of being absorbed in ℛRC, Prsσ,τ[φ]=∑ℛevenPrsσ,τ[◊ℛ]. ^σ,τ_s[ ]\;=\; _RC\ even ^σ,τ_s[ ]. (4) We also record the harmonicity of the satisfaction probability of a prefix-independent objective under a positional pair: writing ws:=Prsσ,τ[φ]w_s:= ^σ,τ_s[ ], ws=∑t∈P(s,t)wt,i.e.w=Pw.w_s\;=\; _t P(s,t)\,w_t, .e. w=Pw. (5) This is immediate from the Markov property together with prefix-independence of φ : conditioned on the first transition s→ts→ t, the remaining play is distributed as a play from t under the same positional pair, and deleting the one-step prefix does not change whether the play satisfies φ . G.1 Optimality conditions Proposition 8 yields the usual one-step optimality (Bellman) conditions. Note that, by compactness of the uncertainty sets, the inner operators below are minima and not merely infima. Proposition 30 (Optimality conditions). For every s∈s , sℳ(φ)=maxa∈minp∈(s,a)p⋅ℳ(φ). v^M_s( )\;=\; _a \ _p (s,a)\ p· v^M( ). (6) Moreover, for the RMC ℳσM^σ induced by a positional agent policy σ, sσ=minp∈(s,σ(s))p⋅σfor every s∈, v^σ_s\;=\; _p (s,σ(s))p· v^σ every s , (7) and the minimum in (7) is attained simultaneously at all states by the positional environment policy of Proposition 8. Proof of Proposition 30. Both identities peel off the first transition out of s and identify the value of the remaining play with the value vector again. This is legitimate because parity is prefix-independent, i.e. whether a path satisfies (C) Parity(C) depends only on (π) Inf(π), so deleting or prepending a finite prefix never changes membership. Proof of (7). Write u:=σu:= v^σ. By the last clause of Proposition 8 there is a positional environment policy τ∗τ of ℳσM^σ with Prtτ∗[φ]=ut ^τ _t[ ]=u_t for every t. Applying (5) to the chain it induces gives us=τ∗(s)⋅u≥minp∈(s,σ(s))p⋅u_s=τ (s)· u≥ _p (s,σ(s))p· u. Conversely, fix p∈(s,σ(s))p (s,σ(s)) and let τp _p be the environment policy that plays p on the first step at s and follows τ∗τ afterwards. It is admissible because p∈(s,σ(s))p (s,σ(s)). By prefix-independence, Prsτp[φ]=∑tp(t)Prtτ∗[φ]=p⋅u _p_s[ ]= _tp(t)\, ^τ _t[ ]=p· u, whence us=infτPrsτ[φ]≤p⋅u_s= _τ ^τ_s[ ]≤ p· u. Minimising over p gives us≤minpp⋅u_s≤ _pp· u, and the two inequalities give (7). The final clause of the statement is the first display: τ∗(s)τ (s) attains the minimum at every s at once. Proof of (6). Write v:=ℳ(φ)v:= v^M( ). (≤)(≤) By Proposition 8 there is a positional agent policy σ∗σ with σ∗=v v^σ =v. Applying (7) to σ∗σ at s, with a∗=σ∗(s)a =σ (s), vs=minp∈(s,a∗)p⋅v≤maxa∈minp∈(s,a)p⋅v.v_s= _p (s,a )p· v\;≤\; _a _p (s,a)p· v. (≥)(≥) By Proposition 8 fix a positional environment policy τ∗τ with supσPrtσ,τ∗[φ]=vt _σ ^σ,τ _t[ ]=v_t for every t. Fixing τ∗τ turns ℳM into an ordinary MDP with transition function δ(t,a)=τ∗(t,a)δ(t,a)=τ (t,a) whose parity value at t is vtv_t. This MDP has a positional optimal agent policy σ¯ σ, so Prtσ¯,τ∗[φ]=vt σ,τ _t[ ]=v_t for every t. Fix a∈a and let σa _a play a on the first step at s and follow σ¯ σ afterwards. By prefix-independence, Prsσa,τ∗[φ]=∑t∈τ∗(s,a)(t)Prtσ¯,τ∗[φ]=τ∗(s,a)⋅v≥minp∈(s,a)p⋅v. _a,τ _s[ ]= _t τ (s,a)(t)\, σ,τ _t[ ]=τ (s,a)· v\;≥\; _p (s,a)p· v. Since vs=supσPrsσ,τ∗[φ]≥Prsσa,τ∗[φ]v_s= _σ ^σ,τ _s[ ]≥ _a,τ _s[ ], we get vs≥minp∈(s,a)p⋅v_s≥ _p (s,a)p· v for every a, and taking the maximum over the finite set A gives (≥)(≥). ∎ G.2 Formal Definition of Value-Class RMDPs Throughout this subsection we fix a positional agent policy σ, write :=σ u:= v^σ for the value vector of the induced RMC ℳσM^σ, and fix a value r of u with Ur:=σ(r)≠∅U_r:= VC^σ(r)≠ . Recall from Section 4 that an action a is tight at s if ν(s,a)=sν(s,a)= u_s, that (s)A u(s) denotes the set of tight actions at s, and that (s,a)P u(s,a) denotes the tight face at (s,a)(s,a). The construction of ℳrM_r restricts ℳM to the states of UrU_r, to the tight actions, and to the tight faces, and merges everything outside UrU_r into a single fresh state. The merging is carried out by the following map. Definition 31 (Collapse map). Let ⊥∉ be a fresh state and let cr:→Ur∪⊥c_r:S→ U_r∪\ \ fix every state of UrU_r and send every state of ∖UrS U_r to ⊥ . The collapse map κr _r is the push-forward of distributions along crc_r, i.e. κr:Δ()→Δ(Ur∪⊥) _r: (S)→ (U_r∪\ \) with κr(p)(t)=p(t)(t∈Ur),κr(p)(⊥)=∑t∈∖Urp(t). _r(p)(t)=p(t) (t∈ U_r), _r(p)( )=\!\! _t U_r\!\!p(t). We extend κr _r to sets of distributions by taking images, κr(X)=κr(p)∣p∈X _r(X)=\ _r(p) p∈ X\. Thus κr _r leaves the mass inside the value class where it is and lumps all remaining mass onto ⊥ . The two cases of Definition 31 are exhaustive and disjoint, so κr(p) _r(p) is again a distribution. Note that κr _r is the restriction to Δ() (S) of a linear map ℝ→ℝUr∪⊥R^S ^U_r∪\ \; in particular it maps polytopes to polytopes, and it is in general not injective, since it forgets how the escaping mass is distributed over ∖UrS U_r. Definition 32 (Value-class RMDP). The value-class RMDP of σ at r is the RMDP ℳr=(r,r,r)M_r=(S_r,A_r,P_r) with coloring Cr:r→[d+1]C_r:S_r→[d+1] given by: 1. r=Ur⊎⊥S_r=U_r \ \ and r=⊎a⊥A_r=A \a_ \; 2. for s∈Urs∈ U_r and a∈(s)a u(s), r(s,a)=κr((s,a));P_r(s,a)= _r\! (P u(s,a) ); 3. r(s,a)=δ⊥P_r(s,a)=\ _ \ for s∈Urs∈ U_r and a∉(s)a u(s), and r(⊥,a)=δ⊥P_r( ,a)=\ _ \ for every a∈ra _r; 4. Cr(s)=C(s)C_r(s)=C(s) for s∈Urs∈ U_r, and Cr(⊥)=2⌈d/2⌉+1C_r( )=2 d/2 +1. The state ⊥ is absorbing and carries an odd color dominating every color of [d][d], so any play reaching ⊥ visits only ⊥ from then on and violates (Cr) Parity(C_r). Leaving the value class is therefore losing for the agent in ℳrM_r, irrespective of the values in ℳM of the states left for; likewise, by item (3), playing a non-tight action is losing. Consequently an optimal agent policy of ℳrM_r plays only tight actions on its almost-sure winning region, and we may and do treat (s)A u(s) as the actions genuinely available at s∈Urs∈ U_r. Lemma 33 (Well-definedness). Every uncertainty set of ℳrM_r is a nonempty polytope, and ℳrM_r is a linearly defined RMDP of description size O(|ℳ|)O(|M|). Moreover (s)≠∅A u(s)≠ for every s∈Urs∈ U_r, and ∑r|ℳr|=O(|ℳ|) _r|M_r|=O(|M|), the sum ranging over the values of u. Proof. The policy σ cannot be improved quantitatively, so, the action σ(s)σ(s) is tight at every s∈s , so (s)≠∅A u(s)≠ . For a∈(s)a u(s) the tight face (s,a)P u(s,a) is the face of (s,a)P(s,a) cut out by the single inequality p⋅≤ν(s,a)p· u≤ν(s,a), hence a nonempty polytope, and r(s,a)P_r(s,a) is its image under the linear map κr _r, hence again a nonempty polytope. For linear definability, r(s,a)=q|∃p:As,ap≤bs,a,p⋅≤s,q=κr(p),P_r(s,a)= \q\ |\ ∃ p:\ A_s,a\,p≤ b_s,a,\ p· u≤ u_s,\ q= _r(p) \, which presents r(s,a)P_r(s,a) as the projection onto the q-coordinates of a polyhedron in the variables (q,p)(q,p), obtained from the description of (s,a)P(s,a) by adjoining one inequality and the defining equalities of κr _r. Note that only u enters this description; the one-step optima ν(s,a)ν(s,a) are used solely in the tightness test of items (2) and (3). Hence ℳrM_r has description size O(|ℳ|)O(|M|). Finally the value classes are pairwise disjoint and r=Ur⊎⊥S_r=U_r \ \, so ∑r|r|≤||+|| _r|S_r|≤|S|+|S| and the total description size of all value-class RMDPs is O(|ℳ|)O(|M|). ∎ Since Lemma 33 makes ℳrM_r a linearly defined RMDP, Proposition 8 applies to it, as do the results of Section 3 instantiated at a fixed positional agent policy. We write Wr=ℳr((Cr))∩UrW_r= AS_M_r( Parity(C_r))∩ U_r for its almost-sure winning region and σr _r for a corresponding positional almost-sure winning policy. G.3 Transfer between the RMDP and its trap value-class RMDPs The trap value-class RMDP ℳrM_r lives over Ur∪⊥U_r∪\ \, so its one-step choices are distributions over Ur∪⊥U_r∪\ \ and not elements of (s,a)⊆Δ()P(s,a) (S). The following lemma does the translation once and for all. It is used at every point below where a play of ℳM is recognised as a play of ℳrM_r or conversely. Recall the collapse map κr:Δ()→Δ(Ur∪⊥),κr(p)(t)=p(t)(t∈Ur),κr(p)(⊥)=p(∖Ur), _r: (S)→ (U_r∪\ \), _r(p)(t)=p(t)\ \ (t∈ U_r), _r(p)( )=p(S U_r), and that r(s,a)=κr(σ(s,a))P_r(s,a)= _r(P v^σ(s,a)) for s∈Urs∈ U_r and a tight at s. Lemma 34 (Transfer). Let =σ u= v^σ, let r<1r<1 with Ur≠∅U_r≠ , let s∈Urs∈ U_r and let a∈(s)a u(s). Then: 1. (Push-forward.) For every p∈(s,a)p u(s,a) we have κr(p)∈r(s,a) _r(p) _r(s,a). 2. (Pull-back.) For every q∈r(s,a)q _r(s,a) there is p∈(s,a)p u(s,a) with κr(p)=q _r(p)=q. Such a p is a legal environment choice of ℳM at (s,a)(s,a) and satisfies p⋅=sp· u= u_s. 3. (Plays.) Let σ′σ be a positional agent policy of ℳM that plays tight actions at every state of UrU_r, and let X⊆UrX U_r. Suppose τ is a positional environment policy of ℳM such that τ(t,σ′(t))τ(t,σ (t)) lies in the tight face at (t,σ′(t))(t,σ (t)) and is supported in X. Then κr∘τ _r τ restricted to X is a legal environment policy of ℳrM_r, σ′σ restricted to X is a legal agent policy of ℳrM_r, and for every x∈Xx∈ X the two induced measures on plays coincide: the play of ℳM from x never leaves X and the corresponding play of ℳrM_r never visits ⊥ . Proof of Lemma 34. (1) is the definition of r(s,a)P_r(s,a) as the image of the tight face. (2) holds because a set-image consists exactly of the points having a preimage. The two properties of p are (s,a)⊆(s,a)P u(s,a) (s,a) and the definition of the tight face together with tightness of a. For (3), we check the three assertions in turn. The agent’s actions are tight, hence available in ℳrM_r. The environment’s choices lie in rP_r by (2). These choices are supported in X⊆UrX U_r, so κr(τ(t,σ′(t)))=τ(t,σ′(t)) _r(τ(t,σ (t)))=τ(t,σ (t)) by (1). The two transition kernels therefore agree on X, and neither play ever leaves X. Equal kernels on X give equal measures on cylinders, hence equal measures on plays. ∎ Note that, by part (4), on plays that stay in UrU_r the models ℳM and ℳrM_r are literally the same Markov chain, and CrC_r agrees with C there. So, such a play satisfies φ if and only if it satisfies (Cr) Parity(C_r). This is the only fact about the collapse that the correctness proofs use. G.4 Markov-chain lemmas Lemma 35 ((Sub/super)martingale decomposition). Let (σ,τ)(σ,τ) be positional, inducing a finite Markov chain with matrix P, and let ∈[0,1] u∈[0,1]^S. 1. If (P)(s)≥(s)(P u)(s)≥ u(s) for all s, then u is constant on every closed recurrent class ℛRC. Write ℛ u_RC for this value. Moreover, (s)≤∑ℛPrs[◊ℛ]ℛ u(s)≤ _RC _s[ ]\, u_RC for all s. 2. Symmetrically, if (P)(s)≤(s)(P u)(s)≤ u(s) for all s, then u is constant on every closed recurrent class and (s)≥∑ℛPrs[◊ℛ]ℛ u(s)≥ _RC _s[ ]\, u_RC. Moreover, in either case the defining inequality is an equality at every state of every closed recurrent class. Proof of Lemma 35. We prove (1); (2) is symmetric. Let ℛRC be a closed recurrent class with stationary distribution μ, so μ>0μ>0 on ℛRC and μ is supported on ℛRC. Since ℛRC is closed, ∑x∈ℛμ(x)(P)(x)=∑y∈ℛ(y)∑x∈ℛμ(x)P(x,y)=∑y∈ℛμ(y)(y) _x μ(x)(P u)(x)= _y u(y) _x μ(x)P(x,y)= _y μ(y) u(y) by stationarity. Comparing with the pointwise inequality (P)(x)≥(x)(P u)(x)≥ u(x) and using μ>0μ>0, every such inequality is an equality on ℛRC; thus u restricted to ℛRC is harmonic for an irreducible finite chain and is therefore constant. For the inequality, (Xn) u(X_n) is a bounded submartingale, so (s)≤[(Xn)] u(s) [ u(X_n)] for all n. The play is absorbed in some ℛRC almost surely and ≡ℛ u≡ u_RC there, so (Xn)→ℛ(π) u(X_n)→ u_RC(π) almost surely, and bounded convergence gives (s)≤∑ℛPrs[◊ℛ]ℛ u(s)≤ _RC _s[ ]\, u_RC. ∎ The next lemma states that a policy that is almost-sure winning for a prefix-independent objective on the whole almost-sure region can never be forced to leave it. Lemma 36 (Invariance of almost-sure regions). Let ℳ′M be an RMDP, let W=ℳ′(φ′)W= AS_M ( ) for a prefix-independent objective φ′ , and let σW _W be an agent policy that is almost-sure winning from every state of W. Then for every w∈Ww∈ W and every environment policy τ, PrwσW,τ[∀n:Xn∈W]=1 _W,τ_w[∀ n:X_n∈ W]=1. Proof of Lemma 36. Suppose towards a contradiction that under some τ the play from w leaves W with positive probability, and fix a history h of positive probability ending in a state s′∉Ws ∉ W. Let τ′τ be any environment policy and let τ′τ be the environment policy that behaves as τ along h and as τ′τ afterwards. Then h still has positive probability under (σW,τ′)( _W,τ ). Since σW _W is almost-sure winning from w, PrwσW,τ′[φ′]=1 _W,τ _w[ ]=1, and conditioning on the positive-probability event h and using prefix-independence of φ′ gives Prs′(σW)|h,τ′[φ′]=1 ^( _W)|_h,τ _s [ ]=1. As τ′τ was arbitrary, the shifted policy (σW)|h( _W)|_h is almost-sure winning from s′s , i.e. s′∈Ws ∈ W, a contradiction. ∎ Applied to the trap value-class RMDPs ℳrM_r, Lemma 36 yields the property of WrW_r announced in Section 4 and used throughout the correctness proofs below: the environment choices available in ℳrM_r cannot push the play out of WrW_r. Since ⊥∉Wr ∉ W_r, this single statement also says that the play cannot leave the value class UrU_r. Lemma 37 (Support in WrW_r). Assume I=∅I= , and let r<1r<1 with Ur≠∅U_r≠ . Then supp(q)⊆Wrsupp(q) W_r for every s∈Wrs∈ W_r and every q∈r(s,σr(s))q _r(s, _r(s)). In particular q(⊥)=0q( )=0, so no environment choice of ℳrM_r available against σr _r leaves UrU_r. Proof of Lemma 37. The objective (Cr) Parity(C_r) is prefix-independent and σr _r is almost-sure winning from every state of Wr⊆ℳr((Cr))W_r AS_M_r( Parity(C_r)), so Lemma 36 applied to ℳrM_r gives Prsσr,τ[∀n:Xn∈Wr]=1 _r,τ_s[∀ n:X_n∈ W_r]=1 for every environment policy τ of ℳrM_r. Were some q∈r(s,σr(s))q _r(s, _r(s)) to place positive mass outside WrW_r, the environment policy playing q at s would leave WrW_r with positive probability. ∎ Remark 38. The policy σr _r plays only tight actions on WrW_r: the only actions available at s∈Urs∈ U_r in ℳrM_r are the tight ones σ(s)A v^σ(s), which form a nonempty set because σ(s)σ(s) is tight by (7). G.5 Environment spoiling Proposition 39 (Environment spoiling on on value-class RMDPs). Let r<1r<1 with Ur≠∅U_r≠ and suppose Wr=ℳr((Cr))=∅W_r= AS_M_r( Parity(C_r))= . Then the environment has a positional policy τr _r on ℳrM_r such that Prsσ′,τr[(Cr)]=0 ^σ , _r_s[ Parity(C_r)]=0 for every agent policy σ′σ and every state s. Proof of Proposition 39. Write φr:=(Cr) _r:= Parity(C_r). The instance ℳrM_r is a linearly defined RMDP: at s∈Urs∈ U_r and a tight, r(s,a)=κr(σ(s,a))P_r(s,a)= _r(P v^σ(s,a)) is the image under a linear map of the face of (s,a)P(s,a) cut out by one additional linear inequality, hence a nonempty polytope, presented as the projection of a linear system in the variables (q,p)(q,p). Also, r(⊥,a)=δ⊥P_r( ,a)=\ _ \. Proposition 8 requires only that the uncertainty sets be nonempty bounded polytopes, and hence applies to ℳrM_r with objective φr _r. It yields that there exists a positional agent policy σ∗σ and a positional environment policy τr _r such that Prsσ∗,τr[φr]=sℳr(φr) ^σ , _r_s[ _r]= v^M_r_s( _r). We claim sℳr(φr)=0 v^M_r_s( _r)=0 for every s. Suppose not, and fix s0s_0 with s0ℳr(φr)>0 v^M_r_s_0( _r)>0. Being positional, (σ∗,τr)(σ , _r) induces a finite Markov chain over Ur∪⊥U_r∪\ \, so by (4) applied with the coloring CrC_r, sℳr(φr)=Prsσ∗,τr[φr]=∑ℛevenPrs[◊ℛ], v^M_r_s( _r)= ^σ , _r_s[ _r]= _RC\ even _s[ ], where “even” refers to maxCr(ℛ) C_r(RC). As s0ℳr(φr)>0 v^M_r_s_0( _r)>0, some even class ℛRC is reached with positive probability. Fix x∈ℛx . From x the chain stays in ℛRC almost surely, so xℳr(φr)=Prxσ∗,τr[φr]=1 v^M_r_x( _r)= ^σ , _r_x[ _r]=1. But σ∗σ secures the value, so infτPrxσ∗,τ[φr]=xℳr(φr)=1 _τ ^σ ,τ_x[ _r]= v^M_r_x( _r)=1, i.e. Prxσ∗,τ[φr]=1 ^σ ,τ_x[ _r]=1 for every environment policy τ of ℳrM_r. Thus σ∗σ is almost-sure winning from x in ℳrM_r, so x∈ℳr(φr)x∈ AS_M_r( _r), contradicting ℳr(φr)=∅ AS_M_r( _r)= . Therefore sℳr(φr)=0 v^M_r_s( _r)=0 for all s, and since τr _r attains the value, Prsσ′,τr[(Cr)]=0 ^σ , _r_s[ Parity(C_r)]=0 for every agent policy σ′σ and every state s. ∎ G.6 Correctness of the improvement steps Proof of Lemma 10. Write :=σ u:= v^σ. Fix a positional environment policy τ and let P be the matrix of the chain induced by (σ′,τ)(σ ,τ). For s∉Is∉ I we have σ′(s)=σ(s)σ (s)=σ(s) and, by (7), (P)(s)=τ(s,σ(s))⋅≥minp∈(s,σ(s))p⋅=s(P u)(s)=τ(s,σ(s))· u≥ _p (s,σ(s))p· u= u_s. For s∈Is∈ I, (P)(s)≥minp∈(s,σ′(s))p⋅=ν(s,σ′(s))=maxaν(s,a)>s(P u)(s)≥ _p (s,σ (s))p· u=ν(s,σ (s))= _aν(s,a)> u_s, since σ′(s)σ (s) maximises ν(s,⋅)ν(s,·). Hence u is a submartingale for P, and by Lemma 35(1) it is constant on every closed recurrent class ℛRC with (s)≤∑ℛPrs[◊ℛ]ℛ u(s)≤ _RC _s[ ]\, u_RC. First, no closed recurrent class meets I: on ℛRC the submartingale inequalities are equalities (Lemma 35), whereas at states of I the inequality is strict. Hence σ′=σ =σ on every closed recurrent class ℛRC. Second, every closed recurrent class ℛRC with ℛ>0 u_RC>0 is even. Let x∈ℛx and let τ~ τ be any environment policy of ℳσM^σ that agrees with τ on ℛRC. Since ℛRC is closed under the kernels of (σ,τ)(σ,τ) and σ′=σ =σ there, the play from x under (σ,τ~)(σ, τ) stays in ℛRC forever and satisfies φ with probability 11 if ℛRC is even and 00 if odd. But Prxσ,τ~[φ]≥infτ′Prxσ,τ′[φ]=xσ=ℛ>0 ^σ, τ_x[ ]≥ _τ ^σ,τ _x[ ]= v^σ_x= u_RC>0, so ℛRC is even. Combining with (4) and using that odd classes have ℛ=0 u_RC=0, Prsσ′,τ[φ]=∑ℛevenPrs[◊ℛ]≥∑ℛPrs[◊ℛ]ℛ≥s. ^σ ,τ_s[ ]= _RC\ even _s[ ]≥ _RC _s[ ]\, u_RC≥ u_s. Taking the infimum over positional τ, which by Proposition 8 applied to the RMC ℳσ′M^σ computes σ′ v^σ , gives σ′≥σ v^σ ≥ v^σ. For strictness at s∈Is∈ I: by (7) applied to ℳσ′M^σ and monotonicity of ↦minpp⋅ u _pp· u, sσ′=minp∈(s,σ′(s))p⋅σ′≥minp∈(s,σ′(s))p⋅σ v^σ _s= _p (s,σ (s))p· v^σ \ ≥\ _p (s,σ (s))p· v^σ =maxaminp∈(s,a)p⋅σ>sσ, = _a _p (s,a)p· v^σ> v^σ_s, where the last equality uses that σ′(s)σ (s) attains the outer maximum defining I. ∎ Proof of Lemma 11. Write :=σ u:= v^σ. Since I=∅I= , s=maxaminp∈(s,a)p⋅for all s, u_s= _a _p (s,a)p· u all s, (8) and the action σ(s)σ(s) attains it by (7); hence every action played by σ′σ is tight: σ(s)σ(s) is tight at s for every s, and σr(s) _r(s) is tight at s for every s∈Wrs∈ W_r by construction of ℳrM_r (Remark 38). Soundness. Fix a positional environment policy τ of ℳM with matrix P (for policy σ′σ ). Tightness gives (P)(s)≥s(P u)(s)≥ u_s for all s, so Lemma 35(1) applies. It suffices to show that every closed recurrent class ℛRC with ℛ>0 u_RC>0 is even. The bound Prsσ′,τ[φ]≥s ^σ ,τ_s[ ]≥ u_s then follows exactly as in Lemma 10, and taking the infimum over positional τ gives σ′≥σ v^σ ≥ v^σ. Let ℛRC be a closed recurrent class and put r:=ℛr:= u_RC. Since ≡r u≡ r on ℛRC we have ℛ⊆UrRC U_r, so CrC_r agrees with C on (π)=ℛ Inf(π)=RC. Moreover, by the last clause of Lemma 35 the submartingale inequality is an equality at every x∈ℛx , that is, τ(x,σ′(x))⋅=xτ(x,σ (x))· u= u_x. Since σ′(x)σ (x) is tight, this places τ(x,σ′(x))τ(x,σ (x)) in the tight face (x,σ′(x))P u(x,σ (x)). It is moreover supported in ℛRC, as ℛRC is closed. Hence Lemma 34(3), applied with X=ℛX=RC, identifies the play of ℳM from any x∈ℛx under (σ′,τ)(σ ,τ) with a play of ℳrM_r under (σ′,κr∘τ)(σ , _r τ) that never visits ⊥ . Two cases. Case 1: ℛ∩Wr=∅RC∩ W_r= . Then σ′=σ =σ on ℛRC, and the argument of Lemma 10 shows that if r>0r>0 then ℛRC is even. Case 2: ℛ∩Wr≠∅RC∩ W_r≠ . Let x∈ℛ∩Wrx ∩ W_r. At states of WrW_r the policy σ′σ plays σr _r, and by the previous paragraph the environment’s choices on ℛRC are, after κr _r, choices of ℳrM_r; hence Lemma 37 applies and every successor of a state of ℛ∩WrRC∩ W_r lies in WrW_r, while lying in ℛRC because ℛRC is closed. Thus the play from x never leaves ℛ∩WrRC∩ W_r, and since ℛRC is a recurrent class every state of ℛRC is visited almost surely, so ℛ⊆WrRC W_r and σ′σ follows σr _r throughout ℛRC. Consequently the play from x is a play of ℳrM_r consistent with σr _r, started in x∈ℳr((Cr))x∈ AS_M_r( Parity(C_r)). It therefore satisfies (Cr) Parity(C_r) almost surely. Now (π)=ℛ Inf(π)=RC almost surely, and Cr=C_r=C on ℛRC. Hence maxC(ℛ) C(RC) is even, i.e. ℛRC is even. This proves the claim, and exactly as in Lemma 10 we conclude σ′≥σ v^σ ≥ v^σ. Strictness on W. Let x∈Wrx∈ W_r, so x=r<1 u_x=r<1. By Proposition 8 applied to the RMC ℳσ′M^σ , fix a positional environment policy τ∗τ attaining σ′ v^σ simultaneously at all states, i.e. tσ′=Prtσ′,τ∗[φ] v^σ _t= ^σ ,τ _t[ ] for all t. Call a state t loose if τ∗(t,σ′(t))⋅>tτ (t,σ (t))· u> u_t and let L be the set of loose states. Observe that since σ′(t)σ (t) is tight, a state t is loose if τ∗(t,σ′(t))τ (t,σ (t)) lies off the tight face (t,σ′(t))P u(t,σ (t)). Let T be the first time the play started at x visits L. Note that T=∞\T=∞\ is exactly the event that the play never visits L. We first show that Pr[φ∣T=∞]=1 [ T=∞]=1 whenever Pr[T=∞]>0 [T=∞]>0. Before the play visits L, the environment’s choices lie on tight faces, so their κr _r-images are available in ℳrM_r by Lemma 34(2). Since σ′=σrσ = _r on WrW_r, Lemma 37 keeps the play inside Wr⊆UrW_r U_r. In particular Xn∈WrX_n∈ W_r for every n≤Tn≤ T, and for every n when T=∞T=∞. Define an environment policy τ~ τ of ℳrM_r by τ~(t,a):=κr(τ∗(t,a)) τ(t,a):= _r(τ (t,a)) whenever t∈Wr∖Lt∈ W_r L and a is tight at t (legal precisely because t is not loose) and by an arbitrary element of r(t,a)P_r(t,a) otherwise. By Lemma 34(3) the chains induced by (σ′,τ∗)(σ ,τ ) in ℳM and by (σ′,τ~)(σ , τ) in ℳrM_r assign the same measure to every set of paths from x avoiding L, since their kernels agree at every state of Wr∖LW_r L. Under (σr,τ~)( _r, τ) the play from x stays in WrW_r and satisfies (Cr) Parity(C_r) almost surely, hence also φ almost surely, as it never visits ⊥ and Cr=C_r=C on UrU_r. Therefore Prxσ′,τ∗[T=∞∩¬φ]=Prxσ′,τ~[T=∞∩¬φ]=0 ^σ ,τ _x[\T=∞\∩ ]= ^σ , τ_x[\T=∞\∩ ]=0, which is the claim. If L=∅L= then T=∞T=∞ almost surely and xσ′=Prxσ′,τ∗[φ]=1>r v^σ _x= ^σ ,τ _x[ ]=1>r, as required. Otherwise set ε:=minτ∗(t,σ′(t))⋅−t|t∈L> 0, := \\,τ (t,σ (t))· u- u_t\ |\ t∈ L\, \\;>\;0, a minimum over at most |||S| states. On T<∞\T<∞\ we have XT∈Wr∩LX_T∈ W_r∩ L, hence (XT)=r u(X_T)=r, and the step taken at time T gives [(XT+1)∣T<∞]=τ∗(XT,σ′(XT))⋅≥r+ε.E[ u(X_T+1) \,T<∞]=τ (X_T,σ (X_T))· u\ ≥\ r+ . By the strong Markov property, prefix-independence of φ , and Prtσ′,τ∗[φ]=tσ′≥tσ=t ^σ ,τ _t[ ]= v^σ _t≥ v^σ_t= u_t (soundness) for the positional continuation from any state t, Pr[φ∣T<∞]=[σ′(XT+1)∣T<∞]≥[(XT+1)∣T<∞]≥r+ε. [ T<∞]=E [ v^σ (X_T+1) T<∞ ]\ ≥\ E [ u(X_T+1) T<∞ ]\ ≥\ r+ . Combining, since xσ′=Prxσ′,τ∗[φ] v^σ _x= ^σ ,τ _x[ ], xσ′≥Pr[T=∞]⋅1+Pr[T<∞]⋅(r+ε)≥min1,r+ε>r=x, v^σ _x\ ≥\ [T=∞]· 1+ [T<∞]·(r+ )\ ≥\ \1,\,r+ \\ >\ r= u_x, the last inequality because r<1r<1. ∎ G.7 Optimality of fixpoints, termination, and complexity Theorem 40 (Optimality of fixpoints). Let σ be a positional agent policy whose value vector σ v^σ satisfies (i) sσ=maxaminp∈(s,a)p⋅σ v^σ_s= _a _p (s,a)p· v^σ for all s (equivalently I=∅I= ), and (i) Wr=ℳr((Cr))=∅W_r= AS_M_r( Parity(C_r))= for every value r<1r<1 of σ v^σ. Then σ=ℳ(φ) v^σ= v^M( ) and σ is optimal. Moreover an optimal positional environment policy exists, obtained by combining, on each value class of value <1<1, the environment’s spoiling policies of the value-class RMDPs (Proposition 39) with value-minimising choices elsewhere. Proof of Theorem 40. Write :=σ u:= v^σ. Since u is guaranteed by σ against every environment policy, ℳ(φ)≥ v^M( )≥ u pointwise, it remains to find a single environment policy τ τ with Prsσ′,τ^[φ]≤sfor every agent policy σ′ and every s. ^σ , τ_s[ ]≤ u_s every agent policy σ and every s. (9) Indeed, (9) gives sℳ(φ)≤s=sσ≤sℳ(φ) v^M_s( )≤ u_s= v^σ_s≤ v^M_s( ), so σ=ℳ(φ) v^σ= v^M( ), the policy σ is optimal (it attains u), and τ τ attains infτsupσ′ _τ _σ and is an optimal environment policy by Proposition 8. Construction of τ τ. By (i) and Proposition 39, for every value r<1r<1 of u the environment has a positional policy τr _r on ℳrM_r that spoils the trap objective uniformly: Prsσ′,τr[(Cr)]=0 ^σ , _r_s[ Parity(C_r)]=0 for every agent policy σ′σ and every state s of ℳrM_r. Equivalently, against τr _r the play in ℳrM_r almost surely either reaches ⊥ or remains in UrU_r forever and violates the original parity condition there. Define the positional environment policy τ τ of ℳM at each pair (s,a)(s,a): • if s∈Urs∈ U_r for some r<1r<1 and a is tight at s: by Lemma 34(2) pick ps,a∈(s,a)p_s,a u(s,a) with κr(ps,a)=τr(s,a) _r(p_s,a)= _r(s,a) and let τ^(s,a):=ps,a τ(s,a):=p_s,a. This is the uncollapsed form of the choice prescribed by τr _r, and it is a legal environment choice of ℳM; • otherwise (a not tight at s, or s=1 u_s=1): let τ^(s,a)∈argminp∈(s,a)p⋅ τ(s,a)∈ _p (s,a)p· u, which is nonempty because (s,a)P(s,a) is a nonempty compact polytope. In all cases τ^(s,a)⋅≤s τ(s,a)· u≤ u_s: for a tight action, by definition, ps,a⋅=sp_s,a· u= u_s, the dot product being taken over the original vector u, i.e. before the collapse and hence including the states outside UrU_r. For a non-tight action minpp⋅<s _pp· u< u_s by (i). Finally, if s=1 u_s=1 then trivially p⋅≤1p· u≤ 1. Proof of (9). Fix a starting state s. With τ τ fixed and positional, the agent faces an ordinary MDP, which by Remark 28 admits a positional optimal agent policy for the parity objective. So, it suffices to bound Prsσ′,τ^[φ] ^σ , τ_s[ ] for positional σ′σ . Let P be the matrix of the finite Markov chain induced by (σ′,τ^)(σ , τ). By what was discussed before and the definition of τ τ, (P)(t)≤t(P u)(t)≤ u_t for all t, so u is a supermartingale and by Lemma 35(2) it is constant on every closed recurrent class ℛRC, with s≥∑ℛPrs[◊ℛ]ℛ u_s≥ _RC _s[ ]\, u_RC. Claim: every even closed recurrent class ℛRC has ℛ=1 u_RC=1. Suppose instead ℛ=r<1 u_RC=r<1; then ℛ⊆UrRC U_r. On ℛRC the supermartingale inequalities are equalities, so for every x∈ℛx the action a=σ′(x)a=σ (x) is tight (a non-tight action gives a strict decrease) and hence τ^(x,a)=px,a τ(x,a)=p_x,a is the uncollapsed tight-face choice prescribed by τr _r. As ℛRC is closed, these choices are supported in ℛ⊆UrRC U_r, so Lemma 34(3) with X=ℛX=RC identifies the play from x under (σ′,τ^)(σ , τ), which stays in ℛRC forever with probability 11, with a play of ℳrM_r under τr _r that never reaches ⊥ . By the spoiling guarantee of τr _r such a play violates (Cr) Parity(C_r) almost surely, and since it never leaves UrU_r, where Cr=C_r=C, it violates φ almost surely. As (π)=ℛ Inf(π)=RC almost surely, maxC(ℛ) C(RC) is odd, contradicting that ℛRC is even. This proves the claim. By (4) and the claim, Prsσ′,τ^[φ]=∑ℛ evenPrs[◊ℛ]=∑ℛ evenPrs[◊ℛ]ℛ≤∑ℛPrs[◊ℛ]ℛ≤s, ^σ , τ_s[ ]= _RC even _s[ ]= _RC even _s[ ]\, u_RC≤ _RC _s[ ]\, u_RC≤ u_s, which is (9). The optimal environment policy τ τ is positional and has exactly the announced structure: uncollapsed tight-face (spoiling) choices inside each value class of value <1<1, and value-minimising choices elsewhere. ∎ Proof of Theorem 12. If (ℳ,σ)≠σ Improve(M,σ)≠σ, then by Lemma 10 or Lemma 11 we have σ′≥σ v^σ ≥ v^σ with strict inequality in at least one coordinate. The value vectors are thus strictly increasing in the product order along the run, so no positional policy is visited twice and the loop terminates within the number of positional agent policies, |||||A|^|S|. On termination σ is a fixpoint: I=∅I= and Wr=∅W_r= for every value r<1r<1, the conditions of Theorem 40. By Theorem 40 the returned policy is optimal and σ=ℳ(φ) v^σ= v^M( ). ∎ Theorem 41 (Complexity). PI performs at most |||||A|^|S| iterations. One iteration solves O(||3+||⋅||)O(|S|^3+|S|·|A|) linear programs, each of size polynomial in |ℳ||M|, performs at most |||S| almost-sure parity computations on polytopic RMDPs of description size O(|ℳ|)O(|M|), and performs O(||2⋅||)O(|S|^2·|A|) additional bookkeeping. Consequently, writing TAS(n)T_AS(n) for the cost of one almost-sure parity computation on an instance of size n, one iteration runs in time poly(|ℳ|)+||⋅TAS(O(|ℳ|))poly(|M|)+|S|· T_AS(O(|M|)), and the whole algorithm in time ||||⋅(poly(|ℳ|)+||⋅TAS(O(|ℳ|)))|A|^|S|· (poly(|M|)+|S|· T_AS(O(|M|)) ). Proof of Theorem 41. The iteration bound is Theorem 12. Consider one call to Improve. Line 1 computes the parity value vector of the linearly defined RMC ℳσM^σ. By Theorem 7 and its proof this takes O(||3)O(|S|^3) linear programs: computing the almost-sure violation set Wodd=()W_odd= OddEC(S) performs O(||3)O(|S|^3) feasibility and maximisation programs (Lemma 5), and the safety program (⋆)( ), which has O(||2)O(|S|^2) variables and polynomially many constraints, is solved once per source state. Note that the cubic bound of Lemma 5 covers the whole nested recursion of OddEC and MecDecomp, and is not the cost of one MEC decomposition multiplied by the number of OddEC nodes: taking the two recursions together, there are at most |||S| levels, the sets processed at any fixed level are pairwise disjoint, and one invocation of (B) MecDecomp(B) costs only O(|B|2)O(|B|^2) linear programs (Theorem 18), so each level costs O(||2)O(|S|^2) programs and the total is O(||3)O(|S|^3) rather than O(||4)O(|S|^4), See the proof of Lemma 5 in Appendix E. Lines 2–4 solve exactly ||⋅|||S|·|A| linear programs, one per pair (s,a)(s,a), each of them a minimisation of a linear functional over the facet description of (s,a)P(s,a). Line 5 and the switch of line 8 are O(||⋅||)O(|S|·|A|) comparisons. This accounts for the O(||3+||⋅||)O(|S|^3+|S|·|A|) programs of the statement; each has size polynomial in |ℳ||M| and is therefore solvable in time polynomial in |ℳ||M|. The loop of lines 11–15 is entered at most |||S| times, once per nonempty value class of value <1<1. Each iteration of the loop assembles ℳrM_r and CrC_r and performs one almost-sure parity computation. The assembly needs no further optimisation. Indeed ℳrM_r has state set Ur∪⊥U_r∪\ \. The actions available at s∈Urs∈ U_r are the tight ones, obtained by comparing the already computed ν(s,a)ν(s,a) with sσ v^σ_s. The colors are inherited from C on UrU_r, with the single fresh odd color 2⌈d/2⌉+12 d/2 +1 at ⊥ and each uncertainty set is r(s,a)=q|∃p:As,ap≤bs,a,p⋅σ≤sσ,q=κr(p),P_r(s,a)= \\,q\ |\ ∃ p:\ A_s,a\,p≤ b_s,a,\ \ p· v^σ≤ v^σ_s,\ \ q= _r(p)\, \, a linear system in (q,p)(q,p) built from the description of (s,a)P(s,a) by adding one inequality and the defining equalities of κr _r. Note that the optima ν(s,a)ν(s,a) enter only through the tightness test: the uncertainty sets themselves are described using σ v^σ alone. Two consequences for the size. First, each ℳrM_r has description size O(|ℳ|)O(|M|) and is written down in time O(|ℳ|)O(|M|). Second, and more sharply, the value classes are pairwise disjoint and ℳrM_r contains only the states of UrU_r, so ∑r<1|ℳr|=O(|ℳ|) _r<1|M_r|=O(|M|): the instances handed to the almost-sure parity procedure during one iteration have total description size O(|ℳ|)O(|M|). Hence the cost of the loop is ∑r<1TAS(|ℳr|)≤||⋅TAS(O(|ℳ|)) _r<1T_AS(|M_r|)≤|S|· T_AS(O(|M|)) plus O(|ℳ|)O(|M|) bookkeeping. Grouping the identification of the value classes, the patching of line 17 and the comparisons above gives the stated O(||2⋅||)O(|S|^2·|A|) bookkeeping, and multiplying by the iteration bound gives the overall running time. ∎ Remark 42 (Space of the almost-sure subroutine). The almost-sure parity procedure of Asadi et al. (2026b) runs in polynomial space, and it is this property that underlies the third item of Theorem 12. Concretely, the procedure is a recursion of depth at most |||S| that stores, at each frame, only a subset of the state space together with O(log||)O( |S|) counters. That is, O(||)O(|S|) bits per frame and O(||2)O(|S|^2) bits over the whole stack, and whose only other work consists of feasibility and optimisation queries against the linear descriptions of the uncertainty sets. Each such query is a linear program of size polynomial in the encoding of the instance, hence solvable in polynomial time and polynomial space, and the space it occupies is released before the next query is issued. The recursion therefore uses polynomial space in total, even though its running time is only quasi-polynomial. Remark 43. A reachability objective () Reach(T) is the parity objective of the coloring that assigns color 22 to the (absorbing) target states and color 11 elsewhere, so our algorithm applies unchanged. For this coloring the qualitative improvement never happens: every value class with r<1r<1 contains no target state, so every state of UrU_r has odd color 11 in C and every state outside UrU_r has the fresh dominating odd color in CrC_r; hence all states are odd-colored under CrC_r and ℳr((Cr))=∅ AS_M_r( Parity(C_r))= automatically. Appendix H Additional Experimental Details Benchmarks. We evaluate both algorithms on three benchmarks. Garnet and Inventory Management support both objectives; Frozen Lake supports only reachability. • Garnet. The N states are partitioned into k+1k+1 disjoint subsets G0,…,GkG_0,…,G_k (we fix k=5k=5), with G0G_0 holding half of the states and containing the initial state s0s_0. Every state has three actions, each leading to m=⌈N⌉m= N distinct successors drawn uniformly at random without replacement. For a state in GiG_i with i>0i>0, all successors are drawn from within GiG_i, so the subset is never left. For a state in G0G_0, the successors are drawn from within G0G_0, but each action additionally diverts a small random fraction of its probability mass to a uniformly random state of a uniformly random subset among G1,…,GkG_1,…,G_k; this is how an action taken in G0G_0 can leave G0G_0 and enter another subset. The nominal transition distribution over the successors of every state–action pair is drawn uniformly from the probability simplex (i.e., Dirichlet(1,…,1)Dirichlet(1,…,1)), and is then wrapped in an L∞L_∞ or L1L_1 uncertainty ball of radius 0.5/m0.5/m or 0.10.1, respectively. For the reachability objective, each subset independently contains one target state and one trap state, and the goal is to reach the target state of some subset. For the parity objective, every state is assigned a color (priority) drawn uniformly from 1,…,|Gi|\1,…,|G_i|\, and the goal is to satisfy the induced parity condition. In the scaling experiments the branching factor is coupled to the size, m=⌈N⌉m= N , so that larger instances are also denser. • Inventory Management. The state is the stock level s∈0,…,Ns∈\0,…,N\ of a warehouse of capacity N. At each step the agent orders a∈0,…,amaxa∈\0,…,a_ \ new units, the demand d∈0,…,dmaxd∈\0,…,d_ \ materializes, and the stock moves deterministically to s′=s+a−ds =s+a-d. If the demand exceeds the available stock (d>s+ad>s+a), or the delivery pushes the stock over the capacity (s+a−d>Ns+a-d>N), the run instead ends in one of two absorbing failure states. We fix dmax=⌈N⌉d_ = N and amax=⌈0.75dmax⌉a_ = 0.75\,d_ , so the number of possible demand values, and hence the branching factor, is m=dmax+1=Θ(N)m=d_ +1= ( N). The nominal demand distribution over 0,…,dmax\0,…,d_ \ is a lightly perturbed uniform (each outcome is weighted by an independent U[0.75,1.25]U[0.75,1.25] factor and the weights are then normalized), drawn independently per state, and is wrapped in an L∞L_∞ or L1L_1 uncertainty ball of radius δ=0.25/mδ=0.25/m or 0.10.1, respectively. Both objectives use a threshold K drawn from U[0.35,0.65]⋅NU[0.35,0.65]· N. Starting from s0=0s_0=0, the reachability objective is to bring the stock up to s≥Ks≥ K, and the parity objective is to keep the stock at s≥Ks≥ K infinitely often. Both objectives also share a second threshold T, drawn uniformly from dmax,…,K\d_ ,…,K\, which governs a larger order option: once the stock reaches s≥Ts≥ T, an additional order of dmaxd_ units becomes available to the agent on top of the amounts 0,…,amax\0,…,a_ \. • Frozen Lake. The agent walks on a k×k× k grid from the top-left cell toward the bottom-right target cell, so the state count is N=k2N=k^2. Each move goes in the intended direction or in one of the two perpendicular directions with probability 13 13 each, giving a branching factor of m≤3m≤ 3 (cut down at the grid’s border). A random 20%20\% of the cells are holes, which are absorbing failure states. The nominal move distribution of each state is wrapped in an L∞L_∞ or L1L_1 uncertainty ball whose radius is drawn per state from U[0,0.125]U[0,0.125] or U[0,0.25]U[0,0.25], respectively. Because the branching factor stays bounded by 33 regardless of N, this benchmark scales to much larger state spaces than the other two. On Frozen Lake we experiment only with the reachability objective (reaching the target cell). Remark 44. The bounds of Theorem 18 and Theorem 41 are worst-case upper bounds on the number of primitive queries against the uncertainty sets, and on all of our benchmarks the number actually issued is considerably smaller. The gap is not incidental, and it is not a property of the particular instances: it follows from the branching factor, and it applies to any family of linearly defined RMDPs whose uncertainty sets are described over few coordinates. We record it here because it is what reconciles the cubic bound of Theorem 41 with the measured solve times of Figure 1. Remark 45. Figure 2 records how many iterations our algorithm and the baseline take on each benchmark. For both of them, the observed counts remain well below the theoretical worst case, which is exponential in the number of states. This agrees with what is commonly reported for policy iteration on stochastic games, where the iteration count is typically polynomial in practice even though no subexponential bound is known. The practical behaviour of our algorithms is thus considerably better than the worst-case analysis predicts. Figure 2: Comparison between number of iterations of the policy iteration algorithm on our benchmarks. The number of iterations is much smaller than the theoretical worst-case bound.