Strategy Synthesis in POMDPs via Game-Based Abstractions

TL;DR

This paper introduces an abstraction refinement framework that converts POMDPs into probabilistic games, enabling efficient strategy synthesis with safety guarantees for large planning problems involving partial observability.

Contribution

It presents a novel method to approximate POMDP strategies through game-based abstractions, improving scalability and safety guarantees over existing approaches.

Findings

Handles problems several orders-of-magnitude larger than existing solvers.

Provides safety guarantees not available in most current POMDP solvers.

Uses abstraction refinement to improve strategy quality iteratively.

Abstract

We study synthesis problems with constraints in partially observable Markov decision processes (POMDPs), where the objective is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Verification and strategy synthesis for POMDPs are, however, computationally intractable in general. We alleviate this difficulty by focusing on planning applications and exploiting typical structural properties of such scenarios; for instance, we assume that the agent has the ability to observe its own position inside an environment. We propose an abstraction refinement framework which turns such a POMDP model into a (fully observable) probabilistic two-player game (PG). For the obtained PGs, efficient verification and synthesis tools allow to determine strategies with optimal safety and performance measures, which approximate optimal schedulers on the POMDP. If the approximation is too coarse to satisfy the given specifications, an refinement scheme improves the computed strategies. As a running example, we use planning problems where an agent moves inside an environment with randomly moving obstacles and restricted observability. We demonstrate that the proposed method advances the state of the art by solving problems several orders-of-magnitude larger than those that can be handled by existing POMDP solvers. Furthermore, this method gives guarantees on safety constraints, which is not supported by the majority of the existing solvers.