Accelerated Learning with Linear Temporal Logic using Differentiable Simulation

TL;DR

This paper presents a novel end-to-end framework integrating linear temporal logic with differentiable simulators, enabling efficient gradient-based reinforcement learning from formal specifications in continuous control tasks.

Contribution

It introduces a differentiable reward mechanism for LTL, connecting formal methods with deep RL, and provides theoretical guarantees and empirical improvements in training speed and performance.

Findings

Accelerates training in complex control tasks

Achieves up to twice the returns of baseline methods

Maintains soundness of formal specifications in RL

Abstract

Ensuring that reinforcement learning (RL) controllers satisfy safety and reliability constraints in real-world settings remains challenging: state-avoidance and constrained Markov decision processes often fail to capture trajectory-level requirements or induce overly conservative behavior. Formal specification languages such as linear temporal logic (LTL) offer correct-by-construction objectives, yet their rewards are typically sparse, and heuristic shaping can undermine correctness. We introduce, to our knowledge, the first end-to-end framework that integrates LTL with differentiable simulators, enabling efficient gradient-based learning directly from formal specifications. Our method relaxes discrete automaton transitions via soft labeling of states, yielding differentiable rewards and state representations that mitigate the sparsity issue intrinsic to LTL while preserving objective soundness. We provide theoretical guarantees connecting B\"uchi acceptance to both discrete and differentiable LTL returns and derive a tunable bound on their discrepancy in deterministic and stochastic settings. Empirically, across complex, nonlinear, contact-rich continuous-control tasks, our approach substantially accelerates training and achieves up to twice the returns of discrete baselines. We further demonstrate compatibility with reward machines, thereby covering co-safe LTL and LTL$_\text{f}$ without modification. By rendering automaton-based rewards differentiable, our work bridges formal methods and deep RL, enabling safe, specification-driven learning in continuous domains.