Imitation Learning with Temporal Logic Constraints
Authors: Zining Fan
He Zhu
Venue: NeurIPS 2025 poster ()
Keywords: reinforcement learning
linear temporal logic
imitation learning
Primary area: reinforcement_learning

Abstract: Designing reinforcement learning agents to satisfy complex temporal objectives expressed in Linear Temporal Logic (LTL), presents significant challenges, particularly in ensuring sample efficiency and task alignment over infinite horizons. Recent works have shown that by leveraging the corresponding Limit Deterministic Büchi Automaton (LDBA) representation, LTL formulas can be translated into variable discounting schemes over LDBA-accepting states to maximize a lower bound on the probability of formula satisfaction. However, the resulting reward signals are inherently sparse, making exploration of LDBA-accepting states increasingly difficult as task horizons lengthen to infinity. In this work, we address these challenges by leveraging finite-length demonstrations to overcome the exploration bottleneck for LTL objectives over infinite horizons. We segment agent exploratory trajectories at LDBA-accepting states and iteratively guide the agent within each segment to learn to efficiently reach these accepting states. By incentivizing the agent to visit LDBA-accepting states from arbitrary states, our approach increases the probability of LTL formula satisfaction without the need for extensive or lengthy demonstrations. We demonstrate the applicability of our method in a variety of high-dimensional continuous control domains. It achieves faster convergence and consistently outperforms baseline approaches.

Imitation Learning with Temporal Logic Constraints
Zining Fan Rutgers University zf zf140@scarletmail rutgers.edi edu
He Zhu Rutgers University hz3750cs rutgers.......... edu
Abstract
Designing reinforcement learning agents to satisfy complex temporal objectives expressed in Linear Temporal Logic (LTLL,, presents significant challenges, par- ticularly in ensuring sample efficiency and task alignment over infinite horizons. Recent works have shown that by leveraging the corresponding Limit Deterministic Bitchi Automaton (LDBA) representation, LTL formulas can be translated into variable discounting schemes over LDBA-accepting states to maximize lower bound on the probability of formula satisfaction. However, the resulting reward signals are inherently sparse, making exploration of LDBA -accepting states increas- ingly difficult as task horizons lengthen to infinity. In this work, we address these challenges by leveraging finite-length demonstrations overcome the exploration bottleneck for LTI. objectives over infinite horizons. We segment agent exploratory trajectories LDBA POBBA-accpptig states and iteratively guide the agent within each segment to learn to efficiently reach these accepting states. By incentivizing the agent to visit accc-pccpiin states from arbitrary states, our approach increases the probability of LTL formula satisfaction without the need for extensive lengthy demonstrations. demonstrate the applicability of our method variety high-dimensional continuous control domains. It achieves faster convergence and consistently outperforms baseline approaches.
Introduction
Linear Temporal Logic (LTL) has been extensively studied an alternative framework for specifying objectives for reinforcement learning (RL) agents [54] 27 13,
62 3 16 63) LTL provides powerful
and flexible language to define tasks with temporal dependencies, such as "cycle between two subgoals while always avoiding unsafe regions" or "eventually reach a goal after completing sequence of particularly challenging when considering infinite horizons, where the agent must maintain behavior that satisfies the objectives indefinitely. These challenges are compounded by the need to ensure sample efficiency high- dimensional, continuous systems.
subtasks" [2]. Designing RL agents to satisfy these objectives
Several recent studies (28 63 [3) have proposed proxy reward schemes derive policies from the Limit Deterministic Büchi Automaton (LDBA) representation of LTL specifications. A trajectory satisfies an LTL formula if and only if it visits an a-cc-picpp state infinitely often. However, these proxy rewards, defined over LDBA acceppiigg states, are inherently sparse, posing challenges for effective exploration toward such states.
To address these limitations, we propose a novel framework, Tol. (Temporal Logic Imitation Learning), which leverages Learning from Demonstrations mitigate reward sparsity in policy optimization for LTL objectives. The high-level idea to combine the structure of LDBAs with finite-length demonstrations to guide exploration. Specifically, TiLoIL segments exploratory agent trajectories at each visit to an LDBA accepting state, treating each segment as sub-trajectory leading toward acceptance. Using these segments, TiLoIL encourages the agent to learn how efficiently reach LDBA accepting states by imitating expert behavior along these sub-trajectories. In essence,
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

TiLoIL encourages the agent to consistently seek LDBA-accepting states from any non accepting states, thereby increasing the likelihood of satisfying infiite-horizae LTL formulas. Along the way, Tollll. learns reward function for reaching L.DBA-accepring states by contrasting successful trajectories with unsuccessful ones. This reward function is then leveraged for policy training, hence reducing the need for extensive or lengthy demonstration data.
Moreover, TiLoIL uses the inherent multistage structure of LTL formulas further densify the reward function to reach the LDBA-acceptin states, At each stage, the reward function provides the agent with rich reward signals specifically tailored that stage. This staged approach improves the efficiency of the learning process compared to treating LDBA-accepting state reaching as a single monolithic procedure.
We demonstrate the effectiveness Til across a range of tasks in high-dimensional continuous systems, which have historically posed significant challenges for L.TL-based RI methods. Our method achieves faster convergence and outperforms baseline approaches, demonstrating superior generalization to unseen scenarios. By leveraging the synergy between LTL specifications, LDBA representations, and demonstration data, TiLoIL provides a practical solution to design RL agents that satisfy complex temporal objectives.
Background and Problem Setup
This section sets up our reinforcement learning problem to solve tasks specified by Linear Temporal Logic (LTL).
2.1 Linear Temporal Logic (LTL)
LTL [50] is specification language that combines atomic propositions (APs) and logical operators describe system behaviors and temporal properties. An atomic proposition AP represents basic indivisible statement about the state of a system that can be true or false at a given time. The logical operators include: not (-), and (A), and implies (-+;; and the temporal operators include: next (X), (G), eventually (F), and until (U). Appendix C defines the syntax and semantics of LTL formulas. For complete introduction, we refer the reader Baier and Katoen (7].
Satattedly/lwwys//lolbll
Example. Consider the Flat World environment in Fig. I with AP = {y. g. r, b} where r labels the red region, g labels the green, y labels the yellow, and b labels the blue. If the task is to eventually reach the yellow zone and remain there, we express this as y = FGy. Alternatively, if we require the agent oscillate infinitely between the yellow, green, and red zones while avoiding the blue zone, we express this as = GF(y A XF(g A XFr)) A G-b, which combines the properties of safety, reachability, and progress.
From LTL to LDBA. The satisfaction of LTL formulas can be formally defined using Limit Deterministic Büchi Automata (LDBAs). An LDBA can be derived from any LTL formula & and keeps track of the progression of tp satisfac- tion [57]
rayapa-a
Definition 2.1 (Limit Deterministic Büchi Au- tomaton (LDBA)). An LDBA is tuple L = EB,EU,, 1 B* bo). where B is a finite set of states, Σ 2AP is alphabet over atomie propositions, pB B x Σ U + B is a tran- sition function, B* C B is set of accepting states, and by E B is the initial state. There ex- ists a mutually exclusive partitioning B B = BDUB, such that B Bp and for (b, (Bp E). then p8 (b, a) C Bp. E is a set of "jump" actions, also known as epsilon-transitionss, for b E By that transitions to BD without evaluating any atomic propositions.
-
Figure 1: Left: FlatWorld Cycle environment with LTL. spec &p = GF(y (F((gFFFr)) A G-b. Right: LDBA for & accepts paths reaching state 3 in- finitely. Blue region b leads to sink.
Example. In the Flarlorld environment (Fig. left) and its corresponding L.TL specification xp GF(y A XF(g A XFr)) A G-b, the LDBA is shown in Fig. (right).

---

An infinite sequence of LDBA actions (a,) E Ex induces a path p = (b:) according to bi+1 = PB ())
Definition 2.2 (Limit Deterministic Büchi Automaton (LDBA)), An LDBA C accepts a path (6)) if and only if the path visits accepting state b* 8 infinitely often, that is: Vt N, 3t t such that by E B
Given an LTL formula yp, we translate into an LDBA L. Satisfaction of yp by an infinite sequence of AP evaluations (w-word) corresponds directly to the acceptance of the path (6:) induced by the w-word in C (Def. 2.2
2.2 Product MDP with LDBA
A Markov Decision Process (MDP) is defined as a tuple .M- = (S,A, po). where S and A represent the state and action spaces, which may be continuous or discrete. The transition kernel P: x A + (SS) describes the system's 's dynamics, representing probability distributions over S. No E (SS) specifies the initial state distribution.
To integrate atomic propositions (APs) into MDP states, as in previous work 63 62
we assume the existence of labeling function F : S - E which returns the atomic propositions that true in that state. The labeling function can be thought of as a collection of event detectors that activate whenever the propositions in AP are satisfied within the environment.
We define control policies over the product space of an MDP M and an LDBA L, aiming to generate accepting trajectories that satisfy an LTL formula yp from which the LDBA L is derived.
Definition 2.3. [Product MDP] Given MDP M PP, and LDBA L. (B, E U E, __p,B,t,00 bo). a product MDP M = (S% A px .M)) synchronizes M with L, where S* = 5 x Ax = A A,E, and p (s, b) = (0())) In-bo- The transition kernel px is defined using
the labeling function F as follows:
P(s' s, if A, 8' = p
(b,, F(s)) a E, b = (b. ==
px ((S'b') (s.b),
(s,
= 1.
0.
otherwise
We say that (s, 6) is an LDBA- --BA-pccgpting product state if E B* Def. 2.3 allows the connection of trajectories (and, consequently, policies) to the satisfaction of given L.L formula. Consider L.T.. formula and its corresponding LDBA L, along with a trajectory = (8i, 0.); o in the product MDP M The trajectory } & (i.e., satisfies up) if and only if accepts the path (h:) the projection of r onto the LDBA states.
S* + A(AX). The probability that satisfies yp can be expressed as the expected value of the indicator for trajectories satisfying yo: P(х + .) = Ersx [[+ Optimizing a policy x for the satisfaction of an LTL specification &p can therefore be formulated as finding 't' E arg max P( + 10) where IT denotes the space of all admissible policies.
Now, consider policy
2.3 Imitation Learning for LTL- CTL-Constrained Tasks
To maximize the probability of satisfying the LTL formula P(T } -) an RL algorithm incentivize the agent to visit LDBA-accepting states as frequently possible [27 63
However, this approach presents significant challenge for exploration due to the inherent sparsity of the feedback: the agent receives rewards only upon making substantial progress toward task completion, such as reaching an accepting state in the LDBA. Visits to multiple non-accepting states within the LDBA during exploration may not provide meaningful learning signals, there is guidance from unexplored regions of the LDBA. Our main idea is to leverage the global structure of the LDBA and integrate with expert task demonstrations to generate a dense reward signal along the LDBA paths for efficient agent exploration.
Expert Demonstrations. TiLoIL assumes expert demonstrations D Despen in the form of sequences of MDP states observed during the execution task by an expert policy, providing information about the regions of the state space relevant for task completion. First, we do not assume that demonstrations are collected in the product MDP. This ensures that the discriminator cannot exploit LDBA state information shortcut to bias its decisions, which could result in uninformed learning
3

---

signals. Second, our demonstrations consist solely of state trajectories, reducing the burden of generating detailed action sequences. This choice also aligns with our goal of learning policies in the action space A of the product MDP. Since expert demonstrations operate within the raw MDP action space A, the demonstrated actions do not include the "jump" actions in AX
Imitation Learning. The introduction of the Generative Adversarial Imitation Learning (GAIL) algorithm [29] has driven significant advances in scalable deep imitation learning methods [23 24
39
48 Beyond adversarial approaches, several imitation learning algorithms aim to match
the state action distributions of the expert and the agent through adversariil techniques, such as
conpaaametric models [38] random network distillation [64], support estimation [IO], Wasserstein
distance minimization [15), and moment matching [59].
In this paper, we adopt the GAIL framework. Recent studies ( have shown that GAIL, and its extensions consistently perform well varying sample sizes. However, TiLolL is not restricted to adversarial approaches and can be extended to other distribution matching imitation learning techniques. TiLoIL shapes reward signals using a discriminator (s), which is trained distinguish between states from high-quality trajectories B comprising expert demonstrations Dexper-andt and states from low low-quality trajectories B consisting of the agent's 's own exploratory rollouts 7 ~ To sampled from M States that resemble those in B receive higher rewards from the discriminator Sa. while those similar to B receive lower rewards. Tol. employs an iterative training procedure, alternating between updating the discriminator J and the policy Tg- The policy is optimized to generate trajectories that are increasingly indistinguishable from expert behavior, by maximizing the shaped reward Tgg (' b), a) tanh(fa Given discount factor y, the policy objective is: Jxx (ó) = Erors IE 7" ro ((st, b,), az)]
Temporal Logic Imitation Learning. Assuming access to expert demonstrations Despent TiLolL jointly optimizes the probabilistic satisfaction of an LTL formula o and the imitation learning objective J,:
π
= arg max (P( - :)) EIl
3 Imitation Learning with LTL Constraints
We emphasize that the learning objectives in our problem formulation, as presented in Eq, D are not in conffict. Among the set of policies that mimic expert demonstrations Despen (i.e., maximize J (o)), there exists at least one policy Ty that adheres to the specified LTL formula fp. Conversely, there exists one policy satisfying the specification yp (i.e., P(T } ()) that also closely aligns with the behavior demonstrated by the expert. We formalize this intuition below:
Theorem 3.1. Let лa and 722 be two policies with corresponding occupancy measures Pr, and Pr For any Linear Temporal Logic (LTL) formula yo the difference in the probabilities of satisfying & under these policies is bounded by twice the total variation distance between their occupancy measures:
[P(T] + P(m $ 2 (Pv Paz);
where the total variation (TV) distance between the distributions Pr. and Prz is given by Drv(pn, Pr.)) 1/2 S, Ipx, (T) Prz (T)
Let Ti be the expert policy ag from which demonstrations are collected, and T2 be the imitation learning policy TT. This theorem shows that minimizing the total variation distance between me and nH leads to policies that maximize LTL satisfaction. The use of GAIL for imitation learning to minimize the IS (eeneenSShanoo) divergence reduces this TV distance, driving policies toward optimal satisfaction of LTL properties. The proof is in Appendix D
Main Challenge. Theorem 3.1 does not directly apply in practice, as the infinite-length demon- strations required by LTL tasks are impractical generate. For tasks with eyclic structures (c.g.. Fig. [p. it is unrealistic to assume that expert demonstrations contain a large number of visits to LDBA- acceppicg states, due to the cost and complexity of constructing such demonstrations. Instead, we assume that demonstrations may include only one or two visits to an accepting state. This high- lights a fundamental tension between the theoretical requirement of infinite visits to LDBA-accepting states and the inherently finite-horizon nature of expert demonstrations. First, the limited learning signal from such sparse demonstration data makes challenging for the agent to generalize its behavior to satisfy LTL constraints over infinite horizons. Second, since environment states near

---

LDBA- accepting states are typically unique to expert demonstrations and differ substantially from the agent's exploratory behavior, particularly in the early stages of training, the discriminator may develop a reward function that assigns higher rewards to these states. Consequently, optimizing J= (e) under finite-length demonstrations could lead the agent to become trapped near an -aceeppc state, where the rewards are higher. In this way, the agent lacks incentive to actually reach the accepting state and then leaves it to initiate another trail aimed at reaching the accepting state again. This would result in suboptimal behavior, as the policy fails to reach LDBA-accepting states frequently enough.
3.1 Segmented Imitation
Our core idea to address the aforementioned main challenge is segmenting agent exploratory trajectories in .Mx based on visits to LDBA-accepting states, where each segment represents a subtrajectory toward an accepting state. From the agent's perspective, each segmented rollout can start in any state within the state space and the goal is to reach an LDBA-accepting state; when the agent reaches accepting state, the next rollout starts directly from its current state, with the goal remaining the same: reaching an LDBA-accepting state. This structure incentivizes the agent to continuously seek LDBA- acceppicn states, regardless of the starting point of each trail, thus encouraging their infinite visits and improving P } () the probability of LTL formula satisfaction. Even if the demonstration contains only a single visit to an accepting state, it can be reused to guide the agent toward efficiently reaching LDBA- -acceppinn states within each segment of its rollout, thereby optimizing (Ø). We formalize our method based on off off-policy Q learning.
Q-Function Update. The Q-function Qo((s b), a) for state and action pairs from MM* is updated by minimizing the Bellman residual using data sampled from a sampled replay buffer B. The loss function is defined as follows:
( = ((((A)))
Qo((o,)),, b), -1)²
The target value i is defined as:
ÿ 1/(1 77), [[((s b)) + 7 [Quarg]
b B* b o B
(4)
where R((ss,) b)) = (()) is the reward from the learned discriminator function fs that separates B+ as segmented expert demonstrations and B as segmented policy rollouts. Here, Qearg = b)) -a a log To (aa(((('',))) is the target Q value computed using a target network with parameters 8, a is the temperature parameter controlling the trade-off between reward and entropy, and log o (s'[(s',))) is the entropy term used to encourage exploration.
we use the discriminator reward in (((s, b)) to train Qo to optimize (Ø) in our learning objectives in Eq. [ encouraging the agent to mimic expert behavior to reach L.BA L.BAA-accptting states. Upon reaching an acceppicn state (s, b) such that E B*, we directly set the target value for ((ss,b), b), a) (for any action a) to r First, this Q value is sufficiently large to incentivize the agent to reach the LDBA-accepting state (s, b), rather than lingering nearby, thereby ensuring continuous progress toward satisfying the LTL constraint. Second. in this way, each segmented rollout does not interfere with others, effectively addressing the main challenge.
Intuitively,
The policy (a(((s b)) is updated by minimizing the entropy-regularizze expected Q-value, balancing exploration and exploitation. The loss is:
Policy (TT) Update.
(Ø) = [((,b)= (Buaaa(-1(s.))) [a log (a (s. b)) - Qo((s,)),,....).)))))),(()) b)]
(5)
Here, the entropy term a log (a b)) promotes exploration, while the Q- term - (Q a) encourages reward maximization.
The following theorem bounds the Q-function update in Eq. relative the optimal Q-value under the assumption of infinite-horizon expert demonstrations:
Theorem 3.2. Let Qo be the learned soft Q-function trained using a modified target value Qtarger I-y in accepting states (s,b) b) where à E B², and soft Bellman backups elsewhere. Assume (a
s, 6) exp (s, b), a)). Suppose that the reward function R[(s, b)) tanh(fu(s)) is bounded
5

---

by R((s,b) b)) E Ruiin R Let Q" be the optimal Q-function under standard soft Bellman backups (without the modified target). Then, for any state-action pair ((s, b). a),
Q)((s,b),a) - Q" ((s,b),,) - ((..) 8max
where k(s,b) b) is the number of steps it takes from (s, b) under Te to reach some accepting state (s/, with V/ E B and 6max == 1- 1 accepting states, Hmin denotes the minimum entropy of Td.
is the worst-case overestimation error at any
The theorem shows that, while Q-values are inflated to make L.BA-accepting states attractive, this overestimation decays exponentially with distance. For states that appear early in a segmented trajec- tory-those farther from acceptance-the corresponding Q-values are significantly overestimated. The learning process therefore remains grounded. The proof is in Appendix D
3.2 Multi-Stage Discriminator Learning
The learning strategy described in Sec. 3.1 still faces challenges when long horizons are required to reach each Lace-aacepting state. We ob- serve that many LTL tasks inherently consist of multiple stages. Take, for example, the FlatWorld Cycle task with the LTL. specification GF(y A XF(g A XFr)) G-b and its LDBA, illustrated in Fig. T Any valid trajectory between the LDBA accept- ing states can be divided into three distinct stages. Initially, the LDBA state is 0 and the agent is in the white space for the first stage of reaching the red zone. Upon reaching the red zone (r), the LDBA transitions from 0 to and the agent is the second stage of reaching the yellow zone. If the agent touches the blue region in the mid- dle at any point, the LDBA transitions into a sink state and remains there for the rest the episode. How can we design staged approach for LDBAs that makes the learning process more efficient compared to treating them as
Discriminator
Discriminator
Discriminator 2
neg
pos
Butfer
Butter Ba
Ba
trajectories reaching red
segmented trajectories reaching green
demonstrations trajectories
trajectories
Figure 2: We illustrate the multistage discriminator for the FlatWorld Cycle environment in Fig [ TiLoIL maintains separate stage buffers to store trajectories corresponding to different LDBA states. Here, the colors of the buffers match the corresponding automaton states in Fig, T Each seg- mented trajectory is assigned to only one stage buffer based on its maximal stage (Eq. 7 Bid holds segmented trajec- tories that do not enter any colored zones, while B,, stores segmented trajectories that visit the red region but do not reach yellow. For Discriminator O, negative data are drawn from buffer Ba, and buffer B1 which stores unsafe trajecto- ries, while positive data are sampled from buffers Bb,, Bbg- and Bbg As such, the discriminator provides reward signals that encourage the agent to reach the red region and beyond.
a single monolithic stage?
We begin by presenting key definitions, followed by an illustration of our proposed approach. Define by ~ by as an acyclic path in the (graph representation of) LDBA L, where by and by are states in C. such that the path begins at 6, ends at bj. and does not include any accepting states by E B other than possibly by if by is an accepting state:
b. ~ by
3 path (b,, b..1...., by) in L such that
(6) by & B" vk + j. and Vk, k # # = by + be.
Define by ~y" by - (b, ~+ by Vb, = by). We define a sink state of an LDBA L as a state b, E B such that p8 (bb. b.. Once the agent transitions to a sink state, it cannot escape, thereby failing to reach any accepting states. Sink states are useful for modeling safety properties, such as globally avoiding the blue obstacle shown in Fig. [
We use SINK(C) to denote all sink states of L.
Multistage Discriminators. In dense reward setting for multistage tasks, the reward of an environment state associated with an LDBA state by should exceed that of by if by ~4 bt, as this encourages the agent to progress toward the LDBA's accepting states. If each state in an LDBA L viewed as an individual stage, a separate discriminator can trained for each stage to serve as a dense reward for that particular stage. By training stage-specific discriminators, we can effectively

---

guide the agent's 's progress through the different stages of the task. To train the discriminators for different stages, we establish positive and negative data for each discriminator. We assign a maximal stage to each trajectory т, which is determined as the L.BAA state that advanced the furthest towards accepting states among all LDBA states within T:
MaxStage(T ((so, bo)..... (sN, bx))) = b, such that path p (b. by) A by E BB.
bby E (bo.-.., .bN 44, by not in (7)
For the discriminator associated with the LDBA state bR. positive data include trajectories r+ with maximal stage MAXSTAGE(F*) progressing beyond by and up to an accepting state, formally expressed as 3by E 8 by- MAXSTAGE(7*) --" by. Conversely, negative data consist of trajectories T that only reach up to by, such that MAXSTAGE(T) ~y by. or hit any sink state MAXSTAGE(T") E SINK(C). An example is given in Fig. 2
Once the positive and negative data for each discriminator for an LDBA state by have been established, we train discriminator fb. that predicts if an MDP state s E S comes from the positive trajectories whose maximal stage is beyond the LDBA state b2. as opposed to the negative trajectories that fail to progress beyond by or trap into sink states. The discriminator is trained using the BCE loss where positive data B+ includes states from -+ trajectories and negative data B consists of states from T trajectories. We note that 3 always includes (segmented) expert demonstrations that surpass all LDBA states on the path toward accepting states.
Multistage Reward Formulation. The next step is to combine these discriminators to create reward function that guides the agent to LDBA-accepting states. Our formulation is inspired by [45] We define our learned reward function for product MDP state in multi-stage task as follows:
R((s, b)) = (bDx(b) + 3 (anh(f((s)
(8)
N(bb)
where (bD computes the length of the longest acyclic path in the LDBA from the initial state to b, serving as an approximation of the stage index of the product MDP state (s, b), and 3 is a hyperparameter. The tanh function is used to bound the output of the discriminators. As the range of the tanh function is (-1, 1). any 8 < ensures that the reward of a state stage i + 1 is always higher than that of stage k. In practice, we use 3 = 3-2 Dividing it by (b), where (b) denotes the length of the longest acyelic path in the LDBA from the initial state to any accepting state through b. scales the rewards to values less than 1.
Main Algorithm. The main algorithm of TiLoIL is summarized in Algorithm | We use SAC (25 for policy training. In addition to the regular replay buffer used in SAC, TiLoIL maintains different stage buffers Bb, to store trajectories corresponding to different LDBA states 6y. Each trajectory is assigned to only one stage buffer based on its maximal stage (Eq. 77. During the training of the discriminators, we sample data from the union of multiple buffers. Policy updates are then guided by reward functions derived from these trained discriminators.
4 Experiments
This section empirically evaluates TiLoIL by addressing the following questions: (Q1) Does TiLolL improve exploration in LTL-constrained tasks? (Q2) Are the new fimeming-foom-ddmmnnstaaiiono strategies TiLolL necessary to learn policies that align with the LTL constraints?
Baselines. To answer Q1, we compare TilolI. with three state-of-the-arr policy optimization al- gorithms for LTL task objectives: (1) LCER (63) a counterfactual experience replay scheme, (2)
Cycler [55]. method focusing on cycle environments, and (3) DRL 2 (6). a direct exploration algo- rithm that encodes LDBAs as a Markov reward process for reward shaping. This evaluation focuses on TiLolL's 's exploration capabilities relative to these RL-based approaches. For Q2, we compare TiLoIL with conventional imitation learning algorithms GAIL 22 PWIL [14] and SQIL (53]. As discussed in Sec. 2.3] TiLoIL can be integrated into any generative adversarial and distribution matching imitation learning methods. However, rather than evaluating a broad range of algorithms, our focus is on assessing how our proposed strategies improve the imitation learning algorithm that it builds on (GAIL). our experiments, we combined SAC (25) with Tol.l.., GAII,, PWIL., and SQII. to perform policy updates on batches of data sampled from the agent's 's replay buffer.
7

---

Algorithm TiLolL Main Algorithm
Require: MDP M, LDBA & = (B, E,E,, pB, B*, (,,,))))))) bo), Demonstration dataset D = {T0, 7 )...)
1: Initialize policy TΦ. critic Qe. replay buffer B
2: Initialize discriminators fou fo..... for by B B*
3: Initialize stage buffers Bbo Bb, Bb..... for by E B
4: Populate the stage buffers for 5* with 'D
5: for each iteration do
6: Sample trajectories T by executing Te in M "M* = x
7: Segment T at LDBA-accepting states (s, b) such that 6 E B to obtain (To -xx _1 : xT 5...f
8: for each trajectory 7 x in { _1x 3-.- do
9:
by + MAXSTAGE(TT*
10:
if b, SINK(C) then
11:
B B1 J {
12:
else
13:
Bb, + Bo, (++
14:
B ( - .
for each gradient step for the discriminators do for each state by in B B \ SINK(C) do
16:
Sample positive data from Us. for all b, s.t. Bb B bu vt bj wn* by
18:
Sample negative data from U Br, U Bb, BB_ for all b, s.t. b, ws* by Update for using BCE loss for each gradient step for the policy T do
19:
20:
21:
Update Qo via Eq. and TH via Eq. 5 by SAC via samples from B
Environments and Tasks. Our benchmarks, as visualized in Fig. 3 include tasks drawn from LCER [63] and DRL (6) complemented by new environments we developed to highlight exploration challenges in LTL tasks. On the top left, GridCivcular Hard is a discrete 2D grid world where the agent moves in four cardinal directions stays stil[] The environment is a cross-shaped grid of five squares, where the center is an obstacle. The agent must repeatedly loop through the outer squares while avoiding the center. Next in the upper row, a point agent in FlatWorld Stabilization must stabilize in the yellow zone, while in FlatWorld Cycle, it oscillates between red, yellow, and green infinitely, always avoiding blue regions. On the left of the second row, the Doggo agent, a 12-DoF quadruped robot (52). must (i) traverse a narrow corridor collision-free (Doggo Avoid) and (ii) sequentially navigate two designated zones (Doggo Navigate). In the bottom-left, Fetch robotic arm (17) performs four tasks: (i) guiding its gripper to a target position while minimizing lateral movements (Fetch Avoid); (ii) achieving horizontal alignment of three cubes (Fetch Align); (iii) placing block into tray when the tray is present, or into the goal region when it is absent (FetchPlace Tray); and (iv) repeatedly moving the cube to the current goal region (red) and pressing the green button to change the goal location, requiring the agent to alternate between goal reaching and button pressing (FetchPlace Button). On the right, in the Carlo environment, the agent drives self-driving simulator based on a bicycle model counterclockwise on circular track, repeatedly visiting two blue regions without crashing. In Cheetah Flip, the HalfCheetah agent performs frontflips to alternate between standing on its front and back legs infinitely. In SixteenRooms, the agent is initially positioned at the center of the bottom-left room. The task requires the agent to follow a circular path indefinitely using one of two possible routes in grid of rooms: a large loop passing through a set of rooms and a smaller loop passing through another subset. The agent must avoid collisions with walls separating rooms and learn to repeatedly traverse one of the valid loops. All task specifications in LTL and additional environment details are provided in Appendix H
While TiLoIL assumes ffnite-length) expert demonstrations, in evaluation, we relax this assumption and use demonstrations that are not necessarily optimal. For our tasks, the demonstrations are generated by designing dense rewards and training individual policies for each stage of a task (e.g., training a policy to reach the yellow zone and another to reach the green zone in Forld Cycle). Trajectories that successfully reach accepting states are collected by sequentially exccuting these policies. Both TiLoIL and the baselines GAIL, PWIL, and SQIL are provided
Demonstrations.
We compared TiLoIL with the baselines in suit of discrete environments from 6 in Appendix

---

GridCirculer Hard
FlatWorld Stabilization
Flat World Cycle
40
(atuuns
Reoumz
Denums
100c 150K 2002
10ck 200k 100k-40Kk
Steps
Steps
Steps
Doggo Avaid
Doggo Navigate
Carlo
Retume
200
200
Pature
10ck 40ck
Flip
5.0
Rahurna
Returs
2.5
L0ok 2001 2008 400k
500k 1M 15M 2M
250k500k 75
Staps
Stops
Staps
Fetch
FetchPlace
StxteenRooom
Bet
20
20
250k Sook 750k 14 Stops
500k
1.5M
200k 400k 6ook BOOK Stops
Stops
TitiiL
LCER
DAL
Cycler
GAIL
PWIL
SQIL
BC
Figure 3: Returns under eventual discounting [63] comparing TiLoIL and the baselines over 10 random seeds. The shaded region indicates the standard deviation.
with only 5 demonstrations. environments with cyclic structures GridCircular, FlarWorld Cycle, Carlo, Cheetah Flip, FetchPlace Button, and SixteenRooms cach trajectory contains at most visits LDBA accepting states. Our goal is to show that even finite-length, non-optimal demonstrations obtained from suboptimal policies that visit LDBA- states only once twice-can can be effectively used to learn policies satisfying LTL objectives over infinite horizons.
Results. In Fig. 3 the x-axis shows the environment steps and the y-axis shows the cumulative
returns under eventual discounting (App. H.3). Computing the probability of LTL satisfactions over infinite horizons requires estimating policy occupancies, which is intractable. This return function, as a proxy for the likelihood of task satisfaction (63, counts visits to acceppiinn states, assigning reward of per visit with future discounts applied only such states.
(Q1) Does TiLoIL help the learning process for LTL-constrained tasks? According to Fig. TiLoIL significantly accelcrates learning compared to the RL-based policy optiiiztionn approaches LCER, 2RL and Cycler. In our experience, Cycler faces challenges in scaling ous environments. Integrating the global structure of an LDBA and with expert task demonstrations, TiLoIL provides informative rewards in each LDBA transition, effectively guiding exploration toward accepting states, advantage absent in LCER. Although DRL also learns an intrinsic reward signal along LDBA paths to aid exploration, TiLoIL provides stronger guidance through demonstrations, allowing faster transitions to Fetch Align and Carlo. In Carlo, TiLoIL completes 3-4 rounds within the track in 500 steps, while the baselines struggle to complete even one.
nigh-dimensional continu-
states, particularly in complex environments, e.g.
(Q2) Are segmented imitation and multistage discriminator learning in TiLoIL necessary? Our results show that TiLolL generates significant lift over its baseline algorithms GAIL,, PWIL and SQIL in the learning curves Fig. for all tasks with cyclic structures, such as Cheetah Flip and FetchPlace Button, highlighting the importance of segmented imitation for generalizing policies to repeated accepting- visits over infinite horizons. other multistage tasks, such as Doggo Navigate, Fetch Align, and SixteenRooms, the improvements over these imitation learning baselines are attributed to the generation of stage-specific rewards that guide intermediate goal achievement, without which the learning signal from monolithic discriminator may lead to flat value landscape.

---

Daggle Arodd
Degge Raziglle
Fatibh Anai
Patch ANg
Cadea
Cleedak Fil
19th 16th 300c
483c
39%6 D0w SCRE
180c 20t S00E
25 500 750 JM
ICee 33% 330 600
3754 15%
525
790
Figure 4: Ablation studies for TiLolL over 10 random seeds using returns under eventual discounting. Results for TiLolL-noSegment are omitted in Doggo and Fetch tasks. For these non non-circular tasks, their LDBAs absorb at accepting states when safety is ensured. Thus, trajectory segmentation has negligible impact, leading to similar reward curves for TioeeeenoSegment and TiLoIL in these tasks.
Ablation Studies. We assess the individual contributions of (a) segmented imitation and (b) multistage discriminator learning to the overall performance. The first ablation, TiLolL-nos LoosemenS,,mmet,, only performs part (b) for multistage discriminator learning. The second ablation TiLolL-noStage only performs part (a) for segmented imitation. Fig. 4 confirms the importance of segmented imitation, as circular tasks (Carlo and Cheetah Flip) cannot be solved without it. Multistage discriminator learning is also crucial to ensure cample-efficient learning in all tasks except Cheetah Flip. TiLolL-noStage performs extremely well in this challenging task. We found that the multistage discriminator in TiloIL incorporates successful trajectories that barely achieve standing on the back legs, sometimes leading the agent to just satisfy this subtask without generating sufficient momentum to round over.
In our reward formulation (Eq. 8). 3 controls the contribution of shaped rewards from multi-stage discriminators. As shown the ablation results in Appendix F.I] a larger 3 yields improved perfor- mance on complex tasks, as the shaped rewards from the discriminator provide effective guidance for learning, Additional ablations in Appendix F22 and Appendix |3 further examine TiLoIL's 's scalability to complex LTL formulas and its robustness to incomplete or unsafe demonstrations.
We experiment with TiLoIL under different numbers of demonstrations and observed that it can effectively bootstrap learning without requiring many demonstrations. See Appendix G details.
5 Related Work
Reinforcement learning from linear temporal logic (LTL) has advanced significantly, with many approaches leveraging structural insights to guide learning [54] [8] (30] 31 12 [3].. Early methods aligned value and policy optimization using product MDPs and reward signals encourage task
satisfaction [ 12
13
27
28
leading to principled approaches that optimize lower bounds 63 To address reward sparsity, several methods emerged: rule-based
37
4
on formula satisfaction [56
approaches 43. accepting frontier function [27 28 rewards for initial visits [11 adapted
annotated maps 677. Automata structure has also been used to learn hierarchical 28 31 355, goal-
conditioned [51), modular (U] policies. Recent works further improve LTL-guided exploration via
meta-learning 62), temporal reward shaping (6), eventual discounting [63] and cyclic temporal
constraints for recurring goals [55). We discuss related work in broader contexts in Appendix B
6 Conclusion
We present TiLoIL, an imitation learning framework for policy optimization under LTL constraints. TiLoIL employs segmented imitation learning to guide the agent toward LDBA-accepting states following task demonstrations from any state within the state space, thus optimizing the satisfaction of the LTL formula over infinite horizons. Furthermore, TilolL integrates LDBA structures with task demonstrations to construct dense reward signals along LDBA paths, facilitating efficient exploration toward accepting states. Our results demonstrate that TiL effectively solves various high-dimensional tasks with limited demonstrations, outperforming various baselines.
Linitations. While TiLoIL demonstrates strong performance in leveraging demonstrations to satisfy LTL objectives, effectively exploiting suboptimal or incomplete demonstrations remains challenging. We hypothesize that integrating more exploratory RL algorithms could mitigate this limitation. Future work should focus on combining TiLolL's exploitation mechanism with exploration strategies that exploit LDBA structure for more efficient learning of LTTL-constrained policies.
10

---

[5] Kai Arulkumaran and Dan Ogawa Lillrank. A pragmatic look deep imitation learning. In Berrin Yanikoglu and Wray L. Buntine, editors, Asian Conference on Machine Learning, ACML 2023, 11-14 November 2023, Istanbul, Turkey, volume 222 of Proceedings of Machine mlr mlr.press/ Reproducibility Statement
The code for TiLoIL is available on htttpp://giiuuu...om//RAAAAA- TiLoIL
Reeeenninannn--eeeeee Group/
Acknowledgements
We thank the anonymous reviewers for their comments and suggestions. This work was supported by NSF Award #CCF-2124155.
References
[1] Pieter Abbeel and Andrew Y Ng. Apprenticeship learning via inverse reinforcement learning. In Proceedings of the twenty- international conference Machine learning, page 1, 2004.
[2] David Abel, Will Dabney, Anna Harutyunyan, Mark K Ho, Michael Littman, Doina Precup, and Satinder Singh. On the expressivity of markov reward. Advances Neural Information Processing Systems, 34:7799-7812, 2021.
[3] Rajeev Alur, Suguman Bansal, Osbert Bastani, and Kishor Jothimurugan. A framework for transforming specifications in reinforcement learning. Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, pages 604-624. Springer, 2022.
[4] Brandon Araki, Xiao Li, Kiran Vodrahalli, Jonathan DeCastro, Micah Fry, and Daniela Rus. The logical options framework. In International Conference on Machine Learning, pages 307-317. PMLR, 2021.
Learming Research, pages 58-73. PMLR, 2023, URL
v222/ wwwukuumaaan222 an24a. html
[6] Marco Bagatella, Andreas Krause, and Georg Martius. Directed exploration in reinforcement learning from linear temporal logic. arXiv preprint arXiv:2408 09495, 2024.
[7] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008
[8] Lionel Blondé and Alexandros Kalousis. Sample-eficiient imitation learning via generative adversarial nets. In Kamalika Chaudhuri and Masashi Sugiyama, editors, The 22nd International Conference on Artificial Intelligence and Statistics, AISTATS 2019, 16-18 April 2019, Naha, Okinawa, Japan, volume 89 Proceedings of Machine Learning Research, pages 3138-3148. PMLR, 2019, URL http:::t/prccceeiiinngea/o/// www.smll....seeseeee www.ppressvvB v89 blde 19a. html
mlr
[9] Alper Kamil Bozkurt, Yu Wang, Michael M Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. 2020 IEEE International Conference on Robotics and Automation (ICRA), pages 10349-10355. IEEE, 2020.
[10] Kianté Brantley, Wen Sun, and Mikael Henaff. Disagreemeent-eeuulaiiid imitation learning. In 8th International Conference Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL https::/ www.neeetoooaeee id= TkgbYyHtwB
[11] Mingyu Cai, Mohammadhosein Hasanbeig, Shaoping Xiao, Alessandro Abate, and Zhen Kan. Modular deep reinforcement learning for continuous motion planning with temporal logic. IEEE Robotics and Automation Letters, 6(4):7973-7980, 2021.
[12] Alberto Camacho, Oscar Chen, Scott Sanner, and Sheila Mcllraith. Non-markovian rewards expressed in Itl: guiding search via reward shaping. In Proceedings of the International Symposium Combinatorial Search, volume 8, pages 159-160, 2017.
11

---

[13] Alberto Camacho, Rodrigo Toro Icarte, Toryn Q Klassen, Richard Anthony Valenzano, and Sheila A Mcllraith. Ld and beyond: Formal languages for reward function specification in reinforcement learning. In IJCAI, volume 19, pages 6065-6073, 2019.
[14] Robert Dadashi, Léonard Hussenot, Matthieu Geist, and Olivier Pietquin. Primal wasserstein imitation learning. arXiv preprini urXiv:2006.04675 2020.
[15] Robert Dadashi, Léonard Hussenot, Matthieu Geist, and Olivier Pietquin. Primal wasserstein imitation learning. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL httpss:t/////
[16] Giuseppe De Giacomo, Antonio Di Stasio, Moshe Vardi, Shufang Zhu, et al. Two-stage technique for Itlf synthesis under Itl assumptions. In Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, pages 304-314, 2020.
[17] R. de Lazcano, K. Andreas, J. Tai, S. R. Lee, and J. Terry. Gymnasium robotics. GitHub, 2023. URL http:://gtthtt com/ Paaaaaaaaauuaaaatt-iiaaaaaaaaaaa www.rrooonnnnnnaaaaaeeaaeoe irriiioon/nmmniinnni Robotics
[18] Xuchu Ding, Stephen L Smith, Calin Belta, and Daniela Rus. Optimal control of markov decision processes with linear temporal logic constraints. IEEE Transactions on Automatic Control, 1244-12244-2257 2014.
[19] Yuqing Du, Ksenia Konyushkova, Misha Denil, Akhil Raju, Jessica Landon, Felix Hill, Nando de Freitas, and Serkan Cabi. Dision-language models success detectors. arXiv preprint arXiv:2303.07280, 2023.
[20] Zeyu Feng, Hao Luan, Kevin Yuchen Ma, and Harold Soh. Diffusion meets options: Hierarchical generative skill composition for cepporally-extendde tasks. arXiv preprint arXiv:2410.02389, 2024.
[21] Chelsea Finn, Paul F. Christiano, Pieter Abbeel, and Sergey Levine. A connection between generative adversarial networks, inverse reinforcement learning, and energy-based models. CoRR, hts//661.003522 2016. http:///:/aaxx http:/aawwwa...raa//aaaa/// 03852
[22] Kevin Frans, Jonathan Ho, Xi Chen, Pieter Abbeel, and John Schulman. Meta learning shared hierarchies. arXiv preprint 1rXiv:1710.09767, 2017.
[23] Justin Fu, Katie Luo, and Sergey Levine. Learning robust rewards with adversarial inverse reinforcement learning. arXiv preprint 1rXiv:1710.112466 2017.
[24] Seyed Kamyar Seyed Ghasemipour, Richard Zemel, and Shixiang Gu. A divergence mini- mization perspective on imitation learning methods. In Conference on robot learning, pages 1277. PMLR, 2020.
[25] Tuomas Haarnoja, Aurick Zhou, Pieter Abbeel, and Sergey Levine Soft actor-critic: Off- policy maximum entropy deep reinforcement learning with a stochastic actor. In International conference on machine learning, pages 1861-1870. PMLR, 2018
[26] Charles Harris, K Jarrod Millman, Stéfan Van Der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J Smith, et al. Array programming with numpy. Nature, 585(7825):357-36,, 2020.
[27] Mohammadhosein Hasanbeig. Alessandro Abate, and Daniel Kroening. Logically-constrainee reinforcement learning. arXiv preprint arXiv:1801.08099, 2018.
[28] Mohammadhosein Hasanbeig, Daniel Kroening, and Alessandro Abate. Deep reinforcement learning with temporal logics. In Formal Modeling and Analysis of Timed Systems: 18th International Conference, FORMATS 2020, Vienna, Austria, September 1-3, 2020, Proceedings 18, pages 1-22. Springer, 2020.
[29] Jonathan Ho and Stefano Ermon. Generative adversarial imitation learning. Advances in neural information processing systems, 29, 2016.
12

---

[30] Rodrigo Toro Icarte, Toryn Klassen, Richard Valenzano, and Sheila Mcllraith. Using reward machines for high-level task specification and decomposition in reinforcement learning. In International Conference on Machine Learning, pages 116... PMLR, 2018.
[31] Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano, and Sheila A Mcllraith. Reward machines: Exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research, 73:177 1711773-22200 2022.
[32] Craig Innes and Subramanian Ramamoorthy. Elaborating on learned demonstrations with temporal logic specifications. arXiv preprint arXiv:2002.00788 00784, 2020.
[33] Mathias Jackermeier and Alessandro Abate. Deepltl: Learning to efficiently satisfy complex Itl specifications for multi-task rl. In The Thirteenth International Conference on Learning Representations.
[34] Rohit Jena, Siddharth Agrawal, and Katia P. Sycara. Addressing reward bias in adversarial imitation learning with neutral reward functions. CoRR, 0e0/2009.09465 2020. URL https
//arxiv. borg/abs//000/ 2009999477999
[35] Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional reinforcement learning from logical specifications. Advances in Neural Information Processing Systems, 34: 14:10026-1000 2021.
[36] Dmitry Kalashnikov, Jacob Varley, Yevgen Chebotar, Benjamin Swanson, Rico Jonschkowski, Chelsea Finn, Sergey Levine, and Karol Hausman. Mt-opt: Continuous multi-tast robotic reinforcement learning at scale. arXiv preprint arXiv:2104.08212 2021.
[37] Yiannis Kantaros. Accelerated reinforcement learning for temporal logic control objectives. In 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 5077-5082. IEEE, 2022.
[38] Kee-Fung Kim and Hyun Soo Park. Imitation learning via kernel mean embedding. In Sheila A. Mcllraith and Kilian Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 3415-3422, AAAI Press, 2018. doi: 10. 00.1609/AAAL.3221.1111. 11720
URL https://dooi: org 10ogg/10..00 1609/ /aaai. v32i1
[39] Ilya Kostrikov, Kumar Krishna Agrawal, Debidatta Dwibedi, Sergey Levine, and Jonathan Tompson. Discriminator-actor--oni Addressing sample inefficiency and reward bias in adversarial imitation learning. arXiv preprint 1809.00800.0299 2018.
[40] Jan Křetínský, Tobias Meggendorfer, Salomon Sickert, and Christopher Ziegler. Rabinizer 4: From ltl to your favourite deterministic automaton. In International Conference on Computer Aided Verification, pages 567-577. Springer, 2018.
[41] Borja G León, Murray Shanahan, and Francesco Belardinelli. Agent. do you see it now? systematic generalisation in deep reinforcement learning. In ICLR Workshop on Agent Learning in Open-Endednees:
[42] Andrew Levy, George Konidaris, Robert Platt, and Kate Saenko. Learning multi-level hierar- chies with hindsight. arXiv preprint arXiv: met::::12200090 2017.
[43] Xiao Li, Cristian- Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RS/ International Conference on Intelligent Robots and Systems (IROS), pages 3834-3839, IEEE, 2017.
[44] Jason Xinyu Liu, Ankit Shah, Eric Rosen, Mingxi Jía, George Konidaris, and Stefanie Tellex Ltl-transfer: Skill transfer for temporal task specification. arXiv preprint 2tt.::200000099 2022.
[45] Tongzhou Mu, Minghua Liu, and Hao Su. Drs: Learning reusable dense rewards for multi-stage tasks. arXiv preprint X4X:22404.16779 2024.
13

---

[46] Ofir Nachum, Shixiang Shane Gu, Honglak Lee, and Sergey Levine. Data-efficient hierarchical reinforcement learning. Advances in neural information processing systems, 31, 2018.
[47] Andrew Y Ng, Stuart Russell, et al. Algorithms for inverse reinforcement learning. In Icml, volume 1, page 2, 2000.
[48] Manu Orsini, Anton Raichuk, Léonard Hussenot, Damien Vincent, Robert Dadashi, Ser- tan Girgin, Matthieu Geist, Olivier Bachem, Olivier Pietquin, and Marcin Andrychow- icz. What matters for adversarial imitation learning? In Marc' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors, Advances in Neural Information Processing Systems 34: Anmual Conference on Neu- ral Information Processing Systems 2021, NeurlPS 2021, December 6-14, 2021, virtual. pages 14656 14668, 2021. URL Abbr:ooot...bbbbb-bbaaaara..... www.raat..t.tt...... www.weis....ppppeee//eep wwtpc/ppppppp/e/eeepeep
[49] Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang. Zachary De Vito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in pytorch. 2017.
[50] Amir Pnueli. The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977), pages 46-57. icce, 1977.
[51] Wenjie Qiu, Wensen Mao, and He Zhu. Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. Advances in Neural Information Processing Systems, 36, 2024.
[52] A. Ray, J. Achiam, and D. Amodei. Benchmarking safe exploration in deep reinforcement learning. GitHub, 2019. URL
[53] Siddharth Reddy, Anca Dragan, and Sergey Levine. Sqil: Imitation learning via reinforcement learning with sparse rewards. arXiv preprint /905 2019.
[54] Dorsa Sadigh, Eric S Kim, Samuel Coogan, S Shankar Sastry, and Sanjit Seshia. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference on Decision and Control, pages 1091-1096. IEEE, 2014.
[55] Ameesh Shah, Cameron Voloshin, Chenxi Yang, Abhinav Verma, Swarat Chaudhuri, and Sanjit A Seshia. Deep policy optimization with temporal logic constraints. arXiv preprint arXiv:2404 1578, 2024.
[56] Daqian Shao and Marta Kwiatkowska. Sample efficient model-free reinforcement learning from Itl specifications with optimality guarantces. arXiv preprint arXiv:2330.001 01811 2023.
[57] Salomon Sickert, Javier Esparza, Stefan Jaax, and Jan Křetínský. Limit-deterministic büchi automata for linear temporal logic. In International Conference on Computer Aided Verification. pages 312-332. Springer, 2016.
[58] Laura Smith, Nikita Dhawan, Marvin Zhang, Pieter Abbeel, and Sergey Levine. Avid: Learning multi-stage tasks via pixel-level translation of human videos. arXiv preprint arXiv: 2019.
[59] Gokul Swamy, Sanjiban Choudhury, J. Andrew Bagnell, and Steven Wu. Of moments and matching: A game-theoretic framework for closing the imitation gap. In Marina Meila and Tong Zhang, editors, Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event, volume 139 of Proceedings of Machine Learn- ing Research, pages 10022-10032. PMLR, 2021. URL UTRLitttp//pprcceddng mlr .press/ v139/ swamy21a. html
[60] Geraud Nangue Tasse Devon Jarvis, Steven James, and Benjamin Rosman. Skill machines: Temporal logic composition in reinforcement learning. 2022.
14

---

[61] M. Towers, J. K. Terry, A. Kwiatkowski, J. U. Balis, G. d. Cola, T. Deleu, M. Goulão, A. Kallinteris, A. KG, M. Krimmel, Perez- Perez-Vicente. A. Pierré, S. Schulhoff, J. J. Tai, A. T. Shen, and O. G. Younis. Gymnasium, 2023. URIhttpps /ttp///eeooo.oooo org/record/8127025 Accessed: 2025-01-28.
[62] Pashootan Vaezipoor, Andrew Ci, Rodrigo A Toro Icarte, and Sheila A Mcilraith. Lt12action: Generalizing Itl instructions for multi-task rl. In International Conference Machine Learning, pages 10497-10508. PMLR, 2021.
[63] Cameron Voloshin, Abhinav Verma, and Yisong Yue. Eventual discounting temporal logic counterfactual experience replay. In International Conference on Machine Learning, pages 35137-35150. PMLR, 2023.
[64] Ruohan Wang. Carlo Ciliberto, Pierluigi Vito Amadori, and Yiannis Demirís. Random expert distillation: Imitation learning via expert policy support estimation. Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 6536-6544, PMLR, 2019. htRphtt::// http:://proceeddngg
mlr. wtt.press/v97 vaness/////wagg99 wwang19d.... .ttml
[65] Yanwei Wang, Nadia Figueroa, Shen Li, Ankit Shah, and Julie Shah. Temporal logic imitation: Learning san-satisficing motion policies from demonstrations. arXiv preprint arXiv:2206. 04632, 2022.
[66] Christopher JCH Watkins and Peter Dayan. Q-learning. Machine learning, 8:279-292, 1992.
[67] Zikang Xiong, Joe Eappen. Daniel Lawson, Ahmed H Qureshi, and Suresh Jagannathan. Co- learning planning and control policies using differentiable formal task constraints. CoRR, 2023.
[68] Daniel Yang, Davin Tjia, Jacob Berg, Dima Damen, Pulkit Agrawal, and Abhishek Gupta. Rank2reward: Learning shaped reward functions from passive video. 2024 IEEE International Conference Robotics and Automation (ICRA), pages 1806-2813. IEEE, 2024.
[69] Konrad Zolna, Alexander Novikov, Ksenia Konyushkova, Caglar Gulcehre, Ziyu Wang, Yusuf Aytar, Misha Denil, Nando de Freitas, and Scott Reed. Offline learning from demonstrations and unlabeled experience. arXiv preprint arXiv:2011 13885, 2020.
15

---

A Impact Statement
This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of our work, none of which we feel must be specifically highlighted here.
B Related Work Discussion
Learning from demonstrations. Learning from demonstration is particularly valuable when de- signing a reward function is challenging. allows agents to learn desired behaviors by observing and mimicking expert demonstrations. Some methods utilize classification-bars
rewards, where reward function is trained by classifying goals [58, 36 [9] or by categorizing demonstration trajecto- ries [69]. However, these rewards are trained exclusively offline datasets, making them vulnerable to exploitation by a reinforcement learning agent.
33 that define subtasks for zero-shot gener- alization to Long-horizon or unseen tasks, TiLoIL focuses on mitigating the inherent exploration challenges in LTL-guided tasks, making it orthogonal to these approaches. Compared to approaches that require large-scale offline pretraining for L.TI. tasks (20. Til.ol.. learns effectively from a small number of expert trajectories. Temporal Logic Imitation 65 integrates high-level LTL planning with pre-existing low-level controllers for continuous motion execution, whereas Til.lI. jointly learns both in end-to-end manner. (32) transforms LTL specifications into differentiable loss function, while TiLoIL addresses tasks where the reward signal from LTL remains sparse where such a differentiable loss approach is infeasible.
Unlike multi-task RL approaches for LTL 60
Inverse reinforcement learning. The above issue can be solved by Inverse Reinforcement Learning. Inverse Reinforcement Learning (IRL) is a crucial tool in learning from demonstrations [1 47). It aims uncovering the underlying reward function from observed behaviors, which particularly useful in scenarios where reward structures are not explicitly defined. Recently, Adversarial Imitation methods have been introduced, functioning Generative Adversarial Networks (GANs). In these approaches, generator (the policy) is trained to maximize the confusion of a discriminator, while the discriminator, acting as a surrogate for the reward function, is trained to differentiate between the agent's trajectories and the expert demonstrations. The introduction GAIL [29] has driven significant advances scalable deep imitation learning 48). Beyond adversarial approaches, several imitation learning algorithms aim to match the state action distributions of the expert and the agent through non- adversarial techniques, such as non- con-paraettric models (38), random network distillation [64]. support estimation Wasserstein distance minimization [5]. and moment matching [59]
Learning (AIL) 29
39
24
23
manner akin to
methods [23] 24 39
34
21
Rank reward learning The above issue could be solved by decomposing the tasks into easier sub-tasks. Hierarchical Reinforcement Learning (HRL) [2 46 42 methods decompose policies into sub- sub-policies, each designed to address specific sub-tasks. Some approaches learn rewards with underlying substructures. DrS [45 decompose tasks by stage indicators, rank2reward (68) by learning videos; some methods
6 63 55 combined Buchi Automaton with the problem of labeling subtasks.
C Linear Temproal Logic
Syntax of LTL The syntax of Linear Temporal Logic (LTL) is defined over a of atomic propo- sitions AP. A state labeling function F S - Σ maps each state E S to subset of atomic propositions Σ 2AP, where Σ is the alphabet formed by the powerset of AP. An LTL formula o is constructed using the following grammar:
true false ppl - (* v) (sp (b) X
Fup Gp (<U*))
where p E AP, and oo and a are LTL formulas. The logical connectives true, false, (negation), (conjunction), and (disjunction) are standard. The temporal operators are: for "next", ", F for "eventually". G for "globally", and U for "until".
Semantics of LTL The semanties of LTI. is defined over infinite sequences of states 7 8o, $1, $,...., where each state s; S is associated with set of atomic propositions F(s.) C AP.
16

---

We write T, += yp to indicate that y holds at position i of the sequence The semantics are given inductively as follows:
i F true
(always holds)
7, à H false
(never holds)
7 F
D F(s)
forp E AP
7 F up
T, 1 p
7, F (p v)
=
r, and r, F v
7 F (0 (V))
7 p or T,
7, F Xp
= Ti++FiP
7 F FOP
=
7 F G
=
Vjži,7,
FG
7 F (DUN)
i d and Vk E [k. s).
English, the semantics of Linear Temporal Logic (LTL) are defined over infinite sequences states So, $1, $2...., where each state s, represents smapshot of the system. A state labeling function F: S + Σ assigns a set of atomic propositions (AP) to each state, indicating which propositions are true. The satisfaction of an LTL formula is evaluated along these sequences. For example, p holds at a state s; if p E F(;;). while Xp requires to hold in the next state 81+1. Temporal operators like Fp ("eventually p') and Gp ("globally p²) extend this reasoning over future states. Similarly, Uu ("vp until v0") requires ip to hold continuously until v becomes true at some future state.
For instance, the formula Fy expresses that the system must eventually reach state where y holds, which could represent a robot reaching target area. The formula G- specifies that b, such as hazardous condition, must always be avoided. More complex behaviors can also be modeled, such as G(Fr), which ensures the system repeatedly visits states where r is true, or G(yUg), where must hold until becomes true. These examples demonstrate how LTL can express diverse temporal properties for dynamic systems.
D Proofs of Theorem 3.1 and 3.2
Theorem 3.1 Let and T2 be two policies with corresponding occupancy measures Px, and Pry For any Linear Temporal Logic (LTT.) formula yo, the difference in the probabilities of satisfying i under these policies is bounded by twice the total variation distance between their occupancy measures:
[P(m F [] P F rl1 <
where the total variation (TV) distance between the distributions Px, and Pr. is given by
1 Div(pa)s Pm2) [1mm (T) pr2(T))
(10)
Proof.
The probability of satisfying under policy म can be expressed as an expectation:
Pim - sp] Er-pe, [1(T [ f 1(7 F p))m. (r)dT.
(11)
Similarly, for policy n2!
PlTt - vp] Erroo [1(7 - 6) = J. 1(7 + p)pp)))))))))))))
(12)
Thus, the absolute difference between these probabilities is:
P| + xl] P[Tz F wl] = 1// 1(T |
Pmo (T))
(13)
Applying the triangle inequality:
P(m -= :l] - P(1z - x]1 & (p (7) (T2((T) dr.
(14)
17

---

By the definition of total variation distance,
J 110m(()) - Paz (T)( =2Drv
(Pop Paz)
(15)
Thus, we obtain the desired bound:
[P(m F - P(T2 dl1 S 2Par P
(16)
This completes the proof.
Theorem 3.2 Let Qo be the learned soft Q-function trained using modified target value Quarger 1-7 in accepting states (s, b) where b B and soft Bellman backups elsewhere. Assume T s, 6) x exp (=,,((,)),, b)). Suppose that the reward function R[(s, b)) tanh(fa bounded by R((s,8) bj) E Ruuin Reuax) Let Q" be the optimal Q-function under standard soft Bellman backups (without the modified target). Then, for any state-action pair ((s, b), a),
Qo((s,b),0) (),,))),)) Q" ((8, b), S
k(x.b) {
6max
where k(s,b, b) is the number of steps it takes from (s, under T to reach some accepting state (' with 6' B*, and 6max == - Rmis t is the worst-case overestimation error at any 1- accepting states. Hmnn denotes the minimum entropy of Td.
I-
Proof. We prove the result by backward induction along the trajectory, using the soft Bellman equation and the definition of 8max-
Base case: At the final step k = k(s, b), the overestimation is at most:
(Rumin + a'Hmin )
6ma 1-7
1 1-7
Inductive step: Suppose at step i we have:
s Q" (($
b.+1). (($441, + h- ( Smax.
Then for step
Qo((si,be,, a:)
= -R((s,, b:)) + > E 1,11
E Ba bim))) [Qo (4111,11,,41,... a')l]
< R(ss, b:)) + y E. 1812
Bal (elnnn((((esnn.ne [Q" ((si+1, i bi+1) 1), a') + x 8-(+t)) 8 maxx]
R(,,, bi)) + E Bs bits
E Balnn (1enn))) [Q" (($141,bb11, b,1)) + k- 1i+ smax]
Q' ((s, bz), a.) + k- 8max
where x² is the optimal policy under Q"
Thus, the overesitmation error at (s, b) can propagate at most k(s,)) 8maxi
De((s,b), s ((s((())) + A(s.6) 8max-
Even though our method clips the Q-value at accepting states to a large constant (e.g., r-3), the theoretical bound shows:
Qo((s,b), (()(((()))))))))))))))(()))))( S Ab(x.)) 6max
18

---

GridAvold Easy
GridAvoid Medium
GridAvold Hard
10
Returns
Returmo
50k
100k 150k 200k
50k
100k 150k 200k Stops
50k 100k 150k 200k
Stops
Steps
GridSequential
Sequenttt Medium
GridSequential Hard
60
20
40-
neturns
20
40
M 4
V
noturns
20
50k 100k 150k
200k
50k
100k
150k
200k
100k 150k 200k
Steps
Stops
Steps
GridCircutar
GridCircular Medium
GridCircutar Hard
15
10
Returns
50k
100k Steps
150k 200k
0
50k 100k
150k Steps
200k
5ok 100k 150k 200k Steps
LCER
DRL2
Figure 5: Discrete environment evaluation. The three rows represent reach avoida,, sequential, and circular tasks, as shown the right.
E Tabular Results
The evaluation environment is deterministic 2D gridworld where the agent move unit in any of the four cardinal directions at each timestep or stay still.
Fig. 5 presents the performance of various algorithms across different GridWorld tasks under Tabular Q-Learning The three rows correspond to distinct task categories: reach-avoidance (top row),
sequential (middle row), and circular (bottom row), with increasing levels of difficulty (Easy, Medium, Hard) from left to right. The x-axis denotes the number of environment steps (up to 200k), while y-axis represents the cumulative returns achieved.
The first row of Figure 5 shows the results in three Grid Avoid environments with LTL specification == F(a) A G-b, with different grid sizes. The agent must navigate around a large area encompassing everything except narrow corridor. The goal area located at the end of this corridor, and the task becomes more challenging as the corridor's 's length increases. Here, the discriminators of our method will assign bad reward whenever the agent exits the corridor, causing the LDBA transition to sink state. The discriminators direct the trajectory to align with the behavior observed in the demonstrations. Therefore, has enhanced learning efficiency. Our approach shows a consistent and significant improvement in returns, especially in the hard setting.
The second and third row of Figure 5 shows the results in Sequential environments with LTL specification o = F(a A (F A XF(c)) and circular environments with LTL specification = GF XF(b G- Here, a. b, and с are different zones. The agent needs to reach each zone in order. The hardness increases with the number of zones, For the sequential task, the number of zones increases progressively, with 4, and zones for the easy, medium, and hard levels, respectively. For the circular task, each mode has 2, 3, and 4 zones. In the first scenario, the agent must visit a specific sequence of zones in a predetermined order. Our method quickly achieves optimal returns, outperforming other methods. In the second scenario, the agent must repeat this sequence indefinitely while avoiding the center of the room. this case, our method not only converges faster but also achieves significantly higher returns compared to other baselines, particularly in the medium and hard settings. For the GridCircular Medium, each trajectory has 72 steps; the GridCircular Hard 1 144 steps in each trajectory.
19

---

Table 1: Effect of the reward- shaping coefficient on TiLolL performance, measured by eventual discounted returns over 10 seeds.
Env
3=0.49
8=1/3
B=1/4
LCER
DRL2
GAIL
CYCLER
GridCircular Hard
3::0
2.411.2
340
FlatWorld Stabilization
47:0
47:10
4740
47=0
46.8+0.5
9.64199
47:00
FlatWorld Cycle
1.511.5
2.311.88
1.5
1.610.66
01:
010
Doggo Avoid
268478
296:174
246=110
4.24:2.55
79,9167.1
164. 164.6-:22
Doggo Navigate
342+:38
246+61
192+81
0+0
45.9+64.7
0+0
0+0
Fetch Avoid
35+1199
36:2.88
3741.5
13.7:
35.7:15.5
34,9:
12.1
Fetch Align
30.146.4
21+15.9
20+1.8
1.8+33
0+0
0=:0
0=:0
Carlo
2.611.1
3.211.8
2.3-0.8
010
0.310.5
010
0.0
CheetahFlip
7.25+1.3
3,542.1
3.3
010
2.545
2.421.6
040
Table Comparison between TiLolL. with multiple discriminators and a shared global discriminator, measured by eventual discounted returns (mean + standard deviation) over seeds.
Eny
TilolL. (multiple discriminators)
TilolL. (shared discriminator)
Doggo Avoid
296:
360+:20
Doggo Navigate
246+61
286:1991
Fetch Avoid
3642.88
37+0.7
Fetch Align
15.
26:1:2
Carlo
3.2
3.9
CheetahFlip
3.5+2.1
3.5
FlatWorld Cycle
2.3
2.810.1
Additional Ablation Studies
F.1 B Sensitivity
In the reward formulation Eq. 3 controls how much the shaped rewards from multi-stage discrimi- nators weigh. Table shows how different values of 3 (0.49. 1 1/4) affect performance across environments, measured by eventual discounted returns over 10 seeds.
All the ablations outperform the baselines. For easy tasks like GridCireular Hard and FlatWorld Stabilization, this hyperparameter doesn't 't have significant impact. Some challenging tasks such Fetch Align and CheetahFlip perform better with larger meaning the shaped reward from the discriminator guides the learning more effectively.
F.2 Scalability: Shared vs. Multiple Discriminators
More complex LTL specifications can increase the number of discriminators, making training more computationally intensive and potentially unstable. We have conducted additional experiments to ad- dress this scalability concern, In our reward formulation in Eq. 8 SIdx (b) serves as an approximation of the stage index of the product MDP state (s. b), is hyperparameter, and fo(s) is discriminator associated with LDBA state b. To mitigate the scalability issue of training a separate discriminator per LDBA state, experiment with single global discriminator f(b, s), which is conditioned on the current LDBA state b, and reformulate the reward as
R((s, b)) SIdx (b) + 3 ttan([((b
N(b
In implementing fbb s). concatenate one-hot encoding 2 K of the LDBA state (where K the number of LDBA states) with the state vector & as input to the discriminator network.
As in the original implementation, we train f(b s) to predict whether an MDP state E S originates from a positive trajectory whose maximal stage exceeds the LDBA state b, as opposed to a negative trajectory that fails to progress beyond b or gets trapped in sink state. As shown in Table 2 the shared global discriminator achieves comparable or better performance than the per-state variant, demonstrating improved scalability without loss of effectiveness.
20

---

We hypothesize that the improvement arises from more efficient data sharing across LDBA states, which stabilizes training and mitigates overfitting to individual states with limited positive samples. This result suggests that structured conditioning of shared discriminator is promising future direction to improve scalability without compromising performance (for example, one could future explore introducing FiLM layers that modulate hidden activations in the shared discriminator based on the LDBA state).
F.3 Robustness under Suboptimal Demonstrations
To examine TiLoIL's ''s robustness under suboptimal demonstrations, we consider cases where demon- strations fail to reach LDBA accepting states. In such cases, the underlying RL component must discover these transitions through exploration. As described in Line 4 of Algorithm | we assign demonstration trajectories to the stage buffers corresponding to LDBA accepting states, even if they fail fully complete the task. Demonstrations that fall short of fully satisfying the LTL for- mula-such as those that progress through some sub-goals or approach accepting states without fully reaching them-can still provide valuable learning signals during training.
We validate this in Carlo environment. This environment involves a self-driving agent trained to follow circular track counterclockwise while visiting two blue regions repeatedly and avoiding crashes. We trained TiLoIL using only failed or incomplete demonstrations, including those that either entered unsafe regions or failed complete full loop by missing one blue region. While there is a performance drop expected- -TiLoLL remains effective, significantly outperforming the RL for LTL baselines and GAIL, as reported in the main paper.
Table 3: Performance comparison between TiLolL trained with original demonstrations and with only unsafe or incomplete demonstrations.
Environment TiLolL (Original Demos)
TiLoIL (Unsafe or Incomplete Demos Only)
Carlo
3.2
2.1
G Demonstrations
G.1
Demonstration Assumption
Our primary contribution is to show that finite-length, non-optimal suboptimal policies that reach LDBA accepting states only once or twice-cal be leveraged to learn policies that satisfy LTL objectives over infinite horizons. The key lies in generalizing from such limited behaviors policies that reach accepting states infinitely often. If demonstrations fail to cover certain transitions to LDBA accepting states, it becomes the responsibility of the underlying RL algorithm (SAC TiLoIL) to discover trajectories that reach those states through its own exploration. TiLoIL is able to leverage the agent's ' own behaviors cetviirr--tosee that have progressed beyond certain LDBA states-as as positive trajectories to train discriminators that guide learning for those trajectories that fail to meet such LDBA states as in A Algorithm [ thereby reducing reliance on large demonstration datasets. However, if the RL algorithm fails to explore L.BA accepting states, TiLolI is likely to fail. A promising future direction is to combine TiLoIL's 's exploitation strategy- which leverages demonstrations with advanced exploration techniques from recent RL-for-LTL algorithms, aiming to overcome the reliance demonstrations bottleneck.
by
G.2 Demonstration Sizes
Demonstrations can be difficult to obtain, especially in complex environments, making it important work with a limited number of demonstrations, In Fig. the results are based on demonstrations. We aim to investigate whether more demonstration data would improve learning. As shown in Fig. 6, the demonstration size does not significantly limit our learning efficiency, though it has some impact challenging tasks like Fetch Align and Cheetah Flip. This is mainly because TiLolL trains multi-stage discriminators from stage-speciff buffers. TilolL. able to leverage the agent's 's own behaviors-ther that have progressed beyond certain LDBA states positive trajectories train
21

---

Dugge
Degge Nangal
FotL Akps
Fat Awai
Carb
Cheelin
133
200c
Figure 6: This figure illustrates our method with different numbers of demonstrations. The lines represent 10, and full-size demonstrations. The full demonstration (number of episodes) varies across environments due to differences in episode length. Specifically, the full demonstration numbers are as follows: Doggo Avoid is 25, Doggo Navigate is 15, Fetch Align and Fetch Avoid are 100, Carlo is 111, and Cheetah Flip is 50.
discriminators that guide learning for those trajectories that fail meet such LDBA states, thereby reducing reliance on large demonstration datasets. We conclude that our method does not require large numbers of demonstrations.
We also compared our method with GAIL, across varying numbers of demonstrations. As shown in Fig. 7 while GAIL improves with more demonstrations, TiL.lL consistently outperforms it by significant margin.
Dogge Avold
Dugge Nodigate
Feech
Felih Aliga
300
200
300
Look
2006
3000
100k
3304
2036
200k
4000
Look
2004
2006
100c
204k
750k
100k:
2008
2004
4000
Figure 7: Returns under eventual discounting comparing TiLoIL with GAIL under different sizes of demonstrations. The full demonstration (number episodes) varies across environments due to differences in episode length.
G.3 Demonstration Lengths
Table 4 illustrates the impact of demonstration length on performance. Performances are measured by eventual discounted returns over 10 seeds. The first column uses demonstrations of 100 steps, while the second and third columns extend this to 200 and 400 steps, respectively. In the Carlo environment, longer demonstrations improve learning outcomes. For CheetahFlip, extending the demonstration length does not help because the demonstrations are suboptimal, and longer trajectories do provide more visits accepting states.
Table 4: Effect of demonstration length on TiLolL performance, measured by eventual discounted returns over seeds.
Env
demo length=100
200
400
Carlo
3.2+1.8 3.5#2.1
1.6::0.7
2.15+10.
CheetahFlip
3.3+2.3
2.3
H Implementation Details
H.1 Environments and Tasks
The experiments presented in this paper conducted within simulated environments.
22

---

H.1.1 Tabular Environments
The environments explored in the Fig. D are variations of the standard gridworld, represented as a 2D grid with the agent occupying single cell. The action space is discrete, comprising five actions: four corresponding to movements in the cardinal directions and one no-op action. The observation space is 2-dimensional, consisting of the agent's 's x and y coordinates.
Although the dynamics are consistent across tasks, the labeling functions mapping MDP states to atomic propositions, as well as task-specific details, differ from each other.
Reach-avoidance Reach-avoidance is assessed in gridworld without obstacles as shown in the first row of 5 The agent starts at one end of a narrow corridor with a unit-width layout. While the opposite end of the corridor is unbounded, the atomic proposition a evaluates to true in all cells of the corridor located beyond a certain fixed distance from the starting position. Conversely, the AP evaluates to true in all areas outside the corridor. The LTL formula is F(a) A G-z. The task's s difficulty increases with the distance to the target zone, set to 7, 9, and 11 for the easy, medium, and hard variants, respectively. Each episode lasts for the minimum number of steps required to reach the target zone, plus an additional 10 steps.
Sequential Sequential task is shown in the second row of Fig. 5 it also takes place in a gridworld without obstacles, consisting of contiguous 7x7 squares aligned horizontally. The agent starts the center of the leftmost square, and in each subsequent square to the right, different atomic proposition (AP) evaluates to true alphabetical order. Specifically, a evaluates to true in the first square to the right of the starting position, b in the second, and so The task's difficulty is scaled by using progressively longer temporal logic formulas: F(a A XF(6 A XFc)). F(a A XF XF(c A XFd))). and F(a A (F XF(cA XF(d XFe)))) for the easy, medium, and hard variants, respectively. Each episode has a fixed length of 72 steps.
Circular Circular tasks are shown in the third row of Fig. They consist of 5 contiguous 7 7 squares arranged in a cross formation. The central zone with stacle, labeled with the atomic proposition and the agent is unable to access it. The re- maining 4 zones are labeled b, c, and d in a counterclockwise order, with the agent ini- tialized near the first zone. Task difficulty is scaled by increasing the number of zones in- volved in the loop, with the following formulas used: Ga (F(()) GF(aAXF(bb) A G-2 for the easy variant, GF XF(b A XFc)) A G-zfor medium, and GF A (b A XF(c A XFd))) A G-z for hard. Each episode has 72 steps for easy and medium mode; hard mode has 144 steps.
FlatWorld Disjunction
cells acts as an ob-
Returns
20
0
100k
200k
300k
400k
Steps
TiLoiL
LCER
DRL2
GALL
Figure 8: Disjunctive LTL objective in Forld The task requires reaching (yellow - green) or (red + green) while avoiding blue. The first row shows that returns under eventual discounting com- paring TiLoIL with the baselines over 10 random seeds. The second row illustrates the trajectories of TiLoIL and LCER. The first image shows TiLoIL starting near the red zone, while the second shows TiLoIL starting near the green zone. The third im- age depicts the LCER trajectory from a red-zone start. Although LCER achieves similar returns to TiLoIL, it fails to adapt its path based on the initial state, always following yellow + green. In con- trast, TiLolL dynamically selects the optimal path (e.g., red - green when starting closer red).
H.1.2 Continuous Environments
Carlo The Carlo environment (illustrated in the second row, last column of Fig. 3 is a simplified self-driving simulator based on a bicycle model for its dynamics. The agent observes its position, velocity, and heading (in radians), resulting in a S-dimensional observation space. The agent controls its heading and throttle, with an action space of [-1, 1J2 For this domain, we use a circular track where the agent starts at the cen- ter of the road at an angle of (1+20) i i= and drives counterclockwise around the circle without crashing. The task is defined by GF(wpo XF )) A G G-erash, to visit the blue regions wpo, up1 repeatedly while avoiding the gray region crash. The episode length is 500.
23

---

Doggo Doggo is 12-DoF quadruped adapted from the most challenging tasks in SafetyGym [52]. designed navigate a flat plane. The observation space is 66-dimensional, the action space is 12 12-dimensional, and each episode lasts 500 steps. Similar to other reach-avoidance tasks, Doggo Avoid requires the agent to navigate directly to a distant goal along straight path, avoiding any detours as shown in the first column, the second row of Fig. 3 In contrast, Doggo Navigate involves navigating through a sequence of two circular zones as shown in the first column, the third row of Fig. 3 These tasks are defined by the following specifications: Fa A G-z for Doggo Avoid and F(a A XF())) for Doggo Navigate. Both tasks have a fixed episode length of 500 steps.
FlatWorld The Flatworld environment (illustrated in the first row of Fig. 3 is two-dimensional
continuous world. The agent, represented by a green dot, starts at position (-1 -I, -1). The dynamics of the environment are defined by: x = x x+ TO where E I2² and a E 0,1 Here we define three tasks Fla FlatWorld Stabilization, WoalWorld Cycle and FlatWorld Disjunction. Flar Stabilization also inspired by the reach-avoidance task in tabular settings, requires the agent to reach the yellow zone at left and avoid the blue zones in the middle. FlatWorld Cycle requires the agent to visit red, yellow, and green zones in order repeatedly while avoid the blue zone. FlatWorld Disjunction requires the agent to visit yellow then green, or red then green while avoid the blue zone. The three tasks are defined by the following specifications: FG()) A G-b for Flat WorlWorld Stabilization, GF(r A XF(g A XFy)) A G-b for FlarWorld Cycle, and (F(y A XFg) V F(r A XFg)) A G-b for Flar FlarWorld Dixjunction. Fig. shows the result for FlatWorld Disjunction. The episode length is 50 for all tasks.
Fetch Fetch environments are based on the widely used Fetch robotic benchmark 17]. We eval- uate two tasks where the agent controls the end effector position of 7-DoF robotic arm using d-imennsional actions over 50-step episodes. Fetch Avoid, inspired by the reach-avoidance task in tabular settings, requires the arm to fully extend while avoiding lateral movements (i.e., reaching the green zone and avoiding red zones as shown in the second row of Fig. B In this task, the observation space is 10-dimensional. Fetch Align, on the other hand, involves interacting with three cubes on one side of the table and aligning them horizontally at the center. For this task, the observation space includes information about the cubes and is 45-dimensional. The two tasks are defined by the following specifications: Fa A G-2 (reach the end of the table while avoiding lateral movements) for Fetch Avoid, and F(a A XF A XFc)) (position the first, second, and third block sequentially) for Fetch Align.
FetchPlace environments are based on the widely used Fetch robotic benchmark [17. We evaluate two tasks where the agent controls the end effector position of 7-DoF robotic arm using 4-dimensional actions over 500-step episodes. In FetchPlace Button, pressing the button causes goal region to appear. The manipulator must (1) press the button, (2) pick up a block, and move it to the goal region, and then (3) repeat this sequence with the goal region appearing in new location each time. In this task, the observation space includes the button information and goal information, and is 31 3--dimensional. FetchPlace Tray contains movable block and two potential destination regions: tray and a goal region. A tray may or may not appear in the scene in each episode. If the tray appears, the agent must place the block into the tray. If the tray is absent, the block should be placed into the goal region. For this task, the observation space includes information about the goal and is 28- dimensional. The two tasks are defined by the following specifications: Fgrasp/ EgraspA/F(GGon ReachedA XF Button Reached (first grasp the block, reach the goal, and then reach the button) for FetchPlace Button, and (-TrayPress Present F(grasp A XF InIT (nTTray)) A (TrayPresent F(grasp A XF I InGoal)) (if tray not present, grasp the block and go into the tray; if tray present, grasp the block and go to the goal) for FetchPlace Tray.
FetchPlace
HalfCheetah HalfCheetah [6], a standard environment in deep reinforcement learning, involves controlling 6-DoF robot in vertical 2D plane. In Cheetah Flip, the agent follows the formula GF A XFd), where each variable corresponds to a specific range of angles for the robot's 's main body. These angles represent the Cheetah standing on its front legs and standing on its back legs, respectively. The task requires the agent to perform a sequence of frontflips to satisfy the formula. The episode length is 1000.
This environment with continuous observation and action space is adapted from the 16 rooms environment (35) In this walled environment with 16 rooms, each room has the same size 8x8 divided by walls and corridors with thickness. We deployed the FlatWorld agent this environment. The task & requires the agent to traverse circular path indefinitely via one of two
SixteenRooms
24

---

and Table Hyperparameters for Q-learning and SoftActorCritic.
HYPERPARAMETER
VALUE
Y a
0.99
0.2
BUFFER SIZE
1 10
BATCH SIZE
64
LEANING STARTS
2000
1-101
Q LEARNING RATE
3-10-*
ACTOR LEARNING RATE
3 3.10-1
CRITIC LEARNING RATE
3-10
DISCRIMINATOR LEARNING RATE
3 1.100T
DISCRIMINATOR UPDATE FREQUENCY
1 STEP
TARGET NETWORK UPDATE FREQUENCY
1 STEP
possible routes. The rooms are arranged in a 4 x 4 grid, and are indexed as room; with i denoting the row index (from left to right) and j the column index (from bottom to top).
The LTL formula:
V
GF A XF(roomi, A XF(room3,4 A (F(romms,)))) V
GF GF(rooms, XF XF (rooms,3 XF (rooms,1 A XF (room4,, A XF((roo,,))))) A AG(-Wall) spec- ifies that the agent must repeatedly visit either one of two possible loops. The large loop (1, 4) (3,
goes through rooms (1,2)
(3,2). The small loop goes through rooms (3,3) - (3, 4) > (4.4) - (4,3). The agent must avoid collisions with wall segments between rooms. The agent departs from the center of the bottom-left
to reach the desired goal positions. The initial state of the agent is created with random noise. The optimal policy needs to identify and traverse the smaller loop repeatedly while avoiding all walls.
H.2 Methods and Algorithms
We utilize SAC 225 and tabular Q learning 666 as the backbone RL algorithm. The architectures of the SAC networks are shown below:
Actor 4 MLP, hidden units(256,256,256)
Critic Networks:3-layer MLP, hidden units(256.256)
Discriminator Networks(Roward):2-aaya MLP.idden units(32)
The corresponding hyperparameters are provided in Table 5 For challenging tasks, we allow more
steps for initial random exploration. For Cheetah Flip, learning starts is 2 10a.
H.3 Metrics
Performance is evaluated using cumulative return under eventual discounting [63] an RL-friendly proxy objective from prior work [27 63 that optimizes lower bound the probability of LTL formula satisfaction.
T.. E arg max Eror REll
Σ r.R (b:)
V?),
1==0
where
R (b:) 1p.EB-
=o=1, 1, P,
Il x (bb)) t=
(17)
(7, b E B
y 7x (6,) (6))= -1, 11 otherwise.
(18)
performance curves represent the mean estimated across 10 seeds, with shaded areas indicating variance.
25

---

H.4
Tools
Our codebase primarily utilizes NumPy 226 for numerical computations and Torch 49 for its autograd capabilities. Additionally, we partially automate the synthesis of LDBAs from LTL formulas using Rabinizer
44).
H.S
Computational Costs
All methods exhibit similar runtimes within their respective settings (tabular or continuous). Each experimental run was conducted using NVIDIA Quadro RTX 6000 GPU. On average, single run took approximately 30 minutes in the tabular setting and 3 hours in the continuous setting.
26

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: Yes, the abstract and introduction clearly state the main claims of the paper, including the background on LTL with RL, motivations and contributions. The conclusions made are based on a wide range of benchmarks and results.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
It is fine to include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: We included clear discussion on the limitations. TiLoIL requires suboptimal demonstrations for imitation learning. So the future work will focus on using suboptimal demonstrations guide agent exploration toward LTL satisfaction.
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or speech-to-text system might not be used reliably provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't acknowledged
the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
27

---

Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
Justification: We included clear theorems and proof at Theorem. 3.1 Appendix [ They are cross linked in the main paper.
Theorem, 3.2 and
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated referenced in the statement of any theorems.
The proofs can either appear the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: We provided the necessary details to reproduce the main experimental results in Appendix [..)] This includes that use SAC and Q learning as a backbone RL algorithm. It shows the structure of the sac network, the structure of the discriminators, and the corresponding hyperparameters.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, No answer this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often good way to accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm.
(b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
28

---

(d)
We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: We include our code and demonstrations as zip file in the supplementary material.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips.co
guuides/CodeSuumisss
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended the paper) is recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: We include the experimental details in Sec. and Appendix Appendix H.2 shows the hyperparameters.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [Yes]
Justification: Our experimental results shown in Fig, Fig.Bamn are over 10 random seeds. The solid line represents the mean, and the shaded area indicates the standard deviation.
Guidelines:
29

---

The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by enror bars, confi-
dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).
If error bars are reported in tables or plots. The authors should explain the text how they were calculated and reference the corresponding figures tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We include the compute resources Appendix H.3
Guidelines:
The answer NA means that the paper does include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported the paper (e.g., preliminary or failed experiments that didn't 't make it into the paper).
9. Code of ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics https::/neurrrr wwtpppsscccpppppcppcceccc wtt.echheeiciiiinieeieenn
Answer: [Yes]
Justification:
Our work fully adheres to the NeurlPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification:
We discuss broader impacts in Appendix A
30

---

Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No. they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considcrations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning conrectly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper deseribe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: Our work does not release any models, datasets, tools that pose high risk misuse or dual-use concerns.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model. for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: We mentioned the assets used in Sec. 4 and cited to their original publica- tions.
Guidelines:
The answer NA means that the paper does not existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
31

---

The name of the license (e.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (c.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the datasets.paperssii paperswi thcode. com/datasets package should be provided. For popular datasets,
has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: Our work included new assets and are submitted in supplementary material. Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember anonymize your assets (if applicable). You either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: Our work does not involve any crowdsourcing activities or research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for rescarch with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based the requirements of your country institution) were obtained?
Answer: [NA]
Justification: Our work does not involve human subjects. So there are no participant risks or Institutional Review Board (IRB) approval.
Guidelines:
32

---

The answer NA means that the paper does not involve crowdsoureing nor research with
human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent)
may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Question:
Does the paper describe the usage of LLMs if it is important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Answer: [NA]
Justification: We only use LLM for writing, editing. or formatting purposes. Our work does not involve the use of LLM in any important or original way.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer to LLM policy http::///earrpssccc/ooorrrrrer/s for what should or should not be described.
33


Reviews:
[{"review_id": "WneHtDXJGM", "reviewer": "Reviewer_r1Rp", "summary": "The paper deals with the problem of imitation learning where the learning agent has access to both a set of positive expert demonstrations, and in addition a task specification in LTL which the expert demonstrations satisfy. Since LTL is evaluated over infinite trajectories, RL approaches design proxy rewards based on accepting states (an LTL formula can be translated to a LDBA state machine, where an infinite trajectory satisfies the LTL if it visits an accepting state infinitely often). The inherent difficulty in this approach is that the rewards are sparse, making exploration difficult. Expert demonstrations can theoretically help, but are by nature finite.\nTo address these difficulties the authors splits trajectories into \"segments\", sub-trajectories between accepting states (these are effectively treated as independent demonstrations), and within those segments they leverage the structure of the LTL formula (as evident in the LDBA) to further recognize \"stages\" of satisfaction of the formula, allowing them to densify the rewards. Their approach falls within the framework of GAIL, alternately training a discriminator to distinguish between states from (suitably defined) positive and negative sub-trajectories, and using the learned discriminator(s) to define dense rewards for policy improvement. They optimize for both satisfaction of the formula (reaching an accepting state) and IL goal of making the policy trajectories indistinguishable from the expert demonstrations. They evaluate their learned policies on a number of standard tasks in high-dimensional spaces (some of them circular, to specifically evaluate the merits of their segmentation method), and test two aspects of their work - comparing it to SOTA policy optimization methods that make use of LTL objectives (but not expert demonstrations) to see if it improves exploration, and to IL methods that do not explicitly leverage LTL specifications.", "questions": "- I understand that non-optimal demonstrations are out of scope, but given that in the real world they exist, what is the effect of adding such demonstrations in practice? Will the results degrade gracefully, or can one sub-optimal demonstration, no matter how close to satisfaction, collapse the entire optimization?\n\n- If the epsilon-transitions have any meaning in your framework, I'd love to see them incorporated into an example (The flatworld perhaps)\n\n- Can this method be adapted to a setting where the observations of the environment are noisy/partially observed? What if I'm only 90% certain I hit 'blue'? I realize it is out of scope, but addressing this in the discussion/limitations would add broader context.", "limitations": "The authors address the main limitation - that the method assumes optimal demonstrations.", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\n- The paper is novel in that it combines the LDBA-MDP product formulation with expert demonstrations, combining global task specification with more local guidance within the segments from the demonstrations.\n\n- The evaluation is presented clearly, the ablation results elucidate the importance of their segmentation technique in cyclical tasks. The results seem good compared to existing SOTA methods.\n\n- The paper is well-written, and related work and context is thoroughly explored. \n\nWeaknesses:\n\n- The contributions of the paper are not clearly outlined. As a non-expert in the field, it took me a while to (hopefully) disentangle the issues of infinite horizon and reward sparsity.\n\n- While epsilon-transitions in the LDBA are formally defined, I struggled to understand from the paper alone what their meaning is in the product MDP. The running example makes no use of them, their relation to deterministic vs non-deterministic states is not mentioned and overall I'm not sure why they were introduced (other than for completeness). Its not a major issue, but for a non-expert it was a sticking point.", "was_revised": true, "final_justification": "I stay with the 5 score. \n\nThe authors thoroughly answered my questions, and this along with their discussions with other reviewers helped me get a better picture regarding the effect of different sub-optimal demonstrations. The other issues were related to clarity of their contributions, and I accept that they will make the appropriate changes.", "rebuttal": "We appreciate your insightful feedback and constructive comments!\n\n**Q1. What is the effect of adding non-optimal demonstrations in practice? Will the results degrade gracefully, or can one sub-optimal demonstration, no matter how close to satisfaction, collapse the entire optimization?**\n\nWe clarify that the assumption of expert demonstrations applies only to our theoretical analysis (e.g., Theorem 3.1). In practice (line 341), our demonstrations are generated by chaining locally trained controllers for each stage of the LTL task. The policies learned in this way are not optimal: when executed repeatedly, they fail to produce trajectories that visit LDBA-accepting states infinitely often. For example, in CheetahFlip, the chained controllers—and thus the collected demonstrations—achieve only one or two rotations, since additional flips require maintaining momentum after reaching an accepting state, which the learned local policies cannot sustain. Similarly, in Carlo, demonstrations rarely reach accepting states more than twice. Despite this suboptimality, TiLoIL learns policies that surpass the demonstrations, empirically achieving higher visitation rates of accepting states in both CheetahFlip and Carlo. A key reason for this is that TiLoIL does not attempt to imitate the demonstrator's actions—in fact, we assume that demonstrations consist only of state trajectories (Line 138). This allows TiLoIL to prioritize task satisfaction over action mimicry, leveraging the logical structure of the LTL objective to generalize beyond the demonstrations.\n\n**Q2. If the epsilon-transitions have any meaning in your framework, I'd love to see them incorporated into an example.**\n\nWe will revise the paper to include the FlatWorld Stabilization environment as an illustrative example to clarify the role of ε-transitions. In this environment, the LTL task is FG $y$, which requires the agent to eventually reach and then remain in the yellow region. The corresponding LDBA consists of three states. The transition from automaton state 0 to state 1 is an ε-transition, which occurs independently of the MDP state—it represents the logical satisfaction of the \"finally\" operator in the LTL formula rather than any concrete observation. Once in state 1, the automaton remains there as long as the agent stays in MDP states satisfying $y$ (i.e., remaining in the yellow region). If $y$ becomes false, the automaton transitions to sink state 2. The learned policy must learn to initiate the ε-transition (Def. 2.3) at the right time and then enter the yellow region, taking actions that ensure the agent stays there indefinitely and avoiding the sink state. This illustrates how ε-transitions enable abstract progression in the automaton that is not tied to any specific environment transition, yet must be orchestrated carefully by the policy in concert with the environment dynamics.\n\n**Q3. Can this method be adapted to a setting where the observations of the environment are noisy/partially observed? What if I'm only 90% certain I hit 'blue'?**\n\nYes! Thanks for the suggestion. Our method can be extended to handle models uncertainty in atomic propositions via belief-based policy learning. In the POMDP setting (environment are noisy/partially observed), the agent has only access an observation distribution $\\omega : \\mathcal{S} \\rightarrow \\Delta \\mathcal{O}$ induced by the state space $\\mathcal{S}$ - the agent observes an observation $o_t \\sim \\omega(s_t)$ and performs an action based on $o_t$ instead of $s_t$. Denote the agent's observation-action history at time $t$ by $h_t = (o_1, a_1, \\ldots, o_{t-1}, a_{t-1}, o_t)$ and the set of all possible histories as $\\mathcal{H}$. In principle we can apply any deep RL approach suitable for POMDPs, such as a recurrent policy $a_t \\sim \\pi(a_t \\mid o_t, b_t)$ that conditions on $h_t$ and the current LDBA state $b_t$. However, we don't have access to the ground-truth labeling function $\\mathcal{L}$ and therefore cannot accurately evaluate $b_t$. As pointed out by the reviewer, we can assume we access to a model $M : \\mathcal{H} \\rightarrow \\Delta(2^{\\mathsf{AP}})$ that predicts probabilities over possible propositional evaluations $\\mathcal{L}$ (e.g. 90% certain agent hitting 'blue'). We therefore can use $M$ to predict a distribution over LDBA states $\\tilde{b}_t \\in \\Delta \\mathcal{B}$:\n* At $t=0$: we initialize the belief $\\tilde{b}_0\\$ to be certain of the initial LDBA state $b_0$.\n* For $t > 0$: we propagate belief forward through possible transitions ${P}^\\mathcal{B}$, using uncertain information about the environment from $M$:\n> The probability that the LDBA is in state $b$ at time $t$ is computed by summing over all possible prior LDBA states $b'$ and all possible atomic proposition sets $\\Sigma \\cup \\mathcal{E}$, and weighing:\n>\n> * whether $P^\\mathcal{B}(b', \\sigma) = b\\$ (i.e., whether the LDBA would transition from $b'$ to $b$ if evaluation $\\sigma$ to atomic propositions were observed),\n> * how likely it was that we were in state $b'$ at $t-1$ (i.e., $\\tilde{b}_{t-1}\\[b']$),\n> * how likely it is that $\\sigma$ is the set of atomic propositions true at time $t$ (from $M(h_t)[\\sigma]$).\n\nThe decision-making module is a policy $\\pi(a_t \\mid h_t, \\tilde{b}_t)$ that then leverages the inferred belief $\\tilde{b}_t$.\n\nAt each time step $t$, we can then compute a soft multi-stage reward from the bank of discriminators: $r_t = \\sum_{b \\in \\mathcal{B}} \\tilde{b}_t[b] \\cdot R((s_t, b))$ for training the agent, where the reward function $R$ is our original multistage reward formulation defined for a product MDP state in Equation (8), Line 302. In this way, $r_t$ smooths out errors in uncertainty in atomic proposition truth values.\n\nTo train each stage-specific discriminator $f_b$ (Line 293), we can similarly compute the belief of a trajectory that has passed LDBA states, storing the trajectories in stage buffer with soft weighting  — e.g., weight a sample by $\\tilde{b}_t[b]$ when training $f_b$.\n\nWe see the integration of our reward shaping into both multi-task frameworks and noisy environments as exciting directions for future work.\n\n**Weakness: The contributions of the paper are not clearly outlined.**\n\nWe appreciate this feedback. Our primary contribution is to show that finite-length demonstrations can be used to overcome the exploration bottleneck inherent in learning for LTL objectives over infinite horizons. We will revise the introduction to include an explicit “Contributions” section that makes our key contributions more visible to readers."}, {"review_id": "NiV6A0Out1", "reviewer": "Reviewer_ifPj", "summary": "This work presents TiLoIL, an imitation learning method for achieving objectives specified using Linear Temporal Logic (LTL). The key innovations are two forms of decomposition: first, segmenting expert trajectories to learn how to reach accepting states in a corresponding LDBA, and second, breaking down tasks into stages to facilitate learning.", "questions": "Please see the points under weaknesses for more detailed discussion. The main questions are:\n\n- Are there any implicit objectives in the demonstrations beyond the LTL specifications?\n- How should TiLoIL be categorized in relation to existing work (e.g., online vs. offline, imitation learning vs. reinforcement learning, or a hybrid)?\n- How are the product MDPs constructed, particularly in continuous domains?\n- What kinds of tasks is TiLoIL likely to succeed or struggle with, and why?\n\nI am willing to adjust my score depending on the responses to the above.", "limitations": "Yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 3, "originality": 3, "strengths_and_weaknesses": "### Strengths:\n\n- Enabling agents to follow temporally extended symbolic objectives is an important problem.\n- Clearly identifies the challenge of using finite trajectories for general LTL rather than resorting to LTLf (LTL over finite traces).  \n- The proposed methodology appears sound, and experimental results demonstrate effectiveness on selected tasks.  \n\n### Weaknesses:\n\n- **Clarity of formulation and demonstrations**: The formulation could be clearer about the nature of the expert demonstrations and how they relate to the LTL objectives. Why don't *all* expert demonstration satisfy the given LTL? The setup is presented as multi-objective, but it seems the primary goal is to find a policy that satisfies LTL constraints, unless there are additional implicit objectives encoded in the demonstrations. Clarification would help.\n\n- **Positioning within the literature**: The related work could be better situated. The second paragraph of Appendix B should be included in the main paper and expanded to clarify the similarities and differences with existing approaches. For example, from my understanding, TiLoIL requires environment interaction, whereas [20] operates in a purely offline setting. [20] also uses trajectory segmentation and does not require expert demonstrations, something noted as future work for TiLoIL. Similar comparisons should be made against the other prior work in a more systematic fashion, e.g., by categorizing the methods.\n\n- **Use of LDBAs in continuous tasks**: It is unclear how LDBAs and product MDPs are constructed and used for tasks with continuous state spaces. Was the state space discretized? Given that LDBAs are worst-case exponential in the size of the LTL formula, this may limit scalability to more complex objectives.\n\n- **Experimental setup and insights**: While TiLoIL performs well on many tasks, the task selection could be more clearly motivated. For example, Minecraft and Pacman appear in [63], while [6] includes two Cheetah variants. Clarifying why these tasks were chosen would help us understand the results. Additionally, it would be valuable to discuss the types of tasks where TiLoIL is likely to succeed or fail, to guide future research. On the Cheetah Flip task, the multi-stage approach appears to have hindered learning. The explanation offered is a good start, but a deeper analysis of failure cases would improve understanding and potential resolutions.", "was_revised": true, "final_justification": "The authors responses helped to clarify the problem setup and situate the work relative to existing methods on learning with LTL objectives/constraints. I do think the work contributes towards an important area. On the downside, the work has limited significance and technical novelty (a subjective opinion) hence not a stronger accept recommendation.", "rebuttal": "We appreciate your insightful feedback and constructive comments!\n\n**Q1. Are there any implicit objectives in the demonstrations beyond the LTL specifications?** \n\n**W1. Why don't all expert demonstration satisfy the given LTL? The setup is presented as multi-objective, but it seems the primary goal is to find a policy that satisfies LTL constraints, unless there are additional implicit objectives encoded in the demonstrations.**\n\nOur approach (TiLoIL) is developed for Imitation Learning *with Temporal Logic Constraints*. For imitation learning, one can simply optimize $\\pi^\\ast = \\arg \\max_{\\pi_\\phi \\in \\Pi} J_\\pi(\\phi) $ where $J_\\pi(\\phi)$ is the GAIL objective minimizing the Jensen-Shannon) divergence between the learning policy and expert policy (Line 159). However, in practice, user-provided demonstrations may be suboptimal due to the cost and complexity of constructing them. Learning solely from finite-length demonstrations does not guarantee deriving a policy that generalizes to infinite horizon LTL tasks. As a concrete example, in our setup, demonstrations are generated by chaining locally trained controllers for each stage of the LTL task (line 341). These policies are not globally optimal: when executed repeatedly, they often fail to produce trajectories that visit LDBA-accepting states infinitely often. In CheetahFlip, the chained controllers—and thus the resulting demonstrations—achieve only one or two rotations, since additional flips require maintaining momentum after reaching an accepting state, which the learned local policies cannot sustain. Similarly, in Carlo, demonstrations rarely reach accepting states more than twice. To address this issue, we add LTL constraints forming a multi-objective learning paradigm: $\\pi^\\ast = \\arg \\max_{\\pi_\\phi \\in \\Pi} \\left( P(\\pi_\\phi \\models \\varphi), J_\\pi(\\phi) \\right)$. The agent not only imitates demonstrations but also maximizes the probability of LTL satisfaction. Under this formalism, despite demonstration suboptimality, TiLoIL learns policies that outperform the demonstrations, empirically visiting accepting states more frequently in both CheetahFlip and Carlo. \n\nAlthough demonstrations do not encode implicit objectives, the multi-objective formulation—combining demonstrations with LTL specifications—provides a compelling advantage: it enables policies to be learned significantly faster than with pure RL, while requiring far fewer demonstrations than classical imitation learning.\n\n**Q2. How should TiLoIL be categorized in relation to existing work (e.g., online vs. offline, imitation learning vs. reinforcement learning, or a hybrid)?**\n\nTiLoIL is a hybrid online imitation learning method. It extends the adversarial imitation learning framework of GAIL to tasks specified by LTL objectives. Like GAIL, it performs online interaction with the environment while training a discriminator on expert demonstrations to provide a shaped reward signal. The demonstrations are used to guide exploration in the early stages, but the policy is improved via reinforcement learning beyond the demonstration quality. Thus, TiLoIL is neither a purely offline method nor standard behavioral cloning—it is an online, adversarial imitation learning approach specialized for structured, infinite-horizon LTL tasks. The primary contribution is to show that *finite-length* demonstrations can be used to overcome the exploration bottleneck inherent in learning LTL objectives over *infinite* horizons.\n\n**Q3. How are the product MDPs constructed, particularly in continuous domains?**\n\n**W3. Use of LDBAs in continuous tasks: Was the state space discretized? Given that LDBAs are worst-case exponential in the size of the LTL formula, this may limit scalability to more complex objectives.**\n\nAs is standard in RL for LTL tasks, we do not explicitly construct the full product MDP, which would be infeasible in continuous domains due to the infinite state space. Instead, we simulate product MDP transitions on-the-fly: at each environment step, we maintain a product state $(s, b) \\in \\mathcal{S} \\times \\mathcal{B}$, where $s$ is the current (continuous) environment state and $b$ is the current LDBA state. Upon taking an action, the environment transitions to a new state $s'$ ($s = s'$ if the action is an epsilon transition), and the automaton transitions to $b'$ according to the LDBA transition relation and the atomic propositions satisfied by $s'$ (Def. 2.3). This approach avoids constructing the full product MDP while preserving correctness, enabling us to learn policies over $\\mathcal{S} \\times \\mathcal{B}$ that satisfy the LTL objective in a *model-free* manner. Crucially, we do not discretize the state space, as such discretization is computationally prohibitive and does not scale to high-dimensional environments.\n\n**Q4. What kinds of tasks is TiLoIL likely to succeed or struggle with, and why?**\n\n**W4. Experimental setup and insights: While TiLoIL performs well on many tasks, the task selection could be more clearly motivated.**\n\nTiLoIL has been tested on all the benchmark environments used in prior work LCER [63] and DRL2 [6]. We exclude Minecraft and Pacman, as these are simple, low-dimensional discrete environments where exploration is not challenging. In fact, TiLoIL can solve these tasks even without demonstrations—random exploration is sufficient to encounter accepting states, enabling TiLoIL to learn a policy with performance comparable to the LCER baseline [63]. We do include the CheetahFlip environment from [6], while omitting the other Cheetah variant, which is structurally similar to DoggoNavigate in both dynamics and LTL structure. In the experiment section, our focus is on evaluating TiLoIL in tasks that involve nontrivial exploration challenges and diverse LTL objectives.\n\nOverall, TiLoIL performs better when demonstrations are of higher quality. As noted in our response to Q1, TiLoIL's relatively weaker performance on CheetahFlip—compared to its ablated variant, though still outperforming all baselines—is primarily due to suboptimal demonstrations. These demonstrations can only achieve one or two rotations and fail to provide sufficient supervision for maintaining the momentum needed to consistently flip while standing on the back leg. Despite this limitation, TiLoIL surpasses the demonstrations, suggesting that its performance is bottlenecked by the quality of the demonstrations rather than its learning capability. In contrast, the ablated variant TiLoIL_noStage focuses on learning to repeatedly stand on the front legs, a posture from which maintaining or regaining forward rotational momentum is easier due to the task's dynamics.\n\nTiLoIL is especially effective in tasks where reaching accepting states requires structured, multi-stage behavior, and where random exploration is insufficient. In such settings, even suboptimal demonstrations that partially reach accepting conditions can significantly help exploration. Conversely, TiLoIL may struggle in tasks where demonstrations fail to sufficiently cover the key transitions in the automaton (e.g., CheetahFlip), or when the LTL formula requires environmental events that demonstrations fail to expose. Overall, TiLoIL’s performance is influenced by both the quality of demonstrations and their coverage of the automaton's structure.\n\n**W2. Positioning within the literature**\n\nWe will revise the paper to move the second paragraph of Appendix B into the main text and expand it to more clearly position TiLoIL in relation to existing approaches. For example, Temporal Logic Imitation integrates LTL-based task specifications with low-level control but assumes a pre-trained continuous controller, limiting its ability to improve low-level behavior. In contrast, TiLoIL jointly learns both high-level logic alignment and low-level control from scratch in an end-to-end manner. Similarly, Diffusion Meets Options, LTLDoG, and CTG are fully offline methods trained on large datasets (e.g., 6,686 trajectories in PushT), whereas TiLoIL operates in an interactive setting and learns from only a handful of expert trajectories (e.g., 5 in Carlo). This makes direct empirical comparisons challenging, but highlights TiLoIL’s efficiency in low-data regimes with structured supervision. We will also expand our discussion to more systematically categorize prior work by (1) their strategies to leverage LDBA structures to address the exploration challenge, (2) whether they leverage automaton structures for hierarchical control, and (3) whether they operate in an online or offline setting."}, {"review_id": "ZyC5uUwIjT", "reviewer": "Reviewer_uyFt", "summary": "This paper tackles the challenge of satisfying LTL objectives in reinforcement learning over infinite horizons by using finite-length demonstrations to guide exploration. The proposed method segments trajectories at accepting states and trains the agent to reach these states from arbitrary points, improving satisfaction probability without requiring long demonstrations. Experiments in high-dimensional continuous control domains show faster convergence and better performance than baseline methods.", "questions": "1. In Eq. (4), the reward is defined as a function of the product state $R((s,b))$, independent of the action $a$. This differs from the standard RL setting, where the reward typically depends on both the state and the action, i.e., $R(s, a)$. Could the authors clarify the rationale behind this formulation and its implications, such as how it may affect the optimality of the learned policy in cases where different actions lead to different outcomes despite receiving the same reward?\n2. For the multi-stage reward formulation, how does the choice of the hyperparameter $\\beta$ affect performance, given that the reward directly influences policy learning? Additionally, since the reward depends on the length of the longest acyclic path, could the authors provide more details on how this is computed and how it impacts learning, especially in cases where the path is long, which may lead to very small or vanishing reward signals?\n3. The proposed method assumes access to expert demonstrations. Could the authors clarify the underlying assumptions about these demonstrations? Specifically, do the demonstrations contain trajectories that visit each accepting state, and do they provide sufficient coverage of the state space? For instance, in the FlatWorld Cycle environment, if the demonstrations only reach the yellow region, how would the method support learning policies that reach the green region? Similarly, if all demonstrations originate from the left side of the environment, would this limit the agent’s ability to explore or learn effectively when initialized from the right side?\n4. In the experiments, how many episodes are averaged per evaluation (in addition to the 10 random seeds) for each environment? Also, aside from Cheetah Flip, are the initial positions of the agents and the placement of regions or objects randomly generated during evaluation?", "limitations": "The proposed method faces scalability challenges due to its multi-stage discriminator learning framework. Specifically, the number of accepting states ($b_N$ in Section 3.2) grows with the complexity of the LTL specification and the number of atomic propositions, leading to a corresponding increase in the number of discriminators. This scaling makes the training process more computationally demanding. Moreover, jointly training multiple discriminators alongside the Q-function and policy introduces additional optimization difficulties and may hinder stable convergence.", "rating": 2, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "The motivation to accelerate policy learning under LTL constraints is clear and well-grounded. The authors present a theoretical analysis of the proposed method and support it with empirical results across diverse tasks and environments. However, key aspects of the design choices and evaluation remain insufficiently justified or explored, as outlined in the questions and limitations below.", "was_revised": true, "final_justification": "I appreciate the authors' clarifications and additional experiments. However, I remain concerned about the scalability of the proposed method with respect to the complexity of LTL specifications, particularly those that induce a large number of LDBA states and multiple accepting states. While the provided results are interesting, they are still limited to relatively simple specifications, and it remains unclear how the method would perform on more complex LTL tasks. The alphabet over the atomic propositions is $2^{AP}$, meaning that LTL specifications can induce LDBAs with a large number of (key) states (e.g., significantly more than the 4 in the authors’ examples) and multiple accepting states (e.g., also significantly more than 2 in their examples). As the authors note, their method requires demonstrations that cover key LDBA transitions, particularly those involving visits to accepting states at least once or twice. However, the minimum number of required demonstrations can scale exponentially with the complexity of the specification, which is intractable to obtain in practice. Besides, when this assumption does not hold, i.e., not all key transitions are covered, introducing additional techniques to encourage the agent to actively explore the uncovered key-transition states would significantly improve the completeness of the proposed method rather than replying on \"the underlying RL algorithm (SAC in TiLoIL) to discover trajectories that reach those states through its own exploration\" as the authors claimed. Moreover, the experiments in the paper are oversimplified, with fixed environment configurations. This partly explains why demonstrations provide substantial benefit. However, such a setup significantly undermines the persuasiveness of the results and the demonstrated effectiveness of the proposed method.", "rebuttal": "We appreciate your insightful feedback and constructive comments!\n\n**Limitation: The proposed method faces scalability challenges due to its multi-stage discriminator learning framework. Specifically, the number of accepting states grows with the complexity of the LTL specification and the number of atomic propositions, leading to a corresponding increase in the number of discriminators. This scaling makes the training process more computationally demanding. Moreover, jointly training multiple discriminators alongside the Q-function and policy introduces additional optimization difficulties and may hinder stable convergence.**\n\nLDBAs are commonly used for LTL-to-automaton translation because they yield automata significantly smaller than deterministic Rabin or full deterministic automata, keeping the automaton size manageable while preserving the structure needed for verification and learning. Particularly, the number of accepting states in an LDBA is small—often just one in our benchmarks—and does not scale with specification complexity. In practice, all benchmark LTL specifications in our work (and related studies) produce LDBAs with ≤ 10 states, resulting in only a small number of discriminators and computationally feasible training. We acknowledge that jointly training multiple components can raise stability concerns; however, TiLoIL exhibited stable convergence in all experiments (see Figs. 3–4) with no instability beyond what is typical in adversarial imitation learning (e.g., GAIL). Our framework can be extended to share parameters across discriminators or use belief-weighted mixtures, which would reduce the number of separate networks needed.\n\n**Q1. In Eq. (4), the reward is defined as a function of the product state $R((s,b))$, independent of the action $a$. This differs from the standard RL setting, where the reward typically depends on both the state and the action, i.e., $R(s, a)$. Could the authors clarify the rationale behind this formulation and its implications?**\n\nOur formulation follows standard practice in automata-guided RL and formal methods, where the objective is to find $\\pi^\\star \\in \\arg\\max_{\\pi\\in\\Pi} P(\\pi\\models\\varphi)$, the policy that maximizes the probability of satisfying an LTL specification $\\varphi$. This probability can be written as the expected value of an indicator over trajectories satisfying $\\varphi$ (Line 120). Therefore, the rewards need only encode *progress toward specification satisfaction* (i.e. reaching an LDBA-accepting state), which is determined solely by the product state $(s,b)$ and not by the specific action taken. On the other hand, although $R((s,b))$ does not directly distinguish between actions, the transition dynamics do: different actions from the same state lead to different future product states, resulting in different expected cumulative rewards. Consequently, the optimal policy remains well-defined, and action choices still affect performance through their impact on future specification progress.\n\n**Q2.1 For the multi-stage reward formulation, how does the choice of the hyperparameter $\\beta$ affect performance, given that the reward directly influences policy learning?**\n\nIn our reward formulation, $\\beta$ controls how much the shaped rewards from multi-stage discriminators weigh. All the experiments in the paper are done by $\\beta = 1/3$, the table below shows how different values of $\\beta: (0.49, 1/3, 1/4)$ affect performance across environments, measured by eventual discounted returns over 10 seeds. \n\n|Env|Beta=0.49|Beta=1/3|Beta=1/4|LCER|DRL2|GAIL|CYCLER|\n|-|-|-|-|-|-|-|-|\n|GridCircular Hard|3±0|3±0|3±0|2.4±1.2|3±0|0±0|3±0|\n|FlatWorld Stabilization|47±0|47±0|47±0|47±0|46.8±0.5|9.6±19|47±0|\n|FlatWorld Cycle|1.5±1.5|2.3±0.8|1.5±0.8|1.6±0.6|0±0|0±0|0±0| \n|Doggo Avoid|268±78|296±74|246±110|4.2±12.5|79.9±67.1|0±0|164.6±125|\n|Doggo Navigate|342±38|246±61|192±28|0±0|45.9±64.7|0±0|0±0|\n|Fetch Avoid|35±1.9|36±2.8|37±1.5|13.7±14.8|35.7±5.5|34.9±6.7|12.1±8.8|\n|Fetch Align|30.1±6.4|21±15.9|20±20|1.8±3.3|0±0|0±0|0±0|\n|Carlo|2.6±1.1|3.2±1.8|2.3±0.3|0±0|0.3±0.5|0±0|0±0| \n|CheetahFlip|7.25±1.3|3.5±2.1|3.3±3.3|0±0|2.5±5|2.4±1.6|0±0|\n\nAll our ablations outperform the baselines. For easy tasks like GridCircular Hard and FlatWorld Stabilization, this hyperparameter doesn't have a significant impact. Some challenging tasks such as Fetch Align and CheetahFlip perform better with larger $\\beta$, meaning the shaped reward from the discriminator guides the learning more effectively.\n\n**Q2.2 Additionally, since the reward depends on the length of the longest acyclic path, could the authors provide more details on how this is computed and how it impacts learning, especially in cases where the path is long, which may lead to very small or vanishing reward signals?**\n\nWe compute the longest acyclic path by performing depth-first search to enumerate all simple paths from a given automaton state to any accepting state. If a state is encountered that is already on the current path, we do not extend the path further through that state. Since LDBAs are typically small and structurally constrained in our benchmarks, this approach remains computationally tractable in all tasks we considered. Normalizing the progress-based reward in Eq. 8 by the length of the longest path is beneficial for stabilizing training as it ensures that all progress signals are kept within a consistent [0,1] range, which helps maintain reward sensitivity throughout training. Empirically, we did not observe vanishing gradient issues—likely due to the sparse nature of LDBAs. \n\n**Q3. The proposed method assumes access to expert demonstrations. Could the authors clarify the underlying assumptions about these demonstrations? Specifically, do the demonstrations contain trajectories that visit each accepting state, and do they provide sufficient coverage of the state space? For instance, in the FlatWorld Cycle environment, if the demonstrations only reach the yellow region, how would the method support learning policies that reach the green region? Similarly, if all demonstrations originate from the left side of the environment, would this limit the agent’s ability to explore or learn effectively when initialized from the right side?**\n\n* TiLoIL assumes that the demonstrations cover key transitions of an LDBA, especially by visiting accepting states at least once or twice  (Line 184), thereby enabling it to identify and learn from successful automaton progressions. We provide a detailed discussion and examples of this assumption in our response to Reviewer Tszg (Q2).\n\n* However, TiLoIL does *not* require the demonstrations to provide sufficient coverage of the state space because it is able to leverage the agent's own behaviors—those that have progressed beyond certain LDBA states—as positive trajectories to train discriminators that guide learning for those trajectories that fail to meet such LDBA states, thereby reducing reliance on large demonstration datasets (Fig. 4 further supports this, as TiLoIL_noStage, which lacks multi-stage discriminators and resembles GAIL, performs worse).  In FlatWorld Cycle, if we use the demonstrations that originate from the left side of the environment, and train the agent starting from the right, it still learns well (converging to 3 returns after 200K steps).\n\n* Importantly, TiLoIL does *not* require user-demonstrations to be of high quality. In practice, user-provided demonstrations may be suboptimal due to the cost and complexity of constructing trajectories that robustly satisfy such objectives. In our setup, demonstrations are generated by chaining locally trained controllers for each stage of the LTL task (line 341). These policies are not globally optimal: when executed repeatedly, they often fail to produce trajectories that visit LDBA-accepting states infinitely often. For example, in CheetahFlip, the chained controllers—and thus the resulting demonstrations—achieve only one or two rotations, since additional flips require maintaining momentum after reaching an accepting state, which the learned local policies cannot sustain. Similarly, in Carlo, demonstrations rarely reach accepting states more than twice. Despite this suboptimality, TiLoIL learns policies that outperform the demonstrations, empirically visiting accepting states more frequently in both CheetahFlip and Carlo.\n\n**Q4. In the experiments, how many episodes are averaged per evaluation (in addition to the 10 random seeds) for each environment? Also, aside from Cheetah Flip, are the initial positions of the agents and the placement of regions or objects randomly generated during evaluation?**\n\nWe evaluated each policy using 10 episodes per random seed, averaged across 10 seeds. The initial positions are random in Doggo, Fetch, and Carlo environments; fixed in FlatWorld environments."}, {"review_id": "nG0IBvFphp", "reviewer": "Reviewer_Tszg", "summary": "In this paper, the authors address the problem of learning to accomplish infinite-horizon tasks posed as LTL formulas. In these tasks, the goal is to repeatedly reach an accepting state in the Limit Deterministic Büchi Automaton (LDBA) that results from the LTL. These tasks are challenging since they have naturally sparse rewards. To address this, the authors propose to leverage segmented finite expert demonstrations and trajectories produced by the learned policy itself. The method enables providing guidance for each segment and results in faster convergence with respect to several baselines.", "questions": "I would really appreciate if the authors can especially focus on Q1 and Q2. I am keen on increasing my score if my doubts are addressed.\n\n**Q1.** The approach seems general enough to be applicable in the context of a finite-horizon task since finite-horizon tasks can also be naturally segmented. Indeed, most of the tasks used in the ablations (`Doggo` and `Fetch`) are finite-horizon in my understanding, since they have absorbing accepting states. However, upon testing the segmentation in the ablation studies (Fig. 4) it is said that there is negligible difference between segmenting and not doing so. My questions on this matter are:\n* Why would segmentation only benefit tasks without absorbing accepting states?\n* Following lines 187-188, does this have something to do with satisfying LTL constraints over infinite horizons being more challenging? Why?\n* Why motivating the use of infinite-horizon tasks but then most of the tasks are finite-horizon?\n* Why are the ablations not performed (or shown) for `GridCircular Hard` or `FlatWorld` tasks?\nPlease let me know I am wrong in saying that tasks with absorbing accepting states do not have an infinite horizon.\n\n**Q2.** In what contexts would finite-length demonstrations (or a finite number of them) be potentially problematic or insufficient? In the considered tasks, the environment never changes after reaching the accepting state (e.g. the yellow area in `FlatWorld Stabilization` does not change location); thus, a single demonstration where the accepting state is reached once seems enough. However, there are infinite-horizon tasks where the environment can change, e.g. see the tasks Cookie (the location of a cookie changes after pressing a button) and Symbol in [1]. Under which circumstances would demonstrations in these settings be useful? Have any inherent assumptions on the demonstrations been made in the submitted work? Is the assumption visiting an accepting state only once or twice stronger than it seems?\n\n**Q3.** Has the effect of having longer or shorter demonstrations (hence, reaching the accepting states more or fewer times) been studied? If not, how do you think it can influence the performance of the algorithm?\n\n**Q4.** Has the approach been compared against methods that leverage the structure of an automaton for reward shaping? For example, potential-based reward shaping is employed in the cited works by Camacho et al. using the minimum distance to the accepting state and performing value iteration over the automaton graph. How about method using hierarchical reinforcement learning, which similarly leverage the decomposition of a task into substages? If not, what are the key differential factors you would expect to see (or if they are not applicable in your context, please explain why).\n\n**References**\n[1] Toro Icarte et al. (2019). Learning Reward Machines for Partially Observable Reinforcement Learning.", "limitations": "Yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 2, "originality": 3, "strengths_and_weaknesses": "## Strengths\n- The motivation and the background are clear and described with the right amount of detail. The running example is of great help throughout the paper.\n- The core contributions (segmentation and discriminating trajectories across multiple stages) are clearly described. The ablation studies assess their impact in different tasks, and clear performance gains are shown.\n- Excellent scholarship -- key works in the area are acknowledged throughout the paper.\n- The assumptions and limitations of the method are clearly highlighted.\n\n## Weaknesses\n- The term *occupancy measures* in line 169 is not defined then. Following a (presumably) new mention in line 349, I understand it is related to task satisfaction. It would be convenient to clarify it in future versions.\n- Figure 5 is key for the paper, but it is in the appendix.\n- The figure for `FlatWorldStabilization` would be clearer if the agent stayed within the yellow zone (for clarity, seems stabilizing seems a bit ambiguous).\n- The emphasis of the paper is on infinite-horizon tasks, but most of the testing tasks (`Doggo` and `Fetch`, as highlighted in Fig. 4) are (or seem) finite-horizon. The motivation upon reaching this prt of the paper becomes unclear [see Question 1].\n- It would be interesting to see how performance changes with demonstrations where an accepting state is reached a variable number of times and highlight potential assumptions on the demonstrations as well as their applicability in contexts where the environment can change [see Questions 2 and 3].\n\n## Minor Comments\n- Line 124: \"incentivize\" -> \"incentivizes\".\n- Line 210: \"data sampled from a sampled replay buffer\" -> Perhaps the authors meant \"data sampled from a replay buffer\".\n- MaxStage in Eq. 7 -> \\textsc{MaxStage} (like in the lines below).\n- Line 328: footnote should go after the dot, i.e. \"...stays still.\\footnote{...}\".\n- The Conclusion should be in its main section (probably left within the Related Work because of lack of space).", "was_revised": true, "final_justification": "In light of the positive answers provided by the authors, I have decided to increase my score. The paper explores a novel direction at the intersection between RL and LTL, focusing on learning policies for infinite-horizon tasks from finite-length imperfect demonstrations. The motivation is clear, the core contributions are well described, and several ablations are performed. Key work in the area---at least the ones I am aware of---are acknowledged.\n\nMy concerns about the method were mainly on the experimental side. Most domains did not seem to be infinite-horizon, but they actually were, despite using absorbing states. Reservations about implicit assumptions on the limitations have also been addressed through domains recommended in the review. Research in the area would benefit from adding them in future research. \n\nIn the discussion with the authors, [some recommendations](https://openreview.net/forum?id=MKLcSmSTQI&noteId=n2J8BZYPNQ) were made for future versions. The authors also [listed](https://openreview.net/forum?id=MKLcSmSTQI&noteId=k6zvvUT3cr) the main \"to-do\" for the following versions, which will strengthen the paper.\n\nIn addition to these, the authors thoroughly addressed the concerns of other reviewers. For future versions, I would especially highlight:\n- Some of the suggested related work and the use of the term \"multi-objective\" by Reviewer ifPj.\n- Following the discussion with Reviewer uyFt, the authors could point out some existing approaches that use rewards encoding _progress toward specification satisfaction_, e.g. the LTL-based works [1, 2], which give a reward of 1 every time the LTL formula is progressed.\n- Assumptions (or lack thereof) in the demonstrations, following Q3 answer to Reviewer uyFt.\n\n[1] Vaezipoor et al. \"LTL2Action: Generalizing LTL Instructions for Multi-Task RL\". ICML 2021.  See Definition 3.2.\n\n[2] Tuli et al. \"Learning to Follow Instructions in Text-Based Games\". NeurIPS 2022. See Section 4.2.", "rebuttal": "We appreciate your insightful feedback and constructive comments!\n\n**Q1.1 Why would segmentation only benefit tasks without absorbing accepting states?**\n\nIn tasks with absorbing accepting states (e.g., Doggo, Fetch), the agent is expected to remain in the accepting state once it is reached, leaving no further progression to segment or imitate—aside from maintaining safety (e.g., avoiding sink states). In such cases, segmentation reduces to a trivial one-step segment exactly at accepting states and primarily serves to provide safety-related reward signals. Segmentation is particularly beneficial for tasks without absorbing accepting states, where the agent must repeatedly visit, leave, and return to accepting states. These tasks exhibit rich, multi-phase behaviors, and segmented imitation enables TiLoIL to learn policies that cycle between accepting states—effectively supporting repeated satisfaction of the LTL objective. **We emphasize that even in tasks with absorbing accepting states, TiLoIL still benefits from multi-stage discriminator learning and reward formulation, as shown in Figure 4.**\n\n**Q1.2 Following lines 187-188, does this have something to do with satisfying LTL constraints over infinite horizons being more challenging? Why?**\n\nLines 187–188 highlight the challenge of imitation learning under LTL constraints: the agent must generalize from *finite-length* demonstrations to satisfying *infinite-horizon* objectives. In practice, user-provided demonstrations may be suboptimal due to the cost and complexity of constructing trajectories that robustly satisfy such objectives. In our setup, demonstrations are generated by chaining locally trained controllers for each stage of the LTL task (line 341). These policies are not globally optimal: when executed repeatedly, they often fail to produce trajectories that visit LDBA-accepting states infinitely often. For example, in CheetahFlip, the chained controllers—and thus the resulting demonstrations—achieve only one or two rotations, since additional flips require maintaining momentum after reaching an accepting state, which the learned local policies cannot sustain. Similarly, in Carlo, demonstrations rarely reach accepting states more than twice. Despite this suboptimality, TiLoIL learns policies that outperform the demonstrations, empirically visiting accepting states more frequently in both CheetahFlip and Carlo.\n\n**Q1.3 Why motivating the use of infinite-horizon tasks but then most of the tasks are finite-horizon? (Please let me know I am wrong in saying that tasks with absorbing accepting states do not have an infinite horizon.)**\n\nWhile several tasks in our benchmark suite include absorbing accepting states, they are still formally infinite-horizon: the agent operates in an unbounded setting where episodes do not terminate upon reaching accepting states. Crucially, the agent must continue to satisfy any ongoing safety properties—e.g., avoiding unsafe regions in Doggo Avoid—even after accepting states are reached. Importantly, 5 out of 9 tasks in our suite require policies with meaningful $\\omega$-regular structure to satisfy the specification—for example, visiting certain regions repeatedly. These tasks truly exhibit the types of behaviors that infinite-horizon LTL specifications are designed to express. We will clarify the distinction between infinite-horizon formulations and absorbing structures in the revised version.\n\n**Q1.4 Why are the ablations not performed (or shown) for GridCircular Hard or FlatWorld tasks?**\n\nThe ablations for GridCircular Hard and FlatWorld are shown below. Both multi-stage reward formulation and segmented imitation are important. Performances are measured by eventual discounted returns over 10 seeds.\n\n|Env|TiLoIL|TiLoIL-noStage|TiLoIL-noSegment|\n|-|-|-|-|\n|FlatWorld Stabilization|47±0|27.5±22.5|None|\n|GridCircular Hard|3.0±0|0±0|0±0|\n|FlatWorld Cycle|2.3±0.8|0±0|0±0|\n\n**Q2. In what contexts would finite-length demonstrations be potentially problematic or insufficient? There are infinite-horizon tasks where the environment can change, e.g. see the tasks Cookie and Symbol in [1]. Under which circumstances would demonstrations in these settings be useful? Have any inherent assumptions on the demonstrations been made in the submitted work? Is the assumption visiting an accepting state only once or twice stronger than it seems?**\n\nA finite number of demonstrations may become insufficient in more dynamic settings, such as those with varying accepting conditions, if they fail to capture the necessary behavioral diversity.\n\nTo evaluate TiLoIL in such settings, we adapted two environments inspired by Cookie and Symbol from [1].\n\n* **Cookie-like task**: We modified the Fetch Pick\\&Place environment by introducing a button on the table. Pressing the button causes a goal region to appear. The manipulator must (1) press the button, (2) pick up a block and move it to the goal region, and then (3) repeat this sequence with the goal region appearing in a new location each time. Compared to the baselines, TiLoIL was the only method that successfully solved this task within 2 million steps, demonstrating its ability to handle changing environments.\n\n* **Symbol-like task**: We redesigned the original Symbol task into the Pick\\&Place environment. The workspace contains a movable block and two potential destination regions: a *tray* and a goal region. A tray may or may not appear in the scene at each episode. The symbolic cue is the presence or absence of the tray:\n\n    * If the tray appears, the agent must place the block into the tray.\n    * If the tray is absent, the block should be placed into the goal region.\n\nThe LTL specification is (tray_present -> F in_tray) && (Not tray_present -> F in\\_goal). This task highlights a core challenge in learning from partial demonstrations. When demonstrations only show placing the block into the goal region (i.e., when the tray is absent), TiLoIL fails to generalize to the unseen tray-present case. It always moves the block to the goal region regardless of tray appearance. However, when demonstrations cover both cases (tray present and tray absent), TiLoIL successfully learns the correct conditional behavior.\n\nThese experiments clarify our assumption: demonstrations must sufficiently cover the behavioral variations necessary to reach the accepting conditions under different modes. When demonstrations cover only a subset of the possible cases, the learned policy may become biased toward that subset and fail to generalize. We will include a clearer articulation of this assumption, along with a discussion of these experiments, in the revised manuscript. We will clarify that “reaching accepting states once or twice” is not a criterion for demonstration quality.  Rather, this was a practical design choice in our experimental setup to showcase that TiLoIL can still succeed even when demonstrations are sparse *for the benchmarks we considered*.\n\n**Q3. Has the effect of having longer or shorter demonstrations (hence, reaching the accepting states more or fewer times) been studied? If not, how do you think it can influence the performance of the algorithm?**\n\nThe table below illustrates the impact of demonstration length on performance. Performances are measured by eventual discounted returns over 10 seeds. The first column uses demonstrations of 100 steps, while the second and third columns extend this to 200 and 400 steps, respectively. In the Carlo environment, longer demonstrations improve learning outcomes. For CheetahFlip, extending the demonstration length does not help because the demonstrations are suboptimal (see Q1.2) and longer trajectories do not provide more visits to accepting states.\n\n|Env|demo length=100|200|400|\n|-|-|-|-|\n|Carlo|1.6±0.7|2.15±0.9|3.2±1.8|\n|CheetahFlip|3.5±2.1|3.3±2.3|2.3±1.8|\n\n**Q4.1 Has the approach been compared against methods that leverage the structure of an automaton for reward shaping?**\n\nIndeed, earlier works by Camacho et al. [12, 13] propose potential-based reward shaping using distances in product MDPs (based on the minimum number of steps to accepting automaton states). Another work [31] extend this idea by computing potential functions via value iteration on a synthesized MDP from the automaton of a temporal property. These approaches are not directly applicable to ω-regular problems. By adopting an LDBA instead of a DFA, and integrating an eventual discounting scheme, more recent approaches introduce reward shaping methods tailored for the full expressiveness of LTL. For example, Bagatella et al. [6] (DRL2) propose a Bayesian method that models LDBAs as Markov reward processes with learned transition kernels, enabling potential-based shaping via high-level value estimation. Similarly, Shah et al. [55] (Cycler) distribute heuristic rewards along LDBA accepting paths. In our paper, we compare TiLoIL against DRL2 and Cycler as the most relevant potential-based reward shaping baselines.  As shown in Fig. 3, TiLoIL consistently outperforms both, demonstrating the benefit of leveraging demonstration guidance.\n\n**Q4.2  How about method using hierarchical reinforcement learning, which similarly leverage the decomposition of a task into substages?**\n\nIndeed, several works within the LTL literature leverage the structure of automata to define hierarchical policies, such as Hasanbeig et al. (2020), Icarte et al. (2022), and Jothimurugan et al. (2021) [28, 31, 35]. These methods decompose the overall task into subtasks associated with automaton transitions, improving sample efficiency. However, a known limitation of such hierarchical approaches is potential suboptimality due to local policy decisions at each subtask level [31]."}]

Author rebuttal:

Meta-review: This paper proposes TiLoIL, an imitation learning method designed to handle infinite-horizon tasks specified using Linear Temporal Logic (LTL). The approach leverages segmented demonstrations and product MDP structure to generate dense rewards and guide exploration. Trajectories are segmented at accepting states, and stages within those segments are used to refine the discriminator training in a GAIL-style framework. Experiments across multiple domains, including continuous control and gridworld settings, show faster convergence and improved performance compared to baselines without LTL guidance.

**Strengths:** The paper addresses an important and timely problem at the intersection of reinforcement learning and formal task specification. It clearly motivates the difficulty of combining LTL with finite demonstrations and proposes a principled way to densify sparse rewards through segmentation and staging. The method is well described, and the ablation studies highlight the value of the segmentation mechanism, particularly in cyclical tasks. Related work is carefully discussed, and the paper demonstrates solid scholarship. During the rebuttal, the authors provided thorough clarifications, new experiments, and detailed responses that improved the clarity of contributions and addressed most reviewers' questions.

**Weaknesses:** While the contributions are meaningful, the evaluation remains somewhat limited in scope. The tested environments are fixed, which simplifies the benefit of demonstrations, and the method’s scalability to more complex LTL specifications with larger automata is not fully established. The approach assumes access to near-optimal demonstrations, and it is unclear how robust it would be to sub-optimal or incomplete ones. While the authors suggest that stronger exploratory RL algorithms could compensate for this, such an argument does not fully address the concern.

**Final Recommendation:** Overall, the paper makes a novel and interesting contribution toward learning policies from demonstrations under infinite-horizon LTL constraints. The authors engaged very constructively during the rebuttal, providing additional results and clarifications. I recommend acceptance (poster). The authors should, however, clearly state in the final version the limitations of their evaluation (fixed environments) and discuss possible directions for overcoming this, as well as strengthen the discussion of assumptions on demonstrations and related work.
Decision: Accept (poster)