Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes

TL;DR

This paper introduces a point-based approach for synthesizing policies in POMDPs that satisfy linear temporal logic specifications, enabling efficient planning in complex, partially observable environments.

Contribution

It presents a novel methodology combining point-based value iteration with logical specification satisfaction in POMDPs, scalable to large domains.

Findings

Efficient approximation of maximum satisfaction probability

Scalability to large POMDPs

Strong performance bounds on policies

Abstract

Autonomous systems are often required to operate in partially observable environments. They must reliably execute a specified objective even with incomplete information about the state of the environment. We propose a methodology to synthesize policies that satisfy a linear temporal logic formula in a partially observable Markov decision process (POMDP). By formulating a planning problem, we show how to use point-based value iteration methods to efficiently approximate the maximum probability of satisfying a desired logical formula and compute the associated belief state policy. We demonstrate that our method scales to large POMDP domains and provides strong bounds on the performance of the resulting policy.