Quantitative Analysis of $ω$-Regular Robust MDPs | AI Research

This paper addresses the quantitative analysis of Robust Markov Decision Processes (RMDPs) with $\omega$-regular objectives, specifically focusing on parity objectives. While previous research established methods for qualitative analysis—determining if a policy guarantees satisfaction with probability one or zero—the exact quantitative problem of calculating the maximum satisfaction probability against an adversarial environment remained unsolved. The authors provide a polynomial-time solution for this problem in RMDPs with linearly defined uncertainty sets.

Solving the Quantitative Parity Problem

The authors define the quantitative value of a state as the supremum of satisfaction probabilities an agent can guarantee against any adversarial environment policy. To solve this, they first analyze Robust Markov Chains (RMCs), which are RMDPs where the agent has only one available action. They formulate a polynomial-size linear program that characterizes the flow of probability mass through the system. By combining this with an analysis of end-components—subsets of states where the environment can force the system to remain—they successfully compute the exact satisfaction probability for parity objectives in polynomial time.

Policy-Iteration for RMDPs

For full RMDPs, where the agent can choose between multiple actions, the authors introduce a policy-iteration algorithm. They establish that both the agent and the environment possess pure memoryless optimal policies. The algorithm functions by iteratively evaluating the RMC induced by the current agent policy. Each iteration applies either a quantitative one-step improvement or a qualitative almost-sure improvement, eventually terminating with the exact value vector and optimal policies for both the agent and the environment.

Linearly Defined Uncertainty

The research focuses on $(s,a)$-rectangular RMDPs using linearly defined uncertainty sets. These sets are described by linear inequalities over transition distributions and auxiliary variables. This approach is significant because it captures standard $L_1$ and $L_\infty$ balls as well as general polytopic uncertainty sets. By using auxiliary variables, the authors maintain a succinct representation of these sets, avoiding the exponential growth in constraints that would occur if the sets were described solely by transition probabilities.

Experimental Performance

The authors implemented their algorithms to test reachability and parity objectives under $L_1$ and $L_\infty$ uncertainty. Their experiments compared the new approach against an explicit reduction to stochastic games. The results indicate that the proposed method scales more effectively on the Garnet and Inventory benchmarks, where the branching factor increases with the size of the instance. Conversely, the explicit reduction method proved faster on the Frozen Lake benchmark, which features a smaller branching factor. The authors note that their method avoids constructing the exponentially larger games required by previous approaches, instead working directly with the linearly defined uncertainty sets.