[Github repo] | [Manually designed STL specs] | [LLM-generated STL specs Github repo] | [LLM-generated STL specs]
Reinforcement learning (RL) for quadruped locomotion commonly depends on fixed, hand-crafted, and Markovian reward functions that may limit interpretability of learned policies and may lack explicit control over gait behaviors. We introduce a framework where distinct gaits are specified using parameterized constraints expressed in Signal Temporal Logic (STL). These include safety bounds, gait synchronization constraints, command tracking, and actuation bounds. From these specifications, we develop a reward shaping mechanism that provides learning agents a dense, continuous reward landscape that encodes desired behavior. We define parametric STL templates for three speed regimes (walking-trot, trot, bound), calibrate their parameters from reference rollouts, and compute rewards from using smooth approximations of STL robustness over the rollouts. The generated rewards can be used to provide shaped gradients compatible with Proximal Policy Optimization (PPO). We instantiate the approach on Google’s Barkour quadruped robot in MuJoCo XLA (MJX). We use parallelization within the simulator to improve training speeds and use domain randomization to robustify learned policies. Compared with hand-crafted rewards, an expert-switching oracle, and Text2Reward, Human-STL maintains high command-tracking success across the evaluated speed range while exhibiting substantially higher consistency with the intended speed-dependent gait structures. Videos can be found on our project website: https://stl-locomotion.github.io/.
Our framework aims interpretable specification-based, gait-aware reward design for quadruped locomotion tasks. The reward component corresponds directly to human-readable requirements.
We compile trajectory datasets from specialized models corresponding to low-speed, mid-speed, and high-speed regimes. Extracted features include:
We define fixed PSTL templates for three locomotion modes, fitting parameters using empirical quantiles from the expert datasets.
The final reward is derived from the quantitative robustness of the active specifications within the current temporal window. The active locomotion mode g(t) ∈ {W, T, B} is selected dynamically based on the commanded forward velocity vxcmd. The scalar reward aggregates safety, tracking, and gait structure robustness alongside a torque-effort penalty.
The locomotion controller is designed for Google’s Barkour vb quadruped robot, modeled and trained using PPO within MuJoCo XLA (MJX). We utilize domain randomization over friction and actuator parameters to robustify the learned policies.
Benchmark comparison over 20 rollouts per commanded velocity. CoT: lower is better; Survival and Success: higher is better.
| vx (m/s) | Gait | Human-STL | GPT-STL | Expert Oracle | Heuristic | Text2Reward | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| CoT ↓ | Surv. ↑ | Succ. ↑ | CoT ↓ | Surv. ↑ | Succ. ↑ | CoT ↓ | Surv. ↑ | Succ. ↑ | CoT ↓ | Surv. ↑ | Succ. ↑ | CoT ↓ | Surv. ↑ | Succ. ↑ | ||
| 0.3 | Walk | 2.1 | 100% | 100% | 2.0 | 100% | 100% | 0.9 | 100% | 100% | 1.1 | 100% | 100% | 1.1 | 100% | 100% |
| 0.5 | Walk | 1.5 | 100% | 100% | 1.6 | 100% | 100% | 0.9 | 100% | 100% | 1.0 | 100% | 100% | 0.8 | 100% | 100% |
| 0.7 | Walk | 1.3 | 100% | 100% | 1.4 | 100% | 100% | 1.0 | 100% | 100% | 1.0 | 100% | 100% | 0.9 | 100% | 100% |
| 1.0 | Trot | 1.2 | 100% | 100% | 1.3 | 100% | 100% | 1.1 | 100% | 100% | 1.1 | 100% | 100% | 1.1 | 100% | 100% |
| 1.3 | Trot | 1.1 | 100% | 100% | 1.2 | 100% | 100% | 1.3 | 100% | 100% | 1.2 | 100% | 100% | 1.1 | 100% | 100% |
| 1.6 | Trot | 1.0 | 100% | 100% | 1.3 | 100% | 100% | 1.3 | 100% | 100% | 1.4 | 100% | 100% | 1.0 | 100% | 100% |
| 1.9 | Bound | 1.1 | 100% | 100% | 1.3 | 100% | 0% | 1.3 | 95% | 0% | 1.4 | 100% | 100% | - | 0% | 0% |
| 2.0 | Bound | 1.1 | 100% | 100% | 1.3 | 100% | 0% | 1.4 | 95% | 0% | 1.4 | 0% | 100% | - | 0% | 0% |
| 2.1 | Bound | 1.2 | 100% | 70% | 1.3 | 100% | 0% | 1.4 | 100% | 0% | 1.4 | 100% | 0% | - | 0% | 0% |
Transition Success Rates
Transition success rates under different temporal windows H. Each transition changes the commanded forward velocity from v1 to v2.
| Transition | v1 (m/s) | v2 (m/s) | H=10 | H=20 | H=30 |
|---|---|---|---|---|---|
| Walk → Trot | 0.3 | 0.8 | 100% | 100% | 95% |
| Walk → Trot | 0.3 | 1.2 | 100% | 100% | 100% |
| Walk → Trot | 0.6 | 0.8 | 100% | 100% | 100% |
| Walk → Trot | 0.6 | 1.2 | 100% | 100% | 100% |
| Trot → Walk | 0.8 | 0.3 | 100% | 100% | 100% |
| Trot → Walk | 1.2 | 0.3 | 100% | 100% | 100% |
| Trot → Walk | 0.8 | 0.6 | 100% | 100% | 100% |
| Trot → Walk | 1.2 | 0.6 | 100% | 100% | 100% |
| Trot → Bound | 1.0 | 1.75 | 90% | 15% | 25% |
| Trot → Bound | 1.0 | 1.9 | 70% | 30% | 35% |
| Trot → Bound | 1.5 | 1.75 | 50% | 15% | 0% |
| Trot → Bound | 1.5 | 1.9 | 0% | 55% | 5% |
| Bound → Trot | 1.75 | 1.0 | 10% | 100% | 50% |
| Bound → Trot | 1.9 | 1.0 | 10% | 85% | 55% |
| Bound → Trot | 1.75 | 1.5 | 0% | 85% | 20% |
| Bound → Trot | 1.9 | 1.5 | 0% | 85% | 40% |
Temporal Window Ablation
Ablation over temporal window size H. Metrics are averaged across all evaluated commanded forward velocities.
| Method | H | CoT | Survival ↑ | Success ↑ |
|---|---|---|---|---|
| GPT-STL | 1 | 1.4 | 100% | 55.6% |
| GPT-STL | 5 | 1.6 | 100% | 55.6% |
| GPT-STL | 10 | 1.4 | 100% | 55.6% |
| GPT-STL | 20 | 1.4 | 100% | 66.7% |
| GPT-STL | 30 | 1.4 | 99.4% | 66.7% |
| Human-STL | 1 | 1.3 | 100% | 100% |
| Human-STL | 5 | 1.1 | 99.4% | 99.4% |
| Human-STL | 10 | 1.4 | 100% | 100% |
| Human-STL | 20 | 1.3 | 99.4% | 99.4% |
| Human-STL | 30 | 1.3 | 100% | 95.6% |
Walk-Trot Gait (vx = 0.4 m/s)
Trot Gait (vx = 1.2 m/s)
Bound Gait (vx = 1.9 m/s)
Below are evaluations of the 6 baselines generated using Large Language Models (LLMs) to automatically synthesize Temporal Logic Specifications. For each baseline, we showcase policies executed at low (0.4 m/s), medium (1.2 m/s), and the highest achieved velocity.
| vx = 0.4 m/s | vx = 1.2 m/s | vx = 1.9 m/s |
| vx = 0.4 m/s | vx = 1.2 m/s | vx = 1.6 m/s |
| vx = 0.4 m/s | vx = 1.2 m/s | vx = 1.3 m/s |
| vx = 0.4 m/s | vx = 1.2 m/s | vx = 1.9 m/s |
| vx = 0.4 m/s | vx = 1.2 m/s | vx = 1.9 m/s |
| vx = 0.4 m/s | vx = 1.2 m/s | vx = 1.6 m/s |
@article{atasever2026learning,
title={Learning Gait-Aware Quadruped Locomotion with Temporal Logic Specifications},
author={Atasever, Merve and Bakirci, Cagan and Corona, Alfredo Reina and Azbijari, Keyan and Deshmukh, Jyotirmoy V},
journal={arXiv preprint arXiv:2607.00442},
year={2026}
}
@article{atasever2026llm,
title={From LLM-Generated Specifications to Learned Quadruped Locomotion},
author={Atasever, Merve and Azbijari, Keyan and Bakirci, Cagan and Corona, Alfredo Reina and Izdas, Tolga and Yang, Richard and Biyik, Erdem and Deshmukh, Jyotirmoy V},
journal={arXiv preprint arXiv:2609.07111},
year={2026}
}