Sample Efficient Model-free Reinforcement Learning from LTL Specifications with Optimality Guarantees

1 Introduction

Linear Temporal Logic (LTL) is a temporal logic language that can encode formulae regarding properties of an infinite sequence of logic propositions. LTL is widely used for the formal specification of high-level objectives for robotics and multi-agent systems, and it is desirable for a system or an agent in the system to learn policies with respect to these high-level specifications. Such systems are modelled as Markov Decision Processes (MDPs), where classic policy synthesis techniques can be adopted if the states and transitions of the MDP are known. However, when the transitions are not known a priori, the optimal policy needs to be learned through interactions with the MDP.

Model-free Reinforcement Learning [Sutton and Barto, 2018], a powerful method to train an agent to choose actions in order to maximize rewards over time in an unknown environment, is a perfect candidate for LTL specification policy learning. However, it is not straightforward to utilize rewardbased RL to learn the optimal policy that maximizes the probability of satisfying LTL specifications [Alur et al., 2021] due to the difficulty of deciding when, where, and how much reward to give to the agent. To this end, most works adopt a method to first transform the LTL specification into an automaton, then build a product MDP using the original environment MDP and the automaton, on which model-free RL algorithms are applied. However, one crucial obstacle still remains, and that is how to properly define the reward that leads an agent to the optimal satisfaction of LTL specification. Several algorithms have been proposed [Hahn et al., 2019; Bozkurt et al., 2019; Hasanbeig et al., 2019] for learning LTL specifications, where, in order to ensure optimality, the key parameters are chosen depending on assumptions or knowledge of the environment MDP. These works normally only prove the existence of the optimality guarantee parameters or provide unnecessarily harsh bounds for them, which might lead to inefficient learning. In addition, it is unclear how to explicitly choose these parameters even with certain knowledge of the environment MDP. Furthermore, the assumed parameters are evaluated in experiments indirectly, either through inspection of the value function or comparison of the expected reward gained, making it difficult to tune the optimality parameters for LTL learning in general MDPs.

In this work, we propose a novel and more general product MDP, reward structure and discounting mechanism that, by leveraging model-free reinforcement learning algorithms, efficiently learns the optimal policy that maximizes the probability of satisfying the LTL specification with guarantees. We demonstrate improved theoretical results on the optimality of our product MDP and the reward structure, with more stringent analysis that yields better bounds on the optimality parameters. Moreover, this analysis sheds light on how to explicitly choose the optimality parameters based on the environment MDP. We also adopt counterfactual imagining that exploits the known high-level LTL specification to further improve the performance of our algorithm. Last but not least, we propose to use the PRISMmodel checker [Kwiatkowska et al., 2011] to directly evaluate the satisfaction probability of the learned policies, providing a platform to directly compare algorithms and tune key parameters. We conduct experiments on several common MDP environments with various challenging LTL tasks, and demonstrate the improved sample efficiency and convergence of our methods.

Our contributions include: (i) a novel product MDP design that incorporates an accepting states counter with a generalized reward structure; (ii) a novel reinforcement learning algorithm that converges to the optimal policy for satisfying LTL specifications, with theoretical optimality guarantees and theoretical analysis results on choosing the key parameters; (iii) the use of counterfactual imagining, a method to exploit the known structure of the LTL specification by creating imagination experiences through counterfactual reasoning; and (iv) direct evaluation of the proposed algorithms through a novel integration of probabilistic model checkers within the evaluation pipeline, with strong empirical results demonstrating better sample efficiency and training convergence.

1.1 RelatedWork

Most works on LTL learning with reward-based RL utilize a product MDP: a product of the environment MDP and an automaton translated from the LTL specification. Sadigh et al. [2014] first used deterministic Rabin automata to create this product with a discounted reward design to learn LTL, while later works adopted a new automaton design, limitdeterministic B¨uchi automata (LDBA) [Sickert et al., 2016]. Hahn et al. [2019] adopted a product MDP with LDBA and augmented it with sink states to reduce the LTL satisfaction problem into a limit-average reward problem with optimality guarantees. Hahn et al. [2020] later modified this approach by including two discount factors with similar optimality guarantee results. Bozkurt et al. [2019] proposed a discounted reward learning algorithm on the product MDP with optimality guarantees, where the discount factor is chosen based on certain assumptions about the unknown environment MDP. To the best of our knowledge, these approaches are the only available to provide optimality guarantees for the full infinite-horizon LTL learning. However, many methods have nevertheless demonstrated empirical results for learning LTL. Hasanbeig et al. [2020; 2019] proposed an accepting frontier function as the reward for the product MDP, while Cai et al. [2021] extended this reward frontier to continuous control tasks.

Due to the difficulty of learning full LTL, many approaches focus on learning restricted finite LTL variants. Giacomo et al. [2013; 2019] proposed the LTLf variant and a corresponding reinforcement learning algorithm; Littman et al. [2017] formulated a learning algorithm for the GLTL variant; Aksaray et al. [2016] proposed to learn Signal Temporal Logic and Li et al. [2016] a truncated LTL variant for robotics applications.

Another related line of work leverages automata to learn non-Markovian rewards. Toro Icarte et al. [2022; 2018] defined a reward machine automaton to represent high-level non-Markovian rewards, while Camacho et al. [2019] introduced a method to learn finite LTL specifications by transforming them into reward machines. However, the expressiveness of reward machines is strictly weaker than that of LTL. Lastly, there are works that exploit other high-level logic specifications to facilitate learning [Andreas et al., 2016; Jiang et al., 2021; Jothimurugan et al., 2020; Jothimurugan et al., 2021], but they are less relevant to reinforcement learning from LTL.

2 Preliminaries

Before formulating our problem, we provide preliminary background on Markov decision processes, linear temporal logic, and reinforcement learning.

2.1 Markov Decision Processes

Definition 1 (Markov Decision Process [Littman, 2001]). A Markov decision process (MDP) M is a tuple (S, s0,A, T,AP,L, r, γ), where S is a finite set of states, s0 ∈ S is the initial state, A is a finite set of actions, T : S ×A× S → [0, 1] is the probabilistic transition function, AP is the set of atomic propositions, L : S → 2AP is the proposition labeling function, r : S × A× S → R is a reward function and γ : S → (0, 1] is a discount function. Let A(s) denote the set of available actions at state s, then, for all s ∈ S, it holds that ∑s′∈S T(s, a, s′ ) = 1 if a ∈ A(s) and 0 otherwise.

An infinite path is a sequence of states σ = s0, s1, s2..., where there exist ai+1 ∈ A(si) such that T (si, ai+1, si+1) > 0 for all i ≥ 0, and a finite path is a finite such sequence. We denote the set of infinite and finite paths of the MDP M as PathsM and FPathsM, respectively. We use σ[i] to denote si, and σ[: i] and σ[i :] to denote the prefix and suffix of the path, respectively. Furthermore, we assume self-loops: if A(s) = ∅ for some state s, we let T(s, a, s) = 1 for some a ∈ A and A(s) = a such that all finite paths can be extended to an infinite one.

A finite-memory policy π for M is a function π : FPathsM → D(A) such that supp(π(σ)) ⊆ A(σ[-1]), where D(A) denotes a distribution over A, supp(d) denotes the support of the distribution and σ[-1] is the last state of a finite path σ. A policy π is memoryless if it only depends on the current state, i.e., σ[-1] = σ′ [-1] implies π(σ) = π(σ′ ), and a policy is deterministic if π(σ) is a point distribution for all σ ∈ FPathsM. For a deterministic memoryless policy, we let π(s) represent π(σ) where σ[-1] = s.

Let PathsMπ ⊆ PathsM denote the subset of infinite paths that follow policy π and we define the probability space (PathsMπ ,FPathsMπ ,Pπ) over PathsMπ in the standardway. Then, for any function f : PathsMπ → R, let Eπ[f] be the expectation of f over the infinite paths of M following π.

A Markov chain (MC) induced by M and deterministic memoryless policy π is a tuple Mπ = (S, s0, Tπ,AP,L), where Tπ(s, s′ ) = T(s, π(s), s′ ). A sink (bottom) strongly connected component (BSCC) of a MC is a set of states C ⊆ S such that, for all pairs s1, s2 ∈ C, there exists a path from s1 to s2 following the transition function Tπ (strongly connected), and there exists no state s′ ∈ S \ C such that Tπ(s, s′ ) > 0 for all s ∈ C (sink).

2.2 Linear Temporal Logic

Linear Temporal Logic (LTL) provides a high-level description for specifications of a system. LTL is very expressive and can describe specifications with infinite horizon.

Definition 2 ([Baier and Katoen, 2008]). An LTL formula over atomic propositions AP is defined by the grammar:

where X represents next and U represents until. Other Boolean and temporal operators are derived as follows: or: φ1 ∨ φ2 = ¬(¬φ1 ∧ ¬φ2); implies: φ1 → φ2 = ¬φ1 ∨ φ2; eventually: F φ = trueU φ; and always: G φ = ¬(F ¬φ).

The satisfaction of an LTL formula φ by an infinite path σ ∈ PathsM is denoted by σ |= φ, and is defined by induction on the structure of φ:

with the satisfaction of Boolean operators defined by their default meaning.

2.3 Reinforcement Learning

Reinforcement learning [Sutton and Barto, 2018] teaches an agent in an unknown environment to select an action from its action space, in order to maximize rewards over time. In most cases the environment is modelled as an MDP M = (S, s0, A, T, AP, L, r, γ). Given a deterministic memoryless policy π, at each time step t, let the agent's current state be st, then the action a = π(st) is chosen and the next state st+1 ∼ T(st, a, ·) together with the immediate reward r(st, a, st+1) is received from the environment. Then, starting at s ∈ S and time step t, the expected discounted reward following π is

where ∏t-1 j=t := 1. The agent's goal is to learn the optimal policy that maximizes the expected discounted reward. Note that we defined a discount function instead of a constant discount factor because it is essential for our proposed LTL learning algorithm to discount the reward depending on the current MDP state.

Q-learning [Watkins and Dayan, 1992] is a widely used approach for model-free RL. It utilizes the idea of the Q function Qπ (s, a), which is the expected discounted reward of taking action a at state s and following policy π after that. The Q function for all optimal policies satisfies the Bellman optimality equations:

At each iteration of the Q-learning algorithm, the agent's experiences, i.e, the next state s′ and immediate reward r(s, a, s′ ), are used to update the Q function:

where α is the learning rate and x α← y represents x ← x + α(y - x). In addition, the optimal policy can be recovered from the optimal Q function Q∗ (s, a) by selecting the action a with the highest state-action pair value in each state s. Qlearning converges to the optimal Q function in the limit given that each state-action pair is visited infinitely often [Watkins and Dayan, 1992], and thus learns the optimal policy.

3 Our Method

Our goal is to formulate a model-free reinforcement learning approach to efficiently learn the optimal policy that maximizes the probability of satisfying an LTL specification with guarantees. We now give an overview of our method. We first transform the LTL objective φ into a limit-deterministic B¨uchi automaton. Then, we introduce a novel product MDP and define a generalized reward structure on it. With this reward structure, we propose a Q-learning algorithm that adopts a collapsed Q function to learn the optimal policy with optimality guarantees. Lastly, we enhance our algorithm with counterfactual imagining that exploits the automaton structure to improve performance while maintaining optimality.

3.1 ProblemFormulation

Given an MDP M = (S, s0,A, T,AP,L, r, γ) with unknown states and transitions and an LTL objective φ, for any policy π of the MDP M, let Pπ(s |= φ) denote the probability of paths from state s following π satisfying the LTL formula φ:

Then, we would like to design a model-free RL algorithm that learns a deterministic memoryless optimal policy πφ that maximizes the probability of M satisfying φ:

3.2 Limit-Deterministic B¨uchi Automata

We first transform the LTL specifications into automata. The common choices of automata include deterministic Rabin automata and non-deterministic B¨uchi automata. In this work, we adopt a B¨uchi automata variant called limit-deterministic B¨uchi automata (LDBA) [Sickert et al., 2016].

Definition 3. A non-deterministic B¨uchi automaton is an automaton A = (AP,Q, q0,∆,F), where AP is the set of atomic propositions, Q is a finite set of states, q0 ∈ Q is the initial state and F ⊆ Q is the set of accepting states. Let Σ = 2AP ∪ {ϵ} be a finite alphabet, then the transition function is given by ∆ : Q × Σ → 2Q.

Definition 4 (LDBA). A B¨uchi automaton is limitdeterministic if Q can be partitioned into a deterministic set and a non-deterministic set, that is, Q = QN ∪ QD, where QN ∩QD = ∅, such that

1. F ⊆QD and q0 ∈ QN;
2. |∆(q, ν)| ≤ 1 for all q ∈ QN and ν ̸= ϵ ∈ Σ;
3. ∆(q, ν) ⊆ QD and |∆(q, ν)| ≤ 1 for all q ∈ QD and ν ∈ Σ;

An LDBA is a B¨uchi automaton where the nondeterminism is limited in the initial component QN of the automaton. An LDBA starts in a non-deterministic initial component and then transitions into a deterministic accepting component QD through ϵ-transitions after reaching an accepting state, where all transitions after this point are deterministic. We follow the formulation of Bozkurt et al. [2019] to extend the alphabets with an ϵ-transition that handles all the non-determinism, meaning only ϵ can transition the automaton state to more then 1 states: |∆(q, ϵ)| > 1. This allows the MDP to synchronise with the automaton, which we will discuss in detail in Section 3.3.

An infinite word W ∈ Σω , where Σω is the set of all infinite words over the alphabet Σ, is accepted by a B¨uchi automaton A if there exists an infinite automaton run θ ∈ Qω from q0, where θ[t + 1] ∈ ∆(θ[t],W[t]), ∀t ≥ 0, such that inf(θ) ∩ F ̸= ∅, where inf(θ) is the set of automaton states that are visited infinitely often in the run θ.

LDBAs are as expressive as the LTL language, and the satisfaction of any given LTL specification φ can be evaluated on the LDBA derived from φ. We use Rabinizer 4 [Kˇret´ınsk´y et al., 2018] to transform LTL formulae into LDBAs. In Figure 1 (left) we give an example of the LDBA derived from the LTL formula "FG a & G !c", where state 1 is the accepting state. LDBAs are different from reward machines [Toro Icarte et al., 2022] because they can express properties satisfiable by infinite paths, which is strictly more expressive than reward machines, and they have different accepting conditions.

3.3 Product MDP

In this section, we propose a novel product MDP of the environment MDP, an LDBA and an integer counter, where the transitions for each component are synchronised. Contrary to the standard product MDP used in the literature [Bozkurt et al., 2019; Hahn et al., 2019; Hasanbeig et al., 2020], this novel product MDP incorporates a counter that counts the number of accepting states visited by paths starting at the initial state.

Definition 5 (Product MDP). Given an MDP M = (S, s0, A, T, AP, L, r, γ), an LDBA A = (AP, Q, q0, ∆, F) and K ∈ N, we construct the product MDP as follows:

where the product states S× = S×Q×[0..K], the initial state s×0 = (s0, q0, 0), the product actions A× = A∪{ϵq | q ∈ Q}, the accepting set F × = S × F × [0..K], and the product transitions T × : S× × A× × S× → [0, 1], which are defined as:

where all other transitions are equal to 0. The product reward r× : S× ×A× × S× → R and the product discount function γ× : S× → (0, 1] that are suitable for LTL learning are defined later in Definition 6.

Furthermore, an infinite path σ of M× satisfies the B¨uchi condition φF if inf(σ) ∩ F × ̸= ∅. With a slight abuse of notation we denote this condition in LTL language as σ |= GF φF, meaning for all M ∈ N, there always exists s× ∈ F × that will be visited in σ[M :].

When an MDP action a ∈ A is taken in the product MDP M×, the alphabet used to transition the LDBA is deduced by applying the label function to the current environment MDP state: L(s) ∈ 2AP . In this case, the LDBA transition δ(q,L(s)) is deterministic. Otherwise, if an ϵ-action ϵˆq ∈ {ϵq | q ∈ Q} is taken, LDBA is transitioned with an ϵtransition, and the non-determinism of δ(q, ϵ) is resolved by transitioning the automaton state to ˆ q. The K counter value is equal to 0 in the initial state, and each time an accepting state is reached, the counter value increases by one until it is capped at K.

Example 1. We motivate our product MDP structure of Definition 5 through an example. In Figure 1 (right), we have a grid environment where the agent can decide to go up, down, left or right. The task is to visit states labeled "a" infinitely often without visiting "c" as described by the LDBA in Figure 1 (left). The MDP starts at (1,0), with walls denoted by solid gray squares. The states in the first row only allow action right as denoted by the right pointing triangle, which leads to a sink at (0,9). There is also a probabilistic gate at (2,0) that transitions the agent randomly to go down or right, and if the agent reaches (2,1), the accepting sink at (2,9) is reachable. Therefore, the optimal policy is to go down from the start and stay in (2,9) if the probabilistic gate at (2,0) transitions the agent to the right. The probability of satisfying this task is the probability of the gate sending you to the right. Intuitively, this environment has some initial accepting states that are easy to explore, but lead to non-accepting sinks, whereas the true optimal path requires more exploration. If we set K = 10 in the product MDP for this task, we can assign very small rewards for the initially visited accepting states and gradually increase the reward as more accepting states are visited to encourage exploration and guide the agent to the optimal policy.

Next, we provide a theorem, which states that the product MDP with B¨uchi condition φF is equivalent, in terms of the optimal policy, to the original MDP with LTL specification φ. The proof of this theorem is provided in Appendix A.1 1 .

Theorem 1 (Satisfiability Equivalence). For any product MDPM× that is induced from LTL formula φ, we have that

Furthermore, a deterministic memoryless policy that maximizes the probability of satisfying the B¨uchi condition φF on the product MDPM×, starting from the initial state, induces a deterministic finite-memory optimal policy that maximizes the probability of satisfying φ on the original MDP M from the initial state.

1 See Appendix in the full version of this paper on arXiv: https: //arxiv.org/abs/2305.01381 [Shao and Kwiatkowska, 2023]

Reward Structure for LTL Learning

We first define a generalized reward structure inM× for LTL learning, and then prove the equivalence between acquiring the highest expected discounted reward and achieving the highest probability of satisfying φF under this reward structure.

Definition 6 (Reward Structure). Given a product MDPM× and a policy π, the product reward function r× : S× ×A× × S× → R is suitable for LTL learning if

where Rn ∈ (0,U] are constants for n ∈ [0..K] and U ∈ (0, 1] is an upper bound on the rewards. The rewards are non-zero only for accepting automaton states, and depend on the value of the K counter.

Then, given a discount factor γ ∈ (0, 1], we define the product discount function γ× : S× → (0, 1] as

and the expected discounted reward following policy π starting at s× and time step t is

The highest K value reached in a path (i.e., the number of accepting states visited in the path) acts as a measure of how promising that path is for satisfying φF. By exploiting it, we can assign varying rewards to accepting states to guide the agent, as discussed in the motivating example in Section 3.3. Next, we provide a lemma stating the properties of the product MDP regarding the satisfaction of the B¨uchi condition φF .

Lemma 1. Given a product MDPM× with its corresponding LTL formula φ and a policy π, we write M×π for the induced Markov chain from π. Let B× F denote the set of states that belong to accepting BSCCs of M×π , and B× ∅ denote the set of states that belong to rejecting BSCCs:

where BSCC(M×π ) is the set of all BSCCs of M×π . We further define more general accepting and rejecting sets:

We then have that Pπ(s× |= GF φF) = 1 ∀s× ∈ BF, Pπ(s× |= GF φF) = 0 ∀s× ∈ B∅ and B∅ ∩ F × = ∅. Furthermore, BF and B∅ are sink sets, meaning once the set is reached, no states outside the set can be reached.

The proof of this lemma is provided in Appendix A.2. Using this lemma, we can now state and proof the main theorem of this paper.

Theorem 2 (Optimality Guarantee). Given an LTL formula φ and a product MDP M×, there exists an upper bound U ∈ (0, 1] for rewards and a discount factor γ ∈ (0, 1] such that for all product rewards r× and product discount functions γ× satisfying Definition 6, the optimal deterministic memoryless policy πr that maximizes the expected discounted reward Gπr 0 (s×0 ) is also an optimal policy πφ that maximizes the probability of satisfying the B¨uchi condition Pπφ (s×0 |= GF φF) on the product MDPM×.

Proof sketch. We now present a sketch of the proof to provide intuition for the main steps and the selection of key parameters. The full proof is provided in Appendix A.3.

To ensure optimality, given a policy π with the product MDP M× and the LTL formula φ, we want to demonstrate a tight bound between the expected discounted reward following π and the probability of π satisfying φ, such that maximizing one quantity is equivalent to maximizing the other.

At a high level, we want to select the two key parameters, the reward upper bound U ∈ (0, 1] and the discount factor γ ∈ (0, 1], to adequately bound: (i) the rewards given for paths that eventually reach rejecting BSCCs (thus not satisfying the LTL specification); and (ii) the discount of rewards received from rejecting states for paths that eventually reach accepting BSCCs.

Algorithm 1: KC Q-learning from LTL

Input: environment MDP M, LTL formula φ 1: translate φ into an LBDAA 2: construct product MDPM× usingMand A 3: initialize Q for each s and q pair 4: for l ← 0 to max episode do 5: initialize (s, q , n) ← (s0, q0, 0) 6: for t ← 0 to max timestep do 7: get policy π derived from Q (e.g., ϵ-greedy) 8: take action a× ← π((s, q , n)) in M× 9: get next product state (s′ , q ′ , n′ ) 10: r ← r×((s, q , n), a×, (s′ , q ′ , n′ )) 11: γ ← γ ′ (s, q , n) 12: Q((s, q), a×) α← r+γmaxa∈A× Q((s′ , q ′ ), a) 13: update (s, q , n) ← (s′ , q ′ , n′ ) 14: gets greedy policy πφ fromQ

• 15: return induced policy onMby removing ϵ-actions

We informally denote by C π∅ the expected number of visits to accepting states before reaching a rejecting BSCC, and (i) can be sufficiently bounded by selecting U = 1/C π∅. Next, we informally write C πF for the expected number of rejecting states visited before reaching an accepting BSCC, and denote by N π the expected steps between visits of accepting states in the accepting BSCC. Intuitively, for (ii), we bound the amount of discount before reaching the accepting BSCC using C πF , and we bound the discount after reaching the BSCC using N π , yielding γ = 1 - 1/(C π∅ ∗ N π + C πF ).

In practice, using upper bounds of C π∅, C πF and N π instead also ensures optimality, and those bounds can be deduced from assumptions about, or knowledge of, the MDP.

As shown in the proof sketch, selecting U = 1/C π∅ and γ = 1-1/(C π∅ ∗N π +C πF ) is sufficient to ensure optimality. Using the example of the probabilistic gate MDP in Figure 1 (right), we have that C π∅ ≈ C πF ≤ 10 and N π = 1, so choosing U = 0.1 and γ = 0.95 is sufficient to guarantee optimality. For more general MDPs, under the common assumption that the number of states |S| and the minimum non-zero transition probability pmin := mins,a,s′ {T (s, a, s′ ) > 0} are known, C π∅ and C πF can be upper bounded by |S|/pmin, while N π can be upper bounded by |S|.

3.4 LTL LearningWith Q-Learning

Employing this product MDP M× and its reward structure, we present Algorithm 1 (KC), a model-free Q-learning algorithm for LTL specifications utilizing the K counter product MDP. The product MDP is constructed on the fly as we explore: for action a× ∈ A, observe the next environment state s′ by taking action a× in environment state s. Then, we compute the next automaton state q ′ using transition function ∆(q , L(s)) and counter n depending on whether n ≤ K and q ′ ∈ F. If a× ∈ {ϵq | q ∈ Q}, update q ′ using the ϵ-transition and leave environment state s and counter n unchanged. However, directly adopting Q-learning on this product MDP yields a Q function defined on the whole product

Algorithm 2: CF+KC Q-learning from LTL

Input: environment MDP M, LTL formula φ 1: translate φ into an LBDAA 2: construct product MDPM× usingMand A 3: initialize Q for each s and q pair 4: for l ← 0 to max episode do 5: initialize (s, q , n) ← (s0, q0, 0) 6: for t ← 0 to max timestep do 7: get policy π derived from Q (e.g., ϵ-greedy) 8: get action a× ← π((s, q , n)) in M× 9: for ¯q ∈ Q do 10: get counterfactual imagination (s′ , ¯q ′ , n′ ) by taking action a× at (s, ¯q, n) 11: r ← r×((s, ¯q , n), a×, (s′ , ¯q ′ , , n′ )) 12: γ ← γ ′ (s, ¯q , n) 13: Q((s, ¯q), a×) α← r + γ maxa∈A× Q((s′ , ¯q ′ ), a) 14: obtain (s′ , q ′ , n′ ) using action a× at (s, q, n) 15: update (s, q , n) ← (s′ , q ′ , n′ )

• 16: gets greedy policy πφ fromQ
• 17: return induced policy onMby removing ϵ-actions

state space S×, meaning the agent needs to learn the Q function for each K value. To improve efficiency, we propose to define the Q function on the environment states S and automaton states Q only, and for a path σ of M×, the update rule for the Q function at time step t is:

where s×t = (st, qt, nt), a×t is the action taken at time step t, s×t+1 = (st+1, qt+1, nt+1) is the next product state, and α is the learning rate. We claim that, with this collapsed Q function, the algorithm returns the optimal policy for satisfying φ because the optimal policy is independent from the K counter, with the proof provided in Appendix A.4.

Theorem 3. Given an environment MDP M and an LTL specification φ with appropriate discount factor γ and reward function r× satisfying Theorem 2, Q-learning for LTL described in Algorithm 1 converges to an optimal policy πφ that maximizes the probability of satisfying φ on M.

3.5 Counterfactual Imagining

Additionally, we propose a method to exploit the structure of the product MDP, specifically the LDBA, to facilitate learning. We use counterfactual reasoning to generate synthetic imaginations: from one state in the environment MDP, imagine we are at each of the automaton states while taking the same actions.

If the agent is at product state (s, q, n) and an action a× ∈ A is chosen, for each ¯q ∈ Q, the next state (s′ , ¯q ′ , n′ ) by taking action a× from (s, ¯q, n) can be computed by first taking the action in environment state, and then computing the next automaton state ¯q ′ = ∆(¯q,L(s)) and the next K

value n′ . The reward for the agent is r×(s, ¯q, ¯n), and we can therefore update the Q function with this enriched set of experiences. These experiences produced by counterfactual imagining are still sampled from M× following the transition function T ×, and hence, when used in conjunction with any off-policy learning algorithms like Q-learning, the optimality guarantees of the algorithm are preserved.

As shown in Algorithm 2 (CF-KC), counterfactual imagining (CF) can be incorporated into our KC Q-learning algorithm by altering a few lines (line 9-12 in Algorithm 2) of code, and it can also be used in combination with other automata product MDP RL algorithms for LTL. Note that the idea of counterfactual imagining is similar to that proposed by Toro Icarte et al. [2022], but our approach has adopted LDBAs in the product MDPs for LTL specification learning.

4 Experimental Results

We evaluate our algorithms on various MDP environments, including the more realistic and challenging stochastic MDP environments 2 . We propose a method to directly evaluate the probability of satisfying LTL specifications by employing probabilistic model checker PRISM [Kwiatkowska et al., 2011]. We build the induced MCMπ from the environment MDP and the policy in PRISM format, and adopt PRISM to compute the exact satisfaction probability of the given LTL specification. We utilize tabular Q-learning as the core offpolicy learning method to implement our three algorithms: Q-learning with K counter reward structure (KC), Q-learning with K counter reward structure and counterfactual imagining (CF+KC), and Q-learning with only counterfactual imagining (CF), in which we set K = 0. We compare the performance of our methods against the methods proposed by Bozkurt et al. [2019], Hahn et al. [2019] and Hasanbeig et al. [2020]. Note that our KC algorithm, in the special case that K = 0 with no counterfactual imagining, is algorithmically equivalent to Bozkurt et al. [2019] when setting their parameter γB = 1 - U. Our methods differ from all other existing methods to the best of our knowledge. The details and setup of the experiments are given in Appendix B.

2 The implementation of our algorithms and experiments can be found on GitHub: https://github.com/shaodaqian/rl-from-ltl

We set the learning rate α = 0.1 and ϵ = 0.1 for exploration. We also set a relatively loose upper bound on rewards U = 0.1 and discount factor γ = 0.99 for all experiments to ensure optimality. Note that the optimality of our algorithms holds for a family of reward structures defined in Definition 6, and for experiments we opt for a specific reward function that linearly increases the reward for accepting states as the value of K increases, namely rn = U · n/K ∀n ∈ [0..K], to facilitate training and exploration. The Q function is optimistically initialized by setting the Q value for all available state-action pairs to 2U. All experiments are run 100 times, where we plot the average satisfaction probability with half standard deviation in the shaded area.

First, we conduct experiments on the probabilistic gate MDP described in Example 1 with task "FG a & G !c", which means reaching only states labeled "a" in the future while never reaching "c" labeled states. We set K = 10 for this task, and in Figure 2 (left), compared to the other three methods, our method KC achieved better sample efficiency and convergence and CF demonstrates better sample efficiency while still lacking training stability. The best performance is achieved by CF+KC, while other methods either exhibit slower convergence (Bozkurt et al. [2019] and Hahn et al. [2019]) or fail to converge (Hasanbeig et al. [2020]) due to the lack of theoretical optimality guarantees.

The second MDP environment is the 8 × 8 frozen lake environment from OpenAI Gym [Brockman et al., 2016]. This environment consists of frozen lake tiles, where the agent has 1/3 chance of moving in the intended direction and 1/3 of going sideways each, with details provided in Appendix B.2. The task is "(GF a | GF b) & G !h", meaning to always reach lake camp "a" or lake camp "b" while never falling into holes "h". We set K = 10 for this task, and in Figure 2 (middle), we observe significantly better sample efficiency for all our methods, especially for CF+KC and CF, which converge to the optimal policy at around 150k training steps. The other three methods, on the other hand, barely start to converge at 1200k training steps. CF performs especially well in this task because the choice of always reaching "a" or "b" can be considered simultaneously during each time step, reducing the sample complexity to explore the environment.

Lastly, we experiment on a slight modification of the more challenging office world environment proposed by Toro Icarte et al. [2022], with details provided in Appendix B.3. We include patches of icy surfaces in the office world, with the task to either patrol in the corridor between "a" and "b", or write letters at "l" and then patrol between getting tea "t" and workplace "w", while never hitting obstacles "o". K = 5 is set for this task for a steeper increase in reward, since the long distance between patrolling states makes visiting many accepting states in each episode time consuming. Figure 2 (right) presents again the performance benefit of our methods, with CF+KC performing the best and CF and KC second and third, respectively. For this challenging task in a large environment, the method of Hahn et al. [2019] requires the highest number of training steps to converge.

Overall, the results demonstrate KC improves both sample efficiency and training stability, especially for challenging tasks. In addition, CF greatly improves sample efficiency, which, combined with KC, achieves the best results.

4.1 Runtime Analysis and Sensitivity Analysis

It is worth mentioning that, for counterfactual imagining, multiple updates to the Q function are performed at each step in the environment. This increases the computational complexity, but the additional inner loop updates on the Q function will only marginally affect the overall computation time if the environment steps are computationally expensive. Taking the office world task as an example, the average time to perform 6 million training steps are 170.9s, 206.3s and 236.1s for KC, CF and CF+KC, respectively. However, the time until convergence to the optimal policies are 96.8s, 70.2s and 27.5s for KC, CF and CF+KC, respectively.

For sensitivity analysis on the key parameters, we run experiments on the probabilistic gate MDP task with different parameters against the default values of U = 0.1, γ = 0.99 and K = 10. As shown in Figure 3, if U(= 0.5) is chosen too high or γ(= 0.9) is chosen too low, the algorithm does not converge to the optimal policy as expected. However, looser parameters U = 0.01 and γ = 0.995 do not harm the performance, which means that, even with limited knowledge of the underlying MDP, our algorithm still performs well with loose parameters. Optimality is not affected by the K value, while the performance is only mildly affected by different K values.

5 Conclusion

We presented a novel model-free reinforcement learning algorithm to learn the optimal policy of satisfying LTL specifications in an unknown stochastic MDP with optimality guarantees. We proposed a novel product MDP, a generalized reward structure and a RL algorithm that ensures convergence to the optimal policy with the appropriate parameters. Furthermore, we incorporated counterfactual imagining, which exploits the LTL specification to create imagination experiences. Lastly, utilizing PRISM [Kwiatkowska et al., 2011], we directly evaluated the performance of our methods and demonstrated superior performance on various MDP environments and LTL tasks.

Future works include exploring other specific reward functions under our generalized reward structure framework, tackling the open problem [Alur et al., 2021] of dropping all assumptions regarding the underlying MDP, and extending the theoretical framework to continuous states and action environment MDPs, which might be addressed through an abstraction of the state space. In addition, utilizing potentialbased reward shaping [Ng et al., 1999][Devlin and Kudenko, 2012] to exploit the semantic class structures of LTL specifications and transferring similar temporal logic knowledge of the agent [Xu and Topcu, 2019] between environments could also be interesting.

Acknowledgments

This work was supported by the EPSRC Prosperity Partnership FAIR (grant number EP/V056883/1). DS acknowledges funding from the Turing Institute and Accenture collaboration. MK receives funding from the ERC under the European Union's Horizon 2020 research and innovation programme (FUN2MODEL, grant agreement No. 834115).