Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Qualitative Analysis of $ω$-Regular Objectives on Robust MDPs

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

TL;DR

The paper addresses qualitative analysis of ω-regular objectives on robust MDPs without structural assumptions, focusing on reachability and parity guarantees with probability 1. It introduces oracle-based algorithms that leverage force and attractor constructs to decide almost-sure reachability and parity, achieving polynomial or quasi-polynomial oracle complexity and extending applicability beyond polytopic uncertainty sets. Empirical evaluation on benchmarks with thousands of states demonstrates the practicality and scalability of the approach, outperforming policy-iteration baselines in reachability and providing competitive parity results. This work advances robust, logic-based planning under uncertainty by delivering tractable, oracle-driven methods for strong correctness guarantees in complex, uncertain environments.

Abstract

Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for $ω$-regular objectives. The qualitative analysis problem asks whether the objective can be ensured with probability 1. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are twofold. We first present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives. We then report experimental results demonstrating the effectiveness of our oracle-based approach on classical RMDP examples from the literature scaling up to thousands of states.

Qualitative Analysis of $ω$-Regular Objectives on Robust MDPs

TL;DR

The paper addresses qualitative analysis of ω-regular objectives on robust MDPs without structural assumptions, focusing on reachability and parity guarantees with probability 1. It introduces oracle-based algorithms that leverage force and attractor constructs to decide almost-sure reachability and parity, achieving polynomial or quasi-polynomial oracle complexity and extending applicability beyond polytopic uncertainty sets. Empirical evaluation on benchmarks with thousands of states demonstrates the practicality and scalability of the approach, outperforming policy-iteration baselines in reachability and providing competitive parity results. This work advances robust, logic-based planning under uncertainty by delivering tractable, oracle-driven methods for strong correctness guarantees in complex, uncertain environments.

Abstract

Robust Markov Decision Processes (RMDPs) generalize classical MDPs that consider uncertainties in transition probabilities by defining a set of possible transition functions. An objective is a set of runs (or infinite trajectories) of the RMDP, and the value for an objective is the maximal probability that the agent can guarantee against the adversarial environment. We consider (a) reachability objectives, where given a target set of states, the goal is to eventually arrive at one of them; and (b) parity objectives, which are a canonical representation for -regular objectives. The qualitative analysis problem asks whether the objective can be ensured with probability 1. In this work, we study the qualitative problem for reachability and parity objectives on RMDPs without making any assumption over the structures of the RMDPs, e.g., unichain or aperiodic. Our contributions are twofold. We first present efficient algorithms with oracle access to uncertainty sets that solve qualitative problems of reachability and parity objectives. We then report experimental results demonstrating the effectiveness of our oracle-based approach on classical RMDP examples from the literature scaling up to thousands of states.
Paper Structure (45 sections, 14 theorems, 29 equations, 2 figures, 2 tables, 9 algorithms)

This paper contains 45 sections, 14 theorems, 29 equations, 2 figures, 2 tables, 9 algorithms.

Table of Contents

  1. Introduction
  2. Robust Markov Decision Processes.
  3. Quantitative vs Logical Objectives.
  4. Quantitative vs Qualitative Analysis.
  5. Contributions.
  6. Technical Novelty.
  7. Related Works on Robust MDPs.
  8. Related Works on $\omega$-regular and Qualitative Analysis.
  9. Model Definition and Preliminaries
  10. MDPs.
  11. Robust MDPs.
  12. Operations over RMDPs.
  13. Policy Types.
  14. Remark.
  15. Objectives and Values.
  16. ...and 30 more sections

Key Result

Lemma 3.0

Given an RMDP $\mathcal{M} = (\mathcal{S}, \mathcal{A}, \mathcal{P})$ with oracles $\mathit{force}^\mathcal{M}_\mathscr{A}$ and $\mathit{force}^\mathcal{M}_\mathscr{E}$ and a target set $T \subseteq \mathcal{S}$, the following assertions holds:

Figures (2)

  • Figure 1: Running example for our algorithms.
  • Figure 2: Runtime comparison of our parity algorithms on the Frozen Lake Model.

Theorems & Definitions (21)

  • Lemma 3.0
  • Lemma 3.0
  • Theorem 3.1
  • Lemma 3.1
  • Theorem 3.2
  • Remark 3.3
  • Corollary 3.3
  • Lemma 3.0
  • proof
  • Lemma 4.0
  • ...and 11 more