Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes
This addresses the challenge of reliable autonomous operation under partial observability for robotics and AI systems, representing an incremental improvement in policy synthesis methods.
The paper tackles the problem of synthesizing policies for autonomous systems to satisfy linear temporal logic formulas in partially observable Markov decision processes (POMDPs), using point-based value iteration to approximate maximum satisfaction probabilities and compute policies, demonstrating scalability to large domains with strong performance bounds.
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.