# Verification of indefinite-horizon POMDPs

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

## Key facts

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

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

- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [Reinforcement Learning under Partial Observability Guided by Learned Environment Models](https://mlsanity.com/paper/2206.11708/) (2022)
- [Learning Explainable and Better Performing Representations of POMDP Strategies](https://mlsanity.com/paper/2401.07656/) (2024)
- [Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives](https://mlsanity.com/paper/2406.02871/) (2024)
- [On the Verification of Belief Programs](https://mlsanity.com/paper/2204.12562/) (2022)
- [Explainable Representation of Finite-Memory Policies for POMDPs using Decision Trees](https://mlsanity.com/paper/2411.13365/) (2024)
- [Robustness Analysis of POMDP Policies to Observation Perturbations](https://mlsanity.com/paper/2604.21256/) (2026)
- [Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning](https://mlsanity.com/paper/2605.14440/) (2026)

## Abstract (arXiv)

The verification problem in MDPs asks whether, for any policy resolving the nondeterminism, the probability that something bad happens is bounded by some given threshold. This verification problem is often overly pessimistic, as the policies it considers may depend on the complete system state. This paper considers the verification problem for partially observable MDPs, in which the policies make their decisions based on (the history of) the observations emitted by the system. We present an abstraction-refinement framework extending previous instantiations of the Lovejoy-approach. Our experiments show that this framework significantly improves the scalability of the approach.