Overview
This research project explores how formal temporal-logic specifications can guide reinforcement-learning-based quadruped locomotion. Instead of relying only on fixed hand-crafted rewards, the approach encodes gait behavior, safety limits, command tracking, and actuation constraints using Signal Temporal Logic.
Approach
Parameterized STL templates are used to describe gait-aware behavior across multiple speed regimes. These specifications are converted into smooth robustness-based reward signals that provide dense learning feedback compatible with PPO.
System and evaluation
The framework is instantiated on Google’s Barkour quadruped in MuJoCo XLA/MJX. Training uses simulator parallelization and domain randomization to improve robustness, and the resulting policies are compared against hand-crafted reward baselines using tracking and stability-oriented evaluation.