Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions

AI summary

Overview

• Research area: Reinforcement learning (formal-specification-driven RL), multi-task learning, linear temporal logic (LTL), automata theory.
• Technical level: Advanced. It assumes familiarity with LTL, Büchi/limit-deterministic automata, MDPs, and deep RL, though the core idea can be grasped at a high level.
• Scope: The paper introduces task embeddings derived from semantically labelled LTL-to-automata translations, and shows they enable a single generalist RL policy to zero-shot execute arbitrary LTL instructions, including specifications where prior methods time out or fail.

What This Paper Is About

LTL is a standard language in formal methods for describing temporally extended objectives (for example, "eventually collect a parcel and then keep that zone clear"), and it is increasingly used to specify RL tasks. Training one policy per formula is impractical because LTL tasks are non-Markovian — the agent needs memory of what it has already seen — and because any small change in the task, such as which items a warehouse robot must collect, forces retraining. This paper asks how to embed any task's automaton state into a finite, semantically meaningful vector so that a single universal policy can be conditioned on it and generalise to unseen tasks, for full LTL rather than only fragments.

Key Contributions

1. Semantic-labelling-based task embeddings. The authors build on the semantic LTL-to-automata translation of Esparza et al. (implemented in Owl), whose LDBA states are labelled not by numeric indices but by LTL formulae: a main formula (M, the remaining language, derived by formula progression) and, when recurrence is present, a breakpoint formula (B) whose progression to tt emits a Büchi acceptance signal and then resets.
2. A concrete, lightweight feature set for these labels. Two feature families are proposed: a trueness feature measuring how much each MDP label moves a formula toward or away from satisfaction, and a propositional attention feature relating pairs of propositions via obligation sets, which counteracts the myopia of trueness alone. Simple complexity measures (such as syntax-tree height) are added so the agent can prefer less complex states when resolving ε-transitions.
3. On-the-fly automaton construction. Because a state's semantic labelling is available without computing the whole automaton, required states are built on demand as MDP labels are observed (initially only the initial state q₀ exists), avoiding the requirement to enumerate the entire automaton upfront.
4. A multi-headed policy architecture for the hybrid action space. The policy mixes continuous or discrete MDP actions with a task-dependent, a-priori-unknown number of ε-actions, so it uses a shared representation MLP over the states in the ε-closure, a linear scoring head λ for ε-actions, and an environment actor head π_env for MDP actions, softmax-normalised over the union. It is trained end-to-end with goal-conditioned RL using PPO and a curriculum of increasingly hard formulae.
5. An empirical study across multiple domains showing state-of-the-art performance and scaling to specifications where existing holistic and decomposition-based methods fail.

Main Findings

• Trueness captures immediate progress. For the running example F r ∧ FG y, the paper reports tr(F r ∧ FG y) = 0.25 and tr(FG y) = 0.5, indicating that progressing to FG y is desirable. In the state whose main formula is G y, the feature value f_tr(G y, {}) = −0.5 signals that terminally not observing y hurts progress.
• Propositional attention supplies non-myopic information. For φ = F r ∧ FG y, f_att⁺(φ, r, r) = 0.0 (after seeing r once, r is irrelevant) while f_att⁺(φ, r, y) = 1.0 (after seeing r, letters containing y are highly promising). This information is already present in the embedding of q₀, so the agent can anticipate its later obligation of FG y while first pursuing F r.
• Trueness is explicitly limited. The authors note it cannot capture deep temporal relations: F r ∧ G ¬r has trueness 0.25 despite being unsatisfiable. It is presented as a propositional approximation of task progress, particularly effective for formulae occurring in practice.
• RQ1 — myopia is overcome. In the conveyor environment with the tasks F(parcel ∧ F hammer) or F(parcel ∧ F wrench), decomposition-based approaches that only condition on the subtask F parcel can achieve at most 50% success, and the paper reports that without the propositional attention feature the approach also only reaches 50%, whereas the full SemLTL converges to the optimal policy.
• RQ2/RQ3 — LetterWorld results. For the finite-horizon Letter task (|Q| = 9, |δ| = 23), LTL2Action scores 0.67 ± 0.12 while DeepLTL and SemLTL both score 0.98 ± 0.01. For Local-Safety [3,3] (|Q| = 233, |δ| = 1,372), LTL2Action scores 0.57 ± 0.07, DeepLTL times out (TO), and SemLTL scores 0.99 ± 0.00. For Global-Safety [4,6] (|Q| = 1,072, |δ| = 6,414), LTL2Action scores 0.12 ± 0.03, DeepLTL times out, and SemLTL scores 0.91 ± 0.01. For Finite-Reactive [8,2] (|Q| = 300, |δ| = 2,115), LTL2Action scores 0.74 ± 0.04, DeepLTL times out, and SemLTL scores 1.00 ± 0.00.
• ZoneEnv results. The paper evaluates a harder ZoneEnv variant with 8 colours (instead of 4) and an RGB-lidar observation space. For the Small task (|Q| = 9, |δ| = 23), the reported success rates are 0.52 ± 0.07 for LTL2Action, 0.93 ± 0.02 for DeepLTL, and 0.92 ± 0.02 for SemLTL. The remaining ZoneEnv rows are cut off in the available content and are therefore not reported here.
• On-the-fly scale is reflected in the table. The reported μ_states column gives values of 4.12 ± 0.02 (Letter, Finite-horizon), 5.38 ± 0.00 (Local-Safety), 6.77 ± 0.04 (Global-Safety), 2.80 ± 0.10 (Finite-Reactive), and 3.40 ± 0.01 (Zones, Small) — far smaller than the corresponding full automaton sizes. The truncated content does not define this column explicitly.
• DeepLTL's cost is the bottleneck it claims. The paper argues DeepLTL must construct the entire LDBA upfront and exhaustively enumerate accepting paths to find an optimal reach-avoid sequence, which is why it times out on the more complex task families above.

Methodology in Plain English

The approach keeps the standard automata-theoretic recipe — convert the current LTL task into a limit-deterministic Büchi automaton, track the current automaton state as memory, and reward visits to accepting states — but changes what the policy sees when it looks at that automaton state. Instead of a meaningless state index or an expensive search over reach-avoid sequences, each state carries a semantic label: the remaining formula (main formula), updated by formula progression each time a new MDP label is observed, plus a breakpoint formula for recurring obligations that resets and emits a Büchi signal when it is fulfilled.

Those formulae are then turned into a fixed-size numeric vector. One component probes the effect of each possible letter by comparing trueness before and after progression, so the agent can see which letters make progress and which violate the task. Another component looks one step further: it progresses the formula with one proposition, computes the obligation sets of the result, and counts how often another proposition appears in them — capturing "if I do this, that becomes the thing that matters." Small complexity measures of the formulae are added so that when the automaton offers several ε-transitions, the agent can prefer simpler states.

Because semantic labels can be produced for a state without building its neighbours, the automaton is grown lazily: only states reachable through actually observed MDP labels are created. The policy itself is a multi-headed network that encodes the MDP state (MLP or CNN depending on the domain), projects each embedding in the ε-closure, scores ε-actions against taking an environment action, and outputs an environment action distribution. Training samples a random formula at the start of each episode, rewards accepting-state visits with 1, and uses a curriculum of progressively harder formulae, with PPO as the underlying algorithm throughout.

Why This Matters

• For research: It connects a mature line of work in formal methods — semantic LTL-to-automata translations developed for parity game solving and reactive synthesis — to deep RL, showing that the annotation those translations provide is exactly the structured signal that multi-task RL needs. It also offers a route past two persistent limitations of prior work: formula progression methods that only support the co-safety (guarantee) fragment, and reach-avoid-sequence methods whose enumeration cost scales with the whole automaton.
• Practical deployment: Policies that execute unseen LTL instructions without retraining suit settings where task specifications change frequently or retraining is infeasible.
• Warehouse and logistics robotics: The paper's running example is a warehouse robot; the conveyor experiment literally pits "collect a parcel then use a hammer" against "collect a parcel then use a wrench," where knowing the second half of the instruction determines which room to enter.
• Mobile robot navigation: The ZoneEnv benchmark is a robotic navigation domain with continuous actions and coloured zones, tested here with 8 colours and an RGB-lidar observation space.
• Safety-critical and verification-adjacent autonomy: Because LTL is the language used to specify system properties in formal verification, agents that act directly on LTL specifications make it easier to carry a specification from design and verification through to deployment.
• Industry relevance: Generalist, specification-conditioned policies reduce the per-task engineering cost of applied RL and are relevant to any organisation that already writes temporal specifications for its systems, from robotics and autonomous driving to process control.

Future Directions

• Richer semantic features. The authors' own example, F r ∧ G ¬r, has trueness 0.25 despite being unsatisfiable, showing the propositional approximation misses some temporal relations. Better features could close that gap.
• Scaling further. SemLTL solved task families with |Q| up to 1,072 and |δ| up to 6,414 where DeepLTL timed out; the natural question is how far the on-the-fly construction and embedding can be pushed on even larger specifications, and whether the curriculum alone is enough to get there.
• Combining with learned representation methods. The paper notes that Giuri et al. (2025) used GNNs to improve DeepLTL's representation learning but inherited its drawbacks; pairing such representation learning with semantic labels is an obvious unexplored combination.
• Beyond LDBA-based acceptance. The rationale section explains that Büchi acceptance converts naturally to a reward signal, unlike Rabin, and is impractical for parity. Whether semantic labelling can be exploited for other automaton types and acceptance conditions remains open.
• Algorithm and architecture independence. The method is stated to be independent of the underlying RL algorithm (PPO was used throughout), leaving room to test other algorithms and policy architectures.

Target Audience

Researchers and graduate students working at the intersection of reinforcement learning and formal methods, especially those interested in LTL- and automaton-based task specification, multi-task and goal-conditioned RL, and zero-shot generalisation to new objectives. It also suits roboticists and applied RL engineers who need generalist agents driven by formal specifications, and formal-methods researchers curious about downstream uses of semantic LTL-to-automata translations beyond synthesis and verification.

Authors’ abstract

We study multi-task reinforcement learning (RL), a setting in which an agent learns a single, universal policy capable of generalising to arbitrary, possibly unseen tasks. We consider tasks specified as linear temporal logic (LTL) formulae, which are commonly used in formal methods to specify properties of systems, and have recently been successfully adopted in RL. In this setting, we present a novel task embedding technique leveraging a new generation of semantic LTL-to-automata translations, originally developed for temporal synthesis. The resulting semantically labelled automata contain rich, structured information in each state that allow us to (i) compute the automaton efficiently on-the-fly, (ii) extract expressive task embeddings used to condition the policy, and (iii) naturally support full LTL. Experimental results in a variety of domains demonstrate that our approach achieves state-of-the-art performance and is able to scale to complex specifications where existing methods fail.