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

1 Introduction

Partially Observable Markov Decision Processes (POMDPs) provide a principled framework for sequential decisionmaking amidst the fog of uncertainty, accounting for both stochastic dynamics and incomplete state information [Kaelbling et al., 1995; Sebastian et al., 2005]. When coupled with ω-regular properties like Linear Temporal Logic (LTL) [Pnueli, 1977], they allow for the synthesis of policies that satisfy complex, temporally extended goals over infinite traces in uncertain, partially observable environments. Therefore, POMDP-LTL synthesis has attracted considerable interest across AI, robotics, and control [Sharan and Burdick, 2014; Bouton et al., 2020; Kalagarla et al., 2024].

Despite its potential, quantitative POMDP-LTL synthesis, aiming to maximise satisfaction probability, remains notably challenging. Optimal policy synthesis for general planning tasks in infinite-horizon POMDPs is undecidable, even for simple reachability objectives, as it necessitates reasoning over an uncountable belief space and may require unbounded memory [Chatterjee et al., 2016]. Practical approaches therefore rely on tractable approximations that reformulate the problem as reward maximisation, with reward functions encoding task satisfaction, and apply approximate solvers such as Point-Based Value Iteration (PBVI) [Pineau et al., 2003] and Partially Observable Monte Carlo Planning (POMCP) [Silver and Veness, 2010].

However, constructing appropriate reward signals for full LTL is non-trivial, since its semantics concern nonterminating behaviour over infinite traces. Existing approaches either restrict attention to finite-trace LTL (LTLf ), which reduces satisfaction to a one-shot reachability problem [Kalagarla et al., 2022; Liu et al., 2021], or apply optimistic reward shaping based on state-space accepting maximal end components (AMECs) [Bouton et al., 2020]. Nevertheless, due to partial observability, POMDP policy synthesis must operate over the belief space, and many objectives such as recurrence and persistence require full LTL. Furthermore, an optimistic reward for POMDP-LTL may assign a positive satisfaction signal to a belief state even when no single beliefbased policy (defined as a policy shared by all states within the belief's support) can realise the implied satisfaction probability. This challenge, which we term the common policy issue, is illustrated in the following example.

Example 1. Consider the POMDP in Figure 1 with action set {a, c} and initial belief b0 = {s1 : 1.0}. The LTL objective φ = □♢(s2 ∨ s3), requiring the system to visit states s2 or s3 infinitely often. Under full observability, two AMECs exist: 1. {s0, s3}, which achieves almost-sure satisfaction (i.e. probability one) by alternating actions a and c, and 2. {s2, s5}, which succeeds by repeatedly playing a. This suggests that all beliefs supported on AMECs yield satisfaction with probability one. However, with partial observability, no belief-based policy supported on {s0, s3} can satisfy φ almost surely: state s0 requires action c, but taking c in s3 leads to the sink s4. Conversely, beliefs supported on {s2, s5} can still satisfy φ almost surely by playing a.

Furthermore, assigning positive reward one to all states within the state-space AMECs (i.e., {s0, s2, s3, s5}) incorrectly suggests that actions a and c are equally optimal at b0. In reality, c is the uniquely optimal action.

More fundamentally, encoding exact LTL satisfaction as a reward signal is undecidable for POMDPs because of the probability leakage inherent in belief transitions, as shown in Example 1 for beliefs supported on {s0, s3}. For such beliefs, deciding whether a policy with positive satisfaction probability exists is undecidable [Baier et al., 2008]. These theoretical barriers make it difficult to construct sound reward signals. Without these, approximate solvers struggle to converge on reliable, belief-based policies for LTL objectives.

Contributions. We bridge the theoretical and practical gaps in quantitative POMDP-LTL synthesis by introducing a novel mechanism for sound reward shaping. In contrast to fixed scalar reward structures, our approach defines reward assignment rules that integrate with an enhanced online POMCP planner. This allows the system to dynamically evaluate rewards and guide the search toward maximising certified satisfaction, thereby enabling reliable belief-based policy synthesis. To the best of our knowledge, this is the first sound and practical anytime synthesis algorithm for full LTL in POMDPs. Our main contributions are summarised as follows: 1) Sound Reward Shaping: We introduce a sound reward shaping mechanism over the belief space by leveraging belief support structures, grounded in the insight that almostsure satisfaction is the only certifiable property in POMDPLTL. A pruning strategy streamlines reward construction, and the resulting rewards provide a certified lower bound on the true LTL satisfaction probability. 2) Sound Anytime Synthesis: We integrate our reward assignment rules into an enhanced POMCP algorithm specialised for anytime LTL synthesis. Once the search reaches a certified belief region, the agent may continue exploring for higher satisfaction or switch to a verified policy that guarantees satisfaction. This offers the first sound and practical method for real-time POMDPLTL synthesis. 3) Empirical Validation: We show that our method synthesises reliable belief-based policies in scenarios where existing approaches fail. We further show its effectiveness and scalability on three standard POMDP benchmarks with diverse LTL tasks.

Related Work. Owing to the undecidability of quantitative synthesis for POMDPs with LTL, prior work has turned to tractable approximations. One possible approach is to restrict policies to randomised finite-state controllers (FSCs) [Chatterjee et al., 2015; Sharan and Burdick, 2014; Ahmadi et al., 2020; Carr et al., 2020; Carr et al., 2021]. However, such finite-memory restrictions impose key limitations: optimisation remains only locally optimal for any fixed memory size, and while performance is highly sensitive to that size, the minimal required memory is undecidable [Madani et al., 1999]. A complementary line of work [Liu et al., 2021; Kalagarla et al., 2022; Kalagarla et al., 2024] considers belief-based policies for finite-trace LTL (LTLf ). However, many complex planning tasks require infinite-horizon recurrence and persistence, necessitating full LTL. [Bouton et al., 2020] addresses this by applying PBVI with reward signals derived from state-based AMECs. As illustrated in Example 1, such state-based reward shaping can be overly optimistic under partial observability. A detailed discussion of related work is provided in Appendix A 1 .

2 Preliminaries and Problem Statement

This section first outlines the preliminaries of LTL and its equivalent Limit-Deterministic B¨uchi Automaton (LDBA) representation. We then provide the foundations of POMDPs and the POMCP algorithm for online planning. Finally, the problem under consideration is formulated.

2.1 Linear Temporal Logic

LTL [Pnueli, 1977] extends propositional logic by introducing temporal operators that enable the specification of task requirements over time. The syntax of an LTL path formula over a finite set of atomic propositions (AP) is defined inductively as follows:

where ⃝ (Next) and U (Until) are temporal operators. Additional derived temporal operators include: ♢φ ≡ trueUφ (Eventually) and □φ ≡ ¬(♢¬φ) (Always). Standard Boolean operators, such as ∨ (or) and → (implies), are used conventionally. The detailed semantics with satisfaction relation of LTL can be found in [Baier and Katoen, 2008]. For a formula φ and an infinite word w = w0w1w2 · · · ∈ (2AP )ω , we write L(φ) to denote the language of φ, which is the set of infinite words over (2AP )ω that satisfy φ.

Every LTL formula admits an equivalent representation as a Nondeterministic B¨uchi Automaton (NBA) [Vardi and Wolper, 1994] that accepts the language L(φ). More recently, a subclass of NBAs, known as limit-deterministic B¨uchi automata, has shown particularly suitable for the quantitative analysis of probabilistic systems [Sickert et al., 2016]. In this paper, we also make use of LDBAs to support our approach.

Definition 1 (LDBA [Sickert et al., 2016]). An LDBA A is defined as a tuple A = (Σ, Q, q0, ∆, Acc) where Σ is an alphabet, Q = Qi ⊎ Qacc is the set of states partitioned into two disjoint sets Qi and Qacc. q0 ∈ Qi is the initial state. ∆ = ∆i ⊎∆acc where: ∆i : Qi × (Σ∪ {ϵ}) → 2Q, ∆acc : Qacc ×Σ → 2Qacc is singleton-valued, and Acc ⊆ Qacc is the accepting set.

An infinite word w ∈ Σω is recognised by an LDBA A if there exists an infinite run r = r0r1r2 · · · ∈ Qω , beginning from q0 and satisfying ri+1 ∈ ∆(ri, ωi) for all i ≥ 0 as well as Inf(r) ∩ Acc ̸= ∅, where Inf(r) denotes transitions in the accepting set appearing infinitely often in r. The set of infinite words accepted by the LDBA A is denoted by L(A). An LTL formula φ over AP can be efficiently translated into an equivalent LDBA A with Σ = 2AP , such that L(A) =

1 An extended version with the appendix is available at https://arxiv.org/pdf/2605.12581

L(φ), using state-of-the-art tools such as Owl [Sickert et al., 2016] and Rabinizer4 [Kˇret´ınsk`y et al., 2018].

2.2 Partially Observable MDPs

In this paper, we consider the following mathematical model: Definition 2 (Labelled POMDPs). A labelled POMDP is defined as a tuple M = (S, S0,A,O, T,Z,L), where S, S0, A, and O are finite sets of states, initial states, actions, and observations, respectively. The state transition function T : S ×A → Dist(S), where T (s, a)(s′ ) denotes the probability of transitioning to state s′ from state s by taking action a. The observation function Z : S ×A → Dist(O), where Z(s′ , a)(o) denotes the probability of observing o after taking action a and reaching state s′ . The labelling function L : S → 2AP maps each state s ∈ S to the set of atomic propositions in AP that hold true at s.

A belief state b of M is a probability distribution over its state space S. Let b0 denote the initial belief state and let B be the set of all possible belief states for a given POMDPM. The belief support of a belief state b ∈ B is the set of states with positive belief, defined as Supp(b) := { s ∈ S | b(s) > 0}. The set of all possible belief supports inM is then given by BSupp := { Θ ⊆ S ∣∣ ∃o ∈ O, ∀s ∈ Θ, o ∈ obs(s)}, where obs : S → 2O . We write b(Θ) := ∑s∈Θ b(s) for the probability mass assigned by b ∈ B to Θ ⊆ S, called its belief mass. The enabled action set at state s is defined as AE(s) := {a ∈ A | Posts(a) ̸= ∅} where Posts(a) = Supp(T (s, a)). We then define AE(Θ) := ⋂s∈Θ AE(s). Without loss of generality, we assume that states with the same observation admit the same set of enabled actions; that is, for any s, s′ ∈ Θ, AE(s) = AE(s′ ) = AE(Θ).

Paths. A history at time t is a finite sequence ht = (a0, o1, . . . , at-1, ot) ∈ (A × O)t capturing the agent's observable interaction with the environment. A belief path is an infinite sequence ρ = (b0, a0, o1, b1, a1, o2, . . . ) in which each belief bt+1 = τ(bt, at, ot+1) is obtained via Bayesian update. The set of such paths starting from b0 is denoted by BPaths(b0). For any ρ, the set of compatible state paths SPaths(ρ) ⊆ S ω contains all sequences (s0, s1, . . . ) such that s0 ∼ b0, st+1 ∼ T(st, at), and ot+1 ∼ Z(st+1, at), consistent with the induced belief evolution.

Policy and LTL Satisfaction. We consider a deterministic belief-based policy π ∈ Π : B → A that maps a belief state to an action. Denote by Π the set of these policies. Under a given policy π, the probability that an LTL specification φ holds at belief state b is denoted by

which measures all belief executions induced by π whose compatible underlying state paths satisfy φ. Accordingly, the satisfaction probability for a POMDP M (under the policy π) with initial belief b0 is defined as PrπM(φ) := Prπb0 (φ).

Undecidability. Optimal policy synthesis for POMDPs is generally undecidable under B¨uchi objectives induced by LTL. [Baier et al., 2008] show that, for B¨uchi objectives, both qualitative verification of positive (non-zero) satisfaction probability and quantitative verification are undecidable. The only property that can be certified is almost-sure satisfaction.

Product POMDP. Analogous to the product construction for MDPs [Baier and Katoen, 2008], the product POMDP M× synchronises the evolution of the POMDPMwith the LDBA Aφ generated from the LTL φ. This allows satisfaction of φ to be checked by tracking accepting runs of the LDBA along paths of M.

Definition 3 (Product POMDP). Given a labelled POMDP M = (S, S0,A,O, T,Z,L) and an LDBA Aφ = (Σ,Q, q0,∆, Acc) from the given LTL formula φ, the product POMDP is a tuple M× = (S×, S× 0 ,A×,O, T ×,Z ×,L×, Acc×) with statespace S× = S ×Q. The set of accepting states is given by Acc× = {(s, q) ∈ S× | q ∈ Acc}.

Given the initial belief state b0 of M, we have b×0 ((s,∆(q0,L(s)))) = b0(s), ∀s ∈ S0. The set of all possible belief states of M× is denoted by B×. The complete definition of the product POMDP is provided in Appendix B.

2.3 Partially Observable Monte-Carlo Planning

POMCP [Silver and Veness, 2010] is a widely adopted online planning algorithm for POMDPs, as it effectively mitigates the curse of dimensionality through state sampling and the curse of history via history sampling with a black-box simulator. At each step t, it uses Monte Carlo Tree Search [Coulom, 2006] to build and explore a search tree rooted at T (ht) = ⟨N(ht), V(ht),P(ht)⟩, where N(ht) tracks the number of visits to the history ht, V(ht) estimates the expected return, and P(ht) holds particles that approximate the belief state bt. Due to space limitations, details on how POMCP works are provided in Appendix C.

2.4 Problem Statement

We study the following policy synthesis problem:

Problem 1. Given a POMDP M and an LTL specification φ, synthesise a deterministic belief-based policy π that maximises the probability of satisfying φ, i.e. maxπ∈Π PrπM(φ).

Following the standard product construction for LTL and probabilistic systems [Baier and Katoen, 2008], we form the product POMDP M× = (S×, S× 0 ,A×,O, T ×,Z ×,L×, Acc×) of the POMDP M with the LDBA Aφ derived from φ (Definition 3). This synchronises the executions of M and Aφ and reduces LTL satisfaction in M to the B¨uchi objective □♢ Acc× in M×:

Accordingly, we further reformulate Problem 1 as an equivalent reward-based policy synthesis problem over M×. The goal is to design a belief-based reward function that induces an optimal policy whose expected reward is equal to the maximum satisfaction probability of B¨uchi objective.

Problem 2 (Reward-Based Policy Synthesis). Given the product POMDP M× induced by a POMDP M and an LTL objective φ, design a belief-based reward function R : B× → [0, 1] and synthesis a policy π× : B× → A× such that

3 Solution Technique

Solving Problem 2 presents significant theoretical hurdles. Encoding LTL satisfaction via a fixed scalar reward is infeasible since assigning an exact reward is equivalent to computing exact satisfaction probabilities, which is known to be undecidable (Section 1). Moreover, even if such a reward were available, maximising the expected reward within a POMDP remains undecidable [Madani et al., 1999]. Practical methods must therefore rely on approximations in both reward shaping and policy synthesis.

We address this gap by proposing a sound approximation framework designed for practical POMDP-LTL synthesis. Exploiting the fact that almost-sure satisfaction is the only certifiable property, we first show that the exact reward signal in Problem 2 can be soundly approximated by the belief mass over certified satisfaction regions derived from the belief-support structure (Section 3.1). We then develop a belief-dependent reward-shaping mechanism that uses a set of assignment rules to generate sound rewards dynamically, together with a pruning strategy that streamlines reward construction (Section 3.2). Finally, we integrate this mechanism into an enhanced POMCP algorithm that steers the search toward maximising certified satisfaction and synthesising reliable belief-based policies (Section 3.3).

3.1 Sound Approximation of Rewards Signal

For POMDPs with B¨uchi objectives, while determining exact or zero satisfaction is undecidable, almost-sure satisfaction fortunately admits a decidable property. Specifically, it depends only on the belief support rather than the precise probability distribution [Chatterjee et al., 2007]: if a belief b is almost-sure winning, then any belief b′ with Supp(b′ ) = Supp(b) is also almost-sure winning. This allows the continuous belief space to be discretised into a finite belief-support MDP (BSMDP), enabling structural evaluation of certified satisfaction over belief support. In this abstraction, each state corresponds to a belief support Θ ⊆ 2S× , and transitions mimic the belief executions in the product POMDP.

Definition 4 (BSMDP [Junges et al., 2021]). Given a product POMDP M× = (S×, S× 0 ,A×,O, T ×,Z ×,L×, Acc×), let B× Supp be belief supports induced byM×. The corresponding BSMDP is the tupleM×BSupp = (B× Supp, Θ0, T × Supp, A×), where Θ0 is the initial belief support, and the transition function T × Supp is defined as Θ′ ∈ T × Supp(Θ, a ∈ A×E (Θ)) if

The BSMDP serves as a formal bridge between qualitative almost-sure satisfaction and general quantitative analysis. By reasoning over the BSMDP, we can identify specific winning supports: subsets of state from which a belief-support based policy exists to satisfy the B¨uchi objective with probability 1. These winning supports enable the construction of a sound reward signal that, for any belief, lower-bounds the true satisfaction probability by the portion of belief mass guaranteed to satisfy the objective almost surely. We now formalise the notion of winning supports and classify beliefs based on their underlying support structure.

Definition 5 (Winning Support and Winning Region). A subset Θ ⊆ S× is a winning support if there exists a beliefsupport policy ˆπ× : B× Supp → A× beginning with Θ such that every state s× ∈ Θ satisfies the LTL objective with probability one under ˆπ×. We denote the union of all winning supports as a winning region W× := ⋃ Θ.

Definition 6 (Belief Categorisation). A belief b× ∈ B× can be categorised by the relationship between its support Supp(b×) and W× as follows:

1. Almost-sure Winning: if Supp(b×) ∈W×;
2. Partially Winning: if ∃Θ ∈W× s.t. Θ ⊂ Supp(b×);
3. Non-Winning: if ∀Θ ∈ W× and Θ ̸⊆ Supp(b×).

Note that even if the initial belief is non-winning, the agent may reach a (partially) winning belief during belief evolution.

Example 2. In the left of Figure 2, beliefs supported on {s×0 , s×1 , s×2 } are not almost-sure winning, but they contains a winning support {s×1 } under action c. The satisfaction probability for any belief supported by {s×0 , s×1 , s×2 } is lowerbounded by the belief mass assigned to {s×1 } by repeating c.

Notably, winning supports are defined with respect to belief-support policies. Since a partially winning belief may contain multiple winning supports (each associated with a distinct policy), obtaining the tightest sound lower bound requires selecting the specific winning support that maximises the belief mass. Simply taking the union of all winning states would result in the common policy issue (as discussed in Example 1), where no single policy can satisfy the entire set. This principle is illustrated in the following example.

Example 3. Consider beliefs supported by {s×3 , s×4 , s×5 , s×6 } in the right of Figure 2. The winning supports and their admissible actions are: {s×3 } with {a}, {s×4 } with {a}, {s×3 , s×4 } with {a}, and {s×6 } with {c}. These cannot be merged into {s×3 , s×4 , s×6 } when computing a sound lower bound, as no single policy is winning for all three states. The tightest lower bound is therefore determined by whichever has the larger belief mass: {s×3 , s×4 } or {s×6 }.

We now define Kb× as the collection of all winning supports contained within the support of a belief state b× in the product POMDP M×. For instance, in Example 3, a belief b× with support {s×3 , s×4 , s×5 , s×6 } would have the set of winning supports Kb× = {{s×3 }, {s×4 }, {s×3 , s×4 }, {s×6 }}. Then a sound belief-based reward signal can be defined as the maximum belief mass assigned to any winning support, reducing Problem 2 to the following sound approximation:

Theorem 1. Given a product POMDP M×, the maximum expected reward in Problem 2 is lower-bounded by a beliefbased policy ˜π× : B× → A× that maximises the probability of reaching a (partially) winning belief b× with maximal belief mass over its winning supports Kb×:

where b×(Θ) is the belief mass assignment to the set of states contained in Θ.

Tightness. The lower bound in Theorem 1 attains the maximum certified LTL satisfaction probability. The remaining gap to the true value reflects satisfaction probability that cannot be certified in finite time, arising from the undecidable leakage illustrated in Example 1.

3.2 Sound Reward Shaping

Theorem 1 allows sound reward signals to be constructed by identifying winning supports in the BSMDP. However, the state space of BSMDP grows exponentially with the state space of the product POMDP, rendering all winning supports and their associated winning policies computationally expensive. To maintain tractability, we extract a sufficient subset of winning supports, together with their almost-sure or partially winning beliefs, by pruning the search space according to two principles: (i) restricting the state space of the BSMDP to obtain a sub-BSMDP; and (ii) focusing on structurally relevant regions within this sub-BSMDP. A sound rewardshaping mechanism is then derived from this refined subset.

Pruned Search Regions. Recall that in fully observable product MDPs with a B¨uchi objective, any satisfying run eventually enters and remains within a state-based AMEC. We hence restrict the BSMDP construction to belief supports that intersect the set of underlying state AMECs E × S inM×:

This restriction gives an over-approximation of the beliefsupport states relevant for satisfaction under belief-based policies, while substantially reducing the BSMDP state space. Moreover, since every winning support ensures almost-sure satisfaction, any belief-support path must almost surely enter a trapping region of the BSMDP in which each support state recurs infinitely often with satisfaction probability one. In the BSMDP, such closed recurrent accepting regions correspond to belief-support accepting MECs (BSAMECs), defined formally below.

Definition 7 (BS-(A)MECs). A belief-support end component (BS-EC) of an BSMDPM×BSupp is a sub-MDP (E,AE) such that the digraph induced by (E,AE) is strongly connected. A belief-support MEC (BS-MEC) is an BS-EC (E,AE) that is not strictly contained in any other BS-EC (E′ , A′E ). We call a BS-MEC (E, AE) accepting (BS-AMEC) if all belief supports Θ ∈ E are winning.

Sufficient Winning Region. We therefore restrict the search for the set of winning-supports ˆW× ( ˆW× ⊆ W×) to those contained in the BS-AMECs of the sub-BSMDP ˆM×BSupp , constructed over belief supports that intersect the state-space AMECs defined in Eq. (2). Any other winning support will almost surely reach ˆW× (thus ˆW× is sufficient).

Algorithm 1 Compute BS-AMECs

Input: BS-MECs (E × BSupp ,AE ×) of sub-BSMDP ˆM×BSupp Output: Sufficient winning region ˆW× 1: ˆW× ← ∅ 2: for all (E,AE) ∈ (E × BSupp , AE ×) do 3: if ∃Θ ∈ E s.t. Θ ⊆ Acc× then 4: ˆW× ← ˆW× ∪ {Θ ∈ E} 5: else 6: Construct the product MDPM×× 7: Compute the winning state set S×× w ofM×× 8: if S×× w = S×× then 9: ˆW× ← ˆW× ∪ {Θ ∈ E}

Determining, however, whether a BS-MEC is accepting is non-trivial, since the presence of Acc× alone is insufficient. As illustrated in Figure 3, a BS-MEC may contain no winning support, may be only partially accepting, or is a BS-AMEC (from left to right in Figure 3). Hence, belief-support information alone is inadequate: one must verify the existence of a belief-support-based policy under which all underlying states are winning. To this end, Algorithm 1 identifies BS-AMECs by constructing an auxiliary product MDP M×× = (S××,A××, T ××, Acc××), where S×× = {(s×,Θ) | s× ∈ Θ,Θ ∈ E}, A××(s×,Θ) = AE ×(Θ), T ××((s×,Θ), a)((s′×,Θ′ )) = T ×(s×, a)(s′×), and Acc×× = {(s×,Θ) ∈ S×× | s× ∈ Acc×}. One can see that M×× couples each BS-MEC with the underlying state-space dynamics, permitting joint reasoning over beliefsupport policies and state transitions. A BS-MEC is accepting iff all states in this product MDP are winning.

Theorem2. Given the sub-BSMDP ˆM×BSupp and its BS-MECs (E × BSupp ,AE ×), Algorithm 1 returns a sound and complete union set ˆW× over all BS-AMECs.

Proof scratch. Soundness. If there exists Θ ∈ E with Θ ⊆ Acc×, then E is a winning support and (E,AE) is a BSAMEC by the MEC property. Otherwise, consider the randomised belief-support policy ¯π× that selects uniformly from AE. If S×× w = S××, every BSCC induced by ¯π× is accepting. By Lemma 1 of [Chatterjee et al., 2010], a corresponding deterministic policy ˜π× exists; hence (E,AE) is a BSAMEC. Completeness. Immediate from Definitions 5 and 7. A full proof is provided in Appendix D.

Sound Reward Assignment Rules. We then define the sound reward structure based on the sufficient winning region ˆW× computed by Algorithm 1. We call a belief support Θ ∈ ˆW× a certified winning support. Furthermore, Θ is called a certified partially winning support if there exists a certified winning support Θ′ ∈ ˆW× such that Θ′ ⊂ Θ. The set of all certified partially winning support is denoted by ˆW× PW . Since a belief b× with certified partially winning support Supp(b×) ∈ ˆW× PW may contain multiple certified winning supports (see Example 3), we let ˆKb× be the collection of all such supports contained within Supp(b×).

Following the lower bound established in Theorem 1, the sound reward function ˆR(·) is defined as:

where b×(Θ) is the belief mass assignment to the set Θ.

3.3 Online POMDP Planning

To synthesise reliable belief-based policies for POMDP-LTL using the proposed sound reward function ˆR(·) in Eq. (3), we develop an enhanced POMCP algorithm as an anytime approximation method. Standard POMCP, however, is not directly applicable, as it relies on Monte Carlo simulations that assign rewards to individual state particles, which is incompatible with our belief-based reward signal. The termination conditions for the Monte Carlo simulation also require rigorous treatment. While entering a belief with a certified winning support is terminal as it already yields the maximum reward, entering a belief with a certified partially winning support is not necessarily so. In the latter case, the agent may continue to explore beliefs that offer higher satisfaction probabilities, a distinction further illustrated in Example 4.

Example 4. Consider a belief node b× in the Monte Carlo search tree with ideal distribution {s×0 : 0.8, s×1 : 0.1, s×2 : 0.1} in the left of Figure 2. It is clear that b× is partially winning since its support contains a winning support {s×1 }. If simulations terminate whenever a particle reaches any (certified) winning support, the resulting satisfaction probability of b× is 0.1 by the belief mass on {s×1 }. However, if simulations do not terminate early and all particles continue exploring, taking action a leads to the belief {s×0 : 0.08, s×1 : 0.73, s×2 : 0.19}, which yields a higher lower bound as 0.73.

We address reward assignment for particles by augmenting each POMCP tree node T (ht+k), which represents the belief b×t+k at time t and simulation depth k, with its groundtruth belief support Θ(ht+k) = Supp(b×t+k ). This support is directly recoverable from the history. Intuitively, the search tree simulates BSMDP: each particle path induces a beliefsupport trace determined only by the history, allowing belief supports to be recovered without explicitly tracking belief distributions. Hence, for each particle s×t+k , we assign reward 1 if the associated belief support Θ(ht+k) is in ˆW×, or if it is in ˆW× PW and the particle lies in a certified winning support Θ ∈ ˆKb×t+k . All remaining particles receive reward 0.

To handle termination for a POMCP tree node with a certified partially winning support, the Upper Confidence Bound (UCB) rule evaluates both terminal and exploratory options. Consider, for instance, a belief b× with support {s×3 , s×4 , s×5 , s×6 }, as shown on the right of Figure 2. As discussed in Example 3, the tightest lower bound for satisfaction is determined by the maximum belief mass assigned to either {s×3 , s×4 } or {s×6 }. Consequently, the UCB selection mechanism identifies the optimal path by switching between: 1) the terminal policy for {s×3 , s×4 } if it carries the dominant mass; 2) the terminal policy for {s×6 } if it is more probable; or 3) any available exploration actions if they promise higher satisfaction through further search. Exploration proceeds until a certified winning support is reached or the maximum depth is exceeded. This mechanism allows the planner to terminate at any time during execution by selecting an optimal beliefsupport policy; the resulting satisfaction probability is then guaranteed by the lower bound maxΘ∈ ˆKb× b×(Θ). The full planning algorithm are given in Appendix E.2.

4 Experiments

We implemented our framework in Python 2 . In the following, we first evaluate a motivating toy example demonstrating that existing methods fail even in simple cases, while our approach succeeds in synthesising reliable belief-based policies. We further assess the effectiveness of our method on three standard POMDP benchmarks under various LTL tasks. The implementation details, experimental setup and additional results are provided in Appendix E and F.

4.1 Motivating Toy Example

Consider the POMDP in Figure 4 with initial belief b0 = {s0 : 1} and actions left (l), right (r), and down (d). The LTL specification is φ = □¬(s2 ∨s7) ∧ □♢(s3 ∨s8), which requires visiting s3 or s8 infinitely often while always avoiding s2 and s7. We compare our approach against optimistic reward shaping [Bouton et al., 2020] and a deterministic FSC variant [Sharan and Burdick, 2014].

Our method. Our analysis identifies a single winning support, {s8}. The sound reward shaping assigns to each belief a value equal to its belief mass on {s8}. Running our solver obtains the following belief-based policy and history: b0 : {s0 : 1} r-→b1 : {s1 : 1} d-→b2 : {s3 : 1} d-→b3 : {s6 : 1} l-→ b4 : {s5 : 1} d-→ b5 : {s7 : 0.2, s8 : 0.8} {s8} ---→. At b5, the policy switches to the belief-support policy for {s8} (e.g.

2 The source code is provided in https://github.com/SafeAutonomy-and-Intelligence-Lab/POMDP-LTL

alternating r and d), ensuring Prπb0 (φ) ≥ 0.8. Experimental details and POMCP values are provided in Appendix F.2.

Existing approaches. Using the optimistic reward shaping in [Bouton et al., 2020] with their PBVI solver reports a satisfaction probability of 1 and forces early termination at the belief b = {s3 : 1}, preventing sufficient exploration of the reachable belief space. Hence, the solver fails to construct αvectors valid for successor beliefs. Since the only exit actions encoded in these α-vectors are r and d, with l absent for any possible satisfaction, execution ultimately results in zero LTL satisfaction. We next consider the deterministic one-memory FSC variant in [Sharan and Burdick, 2014], which collapses to a memoryless observation-based policy. However, no FSC provides positive satisfaction for b0. For observation o0, action r leads to {s1 : 1}, which self-loops under r; action d violates □¬(s2 ∨s7); and action l keeps the system at {s0 : 1}. Larger memory may help, but selecting a suitable memory size is undecidable, making FSC synthesis brittle in practice. Conversely, our deterministic belief-based policy remains executable and offers a meaningful certified lower bound.

4.2 Benchmark Domains and LTLObjectives

Hallway. We evaluate two Hallway models, HW1 and HW2, from [Littman et al., 1995]. The agent moves in an office environment with uncertain location and four orientations, using stochastic forward and left turn actions. A short range sensor reports adjacent walls with some error. Three locations are labelled A, B and C. We consider two LTL objectives: φ1 = ♢A∧□¬B, requiring the agent to eventually reach A while avoiding B at all times, and φ2 = ♢□C, requiring the agent to reach C and remain there indefinitely.

Rock Sample. We follow the rock sample model from [Junges et al., 2021], where a robot moves on an n × n grid with two rocks, each either good G or bad B with initially unknown quality. The robot can move, sense adjacent cells, and sample rocks. We consider two LTL tasks: φ3 = ♢(G∧ ♢E) ∧□¬B, requiring it to first sample a good rock, then reach in an exit state E while never reaching or sampling a bad rock, and φ4 = ♢□G, requiring the robot to collect a good rock and remain there indefinitely.

Grid World. The Grid(n, n) model from [Littman et al., 1995] is an n × n grid where each cell is labelled as a trap (T), goal 1 (G1), or goal 2 (G2). The agent moves left, right, or down, with a 0.2 chance of movement failure, and receives observations of neighbouring cells. We consider three LTL tasks. The first is φ5 = ♢G1 ∧□¬T, requiring the agent to eventually reach G1 while always avoiding traps. The second is φ6 = □(G2 → ♢G1) ∧ □¬T , requiring it to always avoid traps and, whenever it reaches G2, eventually reach G1. The third is φ7 = □♢G1 ∧□¬T , requiring it to visit G1 infinitely often while avoiding traps.

4.3 Results and Discussion

Table 1 summarises the performance of our approach across all tasks. For each case, we report the product model details (|S×|/|O×|/|T ×|), the LTL objective (φi) with its satisfaction probability (PrπM(φ)), the time to construct the sound reward function (SR (s)), and the policy synthesis time using the enhanced POMCP solver (POMCP (s)). Further details on the original models and additional experimental results are provided in Appendix F.4.

The results show that our method synthesises POMDPLTL policies effectively and efficiently, scaling to product models with over forty thousand states, with both sound reward construction and planning completing in about 190 seconds on a single CPU thread. Our approach is particularly effective for LTL tasks such as the reach-persistence objective φ4 and the recurrence objective φ7. Although the underlying state-space AMECs grow proportionally with the model size, they remain confined to a small region of the overall state space, which enables efficient construction of sound reward signals. For example, in the Rock Sample domain, as the model scales, the construction time for the task φ4 increases only from 0.078 to 0.210 seconds.

For the POMCP results, although theory ensures PrM(φ5) ≥ PrM(φ7) as every trace satisfying φ5 also satisfies φ7, we observed PrM(φ5) < PrM(φ7) in practice. This mismatch arises from the differing sizes of their LDBAs: |Aφ5 | = 3 versus |Aφ7 | = 2. The larger automaton for φ5 results a larger product POMDP, requiring more simulations and deeper search for similar approximation quality.

5 Conclusion

This paper presented the first sound and practical anytime belief-based policy synthesis algorithm for full LTL in POMDPs. We approximate undecidable quantitative POMDP-LTL synthesis by seeking policies that maximise verifiable success. Central to this approach is a sound beliefdependent reward-shaping mechanism, integrated into an enhanced POMCP algorithm for reliable policy synthesis. For future work, we plan to extend this sound reward mechanism to a model-free setting, enabling safe POMDP reinforcement learning under LTL objectives.