Learning Gait-Aware Quadruped Locomotion with Temporal Logic Specifications

Technical Summary: Learning Gait-Aware Quadruped Locomotion with Temporal Logic Specifications

Problem Statement
Reinforcement learning (RL) for quadruped locomotion currently relies heavily on fixed, hand-crafted, Markovian reward functions. While effective for learning single dominant gaits (e.g., trotting), these approaches suffer from two primary limitations:

1. Lack of Interpretability: The learned policies are often "black boxes" where the connection between reward terms and specific behavioral failures is opaque.
2. Limited Gait Control: Static reward functions struggle to induce distinct gait regimes (walking-trot, trot, bound) or smooth transitions between them based on speed. They often fail to explicitly enforce the temporal structure of contact patterns required for different speeds, leading to unstable training or poor command tracking at high velocities.

The authors address the challenge of learning a single policy that can adapt its gait structure across multiple speed regimes while maintaining safety, stability, and accurate velocity tracking.

Methodology
The proposed framework replaces heuristic rewards with Signal Temporal Logic (STL) specifications to encode desired behaviors. The core methodology involves:

1. Mode-Dependent Gait Selection:
   The system defines three locomotion modes based on commanded forward velocity ($v_{cmd}$), utilizing the Froude number to determine transition thresholds:

   • Walking-Trot (W): $0 \le v_{cmd} \le 0.7$ m/s.
   • Trot (T): $0.7 < v_{cmd} \le 1.7$ m/s.
   • Bound (B): $v_{cmd} > 1.7$ m/s.
     Hysteresis is applied to prevent mode chattering near transition boundaries.

2. Data-Driven STL Specification Mining:
   Instead of manually tuning logic parameters, the authors use a data-driven approach:

   • Expert Trajectories: They collect 50 expert rollouts per regime (walk-trot, trot, bound) from specialized models.
   • Parametric STL (PSTL) Templates: They define parametric templates for safety (torque limits, roll/pitch bounds, CoM height), velocity tracking, and gait structure (contact patterns, duty factors, phase synchronization).
   • Parameter Calibration: Thresholds for the STL predicates are fitted to the expert data using empirical quantiles (e.g., 99th percentile for error magnitudes) to ensure the specifications are satisfied by successful behaviors without over-penalizing transient noise.

3. Reward Shaping via Robustness:
   The STL specifications are converted into a dense, continuous reward signal using quantitative robustness semantics.

   • Predicates: Specific predicates are defined for each mode (e.g., diagonal phase error for trot, aerial phase occupancy for bound, suppression of diagonal patterns for bound).
   • Aggregation: The robustness values ($\rho$) for safety, tracking, and pattern constraints are aggregated using a sign-preserving soft-min function and normalized via $\tanh(\rho)$ to map to $[-1, 1]$.
   • Final Reward: The scalar reward is a weighted sum of the normalized robustness terms minus an energy-efficiency penalty (torque effort).

4. Training Pipeline:
   The approach is instantiated on Google's Barkour vb quadruped robot within the MuJoCo XLA (MJX) simulator.

   • Algorithm: Proximal Policy Optimization (PPO) is used.
   • Optimization: Parallelization on GPUs and domain randomization are employed to improve training speed and policy robustness.
   • Curriculum: Training starts with lower velocity ranges and gradually expands to include the "bound" regime.

Key Contributions

1. Mode-Aware Logic-Based Rewards: A framework where different commanded speeds activate distinct STL specifications, enabling a single policy to learn multiple gait structures.
2. Data-Driven Parameter Learning: A pipeline that fits parametric gait templates directly from expert trajectories, producing interpretable specifications aligned with actual gait statistics rather than heuristic guesses.
3. Unified Multi-Gait Policy: A single policy that successfully tracks velocity commands across walking, trotting, and bounding regimes, achieving lower command-following errors compared to heuristic baselines.
4. Interpretable Diagnostics: The use of STL robustness signals allows for failure attribution. If a rollout fails, specific violated predicates (e.g., insufficient support, actuator limits) can be identified, providing a practical tool for debugging.

Experimental Results
The authors evaluated the STL-shaped policy against two baselines using hand-crafted rewards (heuristic-best and heuristic-default) on the Barkour robot.

• Metrics: Cost of Transportation (CoT), survival rate, and success rate (defined as average forward speed within $\pm 15\%$ of the command).
• Performance: The STL-based policy demonstrated tighter velocity tracking and more stable training.
• High-Speed Robustness: Crucially, the STL policy maintained perfect survival and success rates across the entire tested velocity range, including high-speed commands ($1.9 - 2.1$ m/s), where the heuristic baselines began to degrade in performance.

Significance and Claims
The paper claims that its framework offers a structured, analyzable, and specification-driven alternative to both black-box latent-representation methods and purely heuristic reward shaping. By encoding locomotion objectives as logical specifications, the approach:

• Provides explicit control over gait behaviors and contact sequences.
• Enhances interpretability by linking policy failures to specific logical violations.
• Solves the engineering challenge of learning a unified policy that adapts its gait structure across speed regimes without requiring separate controllers or complex hierarchical switching mechanisms.

The work demonstrates that formal specifications can be effectively integrated into deep RL pipelines to improve both the performance and the debuggability of legged locomotion policies.