Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives (Extended Abstract)

1 Introduction

Partially observable Markov decision processes (POMDPs) form a prominent model for uncertainty in sequential decision making. They were defined in the 1960s [ ˚Astr¨om, 1965] for operations research and introduced in artificial intelligence by the seminal paper [Kaelbling et al., 1998]. We consider POMDPs from a model-based point of view common in planning and in formal methods. Our goal is to construct exact (as opposed to approximate) algorithms that take as input a complete description of the POMDP and construct a strategy ensuring a given specification. A long line of work has established that most formulations of this problem are undecidable. For instance, even in the extreme case where the agent has no information and the goal is to reach a target state with arbitrarily high probability, complex convergence phenomena occur, implying strong undecidability results [Madani et al., 2003; Gimbert and Oualhadj, 2010; Fijalkow, 2017].

∗Extended abstract of the eponymous paper from the proceedings of AAAI 2025 [Belly et al., 2025].

In this work, we are interested in constructing almostsure strategies, meaning strategies ensuring the specification with probability 1. We consider the class of omegaregular objectives (all expressible as parity objectives), which is a robust class including properties expressible in Linear Temporal Logic [Pnueli, 1977; Giacomo and Vardi, 2013; Bloem et al., 2018]. Determining whether there exists an almost-sure strategy for the subclass of CoB¨uchi objectives (requiring to avoid a target from some point onwards) is undecidable [Chatterjee et al., 2016; Bertrand et al., 2017]. There is a vast body of work towards approximate and practical solutions: for instance, using interpolation in the belief space [Lovejoy, 1991], approximation of the value function [Hauskrecht, 2000], or Monte Carlo tree search approaches [Silver and Veness, 2010]. This is orthogonal to the current paper since we focus on exact algorithms.

Our starting point is a simple approach to construct almost-sure strategies: from the POMDP, we build a Markov decision process (MDP) whose states are supports of the beliefs of the POMDP. In other words, we store information about which states we can be in, but abstract away the probabilities. The belief-support MDP serves as a finite abstraction of the POMDP; one could expect that there exists an almostsure strategy in the POMDP if and only if there exists one in the corresponding belief-support MDP. Unfortunately, this abstraction is neither sound nor complete; we present a simple counterexample in Figure 1.

The fundamental question we ask in this paper is whether there are natural sufficient conditions which make the belief-support abstraction correct. Conceptually, the failure of this abstraction is due to information loss and its accumulation over time.

We introduce a revelation mechanism which restricts information loss by requiring that, almost surely, the agent has eventually about the current state. Intuitively, by forbidding information loss from accumulating for an unbounded amount of time, the revelation mechanism removes the convergence issues leading to undecidability. Practically, we conjecture that revelations are a commonly occurring phenomenon in partial observability; a canonical example is systems that reset with a small observable probability at each step, and therefore reset infinitely often almost surely, and where this reset is observable. We leave to future work to investigate this question further.

Our contributions. We study two properties of POMDPs based on the revelation mechanism, called weakly and strongly revealing POMDPs. We obtain (un)decidability results for both classes. The decidable cases reduce to the analysis of the finite belief-support MDP, which yields a conceptually simple and exact algorithm for a large class of POMDPs. A summary of our contributions for POMDPs is provided in Figure 2. We provide an implementation of the algorithm applied to multiple instances at https://github.com/ gaperez64/pomdps-reveal.

The importance of our results can be appreciated by the following remark: instead of a subclass of POMDPs, the revelation mechanism can be seen as a new semantics for all POMDPs. In that sense, we obtain decidability results for an optimistic semantics of POMDPs which, to the best of our knowledge, has not been done before.

Related works. The closest idea to our notion of revelations that we know of is in [Berwanger and Mathew, 2017], defining a class of partial-information multi-player games with sure (not just almost-sure) revelations. In a quantitative setting, the idea of having actions that reveal the current state at some cost has appeared multiple times in the literature, such as in [Bertrand and Genest, 2011] for POMDPs with quantitative reachability objectives. Recently, activemeasuring POMDPs, with a similar mechanism, have been considered in the online planning community [Bellinger et al., 2021; Krale et al., 2023]. Despite a different setting (online planning vs. model-checking), it carries an intuition similar to our work: precise states can be known, which helps find good strategies. Following the first version of this article, subsequent results on the model of strongly revealing POMDPs were obtained in [Asadi et al., 2026].

This abstract is a shortened version of an article with the same title published in the proceedings of the AAAI 2025 conference [Belly et al., 2025]. A version of the paper with the full proofs is available on arXiv [Belly et al., 2024].

2 Preliminaries

A (discrete) probability distribution on a finite set X is a function d: X → [0, 1] such that ∑x∈X d(x) = 1. The set of all probability distributions on X is denoted D(X). The support supp(d) of a probability distribution d is the set {x ∈ X | d(x) > 0}. We let |X| denote the number of elements in a set X.

2.1 POMDPs

A partially observable Markov decision process (POMDP) is a tuple P = (Q, Act, Sig, δ, q0) such that Q is a finite set of states, Act is a finite set of actions, Sig is a finite set of signals, δ : Q×Act → D(Sig×Q) is the transition function, and q0 ∈ Q is an initial state.

A Markov decision process (MDP) is a tuple M = (Q, Act, δ, q0) where δ : Q × Act → D(Q). Formally, an MDP M = (Q, Act, δ, q0) can be seen as a POMDP P = (Q, Act, Sig, δ, q0) such that Sig = {sq | q ∈ Q} and for all q, q′ , q′′ ∈ Q and a ∈ Act, δ(q, a)(sq′′ , q′ ) > 0 if and only if q′ = q′′ . In practice, it means that the last signal always uniquely determines the current state. MDPs have "complete observation", whereas POMDPs have "partial observation". For a POMDP P = (Q, Act, Sig, δ, q0), we define the underlying MDP of P to be the MDP (Q, Act, δ′ , q0) with δ′ (q, a)(q′ ) = ∑s∈Sig δ(q, a)(s, q′ ).

Remark 1. The observable information in POMDPs is here provided through signals along transitions. This contrasts with state-based observations that partition the state space, which are also frequently used to model POMDPs. Both models are polynomially equivalent. Using signals here makes the definition of strongly revealing (Definition 2) more natural, which is why we opted for this convention.

We refer to the full version for the classical definitions of plays, strategies, probability measures, and objectives.

2.2 Beliefs and Belief Supports

Let P = (Q, Act, Sig, δ, q0) be a POMDP. A belief b ∈ D(Q) is a probability distribution on Q. A belief support b ∈ 2Q \ {∅} is the support of a belief. For brevity, we write 2Q∅ for 2Q \ {∅}. At every step, beliefs and belief supports can be updated when playing an action and observing a signal. We show how to do so for belief supports: we define a function B: 2Q∅ × Act × Sig → 2Q∅ that updates the belief support. For b ∈ 2Q∅ , a ∈ Act, s ∈ Sig, we define B(b, a, s) = {q ′ ∈ Q | ∃q ∈ b, δ(q, a)(s, q ′ ) > 0}. We extend this function in a natural way to a function B∗ : 2Q∅ × (Act · Sig)∗ → 2Q∅ .

Beliefs carry more information than belief supports, as they contain the exact probability of being in a particular state, while belief supports only contain the qualitative information of the possible current states. Observe that when the belief support is a singleton (i.e., b = {q} for some q ∈ Q), knowing the precise belief does not yield more information than knowing the belief support, as all the probability mass is in one of the states. Our "revealing" restrictions on POMDPs defined later will exploit this fact.

2.3 The Belief-Support MDP

For a POMDP P = (Q, Act, Sig, δ, q0), the belief-support MDP of P is the MDP PB = (2Q∅ , Act, δB, {q0}) where for b, b′ ∈ 2Q∅ and a ∈ Act, δB(b, a)(b′ ) > 0 if and only if there is s ∈ Sig such that B(b, a, s) = b′ . We assume the distribution to be uniform over successors with positive probability.

For several simple objectives, the POMDP and its beliefsupport MDP behave in a similar way. For example, sets of belief supports that can be reached with a positive probability are the same in the POMDP and its belief-support MDP; if a set of belief supports is reachable almost surely in the POMDP, it is also the case in the belief-support MDP.

3 Weakly Revealing POMDPs

We define here our first revealing property for POMDPs, which requires that, infinitely often and almost surely, the current state can be deduced by looking at the previous observable history. Formally, we write BP sing = {{q} | q ∈ Q} for the set of singleton belief supports of a POMDP P = (Q, Act, Sig, δ, q0). An observable history h ∈ (Act · Sig)∗ such that B∗ ({q0}, h) ∈ BP sing is called a revelation.

Definition 1 (Weakly revealing). A POMDP P is weakly revealing if, for all strategies σ ∈ Σ(P), we have PPσ [B¨uchi(BP sing )] = 1; i.e., for all strategies, infinitely many revelations occur almost surely.

In particular, POMDPs that "reset" infinitely often, and whose reset can be observed with a dedicated signal, are weakly revealing.

The weakly revealing property is decidable.

Theorem 1. Deciding whether a POMDP is weakly revealing is EXPTIME-complete.

3.1 Soundness of the Belief-Support MDP

In this section, we show that, for weakly revealing POMDPs, the existence of an almost-sure strategy in the belief-support MDP (with an appropriate priority function) implies the existence of an almost-sure strategy in the POMDP.

For the priority function of the belief-support MDP, we consider the "maximal priority" semantics. Formally, let P = (Q, Act, Sig, δ, q0) be a POMDP, and PB be its beliefsupport MDP. Let p: Q → {0, . . . , n} be a priority function on P, inducing the objective Parity(p). We extend this function to the belief-support MDP: for b ∈ 2Q∅ , we define pB(b) = max{p(q) | q ∈ b}.

Without any assumption, the belief-support MDP may be unsound, already for B¨uchi objectives; there may be an almost-sure strategy in the belief-support MDP, but not in the POMDP. An example illustrating this was given in Figure 1. Surprisingly, it is sound for CoB¨uchi objectives without further assumption. Using "max" (and not "min") turns out to be the right choice in our setting. Intuitively, under the right revealing assumptions and the right strategies, if a belief support is visited infinitely often, then all its states will be visited infinitely often, so the maximal priority of the belief support is the one that matters given the parity objective.

Under the weakly revealing semantics, almost-sure strategies of the belief-support MDP carry over to the POMDP for all parity objectives. In other words, the analysis of the belief-support MDP is sound. We recall that pure memoryless strategies suffice to reach the optimal value for parity objectives in MDPs [Chatterjee and Henzinger, 2012].

Proposition 1 (Soundness). Let P = (Q, Act, Sig, δ, q0) be a weakly revealing POMDP with priority function p, and let PB be its belief-support MDP with priority function pB. Assume there is an almost-sure strategy σB for Parity(pB) in PB; by [Chatterjee and Henzinger, 2012], we may assume σB to be pure and memoryless. Then, there is an almost-sure strategy for Parity(p) in P.

3.2 Decidability for Priorities 0, 1, and 2

We show that the existence of an almost-sure strategy in a weakly revealing POMDP implies the existence of an almostsure strategy in its belief-support MDP when priorities are in {0, 1, 2}. This provides a converse to Proposition 1 when priorities are restricted to {0, 1, 2}. We emphasize that parity objectives with priorities {0, 1, 2} encompass both B¨uchi and CoB¨uchi objectives. This result is false without the weakly revealing assumption; see the simple POMDP in Figure 1.

Proposition 2 (Completeness). Let P = (Q, Act, Sig, δ, q0) be a weakly revealing POMDP with priority function p with values in {0, 1, 2}. Let PB be its belief-support MDP with priority function pB. If there is an almost-sure strategy for Parity(p) in P, then there is an almost-sure strategy for Parity(pB) in PB.

Together with an EXPTIME-hardness proof, this yields the following result.

Theorem 2. The existence of an almost-sure strategy for parity objectives with priorities in {0, 1, 2} in weakly revealing POMDPs is EXPTIME-complete.

3.3 Undecidability for Priorities 1, 2, and 3

The previous section suggests that analyzing the beliefsupport MDP is a sound and complete approach for weakly revealing POMDPs with parity objectives with priorities in {0, 1, 2}. One may wonder whether it is complete for any priority function, i.e., if the existence of an almost-sure strategy in a weakly revealing POMDP implies the existence of an almost-sure strategy in its belief-support MDP. Unfortunately, this fails to hold in general, already for priority functions taking values in {1, 2, 3}. Our decidability result is therefore optimal w.r.t. the priorities used.

Theorem3 (Undecidability). The existence of an almost-sure strategy in weakly revealing POMDPs with a parity objective with priorities in {1, 2, 3} is undecidable.

4 Strongly Revealing POMDPs

In this section, we introduce strongly revealing POMDPs, a stronger property entailing that infinitely many revelations occur in a POMDP almost surely. We show that the existence of almost-sure strategies is decidable for strongly revealing POMDPs with arbitrary parity objectives.

We define a notion of revealing signals: for an action a and a state q′ of a POMDP P = (Q, Act, Sig, δ, q0), we define Revealing(a, q′ ) = {s ∈ Sig | ∀r, r′ ∈ Q, r′ ̸= q′ =⇒ δ(r, a)(s, r′ ) = 0} to be the set of signals that indicate surely that the next state is q′ after playing a. For convenience, we define Succ(q, a) = {q′ ∈ Q | ∃s ∈ Sig, δ(q, a)(s, q ′ ) > 0} and Succ(q, a, s) = {q′ ∈ Q | δ(q, a)(s, q ′ ) > 0}.

Definition 2. POMDP P = (Q, Act, Sig, δ, q0) is strongly revealing if any transition between two states for a given action in the underlying MDP of P can also happen with a revealing signal. Formally, P is strongly revealing if for all q, q′ ∈ Q and a ∈ Act, if q′ ∈ Succ(q, a), then there is s ∈ Revealing(a, q ′ ) such that q′ ∈ Succ(q, a, s).

Under this definition, the set of belief supports BP sing is visited infinitely often almost surely from the initial state for any given strategy, so a strongly revealing POMDP is in particular weakly revealing. The strongly revealing property can be decided in polynomial time in the size of a POMDP by simply analyzing every transition.

Example 1. We give an example of a strongly revealing POMDP inspired by the tiger of [Cassandra et al., 1994], depicted in Figure 3. In this environment, an agent has to open the left or the right door, with action aL or aR, respectively. One of them has a (deadly) tiger behind it. Fortunately, the agent can choose to wait and listen (action a?) to inform its decision. Listening results in a signal that is biased towards the true state, i.e., the signal can be sL or sR and the former is more likely if the tiger really is on the left, and vice versa.

We present our version of the tiger environment in which listening guarantees one will eventually discern behind which door there is a tiger. This is achieved by adding new revealing signals sL! and sR! which, importantly, can only be obtained when the tiger is on the left or on the right, respectively. To keep things interesting, these signals can only be obtained with a small probability (yet, their presence already ensures that the POMDP is strongly revealing). We also add signals for death (s⊥) and victory (s⊤), which are missing from the original tiger environment.

The addition of the signals sL! and sR! makes the objective easier to satisfy and therefore changes the semantics of the POMDP; indeed, it is possible to gather more information than in the original tiger environment. However, revealing the deadlock states ⊤ and ⊥ through signals s⊤ and s⊥ is necessary to make the POMDP strongly revealing but does not make the objective easier to satisfy, as no strategy can exit these states anyway.

4.1 Decidability of Parity with Strong Revelations

The soundness of the analysis of the belief-support MDP for strongly revealing POMDPs follows from Proposition 1; it remains to show completeness.

Proposition 3. Let P = (Q, Act, Sig, δ, q0) be a strongly revealing POMDP with a parity objective with priority function p, and PB be its belief-support MDP with priority function pB. If there is an almost-sure strategy for Parity(p) in P, then there is an almost-sure strategy for Parity(pB) in PB.

We obtain as before the decidability of the problem by reducing to the analysis of the belief-support MDP. The proof is similar to that of Theorem 2, simply replacing the use of Proposition 2 by Proposition 3. Together with a proof of EXPTIME-hardness, this yields the following result.

Theorem 4. The existence of an almost-sure strategy for parity in strongly revealing POMDPs is EXPTIME-complete.

4.2 Undecidability of Strongly Revealing Games

We briefly consider here whether the revealing semantics helps in zero-sum two-player partial-information games. In general, such games with CoB¨uchi objectives are undecidable (they encompass POMDPs) while B¨uchi games are decidable for almost-sure strategies [Bertrand et al., 2017; Chatterjee et al., 2013]. We show a negative result: the existence of an almost-sure strategy in two-player CoB¨uchi games with partial information is undecidable, even when restricted to games satisfying a natural extension of the strongly revealing property.

Informally, a game is strongly revealing if for any possible transition between two states with a pair of actions, there is a positive probability of a signal that reveals the second state. This definition generalizes naturally the one for POMDPs.

Theorem 5. The existence of an almost-sure strategy for Player 1 in strongly revealing CoB¨uchi games is undecidable.

Acknowledgments

This work was partially supported by the SAIF project, funded by the "France 2030" government investment plan managed by the French National Research Agency, under the reference ANR-23-PEIA-0006. Pierre Vandenhove was funded by ANR project G4S (ANR-21-CE48-0010-01) and by the Belgian Fonds de la Recherche Scientifique - FNRS through the CDR grant "INSTAP" no. J.0228.26. This work was sparked by discussions with Guillaume Vigeral and Bruno Ziliotto, following a talk on a related model [Vigeral and Ziliotto, 2022].