Ensuring Logic in the Fog: Sound POMDP Synthesis with LTL Objectives
Can Zhou, Yulong Gao, Pian Yu

TL;DR
This paper introduces a sound reward-shaping method for POMDPs with LTL objectives, enabling reliable synthesis of autonomous agents in uncertain environments.
Contribution
It presents a novel belief-dependent reward mechanism integrated into Monte Carlo Planning, ensuring verifiable LTL satisfaction in partially observable settings.
Findings
Effective in scenarios where existing solvers fail
Maintains scalability across diverse benchmarks
Enhances agent navigation under partial observability
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
