Proceedings of Machine Learning Research vol vvv:1–22, 2026
SpecRLBench: A Benchmark for Generalization in Specification-Guided Reinforcement Learning Zijian Guo
ZJGUO @ BU . EDU
Boston University
İlker Işık
IILKER @ BU . EDU
Boston University
H. M. Sabbir Ahmad
SABBIR 92@ BU . EDU
arXiv:2604.24729v1 [cs.LG] 27 Apr 2026
Boston University
Wenchao Li
WENCHAO @ BU . EDU
Boston University
Abstract Specification-guided reinforcement learning (RL) provides a principled framework for encoding complex, temporally extended tasks using formal specifications such as linear temporal logic (LTL). While recent methods have shown promising results, their ability to generalize across unseen specifications and diverse environments remains insufficiently understood. In this work, we introduce SpecRLBench, a benchmark designed to evaluate the generalization capabilities of LTL-based specification-guided RL methods. The benchmark spans multiple difficulty levels across navigation and manipulation domains, incorporating both static and dynamic environments, diverse robot dynamics, and varied observation modalities. Through extensive empirical evaluation, we characterize the strengths and limitations of existing approaches and reveal the challenges that emerge as specification and environment complexity increase. SpecRLBench provides a structured platform for systematic comparison and supports the development of more generalizable specificationguided RL methods. Code is available at https://github.com/BU-DEPEND-Lab/SpecRLBench Keywords: Temporal logic specifications, Reinforcement Learning, Benchmark
1. Introduction Reinforcement learning (RL) enables agents to learn decision-making policies through interaction with their environments. Numerous studies have achieved promising results in domains such as robotics (Jiang et al., 2024; Luo et al., 2025), autonomous driving (Wang et al., 2023b; Zhang et al., 2025; Lu et al., 2025), and healthcare (Gorrepati and Potla, 2025; Choppara and Lokesh, 2025). However, effectively handling complex tasks with long-term temporal structure remains a significant challenge for most existing approaches. For example, a manipulation task may require an arm to reach multiple target regions in a specific order while always avoiding unsafe areas. To specify such complex tasks, various approaches have been proposed. One prominent direction uses natural language instructions (Yang et al., 2021; Mees et al., 2022; Huang et al., 2025; Zakharov and Whiteson, 2025; Kim et al., 2025; Yu et al., 2025), which provide a flexible and intuitive interface for describing desired behaviors. While effective in many settings, natural language specifications can be ambiguous and may lack precise semantics (Pang et al., 2023; Kharyal et al., 2024; Xie et al., 2025), making consistent interpretation and verification challenging. An alternative line of work employs formal specification languages (Araki et al., 2021; Voloshin et al., 2023; Jothimurugan et al., 2025), which offer precise, unambiguous descriptions of desired © 2026 Z. Guo, .̇ Işık, H.M.S. Ahmad & W. Li.
G UO I ŞIK A HMAD L I
behaviors and explicitly capture temporal structure. While specification-guided RL has attracted growing interest, progress in this area is hindered by the lack of a standard benchmark. Existing methods are typically evaluated in isolated environments with limited task diversity, making it difficult to systematically compare approaches or to assess key capabilities such as generalization to unseen specifications (Jackermeier and Abate, 2025; Guo et al., 2025) and robustness to environment variations (Fan and Zhu, 2025; Bagatella et al., 2025). To address this gap, we introduce our benchmark, the Specification-Guided RL Benchmark (SpecRLBench), which provides a diverse set of environments for training and testing specificationguided RL methods, with the goal of enabling systematic evaluation of generalization. Overall, SpecRLBench consists of 19 environment variants spanning multiple difficulty levels across navigation and manipulation domains, incorporating static and dynamic environments, diverse robot dynamics, and varied observation modalities. All environments follow the standard Gym interface (Towers et al., 2024), allowing seamless integration with existing methods and serving as a convenient starting point for developing and testing new ideas. In addition, we conduct a comprehensive empirical study and provide insights into the strengths and limitations of current approaches.
2. Related Work Specification-guided RL. A growing body of work studies RL under explicit task specifications, where desired behaviors are defined using structured or formal representations. Among these, temporal logic has been widely adopted to encode long-horizon objectives and safety-critical requirements, including linear temporal logic (LTL) (Cai et al., 2023; Tasse et al., 2024; Manganaris et al., 2025; Fan and Zhu, 2025; Shah et al., 2025), signal temporal logic (STL) (Aksaray et al., 2016; Guo et al., 2024; Xiong et al., 2024; Wang et al., 2024; Meng and Fan, 2025; Meng et al., 2025; Liu et al., 2025), and other related formalisms (Li et al., 2017; Brafman et al., 2018; Jothimurugan et al., 2019; De Giacomo et al., 2019; Jothimurugan et al., 2021; Furelos-Blanco et al., 2023; Shukla et al., 2024; Roy et al., 2025). Temporal logic has also been used to specify coordinated behaviors and interaction constraints in multi-agent settings to guide policy learning (Eappen and Jagannathan, 2022; Hammond et al., 2021; Wang et al., 2023a; Ardon et al., 2023; Smith et al., 2023; Yalcinkaya et al., 2025). Despite these advances, most existing methods focus on learning policies for a single fixed specification (Hasanbeig et al., 2018; Hahn et al., 2019; Bozkurt et al., 2020; Icarte et al., 2022; Zhou and Li, 2022; Shao and Kwiatkowska, 2023; Le et al., 2024). More recently, the expressiveness of temporal logic and the need to adapt to changing task requirements in real-world applications have drawn increasing attention to generalization across specifications (Vaezipoor et al., 2021; Qiu et al., 2023; Yalcinkaya et al., 2024; Jackermeier and Abate, 2025; Guo et al., 2025; Meng and Fan, 2025). Collectively, these methods highlight the potential of formal specifications for capturing complex behaviors. However, existing evaluations are often conducted within a single environment or a narrowly varying set of environments, limiting insight into how specification-guided methods generalize and scale beyond a particular setting. Existing benchmarks. The study of generalization in specification-guided RL is closely related to several areas, including multi-task RL (Vithayathil Varghese and Mahmoud, 2020), as each specification can be viewed as defining a task, and goal-conditioned RL (Liu et al., 2022), since the representation of a specification effectively serves as the goal signal for policy learning. A number of benchmarks have been proposed in these domains, such as Meta-World (Yu et al., 2020), 2
S PEC RLB ENCH
CompoSuite (Mendez et al., 2022), and CORA (Powers et al., 2022) for multi-task RL, and MiniGrid (Chevalier-Boisvert et al., 2023), BabyAI (Chevalier-Boisvert et al., 2018), D4RL (Fu et al., 2020), and OGBench (Park et al., 2024) for goal-conditioned RL. However, benchmarks such as Meta-World, CompoSuite, and CORA do not explicitly focus on tasks with temporal and logical constraints. Their tasks are typically defined as single-step objectives, such as picking an object or opening a door, and rarely require sequential or temporally structured behaviors. Similarly, D4RL and OGBench primarily emphasize goal-reaching without incorporating temporal and logic requirements. While MiniGrid and BabyAI include instruction-following tasks with some sequential structure, they are limited to discrete-action environments with grid-based observations, and do not cover high-dimensional, continuous-control settings. There also exist benchmarks based on natural language conditioning, such as CALVIN (Mees et al., 2022), LIBERO (Liu et al., 2023), and ImagineBench (Pang et al., 2025). However, these environments are typically designed to evaluate advanced vision-language or vision-language-action models, and thus diverge from the current focus on studying generalization in specification-guided RL under formal specifications.
3. Preliminaries Reinforcement Learning. We model the decision-making problem as a Markov decision process (MDP) defined by the tuple M := (S, A, P, r, γ, d0 ), where S denotes the state space, A is the action space, P : S × A × S → [0, 1] is the transition dynamics, r : S × A → R is the reward function, γ ∈ (0, 1) is the discount factor, and d0 ∈ ∆(S) denotes the initial state distribution. Let π : S×A 7→ [0, 1] denote the policy and τ = {st , at , rt }∞ t=0 denote the trajectory through interaction with the environment, where rt = r(st , at ). In standard RL, the goal is to find P the toptimal policy π ∗ that maximizes the expected discounted cumulative reward: maxπ Eτ ∼π [ ∞ t=0 γ rt ]. Linear temporal logic. Linear Temporal Logic (LTL) (Pnueli, 1977) provides a formal framework for specifying temporal properties over infinite sequences of system states. An LTL formula is constructed from a finite set of atomic propositions AP using Boolean operators, including negation (¬), conjunction (∧), and disjunction (∨), together with temporal operators such as ”until” (U), ”eventually” (F), and ”always” (G). Formally, for a ∈ AP , the syntax is defined recursively as φ := a | ¬φ | φ1 ∧ φ2 | φ1 ∨ φ2 | F φ | G φ | φ1 U φ2 . Intuitively, the formula φ1 U φ2 is satisfied if φ2 holds at some future time step and φ1 holds at all preceding steps. The temporal operator F φ requires that φ be satisfied at least once in the future, whereas G φ requires φ to hold at all time steps from the current point onward. To interpret LTL formulas in an MDP, a labeling function is typically assumed L : S → 2AP , which associates each state with the set of atomic propositions that are true in that state. A trajectory τ thereby induces a trace Tr(τ ) = L(s0 )L(s1 ) . . ., and we write τ |= φ if this trace satisfies the LTL formula φ. Given a policy π, the probability of satisfying φ is defined as Pr(π |= φ) = Eτ ∼π [1[τ |= φ]] , where 1[·] denotes the indicator function. In this context, an optimal policy is one that maximizes the probability of satisfying the given LTL specification.
4. Benchmark As illustrated in Figure 1, the benchmark includes navigation and manipulation tasks in both singleagent and multi-agent settings. The environments cover static and dynamic scenarios with multiple robot dynamics and observation modalities. Together, these design choices enable the construction 3
G UO I ŞIK A HMAD L I
of task variants with different difficulty levels, facilitating evaluation of performance in terms of generalization to unseen specifications and scalability to environment variations.
Figure 1: SpecRLBench overview. SpecRLBench spans navigation and manipulation domains with single-agent and multi-agent settings, covering both discrete and continuous action spaces and multiple observation modalities. This breadth supports tasks of varying difficulty and enables evaluation of current methods under diverse settings. 4.1. Navigation Tasks Environments. The navigation tasks include two environments: LetterWorld and ZoneEnv, adapted from prior work (Vaezipoor et al., 2021; Qiu et al., 2023; Jackermeier and Abate, 2025; Guo et al., 2025). In both environments, the task is to reach target letters or regions while avoiding others, as specified by an LTL formula. The atomic propositions are by default defined as the letters, e.g., AP = {a, b, · · · }, or the colored regions, e.g., AP = {green, blue, · · · }. Users may also specify custom atomic-proposition sets through environment initialization, enabling evaluation of scalability with respect to the number of propositions. To promote generality, the spatial locations of letters or regions are randomly sampled at the beginning of each episode during both training and evaluation. In LetterWorld, the action space is discrete, consisting of up, down, left, and right, and observations are provided as agent-centric grid maps indicating letter locations. In ZoneEnv, we consider multiple robot embodiments with different dynamics, including Point, a simple planar robot with turning and translation; Car, a wheeled robot with differential-drive control; and Ant, a quadrupedal robot. The observation space in ZoneEnv supports both state-based inputs, e.g., LiDAR, and pixel-based inputs, e.g., vision, with the observation modality specified by the user at initialization, allowing evaluation across different sensing modalities. Variants. We include several variants of the environments to capture different sources of complexity. In LetterWorld, partial observability can be enabled by restricting the agent to a limited sensing range instead of providing access to the full grid map. In ZoneEnv, the regions associated with each atomic proposition are static by default; we additionally consider variants with dynamically moving regions to model more realistic, time-varying settings. In these dynamic variants, regions may temporarily overlap and later separate, which allows evaluation of policy robustness under changing environment dynamics and non-stationary task conditions. Users can further specify customized numbers of static and dynamic regions when initializing the environments. We also construct a multi-agent variant of ZoneEnv as LTL naturally supports the specification of multiagent behaviors. In this setting, multiple agents operate simultaneously in a shared environment. 4
S PEC RLB ENCH
Each agent observes the colored regions and the positions of other agents via LiDAR, allowing the specification to encode coordination, synchronization, and ordering constraints among agents. For example, each agent can be assigned an individual sequence of target regions, while at certain stages they must coordinate to reach the same region or different regions at the same time, and then resume their own tasks. This variant enables evaluation of specification-guided RL methods in multi-agent scenarios with shared objectives and inter-agent interactions. 4.2. Manipulation Tasks Environments. The manipulation environments are adapted from (Gallouédec et al., 2021). Similar to the ZoneEnv, different colored regions are placed in the 3D workspace of a 7-DoF robot arm as shown in Figure 1. The task is to reach or avoid specified regions according to a given LTL formula. We consider two operation modes with different granularities of specification. In the first mode, the task specification focuses solely on the grippers of the robotic arm, following prior work (Bagatella et al., 2025; Fan and Zhu, 2025). In this case, atomic propositions are defined over regions that the grippers should reach or avoid, e.g., AP = {green, blue, . . .}. In the second mode, the specification jointly constrains both the robotic arm and the grippers. Accordingly, atomic propositions distinguish between different robot components and regions, e.g., AP = {grippers green, arm green, grippers blue, arm blue, . . .}. This mode more closely reflects real-world manipulation scenarios in which specifications impose constraints on multiple components of the robot simultaneously. In both modes, a range-bearing observation is used, providing the distance and direction to the colored regions. Note that in this manipulation task, we omit explicit grasping and placing behaviors. While such behaviors are important components of real-world manipulation, the goal of this environment is to evaluate temporal logic requirements rather than low-level manipulation skills of the grippers. Grasping and placing can be naturally incorporated as extensions, since these behaviors typically build upon reaching actions; for example, the gripper must first reach a target location near an object before grasping and subsequently placing it elsewhere. 4.3. Environment Interfaces Our benchmark environments follow a standard Gym-compatible interface (Towers et al., 2024), enabling seamless integration with existing RL libraries. Each observation is structured into two components: a proposition-dependent part sAP , which captures information relevant to atomic propositions, e.g., observations of colored zones, and a proposition-independent part s̸=AP , which encodes the agents ego-state, e.g., proprioceptive or kinematic features. This decomposition provides users with the flexibility to use these components jointly or separately, depending on the requirements of the learning algorithm. The labeling function is implemented by evaluating the underlying task state. In navigation tasks, atomic propositions are determined by checking the agents position relative to designated regions, whereas in manipulation tasks, propositions are derived from contact information and interaction states of the robotic arm. At each timestep, the environment returns the set of propositions that are currently satisfied. To avoid imposing method-specific assumptions, the benchmark does not prescribe a particular reward structure. Instead, the default reward is set to zero, allowing users to define rewards or shaping mechanisms appropriate for their learning objectives while relying on the benchmarks ground-truth proposition assignments and specification satisfaction signals for evaluation. More details of the environments can be found in Appendix A.1 5
G UO I ŞIK A HMAD L I
5. Experiments and Analysis Baselines. In this section, we compare representative specification-guided RL methods that target generalization across LTL specifications using our benchmark. Specifically, we consider: (1) LTL2ACTION (Vaezipoor et al., 2021), which applies LTL progression to track the remaining portion of a specification online and employs a graph neural network to encode its evolving structure; (2) GCRL-LTL (Qiu et al., 2023), which uses a heuristic procedure to identify subgoal sequences for satisfying new specifications; (3) D EEP LTL (Jackermeier and Abate, 2025), which learns policies conditioned on embeddings of subgoal sequences; (4) G EN Z-LTL (Guo et al., 2025), which conditions policies only on the current subgoal and satisfies specifications incrementally one subgoal at a time; and (5) RAD-E MBEDDINGS (Yalcinkaya et al., 2024), which pre-trains embeddings over compositions of deterministic finite automata (DFAs) and learns policies conditioned on these automaton-based representations. We use their official implementation and make modifications to the parameters for fair comparison. Details can be found in Appendix B. LTL specifications. For evaluation, we consider a wide range of LTL specifications, including both finite-horizon and infinite-horizon tasks that cover safety, liveness, and their combinations. In both settings, we include: (1) reach-only specifications, where goals are expressed in a nested sequential form of the ”eventually” operator; (2) reach-avoid specifications, which combine goal-reaching with safety constraints through nested compositions of negation, ”until”, and ”eventually”; and (3) more complex specifications that mix reach-only and reach-avoid components to capture richer temporal structure. In addition, for multi-agent settings, we consider specifications that capture both joint and independent behaviors among agents. These diverse specifications enable evaluation across varying levels of temporal complexity, safety requirements, and coordination structure. Some examples of the specifications are listed in Table 1, and the complete list is provided in Appendix A.2. Table 1: Examples of LTL specifications used for evaluation. For specifications in Zone and Arm (grippers-only), b, g, m, and y denote blue, green, magenta, and yellow, respectively. For multi-agents in Zone, the number in the atomic proposition denotes the index of the agent. Finite- ΦIND horizon ΦOOD SingleΦrsp agent InfiniteΦrec horizon Φper Φindep FiniteΦcoop horizon MultiΦmix agent Φrsp InfiniteΦrec horizon Φper
Letter Zone / Arm (grippers-only) ¬(c ∨ d) U ((¬e U l) ∧ (F g)) ¬g U ((b ∨ m) ∧ (¬g U y)) ¬b U ((c ∨ d) ∧ (¬e U (f ∧ F (g ∧ (¬h U (i ∧ F l)))))) F ((b ∨ g) ∧ (¬y U (b ∧ (¬g U m)))) ∧ F (y ∧ (¬b U g)) (G F a) ∧ G (a → (F (b ∧ F c) ∧ (¬d U e))) ∧ G ¬(f ∨ g ∨ h ∨ i) (G F b) ∧ G (b → F g) ∧ G ¬(y ∨ m) (G F a) ∧ (G F b) ∧ (G F c) ∧ (G F d) ∧ (G F e) ∧ G ¬(f ∨ g ∨ h ∨ i ∨ j ∨ k) (G F b) ∧ (G F g) ∧ G ¬(y ∨ m) (F G y) ∧ G ¬(g ∨ b ∨ m) Zone (¬(m 0 ∨ y 0) U (b 0 ∧ F g 0)) ∧ (¬(b 1 ∨ g 1) U (m 1 ∧ F y 1)) F ((b 0 ∧ b 1) ∧ (¬(m 0 ∨ m 1) U ((y 0 ∧ y 1) ∧ F (g 0 ∧ g 1)))) (¬m 0 U y 0) ∧ (¬b 1 U m 1) ∧ F ((b 0 ∧ g 1) ∧ F (g 0 ∧ m 1)) (G F b 0) ∧ (G F g 1) ∧ G (b 0 → F y 1) ∧ G (g 1 → F m 0) ∧ G ¬(y 0 ∨ b 1) (G F (b 0 ∧ g 1)) ∧ (G F (g 0 ∧ y 1)) ∧ G ¬(y 0 ∨ m 1) (F G (y 0 ∧ m 1)) ∧ G ¬(g 0 ∨ b 0 ∨ y 1 ∨ b 1)
Evaluation metrics. For finite-horizon and infinite-horizon tasks, the evaluation metrics are: • (finite) ηs : success rate, the ratio of trajectories that satisfy the specification. • (finite and infinite) ηv : violation rate for specifications involving safety constraints. • (finite and infinite) ηo : others rate, ηo = 1 − ηs − ηv . ηs = 0 for infinite-horizon tasks. • (finite) µ: average number of steps taken to satisfy the specification, computed only over trajectories that satisfy the specification. 6
S PEC RLB ENCH
• (infinite) µacc : average number of visits to accepting states, computed only over trajectories that do not violate the specification (involving safety constraints). Since µ and µacc are conditioned on successful episodes, they are interpreted as a secondary measure of efficiency. The others rate ηo also shows the efficiency of the agent in accomplishing the specified tasks as it captures the fraction of episodes that terminate without either satisfying the specification or violating the safety constraints due to maximum episode length. 5.1. How do the methods generalize to arbitrary LTL specifications? Finite-horizon tasks. We first evaluate the performance of the baselines on finite-horizon tasks. We categorize the specifications into in-distribution (IND) specifications ΦIND , which are sampled from the same distribution used for training, and out-of-distribution (OOD) specifications ΦOOD , which are unseen during training. The results are shown in Table 2. We can observe a consistent performance degradation when moving from IND to OOD specifications, reflected by reduced success rates and increased violation rates. The evaluated methods condition policies on different forms of LTL specifications, including their syntax trees, equivalent automata structures, or corresponding subgoal sequences. However, the specifications sampled during training are often limited, and performance drops on unseen specifications that induce novel automata structures or longer subgoal sequences. This highlights the important role of robust specification representations that can capture unseen specifications and support generalization beyond the training distribution. Table 2: Evaluation results of in-distribution ΦIND and out-of-distribution ΦOOD specifications. We report the success rate ηs , violation rate ηv , and average steps µ to satisfy the complex specifications listed in Table 5. ↑: higher is better; ↓: lower is better. Each value is averaged over 5 seeds, with 100 trajectories per seed. LTL2Action
Arm
Zone
Letter
ηs ↑
ηv ↓
ΦIND 0.59±0.09 0.13±0.04
GCRL-LTL µ↓
6.46±0.74
ηs ↑
ηv ↓
RAD-embeddings µ↓
ηs ↑
ηv ↓
µ↓
DeepLTL ηs ↑
ηv ↓
0.76±0.09 0.07±0.06 12.23±2.63 0.91±0.06 0.08±0.06 13.63±3.01 0.83±0.07 0.03±0.03
GenZ-LTL µ↓ 7.32±1.45
ηs ↑
ηv ↓
0.98±0.03 0.00±0.00
µ↓ 6.82±1.32
ΦOOD 0.01±0.01 0.23±0.14 18.08±3.27 0.66±0.11 0.10±0.10 25.23±1.38 0.79±0.06 0.11±0.05 30.75±3.01 0.70±0.08 0.03±0.03 14.30±0.53 0.94±0.03 0.00±0.00 13.11±0.50 ΦIND 0.58±0.18 0.21±0.13 405.94±135.11 0.85±0.06 0.09±0.06 377.59±80.29 0.92±0.04 0.06±0.05 366.79±77.82 0.84±0.05 0.09±0.05 273.29±66.37 0.98±0.02 0.01±0.01 252.71±51.50 ΦOOD 0.04±0.07 0.40±0.32 824.14±64.46 0.63±0.04 0.11±0.05 726.44±38.83 0.69±0.02 0.15±0.02 715.11±20.63 0.71±0.10 0.13±0.08 564.56±32.40 0.96±0.02 0.01±0.01 499.38±26.37 ΦIND 0.37±0.09 0.13±0.15 72.56±16.75 0.90±0.03 0.10±0.03 24.86±6.18 0.96±0.05 0.01±0.01 41.23±9.04 0.98±0.02 0.01±0.02 25.03±5.95 1.00±0.00 0.00±0.00 23.77±5.27 ΦOOD 0.00±0.00 0.53±0.34
-
0.82±0.07 0.17±0.06 52.80±0.99 0.75±0.09 0.02±0.01 89.82±9.84 0.95±0.03 0.02±0.01 53.28±3.06 1.00±0.01 0.00±0.00 47.81±1.98
Infinite-horizon tasks. We also evaluate the baselines on infinite-horizon tasks. Since LTL specifications admit many possible combinations, it is not feasible to evaluate them exhaustively. In particular, we consider several representative behavior classes: responsive behaviors Φrsp , where visiting one region triggers a requirement to eventually visit another, such as G (α1 ⇒ F α2 ); recurrence behaviors Φrec , which require visiting designated regions infinitely often, such as G F α1 ∧ G F α2 , and persistence behaviors Φper , which require eventually remaining within a target region, such as F G α1 . We also incorporate safety constraints in these specifications, such as G ¬α to assess whether methods can sustain specification satisfaction over long time horizons. The evaluated specifications are listed in Table 5. Compared with finite-horizon tasks, most baselines exhibit a significant rise in violations, highlighting the increased difficulty of maintaining safety over extended executions. GCRL-LTL and DeepLTL use a threshold-based heuristic to handle safety constraints, but setting an appropriate threshold can be challenging, as it may vary across specifications. GenZLTL is the only method that explicitly models safety constraints and consequently shows only a 7
G UO I ŞIK A HMAD L I
slight increase in violation rate. This emphasizes the importance of effectively modeling safety constraints when learning policies to better satisfy LTL specifications. Table 3: Evaluation results of different types of infinite-horizon tasks. We report the violation rate ηv and the average number of visits to accepting states µacc . ↑: higher is better; ↓: lower is better. Each value is averaged over 5 seeds, with 100 trajectories per seed.
Letter
Zone
Arm
Φrsp Φrec Φrsp Φrec Φper Φrsp Φrec Φper
GCRL-LTL µacc ↑ ηv ↓ 6.23±3.02 0.47±0.13 2.24±1.01 0.56±0.12 30.41±8.00 0.44±0.05 30.33±7.33 0.46±0.08 2047.71±2618.72 0.23±0.08 9.59±0.78 0.20±0.02 9.60±0.45 0.25±0.04 1.88±0.35 0.18±0.02
DeepLTL µacc ↑ ηv ↓ 26.00±5.95 0.21±0.04 12.95±3.44 0.37±0.09 43.87±12.44 0.32±0.10 44.64±10.34 0.34±0.13 7039.35±1605.49 0.17±0.05 9.37±1.32 0.06±0.01 8.40±1.26 0.06±0.02 0.77±0.16 0.03±0.03
GenZ-LTL µacc ↑ ηv ↓ 60.49±3.00 0.01±0.01 49.54±2.28 0.03±0.03 55.84±4.22 0.05±0.02 54.91±4.32 0.04±0.02 8042.12±1354.76 0.04±0.02 13.05±0.58 0.01±0.00 12.03±0.53 0.00±0.00 1.00±0.29 0.00±0.00
5.2. How do the methods scale with increasing specification complexity? To further evaluate the generalization, we include reach-only and reach-avoid specifications with increasing sequence length. For reach-only specifications, we additionally vary the number of disjunctions in the reach component, e.g., F (α1 ∨· · ·∨αn ), where the agent can choose among multiple target regions. For the avoid component in reach-avoid specifications, we similarly vary the number of disjunctions in the safety requirement, e.g., ¬(α1 ∨ · · · ∨ αn ) U αn+1 , which requires the agent to avoid multiple regions while progressing toward the target. We primarily use reach-only specifications to evaluate subgoal selection and efficiency, and reach-avoid specifications to assess the ability to satisfy safety constraints while completing the task. Although the reach component in reach-avoid specifications could also be varied, doing so would introduce many additional combinations; therefore, we fix it to a single target for simplicity. The specifications are listed in Table 6, and the results are shown in Figure 2. We report the success rate ηs , violation rate ηv , and the average number of steps µ to satisfy a specification, where µ is normalized by the sequence length to reflect the efficiency of satisfying each subgoal. The optimal normalized step values are computed using Dijkstras algorithm on the subgoal sequences, leveraging the discrete grid-map observation of Letter, and then averaging the resulting path lengths and normalizing by the sequence length.
Figure 2: Evaluation results of reach-only and reach-avoid specifications on Letter with varying sequence length and number of disjunctions of the target to reach/avoid, showing success rate ηs , violation rate ηv , and normalized average steps µ. The specifications are shown in Table 6. Each value is averaged over 5 seeds, with 100 trajectories per seed. For reach-only specifications, increasing the sequence length requires the agent to satisfy more subgoals in sequence, leading to a decrease in success rate ηs for several baselines. For example, 8
S PEC RLB ENCH
when the number of disjunctions is fixed to 0, the success rate consistently drops as the sequence length increases from 2 to 10 for LTL2Action, RAD-embeddings, and DeepLTL. Success rates also tend to decrease as the number of disjunctions increases, as seen for LTL2Action and DeepLTL, reflecting the OOD challenge where learned representations may not capture unseen formulas well. From the normalized average steps µ, efficiency often improves with more disjunctions, as agents have additional options for satisfying the specification. The step metric of GCRL-LTL remains largely unchanged. It uses a weighted graph search over the automaton, but the learned weights may not always capture the optimal satisfaction path. Moreover, while some methods exhibit only small gaps from the optimal normalized steps, others show larger deviations, indicating that longer temporal dependencies and increased disjunctive structure remain challenging and that achieving optimal efficiency is still a key factor in satisfying complex LTL specifications. For reach-avoid specifications, we observe a similar trend in which the success rate decreases as the sequence length increases or as the number of disjunctions grows. Beyond the OOD issue discussed above, safety constraints play a critical role in this setting. As the number of disjunctions increases, the specification imposes stronger safety requirements, such as avoiding a larger set of regions while reaching the target. Although GenZ-LTL treats safety constraints as hard constraints and achieves the lowest violation rate, its success rate still decreases as specifications become more complex. In contrast, the remaining methods do not explicitly model safety; while threshold-based heuristics are used to guide actions, the violation rate increases substantially under stricter safety requirements. This shows that balancing task objectives, which specify the behaviors to be achieved, and safety constraints, which restrict behaviors to be avoided, as expressed by LTL specifications, remains an important challenge. In terms of efficiency, all methods continue to exhibit gaps to the optimal policy, indicating room for improvement in efficiently satisfying unseen specifications. 5.3. How do the methods perform in the multi-agent setting? Table 4: Evaluation results in multi-agent settings. For finite-horizon tasks, we report success rate ηs , violation rate ηv , and average steps to satisfy the specification µ. For infinite-horizon tasks, we report violation rate ηv and average number of visits to accepting states µacc . ↑: higher is better; ↓: lower is better. ηs ↑
GCRL-LTL ηv ↓ 0.15±0.04 0.04±0.03 0.09±0.05
µ↓
ηs ↑
388.48±16.03 523.56±105.66 490.37±92.92
0.63±0.06 0.51±0.12 0.57±0.09
DeepLTL ηv ↓ 0.19±0.08 0.02±0.04 0.17±0.05
µ↓
ηs ↑
246.39±64.40 323.68±72.31 320.97±30.86
0.80±0.05 0.69±0.10 0.80±0.09
GenZ-LTL ηv ↓ 0.06±0.04 0.01±0.01 0.05±0.05
µ↓
Finite-horizon
Φindep Φcoop Φmix
0.60±0.07 0.44±0.11 0.63±0.07
263.27±56.32 325.42±65.37 324.23±25.43
µacc ↑
ηv ↓
µacc ↑
ηv ↓
µacc ↑
ηv ↓
Infinite-horizon
Φrsp Φrec Φper
1681.99±2051.82 8.31±4.16 4.64±1.55
0.26±0.08 0.27±0.09 0.25±0.05
6133.85±2124.63 4.82±2.36 9.05±3.90
0.17±0.05 0.48±0.21 0.36±0.08
6338.64±2482.87 14.31±10.63 29.31±7.71
0.08±0.03 0.07±0.03 0.06±0.03
In this setting, we consider three types of specifications: independent specifications Φindep , which encode separate objectives for individual agents, such as different agents visiting different regions; cooperative specifications Φcoop , which encode shared objectives among agents, such as requiring all agents to visit the same region simultaneously; and mixed specifications Φmix , which combine both independent and cooperative requirements, for example, when one agent follows its own task while all agents are later required to visit the same region. For infinite-horizon tasks, we evaluate mixed specifications that involve the responsive Φrsp , recurrence Φrec , and persistence Φper behaviors mentioned in Section 5.1. The evaluated specifications are listed in Table 5 and the results are 9
G UO I ŞIK A HMAD L I
shown in Table 4. Note that all the methods are designed for the single-agent setting; we evaluate the policies trained in the single-agent setting and deploy them directly in multi-agent environments, similar to shared policies for homogeneous agents (Terry et al., 2020), and collision between agents is not considered. The multi-agent system receives a system-level specification, and it requires the methods themselves to do the task decomposition and allocation for each agent. Among the compared methods, we evaluate GCRL-LTL, DeepLTL and GenZ-LTL, as they can be applied to the multi-agent setting without major modifications. The whole specification is first converted into a corresponding automaton, from which reach-avoid subgoal sequences are extracted. We select the shortest path in the automaton to execute. While this choice may not be optimal, finding the optimal path, i.e., the optimal task allocation among agents, requires further investigations. We then separate the true assignments on a per-agent basis according to agent indices, and a central coordinator monitors the satisfaction of the overall specification. For LTL2Action and RAD-Embeddings, generating actions for each agent based on embeddings of the full system-level specification is inefficient, and it is unclear how to decompose a system-level specification into agent-level specifications. It is also important to note that there exist specifications that may require communication between agents, which the current extended methods cannot satisfy. For example, some tasks require all agents to reach their targets at exactly the same time, or require one agent to delay moving to its target until another agent has completed part of its task. One agent needs to know the status of other agents to make decisions. Handling such specifications would require communication mechanisms or coordination-aware policy design. A recent work, ACC-MARL (Yalcinkaya et al., 2025), targets cooperative tasks by learning a single-agent policy conditioned on embeddings of each agents DFA. We will evaluate this method when its code becomes available. Further experimental results. We also evaluate how the baselines perform under increasing environment complexity, including different robot dynamics and control complexity, observation modalities with full or partial observability, and dynamic environments to assess their robustness to environment variations. Due to page limits, these results are provided in Appendix C.1.
6. Conclusion and Directions for Future Work In this work, we introduced SpecRLBench, a new benchmark aimed at advancing research on the generalization capabilities of specification-guided RL methods. While we have attempted to cover a broad range of factors related to generalization, several limitations remain. First, the set of specifications considered in this benchmark is still limited, and there may exist more diverse and challenging specifications under which current methods could fail. Second, the environments are relatively abstract, e.g., colored zones representing goals, and incorporating environments that are closer to real-world applications would provide a more realistic assessment of practical performance. In addition, many challenges in specification-guided RL remain underexplored, such as maintaining high satisfaction rates and strong efficiency on unseen specifications, achieving generalization of specifications in the multi-agent setting, enabling zero-shot or few-shot adaptation to unseen atomic propositions outside the training distribution, and improving sample efficiency during training. Addressing these challenges is critical for improving the generalization of specification-guided RL. We hope that the benchmark, analyses, and resources presented in this work provide a useful reference for evaluating future methods, encourage continued exploration in this direction, and ultimately contribute to the development of learning-based agents capable of general-purpose behaviors that can be deployed in real-world applications. 10
S PEC RLB ENCH
Acknowledgments This work was supported in part by the U.S. National Science Foundation under grant CCF-2340776.
References Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC), pages 6565–6570. IEEE, 2016. 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. Leo Ardon, Daniel Furelos-Blanco, and Alessandra Russo. Learning reward machines in cooperative multi-agent tasks. In International Conference on Autonomous Agents and Multiagent Systems, pages 43–59. Springer, 2023. Marco Bagatella, Andreas Krause, and Georg Martius. Directed exploration in reinforcement learning from linear temporal logic. Transactions on Machine Learning Research, 2025. ISSN 28358856. Alper Kamil Bozkurt, Yu Wang, Michael M Zavlanos, and Miroslav Pajic. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In 2020 IEEE International Conference on Robotics and Automation (ICRA), pages 10349–10355. IEEE, 2020. Ronen Brafman, Giuseppe De Giacomo, and Fabio Patrizi. Ltlf/ldlf non-markovian rewards. In Proceedings of the AAAI conference on artificial intelligence, volume 32, 2018. Mingyu Cai, Erfan Aasi, Calin Belta, and Cristian-Ioan Vasile. Overcoming exploration: Deep reinforcement learning for continuous control in cluttered environments from temporal logic specifications. IEEE Robotics and Automation Letters, 8(4):2158–2165, 2023. Maxime Chevalier-Boisvert, Dzmitry Bahdanau, Salem Lahlou, Lucas Willems, Chitwan Saharia, Thien Huu Nguyen, and Yoshua Bengio. Babyai: A platform to study the sample efficiency of grounded language learning. arXiv preprint arXiv:1810.08272, 2018. Maxime Chevalier-Boisvert, Bolun Dai, Mark Towers, Rodrigo Perez-Vicente, Lucas Willems, Salem Lahlou, Suman Pal, Pablo Samuel Castro, and Jordan Terry. Minigrid & miniworld: Modular & customizable reinforcement learning environments for goal-oriented tasks. In Advances in Neural Information Processing Systems 36, New Orleans, LA, USA, December 2023. Prashanth Choppara and Bommareddy Lokesh. Efficient task scheduling and load balancing in fog computing for crucial healthcare through deep reinforcement learning. IEEE Access, 2025. Giuseppe De Giacomo, Luca Iocchi, Marco Favorito, and Fabio Patrizi. Foundations for restraining bolts: Reinforcement learning with ltlf/ldlf restraining specifications. In Proceedings of the international conference on automated planning and scheduling, volume 29, pages 128–136, 2019. 11
G UO I ŞIK A HMAD L I
Joe Eappen and Suresh Jagannathan. Distspectrl: Distributing specifications in multi-agent reinforcement learning systems. In Joint European Conference on Machine Learning and Knowledge Discovery in Databases, pages 233–250. Springer, 2022. Zining Fan and He Zhu. Imitation learning with temporal logic constraints. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. Justin Fu, Aviral Kumar, Ofir Nachum, George Tucker, and Sergey Levine. D4rl: Datasets for deep data-driven reinforcement learning. arXiv preprint arXiv:2004.07219, 2020. Daniel Furelos-Blanco, Mark Law, Anders Jonsson, Krysia Broda, and Alessandra Russo. Hierarchies of reward machines. In International Conference on Machine Learning, pages 10494– 10541. PMLR, 2023. Quentin Gallouédec, Nicolas Cazin, Emmanuel Dellandréa, and Liming Chen. panda-gym: OpenSource Goal-Conditioned Environments for Robotic Learning. 4th Robot Learning Workshop: Self-Supervised and Lifelong Learning at NeurIPS, 2021. Leela Prasad Gorrepati and Ravi Teja Potla. A reinforcement learning framework for real-time personalized treatment planning in clinical environments. Engineering, Technology & Applied Science Research, 15(4):24698–24704, 2025. Zijian Guo, Weichao Zhou, and Wenchao Li. Temporal logic specification-conditioned decision transformer for offline safe reinforcement learning. In Forty-first International Conference on Machine Learning, 2024. Zijian Guo, İlker Işık, HM Ahmad, and Wenchao Li. One subgoal at a time: Zero-shot generalization to arbitrary linear temporal logic requirements in multi-task reinforcement learning. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Omega-regular objectives in model-free reinforcement learning. In International conference on tools and algorithms for the construction and analysis of systems, pages 395–412. Springer, 2019. Lewis Hammond, Alessandro Abate, Julian Gutierrez, and Michael Wooldridge. Multi-agent reinforcement learning with temporal logic specifications. arXiv preprint arXiv:2102.00582, 2021. Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Logically-constrained reinforcement learning. arXiv preprint arXiv:1801.08099, 2018. Zilin Huang, Zihao Sheng, Yansong Qu, Junwei You, and Sikai Chen. Vlm-rl: A unified vision language models and reinforcement learning framework for safe autonomous driving. Transportation Research Part C: Emerging Technologies, 180:105321, 2025. Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano, and Sheila A McIlraith. Reward machines: Exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research, 73:173–208, 2022. 12
S PEC RLB ENCH
Mathias Jackermeier and Alessandro Abate. DeepLTL: Learning to efficiently satisfy complex LTL specifications for multi-task RL. In The Thirteenth International Conference on Learning Representations, 2025. Kaiwen Jiang, Zhen Fu, Junde Guo, Wei Zhang, and Hua Chen. Learning whole-body loco-manipulation for omni-directional task space pose tracking with a wheeled-quadrupedalmanipulator. IEEE Robotics and Automation Letters, 2024. Kishor Jothimurugan, Rajeev Alur, and Osbert Bastani. A composable specification language for reinforcement learning tasks. Advances in Neural Information Processing Systems, 32, 2019. Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional reinforcement learning from logical specifications. Advances in Neural Information Processing Systems, 34:10026–10039, 2021. Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Specification-guided reinforcement learning. In George Pappas, Pradeep Ravikumar, and Sanjit A. Seshia, editors, Proceedings of the International Conference on Neuro-symbolic Systems, volume 288 of Proceedings of Machine Learning Research, pages 316–330. PMLR, 28–30 May 2025. Chaitanya Kharyal, Sai Krishna Gottipati, Tanmay Kumar Sinha, Srijita Das, and Matthew E Taylor. Glide-rl: grounded language instruction through demonstration in rl. arXiv preprint arXiv:2401.02991, 2024. Moo Jin Kim, Chelsea Finn, and Percy Liang. Fine-tuning vision-language-action models: Optimizing speed and success. arXiv preprint arXiv:2502.19645, 2025. Xuan Bach Le, Dominik Wagner, Leon Witzman, Alexander Rabinovich, and Luke Ong. Reinforcement learning with ltl and ω-regular objectives via optimality-preserving translation to average rewards. Advances in Neural Information Processing Systems, 37:117109–117132, 2024. Xiao Li, Cristian-Ioan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 3834–3839. IEEE, 2017. Bo Liu, Yifeng Zhu, Chongkai Gao, Yihao Feng, Qiang Liu, Yuke Zhu, and Peter Stone. Libero: Benchmarking knowledge transfer for lifelong robot learning. Advances in Neural Information Processing Systems, 36:44776–44791, 2023. Minghuan Liu, Menghui Zhu, and Weinan Zhang. Goal-conditioned reinforcement learning: Problems and solutions. arXiv preprint arXiv:2201.08299, 2022. Shuo Liu, Wenliang Liu, Wei Xiao, and Calin A Belta. Learning robust and correct controllers guided by feasibility-aware signal temporal logic via barriernet. arXiv preprint arXiv:2512.06973, 2025. Sikai Lu, Yingfeng Cai, Ze Liu, Yubo Lian, Long Chen, and Hai Wang. A preference-based multiagent federated reinforcement learning algorithm framework for trustworthy interactive urban autonomous driving. IEEE Transactions on Intelligent Transportation Systems, 2025. 13
G UO I ŞIK A HMAD L I
Jianlan Luo, Charles Xu, Jeffrey Wu, and Sergey Levine. Precise and dexterous robotic manipulation via human-in-the-loop reinforcement learning. Science Robotics, 10(105):eads5033, 2025. Anastasios Manganaris, Vittorio Giammarino, and Ahmed H Qureshi. Automaton constrained qlearning. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. Oier Mees, Lukas Hermann, Erick Rosete-Beas, and Wolfram Burgard. Calvin: A benchmark for language-conditioned policy learning for long-horizon robot manipulation tasks. IEEE Robotics and Automation Letters, 7(3):7327–7334, 2022. Jorge A Mendez, Marcel Hussing, Meghna Gummadi, and Eric Eaton. Composuite: A compositional reinforcement learning benchmark. arXiv preprint arXiv:2207.04136, 2022. Yue Meng and Chuchu Fan. Telograf: Temporal logic planning via graph-encoded flow matching. In Forty-second International Conference on Machine Learning, 2025. Yue Meng, Fei Chen, and Chuchu Fan. Tgpo: Temporal grounded policy optimization for signal temporal logic tasks. arXiv preprint arXiv:2510.00225, 2025. Jing-Cheng Pang, Xin-Yu Yang, Si-Hang Yang, Xiong-Hui Chen, and Yang Yu. Natural language instruction-following with task-related language development and translation. Advances in Neural Information Processing Systems, 36:9248–9278, 2023. Jing-Cheng Pang, Kaiyuan Li, Yidi Wang, Si-Hang Yang, Shengyi Jiang, and Yang Yu. Imaginebench: Evaluating reinforcement learning with large language model rollouts. arXiv preprint arXiv:2505.10010, 2025. Seohong Park, Kevin Frans, Benjamin Eysenbach, and Sergey Levine. Ogbench: Benchmarking offline goal-conditioned rl. arXiv preprint arXiv:2410.20092, 2024. Amir Pnueli. The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977), pages 46–57. ieee, 1977. Sam Powers, Eliot Xing, Eric Kolve, Roozbeh Mottaghi, and Abhinav Gupta. Cora: Benchmarks, baselines, and metrics as a platform for continual reinforcement learning agents. In Conference on Lifelong Learning Agents, pages 705–743. PMLR, 2022. Wenjie Qiu, Wensen Mao, and He Zhu. Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. Advances in Neural Information Processing Systems, 36:39147– 39175, 2023. Rajarshi Roy, Yash Pote, David Parker, and Marta Kwiatkowska. Learning probabilistic temporal logic specifications for stochastic systems. arXiv preprint arXiv:2505.12107, 2025. Ameesh Shah, Cameron Voloshin, Chenxi Yang, Abhinav Verma, Swarat Chaudhuri, and Sanjit A. Seshia. LTL-constrained policy optimization with cycle experience replay. Transactions on Machine Learning Research, 2025. ISSN 2835-8856. Daqian Shao and Marta Kwiatkowska. Sample efficient model-free reinforcement learning from ltl specifications with optimality guarantees. arXiv preprint arXiv:2305.01381, 2023. 14
S PEC RLB ENCH
Yash Shukla, Tanushree Burman, Abhishek Kulkarni, Robert Wright, Alvaro Velasquez, and Jivko Sinapov. Logical specifications-guided dynamic task sampling for reinforcement learning agents. In 34th International Conference on Automated Planning and Scheduling, 2024. Sophia Smith, Cyrus Neary, and Ufuk Topcu. Automatic decomposition of reward machines for decentralized multiagent reinforcement learning. In 2023 62nd IEEE Conference on Decision and Control (CDC), pages 5423–5430. IEEE, 2023. Geraud Nangue Tasse, Devon Jarvis, Steven James, and Benjamin Rosman. Skill machines: Temporal logic skill composition in reinforcement learning. In The Twelfth International Conference on Learning Representations, 2024. Justin K Terry, Nathaniel Grammel, Sanghyun Son, Benjamin Black, and Aakriti Agrawal. Revisiting parameter sharing in multi-agent deep reinforcement learning. arXiv preprint arXiv:2005.13625, 2020. Mark Towers, Ariel Kwiatkowski, Jordan Terry, John U Balis, Gianluca De Cola, Tristan Deleu, Manuel Goulão, Andreas Kallinteris, Markus Krimmel, Arjun KG, et al. Gymnasium: A standard interface for reinforcement learning environments. arXiv preprint arXiv:2407.17032, 2024. Pashootan Vaezipoor, Andrew C Li, Rodrigo A Toro Icarte, and Sheila A Mcilraith. Ltl2action: Generalizing ltl instructions for multi-task rl. In International Conference on Machine Learning, pages 10497–10508. PMLR, 2021. Nelson Vithayathil Varghese and Qusay H Mahmoud. A survey of multi-task deep reinforcement learning. Electronics, 9(9):1363, 2020. 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. Jiangwei Wang, Shuo Yang, Ziyan An, Songyang Han, Zhili Zhang, Rahul Mangharam, Meiyi Ma, and Fei Miao. Multi-agent reinforcement learning guided by signal temporal logic specifications. arXiv preprint arXiv:2306.06808, 2023a. Jiao Wang, Haoyi Sun, and Can Zhu. Vision-based autonomous driving: A hierarchical reinforcement learning approach. IEEE Transactions on Vehicular Technology, 72(9):11213–11226, 2023b. Siqi Wang, Xunyuan Yin, Shaoyuan Li, and Xiang Yin. Tractable reinforcement learning for signal temporal logic tasks with counterfactual experience replay. IEEE Control Systems Letters, 8: 616–621, 2024. Runpeng Xie, Quanwei Wang, Hao Hu, Zherui Zhou, Ni Mu, Xiyun Li, Yiqin Yang, Shuang Xu, Qianchuan Zhao, and Bo Xu. Dail: Beyond task ambiguity for language-conditioned reinforcement learning. arXiv preprint arXiv:2510.19562, 2025. Zikang Xiong, Daniel Lawson, Joe Eappen, Ahmed H Qureshi, and Suresh Jagannathan. Colearning planning and control policies constrained by differentiable logic specifications. In 2024 15
G UO I ŞIK A HMAD L I
IEEE International Conference on Robotics and Automation (ICRA), pages 14272–14278. IEEE, 2024. Beyazit Yalcinkaya, Niklas Lauffer, Marcell Vazquez-Chanlatte, and Sanjit Seshia. Compositional automata embeddings for goal-conditioned reinforcement learning. Advances in Neural Information Processing Systems, 37:72933–72963, 2024. Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah, Hanna Krasowski, and Sanjit A Seshia. Automata-conditioned cooperative multi-agent reinforcement learning. arXiv preprint arXiv:2511.02304, 2025. Tsung-Yen Yang, Michael Y Hu, Yinlam Chow, Peter J Ramadge, and Karthik Narasimhan. Safe reinforcement learning with natural language constraints. Advances in Neural Information Processing Systems, 34:13794–13808, 2021. Chao Yu, Yuanqing Wang, Zhen Guo, Hao Lin, Si Xu, Hongzhi Zang, Quanlu Zhang, Yongji Wu, Chunyang Zhu, Junhao Hu, et al. Rlinf: Flexible and efficient large-scale reinforcement learning via macro-to-micro flow transformation. arXiv preprint arXiv:2509.15965, 2025. Tianhe Yu, Deirdre Quillen, Zhanpeng He, Ryan Julian, Karol Hausman, Chelsea Finn, and Sergey Levine. Meta-world: A benchmark and evaluation for multi-task and meta reinforcement learning. In Conference on robot learning, pages 1094–1100. PMLR, 2020. Alexey Zakharov and Shimon Whiteson. Goalladder: Incremental goal discovery with visionlanguage models. arXiv preprint arXiv:2506.16396, 2025. Dongkun Zhang, Jiaming Liang, Ke Guo, Sha Lu, Qi Wang, Rong Xiong, Zhenwei Miao, and Yue Wang. Carplanner: Consistent auto-regressive trajectory planning for large-scale reinforcement learning in autonomous driving. In Proceedings of the Computer Vision and Pattern Recognition Conference, pages 17239–17248, 2025. Weichao Zhou and Wenchao Li. A hierarchical bayesian approach to inverse reinforcement learning with symbolic reward machines. In International Conference on Machine Learning, pages 27159–27178. PMLR, 2022.
16
S PEC RLB ENCH
Appendix A. Experimental Settings A.1. Environments The Letter environment is a grid world containing 12 letters corresponding to atomic propositions AP = {a, b, . . . , l}. Each letter appears twice and is randomly placed on the grid. The observation consists of either the entire grid or a partial egocentric view, controlled by a flag that enables or disables partial observability. The agent can move in four directions: up, down, left, and right. The grid is wrapped, meaning that if the agent moves out of bounds, it reappears on the opposite side. The maximum episode length is T = 75. The Zone environment contains colored regions corresponding to atomic propositions AP = {blue, green, magenta, yellow}, along with walls that act as boundaries. We implement three types of robots: Point, Car, and Ant. The action space differs across robots: the Point robot controls rotation and forward/backward movement; the Car uses two independently driven parallel wheels with a free-rolling rear wheel; and the Ant controls the torques applied to its leg joints. Users can also choose between different observation modalities. The observations can consist of LiDAR measurements of the colored regions along with egocentric state information from onboard sensors, or image-based observations captured by a forward-facing camera mounted on the robot. The maximum episode length is T = 1000. Users can also enable moving zones in the Zone environment to introduce dynamic elements for evaluation. For the Arm environment, we implement rangebearing observations that encode the direction and distance to the colored regions. Depending on the selected mode, the observation can include information from the grippers only, or from both the grippers and the robotic arm. The environments follow the standard Gym APIs, and example code for using them is provided below. The default reward is set to zero. The true propositions can be obtained from the info field, and rewards can be defined later based on the algorithm design using this ground-truth labeling. For multi-agent environments, the obs field is a dictionary that contains the observation for each agent. Users can construct additional Wrappers around the environments to define rewards or termination conditions based on the current true propositions and the specified reach or avoid subgoals. For all the baselines evaluated, they use the same reward function: r = 1 if the ”reach” subgoal is achieved and r = −1 if the ”avoid” subgoal is achieved. import gymnasium as gym import specbench # Instantiate an environment env = gym.make(’PointLTL0-v0’) # Set seed for reproducibility seed = 42 # SpecRLBench follows the standard Gym interface obs, info = env.reset(seed=seed) # Sample an action and execute it action = env.action_space.sample() obs, reward, terminal, timeout, info = env.step(action) # Retrieve the currently true propositions active_propositions = info["propositions"]
17
G UO I ŞIK A HMAD L I
A.2. LTL Specifications Table 5: LTL specifications used for evaluation. For specifications in Zone and Arm (grippersonly), b, g, m, and y denote blue, green, magenta, and yellow, respectively. For multiagents in Zone, the number in the atomic proposition denotes the index of the agent. Letter
Zone / Arm (grippers-only)
¬(a ∨ b) U (c ∧ (¬(d ∨ e) U f)) ΦIND
(F y) ∧ (¬(y ∨ g) U (b ∧ F m))
¬(c ∨ d) U ((¬e U l) ∧ (F g))
¬(g ∨ y) U ((¬g U m) ∧ (F b))
¬d U ((e ∨ k) ∧ (¬g U (h ∧ F i)))
¬g U ((b ∨ m) ∧ (¬g U (y ∧ F b)))
¬(e ∨ f) U (g ∧ F (h ∧ (¬i U j)))
¬(g ∨ m) U (b ∧ F (m ∧ (¬y U g)))
horizon
(F a) ∧ (¬(b ∨ c) U (d ∧ F (e ∧ (¬f U (g ∧ F h)))))
(F y) ∧ (¬(y ∨ g) U (b ∧ F (m ∧ (¬y U (g ∧ F b)))))
(¬a U b) ∧ (¬(c ∨ d) U (e ∧ F (f ∧ (¬g U (h ∧ F i)))))
(¬g U b) ∧ (¬(b ∨ y) U (m ∧ F (g ∧ (¬y U (b ∧ F m)))))
¬b U ((c ∨ d) ∧ (¬e U (f ∧ F (g ∧ (¬h U (i ∧ F l))))))
¬g U ((b ∨ m) ∧ (¬g U (y ∧ F (b ∧ (¬y U (m ∧ F b))))))
¬(c ∨ d) U (e ∧ (¬f U (g ∧ F (h ∧ (¬i U (j ∧ F k))))))
¬(y ∨ m) U (b ∧ (¬y U (g ∧ F (m ∧ (¬g U (y ∧ F b))))))
Φrsp
agent
(F b) ∧ (¬(c ∨ d) U (e ∧ F f))
Finite-
ΦOOD
Single-
¬(g ∨ y) U (m ∧ (¬g U b))
Infinitehorizon
Φrec
¬d U ((e ∨ f) ∧ (¬g U (h ∧ F (i ∧ (¬j U (k ∧ F l))))))
¬m U ((y ∨ g) ∧ (¬m U (b ∧ F (m ∧ (¬b U (g ∧ F y))))))
(G F a) ∧ G (a− > (F (b ∧ F c) ∧ (¬d U e))) ∧ G ¬(f ∨ g ∨ h ∨ i)
(G F b) ∧ G (b− > F g) ∧ G ¬(y ∨ m)
(G F f) ∧ G (f− > (F (e ∧ F d) ∧ (¬c U b))) ∧ G ¬(a ∨ g ∨ h ∨ i)
(G F g) ∧ G (g− > F y) ∧ G ¬(b ∨ m)
(G F i) ∧ G (i− > (F (h ∧ F g) ∧ (¬b U a))) ∧ G ¬(c ∨ d ∨ e ∨ f)
(G F m) ∧ G (m− > F y) ∧ G ¬(g ∨ b)
G F a ∧ G F b ∧ G F c ∧ G F d ∧ G F e ∧ G ¬(f ∨ g ∨ h ∨ i ∨ j ∨ k)
G F b ∧ G F g ∧ G ¬(y ∨ m)
G F f ∧ G F g ∧ G F h ∧ G F i ∧ G F j ∧ G ¬(a ∨ b ∨ c ∨ d ∨ e ∨ k)
G F g ∧ G F y ∧ G ¬(b ∨ m)
G F k ∧ G F a ∧ G F b ∧ G F c ∧ G F d ∧ G ¬(e ∨ f ∨ g ∨ h ∨ i ∨ j)
G F m ∧ G F y ∧ G ¬(g ∨ b) F G y ∧ G ¬(g ∨ b ∨ m)
Φper
F G g ∧ G ¬(y ∨ b ∨ m)
-
F G b ∧ G ¬(y ∨ g ∨ m) Arm (grippers-arm) ¬(ag ∨ ay ) U (gm ∧ (¬ag U gb )) (F gy ) ∧ (¬(ay ∨ ag ) U (gb ∧ F gm )) ΦIND
¬(ag ∨ ay ) U ((¬ag U gm ) ∧ (F gb )) ¬ag U ((gb ∨ gm ) ∧ (¬ag U (gy ∧ F gb )))
Finite-
¬(ay ∨ am ) U (gb ∧ F (gm ∧ (¬ay U gg )))
horizon
(F gy ) ∧ (¬(ay ∨ ag ) U (gb ∧ F (gm ∧ (¬ay U (gg ∧ F gb ))))) (¬ag U gb ) ∧ (¬(ab ∨ ay ) U (gm ∧ F (gg ∧ (¬ay U (gb ∧ F gm ))))) ΦOOD
¬ag U ((gb ∨ gm ) ∧ (¬ag U (gy ∧ F (gb ∧ (¬ay U (gm ∧ F gb )))))) ¬(ay ∨ am ) U (gb ∧ (¬ay U (gg ∧ F (gm ∧ (¬ag U (gy ∧ F gb )))))) ¬am U ((gy ∨ gg ) ∧ (¬am U (gb ∧ F (gm ∧ (¬ab U (gg ∧ F gy )))))) Zone (¬(m0 ∨ y0 ) U (b0 ∧ F g0 )) ∧ (¬(b1 ∨ g1 ) U (m1 ∧ F y1 ))
Φindep
(F b0 ) ∧ (¬b0 U (g0 ∧ F y0 )) ∧ (F g1 ) ∧ (¬g1 U (m1 ∧ F b1 )) (¬g0 U ((b0 ∨ m0 ) ∧ (¬g0 U y0 ))) ∧ (¬b1 U ((g1 ∨ y1 ) ∧ (¬b1 U m1 )))
Finitehorizon
¬(m0 ∨ m1 ) U ((b0 ∧ b1 ) ∧ ¬(y0 ∨ y1 ) U (g0 ∧ g1 )) Φcoop
F ((b0 ∧ b1 ) ∧ (¬(m0 ∨ m1 ) U ((y0 ∧ y1 ) ∧ F (g0 ∧ g1 )))) F ((b0 ∧ b1 ) ∧ F ((y0 ∧ y1 ) ∧ ¬(m0 ∨ m1 ) U (g0 ∧ g1 ))) (¬m0 U y0 ) ∧ (¬b1 U m1 ) ∧ F ((b0 ∧ g1 ) ∧ F (g0 ∧ m1 ))
Φmix
(¬y0 U (b0 ∧ F g0 )) ∧ (¬b1 U g1 ) ∧ (¬(y0 ∨ y1 ) U (b0 ∧ b1 ))
Multi-
¬m0 U (b0 ∧ F (m1 ∧ F (b0 ∧ b1 ))) ∧ ¬y1 U (g1 ∧ F (y0 ∧ F (b0 ∧ b1 )))
agent
(G F b0 ) ∧ (G F g1 ) ∧ G (b0 − > F y1 ) ∧ G (g1 − > F m0 ) ∧ G ¬(y0 ∨ b1 ) Φrsp
(G F g0 ) ∧ (G F m1 ) ∧ G (g0 − > F y1 ) ∧ G (m1 − > F b0 ) ∧ G ¬(b1 ∨ m0 ) (G F m0 ) ∧ (G F y1 ) ∧ G (m0 − > F g1 ) ∧ G (y1 − > g0 ) ∧ G ¬(m1 ∨ b0 )
Infinitehorizon
G F (b0 ∧ g1 ) ∧ G F (g0 ∧ y1 ) ∧ G ¬(y0 ∨ m1 ) Φrec
G F (g0 ∧ y1 ) ∧ G F (y0 ∧ b1 ) ∧ G ¬(b0 ∨ m1 ) G F (m0 ∧ b1 ) ∧ G F (b0 ∧ y1 ) ∧ G ¬(g0 ∨ g1 ) F G (y0 ∧ m1 ) ∧ G ¬(g0 ∨ b0 ∨ y1 ∨ b1 )
Φper
F G (g0 ∧ b1 ) ∧ G ¬(y0 ∨ b0 ∨ m1 ∨ y1 ) F G (b0 ∧ y1 ) ∧ G ¬(y0 ∨ g0 ∨ m1 ∨ b1 )
We evaluate the generalization ability of the baselines on a range of specifications, including both finite-horizon and infinite-horizon tasks, as summarized in Table 5 and Table 6. In the single-agent 18
S PEC RLB ENCH
setting, we evaluate performance on in-distribution ΦIND and out-of-distribution ΦOOD specifications, as well as infinite-horizon tasks with response Φrsp , recurrence Φrec , and persistence Φper behaviors. We further study generalization in the Letter environment by varying specification complexity through different sequence lengths and numbers of disjunctions. In the multi-agent setting, for finite-horizon tasks, we evaluate specifications that encode independent Φindep , cooperative Φcoop , and mixed Φmix behaviors that combine both independent and cooperative requirements. For infinite-horizon tasks, we focus on mixed specifications that incorporate response, recurrence, and persistence behaviors. Table 6: Reach-only and reach-avoid specification with varying complexity evaluated in Letter. nseq denotes the sequence length and ndisj denotes the number of disjunctions. We provide some example specifications with nseq = [2, 4] and ndisj = [0, 1]. nseq = 2 Reach-only nseq = 4
nseq = 2 Reach-avoid nseq = 4
ndisj = 0 F (a ∧ F l) F (d ∧ F g) F (f ∧ F k) F (a ∧ F (b ∧ F (c ∧ F d))) F (e ∧ F (f ∧ F (g ∧ F h))) F (i ∧ F (j ∧ F (k ∧ F l))) ¬a U (b ∧ (¬c U d)) ¬e U (f ∧ (¬g U h)) ¬i U (j ∧ (¬k U l)) ¬a U (b ∧ (¬c U (d ∧ (¬e U (f ∧ (¬g U h)))))) ¬e U (f ∧ (¬g U (h ∧ (¬i U (j ∧ (¬k U l)))))) ¬i U (j ∧ (¬k U (l ∧ (¬a U (b ∧ (¬c U d))))))
ndisj = 1 F ((a ∨ b) ∧ F (k ∨ l)) F ((c ∨ d) ∧ F (g ∨ h)) F ((e ∨ f) ∧ F (i ∨ j)) F ((a ∨ b) ∧ F ((c ∨ d) ∧ F ((e ∨ f) ∧ F (g ∨ h)))) F ((e ∨ f) ∧ F ((g ∨ h) ∧ F ((i ∨ j) ∧ F (k ∨ l)))) F ((i ∨ j) ∧ F ((k ∨ l) ∧ F ((a ∨ b) ∧ F (c ∨ d)))) ¬(a ∨ b) U (c ∧ (¬(d ∨ e) U f)) ¬(e ∨ f) U (g ∧ (¬(h ∨ i) U j)) ¬(i ∨ j) U (k ∧ (¬(l ∨ a) U b)) ¬(a ∨ b) U (c ∧ (¬(d ∨ e) U (f ∧ (¬(g ∨ h) U (i ∧ (¬(j ∨ k) U l)))))) ¬(e ∨ f) U (g ∧ (¬(h ∨ i) U (j ∧ (¬(k ∨ l) U (a ∧ (¬(b ∨ c) U d)))))) ¬(i ∨ j) U (k ∧ (¬(l ∨ a) U (b ∧ (¬(c ∨ d) U (e ∧ (¬(f ∨ g) U h))))))
Appendix B. Baselines We use the official codebases of the baselines: LTL2Action1 , GCRL-LTL2 , RAD-embeddings3 , DeepLTL4 , and GenZ-LTL5 . We integrate our environments into the original training and evaluation pipelines of the compared methods. For fair comparison, all methods share the same policy and critic architectures. The actor network is a fully connected network with three hidden layers of sizes [64, 64, 64], and the critic network has two hidden layers of sizes [64, 64]. We use the Adam optimizer with a learning rate of 3 × 10−4 and train all methods for 15M environment interactions. The discount factor is set to γ = 0.94 for Letter, γ = 0.998 for Zone, and γ = 0.99 for Arm. For observation encoders, we use CNN models for grid-map observations in Letter and imagebased observations in Zone. The CNN architecture for Letter uses channels=[16, 32, 64] with kernel size (2, 2). For Zone, we use channels=[16, 32, 64, 64, 32] with kernel size (5, 5), stride = 2, and padding = 1. For LiDAR observations in Zone, we use a fully connected encoder with two hidden layers of sizes [128, 64]. For range-bearing observations in Arm, we use fully connected encoders with two hidden layers of sizes [128, 64] for the grippers-only mode and [256, 64] for the grippers-arm mode. The embeddings of the environment observation and the embeddings related to specifications are concatenated and used as the input to both the actor and critic networks. 1. https://github.com/LTL2Action/LTL2Action 2. https://github.com/RU-Automated-Reasoning-Group/GCRL-LTL 3. https://github.com/RAD-Embeddings/neurips24 4. https://github.com/mathiasj33/deep-ltl 5. https://github.com/BU-DEPEND-Lab/GenZ-LTL
19
G UO I ŞIK A HMAD L I
Appendix C. Further Experimental Results C.1. How do the methods perform under increasing environment complexity?
Figure 3: Evaluation results of in-distribution ΦIND specifications under different robot dynamics and observation modalities. We report the success rate, violation rate, others rate, and normalized average steps to satisfy the specifications. P, C, and A denote the Point, Car, and Ant robots, while L and I denote LiDAR and image-based observations. Each value is averaged over 5 seeds, with 100 trajectories per seed.
Last but not least, we evaluate the methods under varying levels of environment complexity, including different robot dynamics and control complexity, observation modalities with full or partial observability, and dynamic environments, to assess their scalability. For robot dynamics and observation modalities, we use the Zone environment with different robot such as Point, Car, and Ant with LiDAR or image-based observations. Image observations naturally introduce partial observability, and we also evaluate this aspect in the Letter environment by limiting the range of the grid-map observation. To vary control complexity, in addition to the differences in robot dynamics, we also include the Arm environment under two configurations: one that considers only the grippers, and another that considers both the grippers and the robotic arm. The results are shown in Figure 3 and Figure 4. For dynamic environments, we include the Zone environment with moving zones. We can observe several trends. First, as the robot dynamics become more complex (from Point to Car to Ant) or the control space becomes more constrained (from grippers-only to grippersarm), the success rate decreases while the violation rate increases, reflecting the growing difficulty of learning effective control policies. Second, as the observation space becomes higherdimensional (from LiDAR to images) or partially observable (e.g., grid-map observations with a limited sensing range), the success rate further drops and the violation rate increases, as learning the mapping from observations to actions becomes more challenging. Third, when the environment becomes dynamic, the task becomes harder due to additional uncertainty, again leading to lower success rates and higher violation rates. While existing methods can perform well in relatively simple and fully observable settings, their scalability is limited by increased dynamical complexity, constrained control settings, partial observability, and environmental non-stationarity. 20
S PEC RLB ENCH
Figure 4: Evaluation results on in-distribution specifications ΦIND under different settings: partial observability with limited sensing range (left), dynamic environments with moving zones (middle), and different manipulation modes considering only the grippers or both the grippers and the robotic arm (right). We report the success rate ηs , violation rate ηv , and others rate ηo . Each value is averaged over 5 random seeds, with 100 trajectories per seed.
Appendix D. Visualization An illustration of the trajectories of the baselines in the Zone environment is shown in Figure 5. The specification is ¬(g ∨ y) U (m ∧ (¬g U b)), which is listed in Table 5. This specification requires the agent to first reach the magenta region while avoiding green and yellow regions, and then proceed to the blue region while continuing to avoid green. From the trajectories, we observe that the baselines show different behaviors: some agents violate safety constraints and fail to satisfy the specification, while others follow safe paths but take inefficient paths toward the targets, which indicates that there remains room for improvement in both compliance and efficiency.
21
G UO I ŞIK A HMAD L I
Figure 5: Visualization of baseline trajectories for the specification ¬(g ∨ y) U (m ∧ (¬g U b)). The agent is required to first reach the magenta region while avoiding green and yellow regions, and then reach the blue region while continuing to avoid green regions.
22