One-sentence Summary

Researchers from LaBRI, IRIF, and University of Antwerp introduce a revelation mechanism for POMDPs that requires almost sure eventual full observability of the current state, defining weakly and strongly revealing classes in which the almost-sure satisfaction of $\omega$ω-regular objectives becomes decidable by reducing to finite belief-support MDPs.

Key Contributions

• A revelation mechanism is introduced for POMDPs that requires the agent to almost surely obtain full information about the current state eventually, defining weakly and strongly revealing classes where almost-sure strategy existence for given specifications becomes decidable.

• Exact algorithms are constructed for these classes by reducing the problem to a finite belief-support Markov decision process, using a belief-support update function to track possible states and extending reachability and Büchi objectives to sets of belief supports.

• The analysis shows that finite-memory strategies suffice, specifically memoryless strategies on the belief-support MDP that are optimal under the revealing assumptions, and it places these decidable classes near undecidability frontiers such as priority classes {0, 1, 2} versus {1, 2, 3}.

Introduction

Partially observable Markov decision processes are a central model for sequential decision making under uncertainty, but designing exact strategies that guarantee omega-regular specifications is often undecidable, so much prior work relies on approximate planning or empirical reinforcement learning. The authors leverage a finite belief-support MDP abstraction, which tracks only the set of possible current states and ignores probabilities, but show that this abstraction is generally unsound and incomplete because small probability differences can accumulate into information loss that changes almost-sure outcomes. Their main contribution is a revelation mechanism, studied in weak and strong forms, which requires the agent to regain full state information with probability 1 and thereby prevents unbounded accumulation of uncertainty. They prove decidability and undecidability boundaries under these restrictions, show that the decidable cases can be solved by analyzing the belief-support MDP, and provide a simple proof-of-concept algorithm that outperforms tuned deep reinforcement learning baselines on their experiments.

Method

The proposed approach treats almost-sure omega-regular strategy synthesis for POMDPs as a finite abstraction problem. A POMDP is given as $\mathcal{P} = (Q, \mathsf{Act}, \mathsf{Sig}, \delta, q_0)$P=(Q,Act,Sig,δ,q0​), where the agent selects actions from $\mathsf{Act}$Act, observes signals from $\mathsf{Sig}$Sig, and evolves according to the probabilistic transition function $\delta$δ. Because the true state is partially observable, the agent’s relevant knowledge can be summarized by a belief support, which records the set of states that remain possible given the observed signal history.

The central algorithmic module is the belief-support MDP. For a belief support $b$b and an action $a$a, a successor belief support $b'$b′ can be reached with positive probability if there exists a signal $s$s such that the belief-support update yields $b'$b′, i.e.

The belief-support MDP $\mathcal{P}_B$PB​ has as states all non-empty subsets of $Q$Q, keeps the same actions, and assigns uniform probability to successors with positive probability. This construction abstracts away the exact probability distribution inside a belief support while preserving the structure of possible observable histories.

Strategies can also be lifted from the belief-support MDP back to the original POMDP. Given an observable history $h = a_1 s_1 \ldots a_n s_n$h=a1​s1​…an​sn​, one can compute the induced sequence of belief supports and form the belief-support history

If $\sigma_B$σB​ is a strategy in $\mathcal{P}_B$PB​, then the corresponding POMDP strategy is defined by

Thus, once a winning strategy is found in the finite abstraction, it can be executed in the original partially observable system by tracking the belief support during play.

The abstraction alone, however, is not sound in general because it ignores how probability mass can concentrate or vanish over time. A simple counterexample shows that a belief-support MDP may appear winning under a naive priority lifting even when the original POMDP has no almost-sure strategy. This failure is caused by the loss of quantitative information when the belief is compressed into a support. A minimal counterexample is shown below.

To repair this abstraction, the authors introduce revealing semantics. A revelation occurs when the belief support collapses to a singleton set, meaning that the current state has been identified with certainty. Formally, the set of singleton belief supports is

A POMDP is weakly revealing if, for every strategy, singleton belief supports are reached infinitely often with probability one:

Intuitively, weak revealing ensures that the agent is not permanently trapped in uncertainty about the current state. POMDPs with infinitely often observable resets are one natural source of weak revealing behavior. For such POMDPs, the abstract belief-support MDP becomes analytically useful, especially when priorities are lifted using the maximal priority semantics

The key soundness result is that, for weakly revealing POMDPs, if a strategy wins almost surely in the belief-support MDP under this priority extension, then the lifted strategy also wins almost surely in the original POMDP. Since memoryless pure strategies are sufficient for parity objectives in MDPs, the algorithm can search a finite abstract space while preserving almost-sure guarantees.

The abstraction is not only sound but also complete for restricted parity priorities. When priorities are in $\{0,1,2\}${0,1,2}, the existence of an almost-sure strategy in a weakly revealing POMDP is equivalent to the existence of an almost-sure strategy in its belief-support MDP. Because the belief-support MDP has exponential size in the number of POMDP states and parity games on MDPs are solvable in polynomial time, this yields an EXPTIME algorithm for the problem.

Completeness does not extend to all priority functions. For priorities in $\{1,2,3\}${1,2,3}, the belief-support abstraction may reject a POMDP that nevertheless admits an almost-sure strategy. The following example illustrates a weakly revealing POMDP whose belief-support MDP has no winning strategy, although the original POMDP does.

In this example, the agent returns infinitely often to an observable initial state $q_0$q0​ through a dedicated signal. From $q_0$q0​, one action leads to a belief support containing two possible states, both giving a maximal odd priority at the support level, while the other action leads to states that separate the good and bad outcomes. The belief-support MDP sees only the maximal priority of each support and therefore concludes that no winning strategy exists. The original POMDP can succeed because repeated observations can make the agent arbitrarily confident that it is in one branch rather than the other. If the agent repeatedly plays the first action and observes $s_1$s1​ $n$n times in a row, then the conditional probability of being in the desired branch approaches one:

By increasing $n$n round by round, the agent can ensure that the desirable state is visited infinitely often while the bad state is visited only finitely often. Generalizing this construction yields undecidability for almost-sure strategy existence when priorities are in $\{1,2,3\}${1,2,3}.

A stronger condition, strong revealing, restores decidability for arbitrary parity objectives. For a state $q$q, a revealing signal is one that guarantees the next state is $q$q:

A POMDP is strongly revealing if, whenever a transition from $q$q to $q'$q′ is possible under an action, it can also occur with a revealing signal for $q'$q′. Under this condition, singleton belief supports are visited infinitely often for every strategy, so strong revealing implies weak revealing. The property can be checked by scanning transitions, making it polynomial-time decidable in the description size of the POMDP. For strongly revealing POMDPs, the belief-support MDP analysis is both sound and complete for all parity objectives, again yielding EXPTIME-completeness.

One illustrative strongly revealing construction is based on a tiger-style environment. The agent can listen for noisy observations, but the environment is augmented with rare revealing signals that identify the true state with certainty when they occur. These signals give the belief-support abstraction enough information to guarantee eventual disclosure of the hidden state. The modified tiger POMDP is shown below.

The method can also be interpreted as defining an optimistic semantics for all POMDPs. Given an arbitrary POMDP, one can construct an extended POMDP in which every transition has a small probability of emitting an additional signal that reveals the next state. This extended POMDP is strongly revealing. If the extended POMDP has no almost-sure strategy for an omega-regular objective, then the original POMDP also has no almost-sure strategy for that objective. This transforms the revealing results into a sufficient criterion for negative answers even when the original model is not explicitly revealing.

In the implemented proof of concept, the algorithm is compared against off-the-shelf deep reinforcement learning systems trained on an observation wrapper that maintains the current belief support on the fly. The wrapper implements the subset-construction update, so the learning agents receive belief-support states rather than raw observations. The agents are trained with a simple reward scheme where good events yield reward $100$100 and bad events yield reward $-1$−1, using default hyperparameters for a limited number of interaction steps. The evaluation metric tracks, for omega-regular specifications, the number of steps since the last bad event that has not yet been trumped by a future good event. A lower value indicates better satisfaction of the long-run specification. The comparison plot below reports the evolution of this quantity across simulations.