Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives (Extended Abstract)
Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives (Extended Abstract)
Marius Belly, Nathanaƫl Fijalkow, Hugo Gimbert, Florian Horn, Guillermo A. Perez, Pierre Vandenhove
Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence
Sister Conferences Best Papers. Pages 8221-8226.
https://doi.org/10.24963/ijcai.2026/916
Partially observable Markov decision processes (POMDPs) form a prominent model for uncertainty in sequential decision making. We are interested in constructing algorithms with theoretical guarantees to determine whether the agent has a strategy ensuring a given specification with probability 1. This well-studied problem is known to be undecidable already for very simple omega-regular objectives, because of the difficulty of reasoning on uncertain events.
We introduce a revelation mechanism which restricts information loss by requiring that, almost surely, the agent has eventually full information about the current state. Our main technical results are to construct exact algorithms for two classes of POMDPs called weakly and strongly revealing. Importantly, the decidable cases reduce to the analysis of a finite belief-support Markov decision process. This yields a conceptually simple and exact algorithm for a large class of POMDPs.
Keywords:
Agent-based and Multi-agent Systems: Formal verification, validation and synthesis
Planning and Scheduling: POMDPs
