# Ensuring Logic in the Fog: Sound POMDP Synthesis with LTL Objectives

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 27 references that are in the map.
- First posted on arXiv 12 May 2026.

## Builds on (most cited first, 7 of 7)

- [What is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives](https://mlsanity.com/paper/1309.2802/) (2013)
- [Enforcing Almost-Sure Reachability in POMDPs](https://mlsanity.com/paper/2007.00085/) (2020)
- [Stochastic Finite State Control of POMDPs with LTL Specifications](https://mlsanity.com/paper/2001.07679/) (2020)
- [Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications](https://mlsanity.com/paper/1409.3360/) (2014)
- [Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes](https://mlsanity.com/paper/2001.03809/) (2020)
- [Optimal Control of Partially Observable Markov Decision Processes with Finite Linear Temporal Logic Constraints](https://mlsanity.com/paper/2203.09038/) (2022)
- [Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processes](https://mlsanity.com/paper/2305.14736/) (2023)

## Abstract (arXiv)

Synthesising autonomous agents that can navigate uncertain environments while adhering to complex temporal constraints remains a fundamental challenge. While Linear Temporal Logic (LTL) provides a rigorous language for specifying such tasks, the inherent undecidability of qualitatively verifying LTL satisfaction in partially observable Markov decision processes renders quantitative synthesis difficult, especially when designing reliable reward signals for approximate solvers. In this paper, we bridge this gap with a novel, sound reward-shaping mechanism that dynamically generates belief-dependent rewards grounded in certified LTL satisfaction. By integrating this mechanism into an enhanced Monte Carlo Planning framework, we empower agents to navigate the `fog' of partial observability with a search process focused on maximising verifiable success. Our experiments demonstrate that this approach not only thrives in scenarios where existing solvers fail but also maintains effectiveness and scalability across diverse benchmark domains.