Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives

TL;DR

This paper introduces a new class of POMDPs with a revelation mechanism that ensures almost sure eventual full information, leading to exact algorithms for deciding omega-regular objectives in these models.

Contribution

The paper defines weakly and strongly revealing POMDP classes and provides exact, finite-belief MDP-based algorithms for their analysis, expanding decidability results.

Findings

Decidable classes of POMDPs with omega-regular objectives identified

Exact algorithms based on finite belief-support MDPs developed

Revelation mechanism ensures almost sure full information acquisition

Abstract

Partially observable Markov decision processes (POMDPs) form a prominent model for uncertainty in sequential decision making. We are interested in constructing algorithms with theoretical guarantees to determine whether the agent has a strategy ensuring a given specification with probability 1. This well-studied problem is known to be undecidable already for very simple omega-regular objectives, because of the difficulty of reasoning on uncertain events. We introduce a revelation mechanism which restricts information loss by requiring that almost surely the agent has eventually full information of the current state. Our main technical results are to construct exact algorithms for two classes of POMDPs called weakly and strongly revealing. Importantly, the decidable cases reduce to the analysis of a finite belief-support Markov decision process. This yields a conceptually simple and exact algorithm for a large class of POMDPs.