PaperlayerView exact revision on arXiv

Source-linked AI summary

Quantitative Analysis of $ω$-Regular Robust MDPs

Ali Asadi, Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Alipasha Montaseri, Ali Shafiee

arXiv:2608.25968v1cs.AI

TL;DR

The paper addresses exact quantitative parity analysis for rectangular RMDPs with linearly defined uncertainty sets, extending prior qualitative analyses that cannot distinguish policies without almost-sure guarantees. It develops polynomial-time robust-chain analysis and a policy-iteration algorithm, showing that pure memoryless optimal policies exist for both players and computing exact values.

  • Problem

    Prior qualitative analyses do not distinguish among policies when no almost-sure guarantee exists, motivating exact quantitative analysis of parity objectives in RMDPs.

  • Method

    The paper combines a polynomial-time quantitative parity algorithm for robust Markov chains with policy iteration using quantitative one-step and qualitative almost-sure improvements.

  • Results

    The algorithms compute exact values and admit pure stationary memoryless optimal policies for both the agent and the environment.

  • Takeaways & Limitations

    Quantitative parity analysis is tractable in polynomial space for the studied RMDPs, with the decision problem in NP ∩coNP and hardness matching turn-based stochastic parity games.

  • Takeaways & Limitations

    The approach assumes every uncertainty set is linearly defined, including standard L1 and L∞ balls and more general polytopic sets.

Abstract

from arXiv · show

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 $ω$-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.

1 Introduction

The paper studies quantitative parity analysis for rectangular RMDPs with linearly defined uncertainty sets, extending robust optimization to logical correctness objectives. It addresses the open problem of computing exact satisfaction values and presents policy, algorithmic, and experimental contributions.

  • Robust MDPs: Linearly defined uncertainty sets use linear inequalities with existentially quantified auxiliary variables and subsume L1, L∞, and general polytopic uncertainty sets.Auxiliary variables provide succinct descriptions, including for L1 balls whose projection onto transition probabilities alone can have exponentially many facets.
  • Parity and ω-Regular Objectives: Parity objectives represent ω-regular requirements such as safety, reachability, and liveness in robust probabilistic systems.A deterministic parity automaton can be combined with an RMDP to form a product RMDP with a parity objective.
  • Quantitative Analysis: Qualitative almost-sure and positive analyses do not distinguish policies when no almost-sure guarantee exists, leaving quantitative analysis open.The quantitative problem computes values and supports optimal-policy selection beyond yes-or-no guarantees.
  • Contributions: The paper gives a polynomial-time robust-chain algorithm, a policy-iteration method with memoryless optimal policies, and experiments against explicit stochastic-game reduction.Policy iteration combines quantitative one-step improvements with qualitative almost-sure improvements.
  • Related Work: The policy-improvement method works directly with uncertainty polytopes instead of constructing the exponentially larger stochastic game.The robust setting ranges over continua of distributions, rather than only finitely many game vertices.

2 Preliminaries and Model Description

The preliminaries define MDP, RMDP, policy, value, and parity semantics, then state the linearly defined uncertainty-set model and the quantitative parity problem. The section establishes that standard norm balls and general polytopes fit the assumed representation.

  • MDPs and MCs: An MDP specifies finite states, actions, and transition distributions, while a Markov chain is an MDP with a singleton action set.Policies determine action choices and induce probability distributions over infinite paths.
  • RMDPs and RMCs: An RMDP assigns each state-action pair a set of possible transition distributions selected by an environment policy.The environment must choose a distribution from the corresponding uncertainty set after observing the agent’s state-action history.
  • Policies: Positional policies are deterministic and memoryless, and fixing one agent policy induces a robust Markov chain.A positional agent policy is a state-to-action function.
  • Objectives and Values: Parity accepts infinite paths whose maximum color occurring infinitely often is even, and ω-regular objectives reduce to parity objectives.The coloring function maps states to a finite set of colors.
  • Model Assumption: A linearly defined uncertainty set is a projection of a polyhedron onto transition-probability coordinates with existential auxiliary variables.The assumption includes standard L1 and L∞ balls and more general polytopic uncertainty sets.
  • Problem Statement: The quantitative parity problem asks for the value of every state in a linearly defined RMDP with a parity objective.The RMC algorithm introduced later serves as a subprocedure for the RMDP algorithm.

3 Quantitative RMC Analysis Sub-Procedure

The robust Markov-chain subprocedure solves safety and parity quantitatively in polynomial time. It uses flow-based linear programming for safety and maximal-end-component analysis to reduce parity to safety.

  • Safety Analysis: Safety values in linearly defined robust Markov chains are computed with a single linear program based on reachability-flow characterization.The formulation uses expected state visits and edge traversals, with non-negativity, conservation, splitting, and admissibility constraints.
  • Safety Analysis: The admissibility constraint becomes linear by multiplying the uncertainty inequalities by the nonnegative visit variable.This removes the denominator from the flow proportion and preserves inequality direction.
  • Safety Analysis: Safety values and optimal positional environment policies can be computed in polynomial time.The LP optimum equals the safety value for the fixed initial state.
  • Parity Analysis: The parity procedure computes states Wodd from which the environment can violate parity almost surely, then evaluates safety for the complement.OddEC recursively analyzes maximal end-components according to their dominant colors.
  • Parity Analysis: OddEC computes Wodd in polynomial time using maximal-end-component decomposition.MEC decomposition exploits the polytopic structure of the uncertainty sets.
  • Parity Analysis: Parity values and optimal positional environment policies for linearly defined robust Markov chains are computable in polynomial time.The parity value is obtained from the safety LP instantiated with Wodd as the unsafe set.

Quantitative Analysis of ω-Regular RMDPs

The paper establishes positional optimality for both players and develops a policy-iteration algorithm for quantitative parity in linearly defined RMDPs. The algorithm combines quantitative one-step and qualitative almost-sure improvements, terminates after polynomially many improvement calls, and uses polynomial space.

  • Policy Iteration: The policy-iteration algorithm starts from an arbitrary positional agent policy and repeatedly applies Improve until no policy change occurs.At each iteration, the algorithm computes the current value vector and attempts quantitative or qualitative improvement.
  • Positional Determinacy: Positional agent and environment policies suffice for optimality in linearly defined RMDPs with parity objectives.The result follows from a value-preserving reduction to finite turn-based stochastic parity games, although that reduction can be exponentially large.
  • Complexity: The quantitative value decision problem lies in NP ∩ coNP and is at least as hard as the corresponding problem for turn-based stochastic parity games.A polynomial-time solution would also solve turn-based stochastic parity games, whose complexity remains unresolved in the cited passage.
  • Policy Improvement: Quantitative improvement switches actions when a worst-case one-step value strictly exceeds the current state value.The procedure evaluates ν(s, a) = min_p∈P(s,a) p·vσ and changes actions at states where an improvement exists.
  • Policy Improvement: Qualitative improvement analyzes value classes using tight actions and tight faces, then invokes an almost-sure parity procedure on each constructed subproblem.A fresh terminal state with a dominating odd color represents exits from the value class; successful improvements switch the policy on the corresponding states.
  • Correctness and Complexity: Each Improve call either returns a strictly better policy or the same policy, so policy iteration terminates and returns an optimal positional policy.The algorithm terminates after at most |A||S| calls to Improve and runs in polynomial space.

5 Experimental Results

Experiments compare the proposed method with a stochastic-game baseline across benchmark families, uncertainty norms, objectives, and increasing state spaces. The proposed method scales better when branching factors grow, while the baseline is faster when branching is small.

  • Experimental Setup: The experiments compare both algorithms on quantitative parity and reachability objectives across Garnet, Inventory Management, and Frozen Lake benchmarks.Garnet and Inventory Management support both objectives; Frozen Lake supports reachability only, with L1 and L∞ uncertainty balls.
  • Experimental Setup: Figure 1 reports solve time versus state-space size, using means over 10 seeds, standard-deviation bands, and a 120-second timeout.Panels separate benchmarks by columns and L1 versus L∞ uncertainty by rows.
  • Results: When branching grows with instance size, our algorithm scales substantially better than the baseline across both norms and both objectives.This behavior is reported for Garnet and Inventory Management.
  • Results: At the largest sizes where the baseline completes, our algorithm is faster by roughly one to two orders of magnitude and solves instances up to n ≈1200 on Inventory.The baseline exceeds the timeout at a few hundred states, whereas the proposed method solves substantially larger instances.
  • Results: With fixed branching m ≤3, the baseline is roughly an order of magnitude faster on Frozen Lake and scales beyond n ≈10^4.The reduced stochastic game remains close in size to the original RMDP, while the proposed linear-programming solver adds overhead.
  • Results: The observed iteration counts are smaller than the theoretical worst-case exponential bound, although the experiments do not establish polynomial iteration complexity.The paper attributes the gap to behavior commonly observed for policy iteration on stochastic games.

6 Conclusion and Future Works

The paper develops exact quantitative parity analysis for rectangular RMDPs with linearly defined uncertainty sets and identifies both computational results and open extensions. Its approach supports standard norm balls and general projected polytopes without explicitly expanding uncertainty sets into game vertices.

  • Conclusion: The paper computes exact quantitative parity values for (s,a)-rectangular RMDPs with linearly defined uncertainty sets.The setting includes uncertainty sets represented by linear inequalities over transition distributions and auxiliary variables.
  • Conclusion: The robust Markov-chain algorithm casts robust safety as an occupation-measure linear program and reduces parity analysis through maximal-end-component analysis.The resulting algorithm is polynomial-time for the robust Markov-chain case.
  • Conclusion: The RMDP policy-iteration method combines quantitative one-step improvements with qualitative almost-sure improvements and computes exact values with optimal positional policies for both players.The algorithm runs in polynomial space.
  • Open Questions: The decision problem is in NP ∩ coNP and is as hard as turn-based stochastic parity games, while polynomial-time exact value computation remains open.Future directions include nonlinear convex uncertainty, weaker rectangularity assumptions, and learning uncertainty sets from samples.
  • Related Work: Unlike the explicit stochastic-game reduction, the robust improvement procedure works directly with uncertainty polytopes and avoids constructing an exponentially larger game.It uses value classes, tight actions, and tight faces.
  • Uncertainty Sets: The method handles L∞, L1, and general projected polytopes through linear constraints and scaled auxiliary variables.Auxiliary variables provide succinct descriptions for uncertainty sets such as L1 balls.

C Proofs of Lemma 2 and Theorem 3

The proof establishes a polynomial qualitative preprocessing step and characterizes admissible environment behavior through occupation flows. These ingredients connect safety values to reachability of absorbing value-one states and support the linear-program formulation.

  • Setup: The environment uncertainty at each state is represented by a positional policy selecting a distribution from the state’s admissible polytope.The robust Markov chain has one action, so only the environment chooses transitions.
  • Qualitative Preprocessing: Qualitative preprocessing computes value-one and value-zero state sets in polynomial time and makes them absorbing without changing safety values elsewhere.Value-one states are safe under every policy, while some policy is unsafe almost surely from value-zero states.
  • Occupation Measures: The resulting optimal occupation measure has finite expected visits in unresolved states, and safety coincides with reaching the value-one absorbing set.This permits safety probability to be represented through occupation flows.
  • Optimal Policy Structure: For an optimal positional environment policy, every reachable bottom strongly connected component intersects the absorbing value-zero or value-one sets.Otherwise, a reachable component contained in the unresolved states would permit a policy switch that lowers safety probability, contradicting optimality.
  • Flow Characterization: At each state, nonnegative outgoing flows with the correct total mass and scaled uncertainty constraints are equivalent to flow induced by an admissible transition distribution.This equivalence also covers the zero-occupation case.

C.4 Proof of Lemma 2

The proof shows that the occupation-measure linear program exactly matches the robust safety value. It proves both directions by converting optimal policies to feasible occupations and feasible solutions back to positional policies.

  • Upper Bound: An optimal positional environment policy has a finite occupation measure that satisfies the program’s nonnegativity, conservation, splitting, and admissibility constraints.Its objective equals the probability of reaching the value-one absorbing set, which equals its robust safety probability.
  • Lower Bound: Every feasible program solution defines a positional environment policy by normalizing positive outgoing flows and choosing an arbitrary admissible distribution at zero-flow states.The flow characterization guarantees that the resulting policy is valid.
  • Lower Bound: The induced policy reproduces the feasible state occupancies by induction and reaches the absorbing value-zero or value-one sets almost surely.Finite occupation follows from the feasible solution’s constraints.
  • Lower Bound: After absorption, selecting safe behavior in value-one states and unsafe-almost-sure behavior in value-zero states makes safety equivalent to reaching the value-one set.Therefore the robust safety value is at most the program optimum, completing equality with the reverse inequality.
  • Conclusion: The program optimum equals the robust safety value from the initial state.This equality is obtained by combining the two inequalities.

C.5 Proof of Theorem 3

The proof establishes polynomial-time computability of robust safety values and corresponding optimal positional policies using polynomial-size linear programs.

  • The sets S=1 and S=0 are computable in polynomial time, with safety values 1 and 0 respectively.
  • The program (⋆) has O(|S|^2) variables and polynomially many constraints under the stated assumption.
  • Solving (⋆) once per source state computes all remaining safety values in polynomial time.
  • The computation also yields corresponding optimal positional policies.

D MecDecomp Procedure for Computing MEC Decompositions of RMCs

MecDecomp computes maximal end-components by repeatedly removing states that cannot remain closed, then splitting the remainder into strongly connected components. Linear-programming queries implement both operations and give an overall polynomial-time procedure.

  • Definitions: An end-component is a nonempty closed set whose internal transition graph is strongly connected; a MEC is maximal under inclusion.
  • Procedure: MecDecomp removes states with no admissible distribution supported inside the current candidate, then recursively processes its strongly connected components.
  • LP primitives: Closure feasibility is tested by linear programs, while graph edges are identified by maximizing each possible successor probability.
  • LP primitives: The resulting internal graph’s strongly connected components are computed with Tarjan’s algorithm in linear graph time.
  • Correctness: MECs are pairwise disjoint, and the recursive decomposition returns exactly the MECs contained in the input set.
  • Complexity: A single call performs O(|B|^2) LP queries excluding recursion, while the complete algorithm uses O(|S|^3) queries and runs in polynomial time.

E Proofs of Lemmas 5 and 6

The proofs characterize parity violations through end-components with odd dominant colors. They construct Wodd, show that violations are equivalent in value to reaching Wodd, and derive a polynomial-time safety reduction.

  • Odd end-components: From every state in Wodd, a positional policy can keep the process inside Wodd while enforcing an odd dominant color almost surely.
  • Reaching Wodd: Every parity-violating play under a positional environment policy reaches Wodd except on a null event.
  • Odd end-components: Wodd contains exactly the states lying in end-components whose dominant color is odd.
  • Complexity: The combined recursion analysis avoids an apparent O(|S|^4) bound by counting MEC-decomposition calls level by level.
  • Value reduction: The environment’s maximal probability of violating parity equals its maximal probability of reaching Wodd.
  • Value reduction: The parity value therefore equals the safety value of Safe(S \ Wodd), computable with an optimal positional environment policy in polynomial time.

F Proof of Proposition 8 and Corollary 9

The proof reduces a linearly defined robust MDP to a finite turn-based stochastic parity game by replacing each uncertainty polytope with its vertices. The reduction preserves values and supports positional-strategy conclusions.

  • Polytope reduction: Each linearly described uncertainty set is a bounded polytope whose admissible distributions are convex combinations of finitely many vertices.
  • Game construction: The finite game has agent vertices, environment vertices for state-action pairs, and probabilistic vertices for chosen uncertainty-polytope vertices.
  • Game construction: The agent selects an action, the environment selects a polytope vertex, and probability sampling determines the next state.
  • Play projection: Auxiliary game vertices receive color 0, so projecting a game play onto states preserves the maximal color occurring infinitely often and thus the parity outcome.
  • Strategy correspondence: Randomized choices among polytope vertices realize exactly the original uncertainty set, while pure vertex choices realize individual extreme-point distributions.
  • Value preservation: The game and robust MDP have equal parity values, and the one-player correspondence preserves positional policies.

F.4 Proof of Proposition 8

The vertex-game construction establishes positional determinacy for linearly defined RMDPs: both players have optimal pure memoryless policies, and the optimization orders coincide. It also supports the complexity characterization that quantitative parity lies in NP ∩ coNP and is at least as hard as stochastic-game parity.

  • Positional determinacy: Optimal agent and environment policies can both be chosen positional, with the environment selecting vertices of uncertainty polytopes.The vertex-game strategies map back to a positional agent policy and a positional environment policy using vertex distributions.
  • Positional determinacy: The RMDP is determined: supσ infτ equals infτ supσ for every state and parity objective.The mapped strategies preserve one-step distributions and values between the vertex game and the RMDP.
  • Complexity: Positional certificates have polynomial size, including rational encodings of environment-selected uncertainty-polytope vertices.Vertex membership is decidable in polynomial time for linearly defined uncertainty sets.
  • Complexity: RMDP-Parity belongs to NP ∩ coNP, using positional agent and environment policies as certificates.Verification reduces to constructing an induced robust Markov chain or ordinary MDP and comparing its exactly computed value with the threshold.
  • Complexity: SG-Parity reduces polynomially to RMDP-Parity, because stochastic games are special cases whose uncertainty sets are convex hulls of Dirac distributions.Thus the robust problem inherits the stochastic-game lower bound and the associated NP ∩ coNP barrier.

G.5 Environment spoiling

Environment spoiling is analyzed on value-class RMDPs by combining almost-sure regions, tight actions, and invariant supports. When the relevant almost-sure winning region is empty, a positional environment policy forces parity violation with probability one.

  • Environment spoiling: If the almost-sure winning region Wr is empty for a value class r < 1, a positional environment policy spoils parity uniformly.The policy achieves probability zero for every agent policy and every state in the value-class RMDP.
  • Environment spoiling: The spoiling proof uses recurrent classes: positive parity value would imply an even recurrent class and hence an almost-sure winning state, contradicting Wr = ∅.The contradiction establishes zero quantitative value throughout the trap instance.
  • Environment spoiling: Quantitative policy improvement preserves or increases the agent value by using tight actions and the submartingale structure of the current value vector.Closed recurrent classes with positive value must be even, while states in the improved region receive strict improvement.
  • Environment spoiling: For a state of value r < 1, visiting a loose state creates an expected increase of at least ε, yielding a value strictly above r.If loose states are never visited, the induced value-class policy gives parity satisfaction with probability one; otherwise the ε gain proves strictness.

G.7 Optimality of fixpoints, termination, and complexity

The paper characterizes optimal fixpoints through absent quantitative and almost-sure improvements, then proves policy iteration terminates and returns an optimal policy. Its complexity is bounded by the number of positional agent policies and calls to the almost-sure parity subroutine.

  • Optimality of fixpoints: A positional policy is optimal when no quantitative improvement exists and every value class below one has an empty almost-sure winning region.These are the two fixpoint conditions used to invoke the optimality theorem.
  • Optimality of fixpoints: The constructed optimal environment policy uses spoiling tight-face choices in value classes below one and value-minimizing choices elsewhere.This single positional policy bounds every agent policy by the current value vector and attains the RMDP value.
  • Termination: Policy iteration terminates after at most |A|^|S| iterations because value vectors strictly increase whenever the agent policy changes.No positional agent policy is revisited, and termination yields a fixpoint satisfying the optimality conditions.
  • Complexity: One iteration solves O(|S|^3 + |S| · |A|) linear programs and performs at most |S| almost-sure parity computations.Its time is poly(|M|) + |S| · TAS(O(|M|)), while the full algorithm multiplies this by the iteration bound.
  • Complexity: The almost-sure subroutine uses polynomial space, with recursion depth at most |S| and O(|S|^2) bits over its stack.Reachability is handled unchanged as a parity objective with target states colored 2 and other states colored 1.

H Additional Experimental Details

Experiments cover Garnet, Inventory Management, and Frozen Lake, using reachability and parity objectives where applicable. Across benchmarks, observed policy-iteration behavior is substantially better than worst-case bounds, including fewer iterations and primitive queries.

  • Benchmarks: The evaluation uses Garnet and Inventory Management for both reachability and parity, while Frozen Lake supports only reachability.
  • Garnet: Garnet partitions states into k + 1 subsets, with transitions mostly contained within subsets and additional diversions from G0 to other subsets.The construction fixes k = 5 and gives every state three actions with randomly generated successors.
  • Inventory Management: Inventory Management models warehouse stock with ordering and demand decisions, with overstock and unmet-demand outcomes mapped to absorbing failure states.The demand branching factor scales as m = Θ(N), and both objectives use a threshold K drawn from U[0.35, 0.65] · N.
  • Frozen Lake: Frozen Lake has branching factor at most 3 regardless of N, allowing it to scale to larger state spaces than Garnet and Inventory Management.The benchmark includes randomly placed absorbing failure holes and is evaluated only on reachability.
  • Results: Observed iteration counts for the proposed algorithm and baseline remain well below the exponential theoretical worst case.The experiments also issue considerably fewer primitive uncertainty-set queries than worst-case bounds, with the gap attributed to small branching descriptions.
Loading 2608.25968v1…