---
title: "Quantitative Analysis of ω-Regular Robust MDPs"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2608.25968v1"
permalink: "https://feed.astralor.com/items/itm_8ac7262dc192da9350dc8fe0"
published: "2026-08-26T16:26:13.000Z"
score: 79
channel: "ai"
tags: ["ω-regular Objectives","Parity Objectives","Policy Iteration","Stochastic Games","Robust MDP"]
---

# Quantitative Analysis of ω-Regular Robust MDPs

## AI commentary

> This paper pushes the analysis of RMDPs from qualitative to quantitative, a substantial step for formal verification. It is worth reading for researchers working on robust planning, safe reinforcement learning, and automata-based verification. The combination of policy iteration with qualitative improvements is also inspiring.

## At a glance

This paper studies the quantitative analysis of parity objectives in (s,a)-rectangular Robust Markov Decision Processes (RMDPs) with linearly defined uncertainty sets. The authors show that both the agent and the environment admit pure memoryless optimal policies. They then propose a policy iteration algorithm that combines quantitative one-step improvements with qualitative almost-sure improvements, yielding a polynomial-time algorithm for quantitative parity on linearly defined robust Markov chains. Experiments demonstrate that this approach outperforms an explicit reduction to stochastic games. This work extends prior qualitative results to the exact quantitative setting, providing a foundation for verifying ω-regular properties in robust decision-making systems.

## Key points

- Proves that both agent and environment admit pure memoryless optimal policies in robust MDPs.
- Proposes a policy iteration algorithm combining quantitative one-step and qualitative almost-sure improvements.
- Achieves polynomial-time solving of quantitative parity on linearly defined robust Markov chains.
- Experiments show the algorithm outperforms explicit reduction to stochastic games.

## Full text

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.

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_8ac7262dc192da9350dc8fe0