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

arXiv: https://arxiv.org/abs/2001.03809 · HTML: https://mlsanity.com/paper/2001.03809/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Jan 2020.

## Built on by (most cited first, 8 of 8)

- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [Symbolic Reinforcement Learning for Safe RAN Control](https://mlsanity.com/paper/2103.06602/) (2021)
- [Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processes](https://mlsanity.com/paper/2305.14736/) (2023)
- [Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives](https://mlsanity.com/paper/2406.02871/) (2024)
- [Model-free Motion Planning of Autonomous Agents for Complex Tasks in Partially Observable Environments](https://mlsanity.com/paper/2305.00561/) (2023)
- [Safe RAN control: A Symbolic Reinforcement Learning Approach](https://mlsanity.com/paper/2106.01977/) (2021)
- [Control Synthesis in Partially Observable Environments for Complex Perception-Related Objectives](https://mlsanity.com/paper/2507.02942/) (2025)
- [Ensuring Logic in the Fog: Sound POMDP Synthesis with LTL Objectives](https://mlsanity.com/paper/2605.12581/) (2026)

## Abstract (arXiv)

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.