What is Decidable about Partially Observable Markov Decision Processes with {\omega}-Regular Objectives

TL;DR

This paper investigates the decidability of qualitative analysis problems in POMDPs with -regular (parity) objectives, establishing decidability and complexity results for strategies with finite memory.

Contribution

It proves the decidability of qualitative analysis for POMDPs with all parity objectives under finite-memory strategies, with optimal complexity bounds.

Findings

Decidability of qualitative analysis for POMDPs with parity objectives.

EXPTIME-completeness of the analysis problems.

Optimal exponential memory bounds for strategies.

Abstract

We consider partially observable Markov decision processes (POMDPs) with {\omega}-regular conditions specified as parity objectives. The class of {\omega}-regular languages extends regular languages to infinite strings and provides a robust specification language to express all properties used in verification, and parity objectives are canonical forms to express {\omega}-regular conditions. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satis- fied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite- memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives.