A PSPACE Algorithm for Almost-Sure Rabin Objectives in Multi-Environment MDPs

TL;DR

This paper establishes that deciding almost-sure Rabin objectives in multi-environment MDPs is PSPACE-complete, providing clarity on the computational complexity of these problems in uncertain, multi-environment settings.

Contribution

It proves PSPACE-completeness for almost-sure Rabin objectives in MEMDPs, contrasting with the higher complexity or undecidability in related models.

Findings

PSPACE-completeness result for MEMDPs with Rabin objectives

Complexity landscape clarified for multi-environment MDPs

Contrasts with POMDPs where problems are harder or undecidable

Abstract

Markov Decision Processes (MDPs) model systems with uncertain transition dynamics. Multiple-environment MDPs (MEMDPs) extend MDPs. They intuitively reflect finite sets of MDPs that share the same state and action spaces but differ in the transition dynamics. The key objective in MEMDPs is to find a single policy that satisfies a given objective in every associated MDP. The main result of this paper is PSPACE-completeness for almost-sure Rabin objectives in MEMDPs. This result clarifies the complexity landscape for MEMDPs and contrasts with results for the more general class of partially observable MDPs (POMDPs), where almost-sure reachability is already EXPTIME-complete, and almost-sure Rabin objectives are undecidable.