Efficient Bayes-Adaptive Reinforcement Learning with Temporal Logic Specifications

# Efficient Bayes-Adaptive Reinforcement Learningwith Temporal Logic Specifications
Source: [https://arxiv.org/html/2609.20954](https://arxiv.org/html/2609.20954)
Alessandro Abate††thanks:Both authors are with the Department of Computer Science, University of Oxford, United Kingdom\{jonathan\.hau,alessandro\.abate\}@cs\.ox\.ac\.uk††thanks:©˜2026 IEEE\. Personal use of this material is permitted\. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works\.

###### Abstract

We present a novel end\-to\-end model\-based Reinforcement Learning \(RL\) algorithm for efficient policy synthesis under given Linear Temporal Logic \(LTL\) specifications \(e\.g\., safety or reachability\) in unknown environments\. To do so, a Limit\-Deterministic Büchi Automaton \(LDBA\) representation of the LTL task is synchronised with a Bayes\-Adaptive Markov Decision Process \(BAMDP\) representation of the environment, which allows us to leverage an enhanced exploration\-exploitation trade\-off that is achieved via Bayesian RL, as opposed to traditional non\-Bayesian approaches\. We further propose a novel Bayes\-Adaptive Monte\-Carlo Planning \(BAMCP\) algorithm to allow for approximate Bayes\-optimal strategy synthesis in the synchronised BAMDP construct\. A range of finite\- and infinite\-horizon task experiments demonstrate the effectiveness of our approach in terms of both property satisfaction and sample efficiency, when compared to traditional model\-free approaches\. Additional ablation studies also successfully highlight the value of the novel BAMCP algorithm in comparison to classical BAMCP for LTL task satisfaction\. Finally, we also showcase a successful application of our approach forcautiousRL, namely to reduce the number of task violations incurred during policy training\.

## IIntroduction

Linear Temporal Logic \(LTL\) is an established formal specification framework that enables the precise definition of non\-Markovian, temporal tasks on the state space of a given environment\. In this work we construe tasks as goals or objectives, alternatively as requirements or constraints, on the agent\. As such, LTL is a powerful tool that can be leveraged in Reinforcement Learning \(RL\) to develop agents that can synthesise policies maximising the probability of satisfying a requirement specified by an LTL formula; this is a framework we refer to asLogically\-Constrained RL \(LCRL\)\[[1](https://arxiv.org/html/2609.20954#bib.bib3)\]\. The majority of the existing work in this area focuses on model\-free methods that synthesise policies without learning or maintaining a model of the environment\[[1](https://arxiv.org/html/2609.20954#bib.bib3),[2](https://arxiv.org/html/2609.20954#bib.bib7),[3](https://arxiv.org/html/2609.20954#bib.bib8),[4](https://arxiv.org/html/2609.20954#bib.bib10)\]\. Since these approaches work purely through feedback from the environment, they can under\-perform in environments with sparse rewards as it is the case of temporally\-extended LTL specifications, which provide positive rewards exclusively once fully satisfied \(effectively, at the end of the episode\)\.

Motivated by this observation, we look towards model\-based Bayesian RL as an approach that can help to mitigate such limitations\. Through the Bayesian framework, we can represent the MDP as a Bayes\-Adaptive Markov Decision Process \(BAMDP\)\. This enables an agent to learn by balancing the exploration\-exploitation trade off that is prevalent in environments with unknown dynamics\[[5](https://arxiv.org/html/2609.20954#bib.bib21),[6](https://arxiv.org/html/2609.20954#bib.bib22)\]\. In such model\-based setups, Monte\-Carlo Tree Search \(MCTS\) is often used as the planning algorithm\[[7](https://arxiv.org/html/2609.20954#bib.bib20),[8](https://arxiv.org/html/2609.20954#bib.bib31)\]: the Bayes\-Adaptive Monte\-Carlo Planning \(BAMCP\) algorithm\[[9](https://arxiv.org/html/2609.20954#bib.bib23)\]is a known and efficient MCTS planning method for solving BAMDPs\. The BAMCP algorithm is an integral part of modern approaches to policy synthesis in unknown environments\[[10](https://arxiv.org/html/2609.20954#bib.bib33),[11](https://arxiv.org/html/2609.20954#bib.bib34),[12](https://arxiv.org/html/2609.20954#bib.bib35)\]\. As all of these works do not focus on temporally\-extended tasks, there is a need to integrate the Bayesian planning approach with the LCRL framework in order to derive an efficient way of learning policies that maximise the satisfaction of LTL objectives\. Accordingly, the main contributions of this work are the following:

1. 1\.We propose a novel, end\-to\-end model\-based RL method that applies a Bayesian planning approach to efficiently synthesize a Bayes\-optimal policy for maximising the probability of satisfaction of a given temporal logic specification expressed in LTL\.
2. 2\.To this end, we also propose a planning algorithm that can approximate the Bayes\-optimal action at a given hyperstate tosatisfy LTL objectiveswithin discrete or continuous state spaces\.
3. 3\.We perform a wide range of experiments that validate the effectiveness of our approach compared to existing architectures with respect to both the probability of property satisfaction and sample efficiency\. Further, we demonstrate the importance of our proposed planning algorithm in Contribution \(2\) through ablation studies, where our proposed algorithm is shown to clearly outperform classical BAMCP for task satisfaction\.
4. 4\.In line withcautiousRL goals, we further demonstrate the advantages of employing our model\-based framework over a model\-free approach, by leveraging the ability of the earlier to reduce the number of violations of the specification made during policy training \(in addition to the earlier features at deployment\)\.

## IIRelated Work

The specification of tasks as LTL formulae in the framework of RL has been studied from many different viewpoints\[[13](https://arxiv.org/html/2609.20954#bib.bib4),[14](https://arxiv.org/html/2609.20954#bib.bib5),[15](https://arxiv.org/html/2609.20954#bib.bib6)\], with the majority of approaches focusing on model\-free RL\[[1](https://arxiv.org/html/2609.20954#bib.bib3),[2](https://arxiv.org/html/2609.20954#bib.bib7),[3](https://arxiv.org/html/2609.20954#bib.bib8)\]and a few \- mostly focussing on safety studies \- embracing a model\-based setup\[[16](https://arxiv.org/html/2609.20954#bib.bib2),[17](https://arxiv.org/html/2609.20954#bib.bib1)\]\. As the latter studies, our Bayes\-adaptive approach follows a model\-based framework, where the learned generative model of the environment enables leveraging accurate uncertainty quantification to guide and improve exploration in the original context of RL under LTL\-specified tasks\.

The work by Voloshin et al\.\[[18](https://arxiv.org/html/2609.20954#bib.bib9)\]applies a model\-based approach to satisfying LTL constraints: a constructed model of the environment allows to sample approximately\-correct transition dynamics, from which accepting maximal end\-components of the underlying MDP can be computed; this reduces policy synthesis to a reachability problem, where an optimal policy can be obtained via Bellman policy iteration on the learnt model\.

Whilst in that work the model is assumed to be fixed in order to obtain the policy downstream, our Bayes\-adaptive framework instead learns a Bayesian model alongside the synthesis of the policy that is accordingly optimal for satisfaction of the LTL task\. Alternative model\-based approaches\[[19](https://arxiv.org/html/2609.20954#bib.bib11),[20](https://arxiv.org/html/2609.20954#bib.bib12)\]break down the problem into reach\-avoid sub\-problems, and guarantee specification satisfaction via control barrier certificates: our work instead defines a flexible, LDBA\-based reward function with which the synthesised policy automatically guarantees maximal satisfaction probability\. Further, our work does not make any restrictive assumptions on the type of MDP or environment\.

There exist a few results that have applied the Bayesian framework to control synthesis with LTL specifications:\[[21](https://arxiv.org/html/2609.20954#bib.bib13)\]focuses on partially observable MDPs with unknown transition probabilities, using Point\-Based Value Iteration\[[22](https://arxiv.org/html/2609.20954#bib.bib14),[23](https://arxiv.org/html/2609.20954#bib.bib15)\], however it does not scale well to high dimensions\. In contrast, our work is applicable to all environment types and can easily be adapted for high\-dimensional and continuous state and action spaces: here we compute the optimal policy by using a Bayes\-Adaptive MDP setup, which is similar to some other work\[[24](https://arxiv.org/html/2609.20954#bib.bib16),[25](https://arxiv.org/html/2609.20954#bib.bib17)\], but these however are standard reward\-based approaches that do not work with LTL specifications\.

## IIIPreliminaries

### III\-AMarkov Decision Processes and RL

AMarkov Decision Process\(MDP\) is a tuple⟨𝒮,𝒜,𝒫,𝒮0,𝒜​𝒫,L⟩\\langle\\mathcal\{S\},\\mathcal\{A\},\\mathcal\{P\},\\mathcal\{S\}\_\{0\},\\mathcal\{AP\},L\\rangle, where:𝒮\\mathcal\{S\}is a set of states;𝒜\\mathcal\{A\}is a set of actions;𝒫:𝒮×𝒜→𝒮\\mathcal\{P\}:\\mathcal\{S\}\\times\\mathcal\{A\}\\rightarrow\\mathcal\{S\}is the transition probability function;𝒮0⊆𝒮\\mathcal\{S\}\_\{0\}\\subseteq\\mathcal\{S\}is the set of initial states;𝒜​𝒫\\mathcal\{AP\}is a finite set of atomic propositions;L:𝒮→2𝒜​𝒫L:\\mathcal\{S\}\\rightarrow 2^\{\\mathcal\{AP\}\}is a labelling function that assigns a set of atomic propositions to each state\.

A \(deterministic and memory\-less\)policyπ:𝒮×𝒜→\[0,1\]\\pi:\\mathcal\{S\}\\times\\mathcal\{A\}\\rightarrow\[0,1\]is a map from states to a probability distribution over actions\. Executing a policy on the MDP generates a \(potentially infinite\) sequence of states and actionsτ=s0​a0​s1​a1​…\\tau=s\_\{0\}a\_\{0\}s\_\{1\}a\_\{1\}\.\.\., called atrajectory, such thatsi∈𝒮s\_\{i\}\\in\\mathcal\{S\},ai=π⁡\(si\)a\_\{i\}=\\pi\(s\_\{i\}\), andP⁡\(si,ai,si\+1\)\>0P\(s\_\{i\},a\_\{i\},s\_\{i\+1\}\)\>0for alli≥0i\\geq 0\. We writeτ∼π\\tau\\sim\\pito denote that the distribution of possible trajectories depends on the given policyπ\\pi\.

LetR:𝒮×𝒜×𝒮→ℝR:\\mathcal\{S\}\\times\\mathcal\{A\}\\times\\mathcal\{S\}\\rightarrow\\mathbb\{R\}be a reward function associated with the MDP andγ∈\(0,1\)\\gamma\\in\(0,1\)be the discount factor\. Then the goal of RL is to maximise theexpected discounted return,J⁡\(π\)=𝔼τ∼π​\[∑t=0∞γt​rt\]J\(\\pi\)=\\mathbb\{E\}\_\{\\tau\\sim\\pi\}\[\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}r\_\{t\}\], wherert=R⁡\(st,at,st\+1\)r\_\{t\}=R\(s\_\{t\},a\_\{t\},s\_\{t\+1\}\)\. Thevalue functionfor a given policy is the expected discounted return when starting from statessand executing policyπ\\pi,Vπ​\(s\)=𝔼τ∼π​\[∑t=0∞γt​rt\|s0=s\]V^\{\\pi\}\(s\)=\\mathbb\{E\}\_\{\\tau\\sim\\pi\}\[\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}r\_\{t\}\|s\_\{0\}=s\]\. The optimal policyπ∗\\pi^\{\*\}maximises this value function within the class of policies defined above\.

### III\-BSpecifications \- LTL and Automata

We specify temporally\-extended requirements via Linear Temporal Logic \(LTL\)\. LTL formulae are built up from atomic propositions in𝒜​𝒫\\mathcal\{AP\}according to the following syntax\[[26](https://arxiv.org/html/2609.20954#bib.bib18)\]:

ψ::=t​r​u​e\|a\|ψ∧ψ​\|¬ψ\|​𝐗​ψ\|ψ​𝐔​ψ\.\\psi::=true\\,\|\\,a\\,\|\\,\\psi\\land\\psi\\,\|\\,\\neg\\psi\\,\|\\,\\mathbf\{X\}\\psi\\,\|\\,\\psi\\mathbf\{U\}\\psi\.\(1\)Herea∈𝒜​𝒫a\\in\\mathcal\{AP\}, and the operators𝐗\\mathbf\{X\}and𝐔\\mathbf\{U\}are thenextanduntiloperators respectively\. We further make use of thealwaysandeventuallyoperators, defined as𝐆​ψ≡¬𝐅​¬ψ\\mathbf\{G\}\\psi\\equiv\\neg\\mathbf\{F\}\\neg\\psi, where𝐅​ψ≡t​r​u​e​𝐔​ψ\\mathbf\{F\}\\psi\\equiv true\\,\\mathbf\{U\}\\psi\.

A given trajectoryτ\\tauof an MDP satisfies an atomic propositionaaif the initial state is labelled withaa, i\.e\.,a∈L⁡\(s0\)a\\in L\(s\_\{0\}\)\. This is denoted asτ⊧a\\tau\\models a\. Similarly,τ⊧𝐗​ψ\\tau\\models\\mathbf\{X\}\\psiifτ⁡\[1​…\]⊧ψ\\tau\[1\\ldots\]\\models\\psi; finallyτ⊧ψ1​𝐔​ψ2\\tau\\models\\psi\_\{1\}\\mathbf\{U\}\\psi\_\{2\}if∃k≥0\\exists k\\geq 0s\.t\.τ⁡\[k​…\]⊧ψ2\\tau\[k\\ldots\]\\models\\psi\_\{2\}and∀i<k,τ⁡\[i​…\]⊧ψ1\\forall i<k,\\tau\[i\\ldots\]\\models\\psi\_\{1\}\. Starting from an initial states0s\_\{0\}of an MDP, we then define theprobability of satisfying an LTL formulaψ\\psiasℙ⁡\(τs0π⊧ψ\)\\mathbb\{P\}\(\\tau^\{\\pi\}\_\{s\_\{0\}\}\\models\\psi\), whereτs0π\\tau^\{\\pi\}\_\{s\_\{0\}\}is the collection of all trajectoriesτ\\taugenerated by the MDP executing policyπ\\pifrom the initial states0s\_\{0\}, andℙ\\mathbb\{P\}denotes the measure on the underlying product probability space \(which we implicitly leveraged above to define expected values𝔼\\mathbb\{E\}\)\.

Any LTL formula can be represented via finite\-state automata \(e\.g\., Deterministic Rabin Automata \(DRA\)\[[27](https://arxiv.org/html/2609.20954#bib.bib29)\]and Limit\-Deterministic Büchi Automata \(LDBA\)\[[28](https://arxiv.org/html/2609.20954#bib.bib19),[1](https://arxiv.org/html/2609.20954#bib.bib3),[29](https://arxiv.org/html/2609.20954#bib.bib25)\]\)\. In this work, we utilise LTL\-to\-LDBA conversion for two reasons: firstly, a DRA representation can result in a doubly exponential blow\-up in the size of the automaton\[[27](https://arxiv.org/html/2609.20954#bib.bib29)\], leading to a generally larger product MDP\[[30](https://arxiv.org/html/2609.20954#bib.bib30)\]\. Secondly, the LDBA accepting condition is simpler, making it easier to use when constructing a suitable reward function\.

An LDBA is a tuple⟨𝒬,qo,Σ,ℱ,Δ,𝜺⟩\\langle\\mathcal\{Q\},q\_\{o\},\\Sigma,\\mathcal\{F\},\\Delta,\\boldsymbol\{\\varepsilon\}\\ranglewhere𝒬\\mathcal\{Q\}is a finite set of states;q0∈𝒬q\_\{0\}\\in\\mathcal\{Q\}is the initial state;Σ=2𝒜​𝒫\\Sigma=2^\{\\mathcal\{AP\}\}is a finite alphabet over the set of atomic propositions;ℱ\\mathcal\{F\}is the set of accepting states andΔ:𝒬×Σ→2𝒬\\Delta:\\mathcal\{Q\}\\times\\Sigma\\rightarrow 2^\{\\mathcal\{Q\}\}is the transition function\. Further, an LDBA is characterised by the fact that𝒬\\mathcal\{Q\}is partitioned into two disjoint sets𝒬=𝒬N∪𝒬D\\mathcal\{Q\}=\\mathcal\{Q\}\_\{N\}\\cup\\mathcal\{Q\}\_\{D\}such thatℱ⊆𝒬D\\mathcal\{F\}\\subseteq\\mathcal\{Q\}\_\{D\}andΔ⁡\(q,α\)∈𝒬D\\Delta\(q,\\alpha\)\\in\\mathcal\{Q\}\_\{D\}for allq∈𝒬Dq\\in\\mathcal\{Q\}\_\{D\}andα∈Σ\\alpha\\in\\Sigma\. In other words, an LDBA is constructed via an initial part𝒬N\\mathcal\{Q\}\_\{N\}and an accepting part𝒬D\\mathcal\{Q\}\_\{D\}; once𝒬D\\mathcal\{Q\}\_\{D\}is reached then the automaton cannot leave this set of states\. The set𝜺\\boldsymbol\{\\varepsilon\}contains all the non\-deterministic jump transitions, denoted asϵ\\epsilon\-transitions, that enable the automaton to transition from𝒬N\\mathcal\{Q\}\_\{N\}to𝒬D\\mathcal\{Q\}\_\{D\}without reading any input\. An infinite pathσ=q0​q1​…\\sigma=q\_\{0\}q\_\{1\}\.\.\.is accepted by the LDBA ifInf⁡\(σ\)∪ℱ≠∅\\mathrm\{Inf\}\(\\sigma\)\\cup\\mathcal\{F\}\\neq\\emptysetwhereInf\\mathrm\{Inf\}is the set of states visited byσ\\sigmainfinitely often\.

### III\-CSynchronising Model and Specification \- Product MDP

The synchronisation of an MDP with an LDBA representation of the LTL specification to be satisfied leads to the construction of a new structure, referred to as theproduct MDP: this is useful to employ RL techniques to synthesize policies on the MDP that satisfy the given LTL property\. For the setup under study, deterministic and memoryless policies \(as defined above\) that are function of the product\-space, suffice\.

###### Definition 1\(Product MDP\)

For MDPℳ=\\mathcal\{M\}= ⟨𝒮,𝒜,𝒫,s0,𝒜​𝒫,L⟩\\langle\\mathcal\{S\},\\mathcal\{A\},\\mathcal\{P\},s\_\{0\},\\mathcal\{AP\},L\\rangleand LDBAℒ=⟨𝒬,qo,Σ,ℱ,Δ,𝛆⟩\\mathcal\{L\}=\\langle\\mathcal\{Q\},q\_\{o\},\\Sigma,\\mathcal\{F\},\\Delta,\\boldsymbol\{\\varepsilon\}\\rangle, the product MDP is defined as the MDP

ℳψ=ℳ×ℒ=⟨𝒮⊗,𝒜⊗,𝒫⊗,s0⊗,𝒜​𝒫⊗,L⊗,ℱ⊗⟩\.\\mathcal\{M\}^\{\\psi\}=\\mathcal\{M\}\\times\\mathcal\{L\}=\\langle\\mathcal\{S\}^\{\\otimes\},\\mathcal\{A\}^\{\\otimes\},\\mathcal\{P\}^\{\\otimes\},s\_\{0\}^\{\\otimes\},\\mathcal\{AP\}^\{\\otimes\},L^\{\\otimes\},\\mathcal\{F\}^\{\\otimes\}\\rangle\.ℳψ\\mathcal\{M\}^\{\\psi\}has state space𝒮⊗=𝒮×𝒬\\mathcal\{S\}^\{\\otimes\}=\\mathcal\{S\}\\times\\mathcal\{Q\}, action space𝒜⊗=𝒜×𝛆\\mathcal\{A\}^\{\\otimes\}=\\mathcal\{A\}\\times\\boldsymbol\{\\varepsilon\}, initial states0⊗=\(s0,q0\)s\_\{0\}^\{\\otimes\}=\(s\_\{0\},q\_\{0\}\), set of atomic propositions𝒜​𝒫⊗=𝒬\\mathcal\{AP\}^\{\\otimes\}=\\mathcal\{Q\}, labelling functionℒ⊗:𝒮⊗→2𝒬\\mathcal\{L\}^\{\\otimes\}:\\mathcal\{S\}^\{\\otimes\}\\rightarrow 2^\{\\mathcal\{Q\}\}, and the set of accepting statesℱ⊗=\{F1⊗,…\}\\mathcal\{F\}^\{\\otimes\}=\\\{F\_\{1\}^\{\\otimes\},\.\.\.\\\}whereFj⊗=𝒮×FjF\_\{j\}^\{\\otimes\}=\\mathcal\{S\}\\times F\_\{j\}\. Finally, ifsi⊗=\(si,qi\)s\_\{i\}^\{\\otimes\}=\(s\_\{i\},q\_\{i\}\), then the transition function is given by:

𝒫⊗​\(si⊗,a,sj⊗\)=\{𝒫⁡\(si,a,sj\)ifa∈𝒜andqj∈Δ⁡\(qi,L⁡\(sj\)\),1ifa=ϵqj;qj∈Δ⁡\(qi,ϵqj\);si=sj,0otherwise\.\\mathcal\{P\}^\{\\otimes\}\(s\_\{i\}^\{\\otimes\},a,s\_\{j\}^\{\\otimes\}\)=\\begin\{cases\}\\mathcal\{P\}\(s\_\{i\},a,s\_\{j\}\)&\\text\{if $a\\in\\mathcal\{A\}$ and $q\_\{j\}\\in\\Delta\(q\_\{i\},L\(s\_\{j\}\)\)$, \}\\\\ 1&\\text\{if $a=\\epsilon\_\{q\_\{j\}\}$; $q\_\{j\}\\in\\Delta\(q\_\{i\},\\epsilon\_\{q\_\{j\}\}\)$; $s\_\{i\}=s\_\{j\}$, \}\\\\ 0&\\text\{otherwise\.\}\\end\{cases\}

## IVProblem Definition

We are now equipped with all ingredients to provide the following formal problem statement:

Considering an unknown MDPℳ\\mathcal\{M\}and a given LTL specificationψ\\psito be satisfied, find an optimal policyπ∗\\pi^\{\*\}such that the probability of satisfying the specification from any state is maximised, i\.e\.:π∗=argmax𝜋​𝔼τ∼π​\[ℙ⁡\(τ⊧ψ\)\]\.\\pi^\{\*\}=\\underset\{\\pi\}\{\\mathrm\{argmax\}\}\\;\\underset\{\\tau\\sim\\pi\}\{\\mathbb\{E\}\}\\left\[\\mathbb\{P\}\(\\tau\\models\\psi\)\\right\]\.

## VBayes\-Adaptive RL with LTL Specifications

### V\-ABayesian RL: The Bayes\-Adaptive MDP

In a Bayesian setting, the agent maintains and updates abeliefbbover the unknown transition and/or reward function, which corresponds to a \(posterior\) distribution over model parameters that is conditioned on the agent’s history of visited states and executed actionshth\_\{t\}, i\.e\.,bt=p⁡\(𝒫,ℛ\|ht\)b\_\{t\}=p\(\\mathcal\{P\},\\mathcal\{R\}\|h\_\{t\}\)\. The set of possible beliefsbbis contained within thebelief spaceℬ\\mathcal\{B\}\. In order to account for model uncertainty during decision making, the state space is augmented with the belief state, resulting in the BAMDP formulation\[[5](https://arxiv.org/html/2609.20954#bib.bib21),[6](https://arxiv.org/html/2609.20954#bib.bib22)\]\. Consider an MDP with unknown transition dynamics,ℳ=⟨𝒮,𝒜,𝒫,s0,𝒜​𝒫,L⟩\\mathcal\{M\}=\\langle\\mathcal\{S\},\\mathcal\{A\},\\mathcal\{P\},s\_\{0\},\\mathcal\{AP\},L\\rangle, then the corresponding BAMDP is given by the tuple⟨𝒮\+,𝒜,𝒫\+,s0\+,𝒜​𝒫,L⟩\\langle\\mathcal\{S\}^\{\+\},\\mathcal\{A\},\\mathcal\{P\}^\{\+\},s\_\{0\}^\{\+\},\\mathcal\{AP\},L\\rangle, where:𝒮\+=𝒮×ℬ\\mathcal\{S\}^\{\+\}=\\mathcal\{S\}\\times\\mathcal\{B\}is the set ofhyper\-states, i\.e\., the Cartesian product of the MDP state space𝒮\\mathcal\{S\}and the belief spaceℬ\\mathcal\{B\}ands0\+∈𝒮\+s\_\{0\}^\{\+\}\\in\\mathcal\{S\}^\{\+\}is the initial hyper\-state\.𝒫\+:𝒮\+×𝒜→𝒮\+\\mathcal\{P^\{\+\}\}:\\mathcal\{S\}^\{\+\}\\times\\mathcal\{A\}\\rightarrow\\mathcal\{S\}^\{\+\}is the transition probability function for the BAMDP and is derived as follows:

𝒫\+​\(st\+1\+\|st\+,at\)\\displaystyle\\mathcal\{P^\{\+\}\}\(s^\{\+\}\_\{t\+1\}\|s^\{\+\}\_\{t\},a\_\{t\}\)=𝒫\+\(st\+1,bt\+1\|st,at,bt\)\\displaystyle=\\mathcal\{P^\{\+\}\}\(s\_\{t\+1\},b\_\{t\+1\}\|s\_\{t\},a\_\{t\},b\_\{t\}\)=𝒫\+​\(st\+1\|st,at,bt\)​𝒫\+​\(bt\+1\|st,at,bt,st\+1\)\\displaystyle=\\mathcal\{P^\{\+\}\}\(s\_\{t\+1\}\|s\_\{t\},a\_\{t\},b\_\{t\}\)\\mathcal\{P^\{\+\}\}\(b\_\{t\+1\}\|s\_\{t\},a\_\{t\},b\_\{t\},s\_\{t\+1\}\)=𝔼bt\[𝒫\(st\+1\|st,at\)\]δ\(bt\+1=p\(𝒫\|h:t\+1\)\)\.\\displaystyle=\\mathbb\{E\}\_\{b\_\{t\}\}\[\\mathcal\{P\}\(s\_\{t\+1\}\|s\_\{t\},a\_\{t\}\)\]\\delta\(b\_\{t\+1\}=p\(\\mathcal\{P\}\|h\_\{:t\+1\}\)\)\.
It holds that the optimal policy for the BAMDP maximises the following value function in each augmented state\[[5](https://arxiv.org/html/2609.20954#bib.bib21)\]:

V∗​\(st\+\)=max𝑎​∑s′𝒫\+​\(st\+1\|st\+,at\)​\[r⁡\(s,a,s′\)\+γ​V∗​\(st\+1\+\)\]\.V^\{\*\}\(s^\{\+\}\_\{t\}\)=\\underset\{a\}\{\\mathrm\{max\}\}\\sum\_\{s^\{\\prime\}\}\\mathcal\{P^\{\+\}\}\(s\_\{t\+1\}\|s^\{\+\}\_\{t\},a\_\{t\}\)\\left\[r\(s,a,s^\{\\prime\}\)\+\\gamma V^\{\*\}\(s^\{\+\}\_\{t\+1\}\)\\right\]\.\(2\)
A policy that maximises this value function is calledBayes\-optimaland optimises decision making under the uncertainty of the unknown transition function\.

### V\-BProduct BAMDP

In Section[III\-C](https://arxiv.org/html/2609.20954#S3.SS3), we motivated the construction of theProduct MDPto enable the synthesis of policies on the MDP that also satisfy the given property\. In our setup, the dynamics of the environment are unknown and hence a Bayesian treatment allows the natural balance between exploration and exploitation\. Hence, we synchronise the BAMDP representation with the LDBA to form theProduct BAMDP\. This is defined in an analogous way to the product MDP \(see Definition[1](https://arxiv.org/html/2609.20954#Thmdfn1)\), but instead the product state space is derived as𝒮⊗=𝒮\+×𝒬\\mathcal\{S\}^\{\\otimes\}=\\mathcal\{S\}^\{\+\}\\times\\mathcal\{Q\}\(i\.e\., the synchronisation of the LTL automata state with the BAMDP hyperstates\+∈𝒮\+s^\{\+\}\\in\\mathcal\{S\}^\{\+\}rather than with just the MDP stateOPENs∈𝒮\)s\\in\\mathcal\{S\}\)\.

Given LTL specifications define temporal properties, then a policy satisfying the property may be non\-Markovian \(i\.e\., rely on some knowledge of historical states or actions\)\. The product BAMDP allows us to simultaneously keep track of state progression in both the BAMDP and the LDBA\. As such, we can consider only Markovian \(memoryless\) policies of the formπ⁡\(a\|s\+,q\)\\pi\(a\|s^\{\+\},q\), as the additional state dimension adds the required memory to track LTL specification satisfaction\[[31](https://arxiv.org/html/2609.20954#bib.bib26)\]\.

### V\-CBayes\-Adaptive Monte\-Carlo Planning in Product\-BAMDPs

The dynamics of a BAMDP \(and hence product BAMDP\) can be expressed analytically, and hence it is theoretically possible to solve it as a general MDP\. However, in practice it is often computationally intractable to do so\[[9](https://arxiv.org/html/2609.20954#bib.bib23)\]\. A popular approximate Bayes\-Adaptive algorithm that addresses this issue is the Bayes\-Adaptive Monte\-Carlo Planning \(BAMCP\) algorithm\[[9](https://arxiv.org/html/2609.20954#bib.bib23)\]\. This applies Monte\-Carlo Tree Search \(MCTS\) to the BAMDP model to enable an agent to approximately determine the best action at a given hyper\-state by using a tree search\. However, previous works of BAMCP for both discrete and continuous cases were limited to pure BAMDPs\[[9](https://arxiv.org/html/2609.20954#bib.bib23),[11](https://arxiv.org/html/2609.20954#bib.bib34)\]\. In this section, we present a novel planning method to approximate the Bayes\-optimal action at a given hyperstate forproductBAMDPs with discrete or continuous state spaces\.

#### Overview of the Algorithm

Algorithm[1](https://arxiv.org/html/2609.20954#alg1)illustrates the high\-level overview of the proposed algorithm, which we refer to asProduct\-BAMCP \(P\-BAMCP\)\. As with standard BAMCP, each simulation conducts a tree search from the initial root node to some unvisited node\. Action selection is performed using the Upper Confidence Tree \(UCT\) method\[[32](https://arxiv.org/html/2609.20954#bib.bib39)\]in the discrete environments and the Polynomial Upper Confidence Tree \(PUCT\) method\[[33](https://arxiv.org/html/2609.20954#bib.bib36)\]in the continuous environments, where we have modified the approaches to incorporate the product hyperstatess⊗=\(s,b,q\)s^\{\\otimes\}=\(s,b,q\)instead of the standard MDP states\.

After each action selection, we use the sampled model to obtain the successor states′∼𝒫θ\(s,a\)s^\{\{\}^\{\\prime\}\}\\sim\\mathcal\{P\}\_\{\\theta\}\(s,a\)\. The belief vector is updated \(we discuss the belief vector later in this section\), and we also obtain the successor automata state by extracting the label of the successor state and applying the transition function of the LDBA\. A reward from the transition is then obtained from our adaptive reward functionRΦ:𝒮⊗×𝒜×𝒮⊗→ℝR\_\{\\Phi\}:\\mathcal\{S\}^\{\\otimes\}\\times\\mathcal\{A\}\\times\\mathcal\{S\}^\{\\otimes\}\\rightarrow\\mathbb\{R\}that we detail in Section[VI\-B](https://arxiv.org/html/2609.20954#S6.SS2)\. We recursively repeat this process until we reach an unvisited node\. An approximation of the value of the unvisited node is obtained and backpropagated through the search tree back to the root node\. Repeating this process forns​i​m​sn\_\{sims\}allows us to approximate the bayes\-optimal action at the root node in the product BAMDP\.

#### Leaf Node Value Approximation

An unvisited node represents the leaf node of the current search tree, and requires a method to approximate the value function at the leaf node \(referred to asValue\(s⊗\)\(s^\{\\otimes\}\)in Algorithm[1](https://arxiv.org/html/2609.20954#alg1)\)\. The exact method depends on the type of environment\. In the discrete case, we employ the use of Monte\-Carlo estimation where a rollout policyπr​o\\pi\_\{ro\}is used to select actions for the remainder of the trajectory simulation \(until termination or reaching the search horizon\)\. The reward obtained from this rollout is then back\-propagated through the nodes in the trajectory\. For our experiments, this rollout policy is the currently learned policy obtained as result of applying Q\-learning on the samples\(s,a,r,s′\)\(s,a,r,s^\{\\prime\}\)generated from interactions between the P\-BAMCP agent and the environment\[[9](https://arxiv.org/html/2609.20954#bib.bib23)\]\. In the continuous state case, we directly query the neural network \(in this work we employ a Deep Q\-Network \(DQN\)\[[34](https://arxiv.org/html/2609.20954#bib.bib32)\]\)\.

#### Sink States

In classical BAMCP, if the search tree reaches the predefined search horizondm​a​xd\_\{max\}then the search is terminated early and a value of 0 is backpropagated\. In P\-BAMCP, we track the automata state in order to track the task progression and hence we have another early\-stopping condition to consider\.

###### Definition 2\(Non\-accepting Sink Component\)

Letℒ=⟨𝒬,qo,Σ,ℱ,Δ,𝛆⟩\\mathcal\{L\}=\\langle\\mathcal\{Q\},q\_\{o\},\\Sigma,\\mathcal\{F\},\\Delta,\\boldsymbol\{\\varepsilon\}\\ranglebe an LDBA\. Then a non\-accepting sink component ofℒ\\mathcal\{L\}is a subsetQ⊂𝒬Q\\subset\\mathcal\{Q\}such that the states ofQQform a strongly connected graph that does not contain all accepting sets inℱ\\mathcal\{F\}, and of which there is no superset ofQQthat also forms a strongly connected graph\.

When a non\-accepting sink component is entered, then it is impossible to escape from given the strongly connected nature of the component\. Further, as the sink component does not contain all of the accepting states, then it is impossible to visit all of the accepting sets infinitely often\. As such, reaching any non\-accepting sink component will result in the inability to satisfy the required LTL specification\. We denote the union of all non\-accepting sink components as the set𝔑\\mathfrak\{N\}\. Accordingly, if the search tree ever enters a state withq∈𝔑q\\in\\mathfrak\{N\}, then we can terminate the search tree early and backpropagate a value of 0 \(since we know the task has been failed\)\.

#### Posterior Distribution

As detailed in Section[V\-A](https://arxiv.org/html/2609.20954#S5.SS1), we need to maintain a belief over the unknown parameters and then update them viaBelief\_Update\(b\)\(b\)after experiencing a new transition\. In the discrete case, we leverage a Dirichlet\-Multinomial model, a known class of probabilistic models that takes advantage of conjugacy between the two distributions, reducing the Bayesian updates of posterior parameters to observed visit counts of each state\[[6](https://arxiv.org/html/2609.20954#bib.bib22)\]\. In the continuous environments, we can no longer feasibly track counts of all individual transition tuples\. Instead, we make use of the fact that an ensemble of neural networks can approximate a function with uncertainty quantification\[[35](https://arxiv.org/html/2609.20954#bib.bib37)\]\. We learn a ensemble of dynamics models\{𝒫θ1,…,𝒫θN\}\\\{\\mathcal\{P\}\_\{\\theta\}^\{1\},\.\.\.,\\mathcal\{P\}\_\{\\theta\}^\{N\}\\\}, whereθ\\thetaparametrises the unknown transition function\. The belief over the unknown transition function \(and/or reward function\) can be considered to be a vector ofNNprobabilities, where theit​hi^\{th\}probability denotes the probability of being in an MDP governed by𝒫θi\\mathcal\{P\}\_\{\\theta\}^\{i\}\. Initially, we consider there to be an equal probability for each dynamics model,b0=\[1/N,…,1/N\]b\_\{0\}=\[1/N,\.\.\.,1/N\]\. After observing a transition tuple\(s,a,r,s′\)\(s,a,r,s^\{\\prime\}\), we can update the belief as follows\[[11](https://arxiv.org/html/2609.20954#bib.bib34)\]:

bt\+1\(i\)=bt\(i\)𝒫θi\(s′\|s,a\)ℛθi\(s′\|s,a\),i=1,…,N\.b\_\{t\+1\}\(i\)=b\_\{t\}\(i\)\\mathcal\{P\}\_\{\\theta\}^\{i\}\(s^\{\\prime\}\|s,a\)\\mathcal\{R\}\_\{\\theta\}^\{i\}\(s^\{\\prime\}\|s,a\),\\hskip 10\.00002pti=1,\.\.\.,N\.
Algorithm 1Product BAMCP \(P\-BAMCP\)1:

s⊗,ns​i​m​s,dm​a​xs^\{\\otimes\},n\_\{sims\},d\_\{max\}
2:functionSearch\(

s⊗=\(s,b,q\),ns​i​m​ss^\{\\otimes\}=\(s,b,q\),n\_\{sims\}\)

3:for

n=1​…​ns​i​m​sn=1\.\.\.n\_\{sims\}do

4:

θ∼P⁡\(θ\|b\)\\theta\\sim P\(\\theta\|b\)
5:Simulate\(

s⊗,θs^\{\\otimes\},\\theta\)

6:endfor

7:return

a​r​g​m​a​x𝑎​Q​\(s⊗,a\)\\underset\{a\}\{argmax\}\\hskip 1\.42271ptQ\(s^\{\\otimes\},a\)
8:endfunction

9:

10:functionSimulate\(

s⊗,θ,ds^\{\\otimes\},\\theta,d\)

11:if

d≥dm​a​xd\\geq d\_\{max\}or

q∈𝔑q\\in\\mathfrak\{N\}then

12:return0

13:endif

14:if

N⁡\(s⊗\)=0N\(s^\{\\otimes\}\)=0then

15:for

a∈𝒜a\\in\\mathcal\{A\}do

16:

N⁡\(s⊗,a\)←0N\(s^\{\\otimes\},a\)\\leftarrow 0
17:

Q⁡\(s⊗,a\)←0Q\(s^\{\\otimes\},a\)\\leftarrow 0
18:endfor

19:

R←R\\leftarrowValue\(s⊗\)\(s^\{\\otimes\}\)

20:

N⁡\(s⊗\)←N⁡\(s⊗\)\+1N\(s^\{\\otimes\}\)\\leftarrow N\(s^\{\\otimes\}\)\+1
21:

N⁡\(s⊗,a\)←N⁡\(s⊗,a\)\+1N\(s^\{\\otimes\},a\)\\leftarrow N\(s^\{\\otimes\},a\)\+1
22:else

23:

a←a​r​g​m​a​xj∈𝒜​Q​\(s⊗,j\)\+c​PU​C​T​N⁡\(s⊗\)1\+N⁡\(s⊗,a\)a\\leftarrow\\underset\{j\\in\\mathcal\{A\}\}\{argmax\}\\hskip 1\.42271ptQ\(s^\{\\otimes\},j\)\+cP\_\{UCT\}\\frac\{\\sqrt\{N\(s^\{\\otimes\}\)\}\}\{1\+N\(s^\{\\otimes\},a\)\}
24:

s′∼𝒫θ\(s,a\)s^\{\{\}^\{\\prime\}\}\\sim\\mathcal\{P\}\_\{\\theta\}\(s,a\)
25:

b′←b^\{\{\}^\{\\prime\}\}\\leftarrowBelief\_Update\(b\)\(b\)

26:

q′←Δ\(q,L\(s′\)\)q^\{\{\}^\{\\prime\}\}\\leftarrow\\Delta\(q,L\(s^\{\\prime\}\)\)
27:

r∼RΦ\(s⊗,a,s⊗′\)\)r\\sim R\_\{\\Phi\}\(s^\{\\otimes\},a,s^\{\\otimes^\{\\prime\}\}\)\)
28:

N⁡\(s⊗\)←N⁡\(s⊗\)\+1N\(s^\{\\otimes\}\)\\leftarrow N\(s^\{\\otimes\}\)\+1
29:

N⁡\(s⊗,a\)←N⁡\(s⊗,a\)\+1N\(s^\{\\otimes\},a\)\\leftarrow N\(s^\{\\otimes\},a\)\+1
30:

R←r\+γSimulate\(s⊗′,θ,d\+1\)R\\leftarrow r\+\\gamma\\texttt\{Simulate\}\(s^\{\\otimes^\{\\prime\}\},\\theta,d\+1\)
31:endif

32:

Q⁡\(s⊗,a\)←Q⁡\(s⊗,a\)\+α⁡\[R−Q⁡\(s⊗,a\)\]Q\(s^\{\\otimes\},a\)\\leftarrow Q\(s^\{\\otimes\},a\)\+\\alpha\[R\-Q\(s^\{\\otimes\},a\)\]
33:return

RR
34:endfunction

## VIBA\-LCRL Algorithm

### VI\-AOverview of the Approach

The pseudocode for BA\-LCRL is described in Algorithm[2](https://arxiv.org/html/2609.20954#alg2), and consists of four main steps:

1. 1\.LTL\-to\-LDBA Conversion:Given any LTL specification, we convert it to an equivalent LDBA representation\.
2. 2\.P\-BAMCP:At each step, we leverage the learned model and plan using P\-BAMCP to determine the next best action to execute in the environment\.
3. 3\.Bayesian Inference:The transition tuple\(s,a,r,s′\)\(s,a,r,s^\{\\prime\}\)generated from executing the action in the environment is used to update our belief\.
4. 4\.Update Q\-Values:The table/network used to estimate Q\-values is updated \(e\.g\., using sampled trajectories from the replay buffer\)\.

Algorithm 2Overview of BA\-LCRL1:LTL Specification

ψ\\psi
2:Bayes\-optimal policy

π∗\\pi^\{\*\}
3:Convert

ψ\\psito LDBA

ℒ\\mathcal\{L\}
4:Initialise frontier sets \(accepting

𝔽\\mathbb\{F\}, tracking

𝕋\\mathbb\{T\}\) and sink set

𝔑\\mathfrak\{N\}
5:Initialise

s​t​e​p=0step=0and

e​p​o​c​h=0epoch=0
6:whilenot convergeddo

7:

e​p​o​c​h←e​p​o​c​h\+1epoch\\leftarrow epoch\+1
8:

s⊗=\(s0\+,q0\)s^\{\\otimes\}=\(s^\{\+\}\_\{0\},q\_\{0\}\)
9:while

\(q∉𝔑\)∧\(s​t​e​p<s​t​e​p​\_​t​h​r​e​s​h​o​l​d\)\(q\\notin\\mathfrak\{N\}\)\\wedge\(step<step\\\_threshold\)do

10:

s​t​e​p←s​t​e​p\+1step\\leftarrow step\+1
11:

a∗←P\-BAMCP​\(s⊗\)a^\{\*\}\\leftarrow\\text\{P\-BAMCP\}\(s^\{\\otimes\}\)
12:Execute

a∗a^\{\*\}and move to

s′s^\{\\prime\}
13:Update

q←q′q\\leftarrow q^\{\\prime\}via known automaton transitions

14:Update

b←b′b\\leftarrow b^\{\\prime\}via Bayesian Inference

15:Receive reward

RΦ\(s⊗,a∗,s⊗′\)R\_\{\\Phi\}\(s^\{\\otimes\},a^\{\*\},s^\{\\otimes^\{\\prime\}\}\)
16:Update

𝔽←A​c​c​\(q′,𝔽\)\\mathbb\{F\}\\leftarrow Acc\(q^\{\\prime\},\\mathbb\{F\}\)and

𝕋←Tℒ​\(q′,𝕋\)\\mathbb\{T\}\\leftarrow T\_\{\\mathcal\{L\}\}\(q^\{\\prime\},\\mathbb\{T\}\)
17:Update

Qπ​\(s⊗,a∗\)Q^\{\\pi\}\(s^\{\\otimes\},a^\{\*\}\)
18:

s⊗←s⊗′s^\{\\otimes\}\\leftarrow s^\{\\otimes^\{\\prime\}\}
19:endwhile

20:endwhile

### VI\-BHandling Sparse Rewards in LTL\-augmented State Spaces: Reward Shaping

The generation of rewards from LTL objectives in RL is typically achieved via some form of reward machine\[[36](https://arxiv.org/html/2609.20954#bib.bib38)\]\. In this work, we use an LDBA\-based adaptive reward function similar to Hasanbeig et al\.\[[1](https://arxiv.org/html/2609.20954#bib.bib3)\]:

R\(s⊗,a,s⊗′\)=\{rpifq′∈𝔽,0otherwise,R\(s^\{\\otimes\},a,s^\{\\otimes^\{\\prime\}\}\)=\\begin\{cases\}r\_\{p\}&\\text\{if $q^\{\\prime\}\\in\\mathbb\{F\}$, \}\\\\ 0&\\text\{otherwise,\}\\end\{cases\}\(3\)where we refer to the set𝔽\\mathbb\{F\}as theaccepting frontier setwhich tracks the unvisited accepting sets that need to be visited to eventually satisfy the LTL specification\.

However, such a reward function only provides rewards upon reaching the accepting sets \(i\.e\., task completion\), with no regard to how many steps in the MDP are required before such conditions are achieved\. This results in reward sparsity, especially in our Bayes\-adaptive setup, as we are applying this reward function over a BAMDP where the state space is infinite \(as detailed in Section[V\-A](https://arxiv.org/html/2609.20954#S5.SS1)\)\.

Following the work by Yuan et al\.\[[29](https://arxiv.org/html/2609.20954#bib.bib25)\], we can augment the base reward function via a potential functionΦ:𝒮⊗→ℝ\\Phi:\\mathcal\{S\}^\{\\otimes\}\\rightarrow\\mathbb\{R\}such that the reward function becomes:

RΦ\(s⊗,a,s⊗′\)=R\(s⊗,a,s⊗′\)\+γΦ\(s⊗′\)−Φ\(s⊗\)\.R\_\{\\Phi\}\(s^\{\\otimes\},a,s^\{\\otimes^\{\\prime\}\}\)=R\(s^\{\\otimes\},a,s^\{\\otimes^\{\\prime\}\}\)\+\\gamma\\Phi\(s^\{\\otimes^\{\\prime\}\}\)\-\\Phi\(s^\{\\otimes\}\)\.\(4\)
Importantly, we note that applying such a transformation does not affect the set of optimal policies otherwise obtained using the base reward function\[[37](https://arxiv.org/html/2609.20954#bib.bib27)\], and thus only acts to improve training convergence\.

We can then define the following potential function:

Φ⁡\(s⊗\)=\{η​rpifq∈𝕋,0otherwise,\\Phi\(s^\{\\otimes\}\)=\\begin\{cases\}\\eta r\_\{p\}&\\text\{if $q\\in\\mathbb\{T\}$, \}\\\\ 0&\\text\{otherwise,\}\\end\{cases\}\(5\)where0<η<10<\\eta<1is a shaping parameter and the set𝕋\\mathbb\{T\}is thetracking frontier setwhich tracks the unvisited intermediate automaton states on the path to an accepting set\. Intuitively, this is a reward function that provides a smaller positive rewardη​rp\\eta r\_\{p\}for traversing the automaton towards an accepting set, and then provides a larger positive rewardrpr\_\{p\}for reaching an accepting set \(thereby mitigating the issue of reward sparsity\)\.

### VI\-CUpdating the Tracking Sets

As detailed in the previous section \(and captured in Line 14 of Algorithm[2](https://arxiv.org/html/2609.20954#alg2)\), we need to maintain and update both the frontier sets to ensure that our adaptive reward only provides reward forprogressiontowards the accepting sets \(so that the agent doesn’t just move back and forth between two intermediate automata states and still receive reward\), and then for visiting each of the accepting states in turn \(as we need the agent to visitallof the accepting sets infinitely often to satisfy the LTL objective\)\.

Consider an LDBAℒ=⟨𝒬,qo,Σ,ℱ,Δ,𝜺⟩\\mathcal\{L\}=\\langle\\mathcal\{Q\},q\_\{o\},\\Sigma,\\mathcal\{F\},\\Delta,\\boldsymbol\{\\varepsilon\}\\rangle, whereℱ=\{F1,…,Fn\}\\mathcal\{F\}=\\\{F\_\{1\},\.\.\.,F\_\{n\}\\\}is the set of accepting sets,𝔑=\{N1,…,Nk\}\\mathfrak\{N\}=\\\{N\_\{1\},\.\.\.,N\_\{k\}\\\}is the set of non\-accepting sink components and then letQs​i​n​k=\{q∈𝒬\|q∈Ni,∀i∈\{1,…,k\}\}Q\_\{sink\}=\\\{q\\in\\mathcal\{Q\}\|q\\in N\_\{i\},\\forall i\\in\\\{1,\.\.\.,k\\\}\\\}be the set of sink states\. Then we can define a tracking frontier function,Tℒ:𝒬×𝒬→2𝒬T\_\{\\mathcal\{L\}\}:\\mathcal\{Q\}\\times\\mathcal\{Q\}\\rightarrow 2^\{\\mathcal\{Q\}\}over the tracking frontier set𝕋\\mathbb\{T\}and a BooleanBB, such that upon a transition from product states⊗=\(s\+,q\)s^\{\\otimes\}=\(s^\{\+\},q\)to successor product states⊗′=\(s\+′,q′\)s^\{\\otimes^\{\\prime\}\}=\(s^\{\+^\{\\prime\}\},q^\{\\prime\}\)\[[38](https://arxiv.org/html/2609.20954#bib.bib28)\]:

Tℒ​\(q′,𝕋\)=\{𝕋\\q′ifq∈𝕋,𝒬\\\(q0∪Qs​i​n​k∪q′\)ifB=T​r​u​e,𝕋otherwise,T\_\{\\mathcal\{L\}\}\(q^\{\\prime\},\\mathbb\{T\}\)=\\begin\{cases\}\\mathbb\{T\}\\backslash q^\{\\prime\}&\\text\{if $q\\in\\mathbb\{T\}$,\}\\\\ \\mathcal\{Q\}\\backslash\(q\_\{0\}\\cup Q\_\{sink\}\\cup q^\{\\prime\}\)&\\text\{if $B=True$,\}\\\\ \\mathbb\{T\}&\\text\{otherwise,\}\\end\{cases\}where we use the BooleanBBto only hold True when all accepting sets have been visited once \(i\.e\., when the accepting frontier set𝔽\\mathbb\{F\}becomes empty\)\. As such, the tracking frontier function ensures the set𝕋\\mathbb\{T\}maintains the set of unvisited non\-accepting and non\-sink states in the current round\.

We can also define an accepting frontier function,Aℒ:𝒬×ℱ→2𝒬A\_\{\\mathcal\{L\}\}:\\mathcal\{Q\}\\times\\mathcal\{F\}\\rightarrow 2^\{\\mathcal\{Q\}\}over the accepting frontier set𝔽⊂ℱ\\mathbb\{F\}\\subset\\mathcal\{F\}\[[1](https://arxiv.org/html/2609.20954#bib.bib3)\]:

Aℒ​\(q,𝔽\)=\{𝔽\\Fjifq∈Fjand𝔽≠\{Fj\},ℱ\\Fjifq∈Fjand𝔽=\{Fj\},𝔽otherwise\.A\_\{\\mathcal\{L\}\}\(q,\\mathbb\{F\}\)=\\begin\{cases\}\\mathbb\{F\}\\backslash F\_\{j\}&\\text\{if $q\\in F\_\{j\}$ and $\\mathbb\{F\}\\neq\\\{F\_\{j\}\\\}$, \}\\\\ \\mathcal\{F\}\\backslash F\_\{j\}&\\text\{if $q\\in F\_\{j\}$ and $\\mathbb\{F\}=\\\{F\_\{j\}\\\}$, \}\\\\ \\mathbb\{F\}&\\text\{otherwise\.\}\\end\{cases\}So ifq∈Fjq\\in F\_\{j\}, then the function callAℒ​\(q,𝔽\)A\_\{\\mathcal\{L\}\}\(q,\\mathbb\{F\}\)will output a set containing the elements of𝔽\\mathbb\{F\}minus the accepting setFjF\_\{j\}that has just been visited\. In the case where𝔽=\{Fj\}\\mathbb\{F\}=\\\{F\_\{j\}\\\}, then we ”reset” the set𝔽\\mathbb\{F\}to contain all accepting states \(i\.e\., set𝔽=ℱ\\mathbb\{F\}=\\mathcal\{F\}\) and then remove the recently visited accepting setFjF\_\{j\}\. As such, the agent is guided towards visiting each of the accepting sets infinitely often\.

## VIIExperiments

In this section, we empirically validate the performance of the BA\-LCRL algorithm against the model\-free approach\. We further showcase the advantage of learning a generative model to enhance safe policy training \(cautious RL\)\.

### VII\-AExperimental Setup

#### Environments

In the discrete case, we evaluate on a 10 x 10 slippery\-grid MDP\[[9](https://arxiv.org/html/2609.20954#bib.bib23),[1](https://arxiv.org/html/2609.20954#bib.bib3)\]\. For continuous\-state experiments, we employ the Cartpole environment from the Open AI Gym package\[[39](https://arxiv.org/html/2609.20954#bib.bib24)\]\. In all environments, state labels are superimposed on the environment, based on the LTL specificationψ\\psi\.

#### Tasks

In the discrete case, we consider several classes of task: sequential \(non\-Markovian\)reachabilitytasks \(ψ1:F​g1\\psi\_\{1\}:\\text\{F\}g\_\{1\}andψ3:F​\(g1∧XF​\(g2∧XF​g3\)\)\\psi\_\{3\}:\\text\{F\}\(g\_\{1\}\\wedge\\text\{XF\}\(g\_\{2\}\\wedge\\text\{XF\}g\_\{3\}\)\)\);reach\-avoidtasks \(ψ2:F​\(g1∧XF​\(g2\)\)∧G​¬a\\psi\_\{2\}:\\text\{F\}\(g\_\{1\}\\wedge\\text\{XF\}\(g\_\{2\}\)\)\\wedge\\text\{G\}\\neg a\);infinite\-horizon recurrencerequirements \(ψ4:GF​g1∧GF​g2\\psi\_\{4\}:\\text\{GF\}g\_\{1\}\\wedge\\text\{GF\}g\_\{2\}\)\. In the Cartpole environment, we consider two tasks corresponding to keeping the pole upwards whilst avoiding unsafe zones \(ψ5:G​u​p∧G​¬a\\psi\_\{5\}:\\text\{G\}up\\wedge\\text\{G\}\\neg a\) and an extension to also traverse the cart to a given position \(ψ6:G​u​p∧GF​g1∧G​¬a\\psi\_\{6\}:\\text\{G\}up\\wedge\\text\{GF\}g\_\{1\}\\wedge\\text\{G\}\\neg a\)\.

#### Baselines

With focus on RL with temporally\-extended \(non\-Markovian\) tasks, theLCRLapproach by Hasanbeig et\. al\.\[[4](https://arxiv.org/html/2609.20954#bib.bib10)\]consist of the model\-free, non\-Bayesian version of our approach\. This baseline tells us whether our approach is able to learn the optimal solution, and also highlights any advantages of employing a model\-based setup\.

#### Performance Metrics

For finite\-horizon tasks \(ψ1,ψ2,ψ3,ψ6\\psi\_\{1\},\\psi\_\{2\},\\psi\_\{3\},\\psi\_\{6\}\), we measure the averageProperty Satisfaction Probability\(PSP\) which measures the average probability that the given LTL specification was satisfied during the test phase\. In line with similar works, performance for infinite\-horizon tasks \(ψ4,ψ5\\psi\_\{4\},\\psi\_\{5\}\) is measured by the averagenumber of visits to accepting sets\(i\.e\., the average number of completed cycles\)\[[15](https://arxiv.org/html/2609.20954#bib.bib6)\]\. For both metrics, a higher value is better\.

## VIIIResults and Discussion

### VIII\-APerformance and Competitiveness

Table[I](https://arxiv.org/html/2609.20954#S8.T1)compares the average performance metric achieved during test time between BA\-LCRL and the standard LCRL approach\. Our BA\-LCRL approach clearly outperforms the LCRL baseline in terms of both convergence speed and final satisfaction probability \(where there exists a difference\)\. This illustrates that our approach is able to successfully learn and exploit a generative model on\-the\-fly to achieve more efficient learning without compromising the final satisfaction probability\. We note that achieving the maximum score \(i\.e\., reaching the step limit of 200 forψ5\\psi\_\{5\}and achieving 100% PSP forψ6\\psi\_\{6\}\) is possible in Cartpole as the dynamics are fully deterministic, unlike in Slippery Grid where there are stochastic transition dynamics\.

TABLE I:Average performance metric results for each task\. Best values are in bold\.
### VIII\-BAblation Study: BAMCP vs\. P\-BAMCP

In Section[V\-C](https://arxiv.org/html/2609.20954#S5.SS3), we introduced P\-BAMCP, an algorithm that effectively plans in the product BAMDP\. We conducted an ablation study to demonstrate the performance of this algorithm in comparison to the standard BAMCP algorithm\. In particular, we trained an agent to satisfyψ3\\psi\_\{3\}andψ4\\psi\_\{4\}using standard BAMCP for the same number of episodes that P\-BAMCP required to converge \(as per Table[I](https://arxiv.org/html/2609.20954#S8.T1)\)\. Table[II](https://arxiv.org/html/2609.20954#S8.T2)summarises the average performance metric achieved by the standard BAMCP algorithm \(with the relevant values for P\-BAMCP drawn from Table[I](https://arxiv.org/html/2609.20954#S8.T1)for reference\)\. In both cases, it is clear that the proposed P\-BAMCP algorithm vastly outperforms the classical BAMCP algorithm, with the classical algorithm especially struggling with the infinite horizon specificationψ4\\psi\_\{4\}where it only achieved a few random successes\. These results demonstrate the importance of the P\-BAMCP algorithm when trying to approximate the bayes\-optimal action for satisfying LTL tasks and highlight the necessity of augmenting the search tree states with the automata states to enable the agent to track task progression during the planning phase as well\.

TABLE II:Average performance metric results for each task when using classical BAMCP\. P\-BAMCP values extracted from Table[I](https://arxiv.org/html/2609.20954#S8.T1)for reference\. Best values are in bold\.
### VIII\-CAblation Study: Effect of Reward Shaping

We conducted an ablation study to validate the necessity of reward shaping \(particularly for sequential tasks, as detailed in Section[VI\-B](https://arxiv.org/html/2609.20954#S6.SS2)\) by performing the multi\-step sequential taskψ3\\psi\_\{3\}without reward augmentation\. With reward shaping, BA\-LCRL converged in 75 training episodes\. However, without reward shaping, BA\-LCRL only achieves an average PSP of 5\.67% in the same number of training episodes \(as seen in Table[III](https://arxiv.org/html/2609.20954#S8.T3)\)\. BA\-LCRL without reward shaping does eventually converge to a similar maximum PSP, but expectedly requires a lot more training episodes to do so\. This highlights the necessity of reward shaping to mitigate convergence issues caused by reward sparsity and guide the agent through the sub\-tasks of the LDBA to reach the accepting sets\. This is especially important for long sequential tasks consisting of many intermediate automata states in sequence \(as seen above, performance in evenψ3\\psi\_\{3\}which consists of only 3 sequential sub\-tasks is massively impacted without the reward shaping\)\.

TABLE III:Average satisfaction probability for taskψ3\\psi\_\{3\}using BA\-LCRL without additional reward shaping\.
### VIII\-DBA\-LCRL Architecture for Cautious RL

We now showcase an example of the benefit from being able to use a Bayesian planning approach to LCRL to encourage certain behaviours without needing to manipulate the properties or dynamics of the real environment\. Specifically, we introduced a one\-step lookahead component after the MCTS stage \(we will now refer to this approach asCautious BA\-LCRL\)\. Letpu​n​s​a​f​ep\_\{unsafe\}be the probability that executing some actionaain MDP statessresults in a transition to a successor MDP state that contains an unsafe label \(i\.e\., would result in the automata moving into a sink component\), and introduce some threshold probabilityτt​h​r​e​s​h​o​l​d\\tau\_\{threshold\}\. Then, the one step lookahead can be summarised as follows:

1. 1\.At a given state, perform MCTS to determine the next action to be taken \(as per Algorithm[2](https://arxiv.org/html/2609.20954#alg2)\)\.
2. 2\.Perform a one\-step lookahead: Use the model to see ifpu​n​s​a​f​e\>τt​h​r​e​s​h​o​l​dp\_\{unsafe\}\>\\tau\_\{threshold\}\. If so, then we instead select the second best action as determined by the MCTS in \(1\)\.

The results in Table[IV](https://arxiv.org/html/2609.20954#S8.T4)demonstrate that just by using a one\-step lookahead, we can reduce the number of violations incurred during training \(at convergence with 40 episodes of training, Cautious BA\-LCRL reduces violations by approximately 13%\)\. Additionally, due to the reduction in violations, the agent is able to interact more with the environment during episodes, resulting in generally improved average PSP achieved at any given training time\. These results further illustrate the potential of our approach as a framework from which there are many avenues of future work towards safe RL\.

TABLE IV:Comparison between Cautious BA\-LCRL and BA\-LCRL when training to satisfyψ2\\psi\_\{2\}\. Best values are in bold\.

## IXConclusions

In this work we have introducedBA\-LCRL, a Bayesian model\-based approach for synthesizing optimal policies for satisfying a task defined through LTL formulae\. By leveraging P\-BAMCP, our method demonstrates strong performance in terms of satisfaction probability and improved sample efficiency over the traditional model\-free approach across a range of finite\- and infinite\-horizon specifications\. Finally, we showcased the potential of our approach by adding a simple one\-step lookahead component to the planning stage which reduced the number of task violations incurred during the training phase\.

## References

- \[1\]M\. Hasanbeig, A\. Abate, and D\. Kroening\(2019\)Logically\-constrained reinforcement learning\.External Links:1801\.08099,[Link](https://arxiv.org/abs/1801.08099)Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p1.1),[§II](https://arxiv.org/html/2609.20954#S2.p1.1),[§III\-B](https://arxiv.org/html/2609.20954#S3.SS2.p3.1),[§VI\-B](https://arxiv.org/html/2609.20954#S6.SS2.p1.1),[§VI\-C](https://arxiv.org/html/2609.20954#S6.SS3.p3.1),[§VII\-A](https://arxiv.org/html/2609.20954#S7.SS1.SSS0.Px1.p1.1)\.
- \[2\]E\. M\. Hahn, M\. Perez, S\. Schewe, F\. Somenzi, A\. Trivedi, and D\. Wojtczak\(2019\)Omega\-regular objectives in model\-free reinforcement learning\.InTools and Algorithms for the Construction and Analysis of Systems: 25th International Conference,pp\. 395–412\.External Links:ISBN 978\-3\-030\-17461\-3Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p1.1),[§II](https://arxiv.org/html/2609.20954#S2.p1.1)\.
- \[3\]E\. M\. Hahn, M\. Perez, S\. Schewe, F\. Somenzi, A\. Trivedi, and D\. Wojtczak\(2020\)Faithful and effective reward schemes for model\-free reinforcement learning of omega\-regular objectives\.InAutomated Technology for Verification and Analysis,External Links:[Document](https://dx.doi.org/10.1007/978-3-030-59152-6%5F6),ISBN 978\-3\-030\-59151\-9Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p1.1),[§II](https://arxiv.org/html/2609.20954#S2.p1.1)\.
- \[4\]H\. Hasanbeig, D\. Kroening, and A\. Abate\(2023\)Certified reinforcement learning with logic guidance\.Artificial Intelligence322,pp\. 103949\.External Links:ISSN 0004\-3702Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p1.1),[§VII\-A](https://arxiv.org/html/2609.20954#S7.SS1.SSS0.Px3.p1.1)\.
- \[5\]M\. O\. Duff and A\. Barto\(2002\)Optimal learning: computational procedures for bayes\-adaptive markov decision processes\.Ph\.D\. Thesis,University of Massachusetts Amherst\.Note:AAI3039353External Links:ISBN 0493525734Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1),[§V\-A](https://arxiv.org/html/2609.20954#S5.SS1.p1.1),[§V\-A](https://arxiv.org/html/2609.20954#S5.SS1.p2.1)\.
- \[6\]M\. Ghavamzadeh, S\. Mannor, J\. Pineau, and A\. Tamar\(2015\)Convex optimization: algorithms and complexity\.Foundations and Trends® in Machine Learning8\(5–6\),pp\. 359–483\.External Links:ISSN 1935\-8245Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1),[§V\-A](https://arxiv.org/html/2609.20954#S5.SS1.p1.1),[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.SSS0.Px4.p1.1)\.
- \[7\]D\. Silver, A\. Huang, C\. Maddison, A\. Guez, L\. Sifre, G\. Driessche, J\. Schrittwieser, I\. Antonoglou, V\. Panneershelvam, M\. Lanctot, S\. Dieleman, D\. Grewe, J\. Nham, N\. Kalchbrenner, I\. Sutskever, T\. Lillicrap, M\. Leach, K\. Kavukcuoglu, T\. Graepel, and D\. Hassabis\(2016\)Mastering the game of go with deep neural networks and tree search\.Nature529,pp\. 484–489\.External Links:[Document](https://dx.doi.org/10.1038/nature16961)Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1)\.
- \[8\]T\. Pepels, M\. Winands, and M\. Lanctot\(2014\)Real\-time monte\-carlo tree search in ms pac\-man\.Computational Intelligence and AI in Games, IEEE Transactions on6,pp\. 245–257\.External Links:[Document](https://dx.doi.org/10.1109/TCIAIG.2013.2291577)Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1)\.
- \[9\]A\. Guez, D\. Silver, and P\. Dayan\(2012\)Efficient bayes\-adaptive reinforcement learning using sample\-based search\.Advances in Neural Information Processing Systems2,pp\.\.Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1),[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.SSS0.Px2.p1.1),[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.p1.1),[§VII\-A](https://arxiv.org/html/2609.20954#S7.SS1.SSS0.Px1.p1.1)\.
- \[10\]M\. Budd, P\. Duckworth, N\. Hawes, and B\. Lacerda\(2023\)Bayesian reinforcement learning for single\-episode missions in partially unknown environments\.InProceedings of The 6th Conference on Robot Learning,Proceedings of Machine Learning Research, Vol\.205,pp\. 1189–1198\.Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1)\.
- \[11\]J\. Chen, W\. Chen, and J\. Schneider\(2025\)Bayes adaptive monte carlo tree search for offline model\-based reinforcement learning\.External Links:2410\.11234,[Link](https://arxiv.org/abs/2410.11234)Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1),[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.SSS0.Px4.p1.1),[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.p1.1)\.
- \[12\]M\. Rigter, B\. Lacerda, and N\. Hawes\(2021\)Risk\-averse bayes\-adaptive reinforcement learning\.InProceedings of the 35th International Conference on Neural Information Processing Systems,NIPS ’21,Red Hook, NY, USA\.External Links:ISBN 9781713845393Cited by:[§I](https://arxiv.org/html/2609.20954#S1.p2.1)\.
- \[13\]E\. M\. Wolff, U\. Topcu, and R\. M\. Murray\(2012\)Robust control of uncertain markov decision processes with temporal logic specifications\.In2012 IEEE 51st IEEE Conference on Decision and Control \(CDC\),Vol\.,pp\. 3372–3379\.External Links:[Document](https://dx.doi.org/10.1109/CDC.2012.6426174)Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p1.1)\.
- \[14\]G\. D\. Giacomo, L\. Iocchi, M\. Favorito, and F\. Patrizi\(2019\)Foundations for restraining bolts: reinforcement learning with ltlf/ldlf restraining specifications\.External Links:1807\.06333,[Link](https://arxiv.org/abs/1807.06333)Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p1.1)\.
- \[15\]M\. Jackermeier and A\. Abate\(2025\)DeepLTL: learning to efficiently satisfy complex ltl specifications for multi\-task rl\.External Links:2410\.04631,[Link](https://arxiv.org/abs/2410.04631)Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p1.1),[§VII\-A](https://arxiv.org/html/2609.20954#S7.SS1.SSS0.Px4.p1.1)\.
- \[16\]M\. Hasanbeig, A\. Abate, and D\. Kroening\(2020\)Cautious reinforcement learning with logical constraints\.External Links:2002\.12156,[Link](https://arxiv.org/abs/2002.12156)Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p1.1)\.
- \[17\]R\. N\. L\. Mitta, H\. Hasanbeig, D\. Kroening, and A\. Abate\(2022\)Risk\-aware bayesian reinforcement learning for cautious exploration\.InNeurIPS ML Safety Workshop,Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p1.1)\.
- \[18\]C\. Voloshin, H\. M\. Le, S\. Chaudhuri, and Y\. Yue\(2022\)Policy optimization with linear temporal logic constraints\.InProceedings of the 36th International Conference on Neural Information Processing Systems,NIPS ’22\.External Links:ISBN 9781713871088Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p2.1)\.
- \[19\]M\. H\. Cohen, Z\. Serlin, K\. Leahy, and C\. Belta\(2023\)Temporal logic guided safe model\-based reinforcement learning: a hybrid systems approach\.Nonlinear Analysis: Hybrid Systems47,pp\. 101295\.External Links:ISSN 1751\-570XCited by:[§II](https://arxiv.org/html/2609.20954#S2.p3.1)\.
- \[20\]M\. H\. Cohen and C\. Belta\(2021\)Model\-based reinforcement learning for approximate optimal control with temporal logic specifications\.InProceedings of the 24th International Conference on Hybrid Systems: Computation and Control,HSCC ’21\.External Links:ISBN 9781450383394Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p3.1)\.
- \[21\]Y\. Wang, A\. K\. Bozkurt, and M\. Pajic\(2021\)Reinforcement learning with temporal logic constraints for partially\-observable markov decision processes\.External Links:2104\.01612,[Link](https://arxiv.org/abs/2104.01612)Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p4.1)\.
- \[22\]J\. Pineau, G\. Gordon, and S\. Thrun\(2003\)Point\-based value iteration: an anytime algorithm for pomdps\.InProceedings of the 18th International Joint Conference on Artificial Intelligence,IJCAI’03,pp\. 1025–1030\.Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p4.1)\.
- \[23\]J\. M\. Porta, N\. Vlassis, M\. T\.J\. Spaan, and P\. Poupart\(2006\)Point\-based value iteration for continuous pomdps\.Journal of Machine Learning Research7\(83\),pp\. 2329–2367\.Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p4.1)\.
- \[24\]L\. Zintgraf, S\. Schulze, C\. Lu, L\. Feng, M\. Igl, K\. Shiarlis, Y\. Gal, K\. Hofmann, and S\. Whiteson\(2021\)VariBAD: variational bayes\-adaptive deep rl via meta\-learning\.22\(1\)\.External Links:ISSN 1532\-4435Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p4.1)\.
- \[25\]J\. Humplik, A\. Galashov, L\. Hasenclever, P\. A\. Ortega, Y\. W\. Teh, and N\. Heess\(2019\)Meta reinforcement learning as task inference\.CoRRabs/1905\.06424\.External Links:[Link](http://arxiv.org/abs/1905.06424),1905\.06424Cited by:[§II](https://arxiv.org/html/2609.20954#S2.p4.1)\.
- \[26\]A\. Pnueli\(1977\)The temporal logic of programs\.In18th Annual Symposium on Foundations of Computer Science \(sfcs 1977\),Vol\.,pp\. 46–57\.External Links:[Document](https://dx.doi.org/10.1109/SFCS.1977.32)Cited by:[§III\-B](https://arxiv.org/html/2609.20954#S3.SS2.p1.1)\.
- \[27\]R\. Alur and S\. La Torre\(2004\)Deterministic generators and games for ltl fragments\.ACM Trans\. Comput\. Logic5\(1\),pp\. 1–25\.External Links:ISSN 1529\-3785Cited by:[§III\-B](https://arxiv.org/html/2609.20954#S3.SS2.p3.1)\.
- \[28\]S\. Sickert, J\. Esparza, S\. Jaax, and J\. Křetínský\(2016\)Limit\-deterministic büchi automata for linear temporal logic\.Vol\.9780,pp\. 312–332\.Cited by:[§III\-B](https://arxiv.org/html/2609.20954#S3.SS2.p3.1)\.
- \[29\]L\. Yuan, M\. Hasanbeig, A\. Abate, and D\. Kroening\(2019\)Modular deep reinforcement learning with temporal logic specifications\.ArXivabs/1909\.11591\.External Links:[Link](https://api.semanticscholar.org/CorpusID:202750317)Cited by:[§III\-B](https://arxiv.org/html/2609.20954#S3.SS2.p3.1),[§VI\-B](https://arxiv.org/html/2609.20954#S6.SS2.p4.1)\.
- \[30\]S\. Sickert and J\. Křetínský\(2016\)MoChiBA: probabilistic ltl model checking using limit\-deterministic büchi automata\.InAutomated Technology for Verification and Analysis,Cham,pp\. 130–137\.Cited by:[§III\-B](https://arxiv.org/html/2609.20954#S3.SS2.p3.1)\.
- \[31\]C\. Baier and J\. Katoen\(2008\)Principles of model checking \(representation and mind series\)\.The MIT Press\.External Links:ISBN 026202649XCited by:[§V\-B](https://arxiv.org/html/2609.20954#S5.SS2.p2.1)\.
- \[32\]L\. Kocsis and C\. Szepesvári\(2006\)Bandit based monte\-carlo planning\.InMachine Learning: ECML 2006,pp\. 282–293\.Cited by:[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.SSS0.Px1.p1.1)\.
- \[33\]D\. Auger, A\. Couëtoux, and O\. Teytaud\(2013\)Continuous upper confidence trees with polynomial exploration – consistency\.InMachine Learning and Knowledge Discovery in Databases,H\. Blockeel, K\. Kersting, S\. Nijssen, and F\. Železný \(Eds\.\),Berlin, Heidelberg,pp\. 194–209\.External Links:ISBN 978\-3\-642\-40988\-2Cited by:[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.SSS0.Px1.p1.1)\.
- \[34\]V\. Mnih, K\. Kavukcuoglu, D\. Silver, A\. Graves, I\. Antonoglou, D\. Wierstra, and M\. Riedmiller\(2013\)Playing atari with deep reinforcement learning\.pp\.\.Cited by:[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.SSS0.Px2.p1.1)\.
- \[35\]B\. Lakshminarayanan, A\. Pritzel, and C\. Blundell\(2017\)Simple and scalable predictive uncertainty estimation using deep ensembles\.InAdvances in Neural Information Processing Systems,Vol\.30\.Cited by:[§V\-C](https://arxiv.org/html/2609.20954#S5.SS3.SSS0.Px4.p1.1)\.
- \[36\]R\. Toro Icarte, T\. Q\. Klassen, R\. Valenzano, and S\. A\. McIlraith\(2022\)Reward machines: exploiting reward function structure in reinforcement learning\.J\. Artif\. Int\. Res\.73\.External Links:ISSN 1076\-9757Cited by:[§VI\-B](https://arxiv.org/html/2609.20954#S6.SS2.p1.1)\.
- \[37\]A\. Y\. Ng, D\. Harada, and S\. J\. Russell\(1999\)Policy invariance under reward transformations: theory and application to reward shaping\.InProceedings of the Sixteenth International Conference on Machine Learning,ICML ’99,pp\. 278–287\.External Links:ISBN 1558606122Cited by:[§VI\-B](https://arxiv.org/html/2609.20954#S6.SS2.p5.1)\.
- \[38\]M\. Cai, M\. Hasanbeig, S\. Xiao, A\. Abate, and Z\. Kan\(2021\)Modular deep reinforcement learning for continuous motion planning with temporal logic\.IEEE Robotics and Automation Letters6\(4\),pp\. 7973–7980\.External Links:[Document](https://dx.doi.org/10.1109/LRA.2021.3101544)Cited by:[§VI\-C](https://arxiv.org/html/2609.20954#S6.SS3.p2.1)\.
- \[39\]G\. Brockman, V\. Cheung, L\. Pettersson, J\. Schneider, J\. Schulman, J\. Tang, and W\. Zaremba\(2016\)OpenAI gym\.External Links:arXiv:1606\.01540Cited by:[§VII\-A](https://arxiv.org/html/2609.20954#S7.SS1.SSS0.Px1.p1.1)\.