Qualitative Analysis of $\omega$-Regular Objectives on Robust MDPs

TL;DR

This paper develops efficient algorithms for qualitative analysis of $$-regular objectives in robust MDPs, enabling verification of reachability and parity objectives under uncertainty without structural assumptions.

Contribution

It introduces oracle-based algorithms for qualitative analysis of reachability and parity objectives in RMDPs, applicable to large, unstructured models.

Findings

Algorithms effectively solve qualitative problems in large RMDPs

Experimental results demonstrate scalability to thousands of states

Approach works without assumptions on RMDP structure

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 $\omega$-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.