Paper deep dive
Learning Gait-Aware Quadruped Locomotion with Temporal Logic Specifications
Merve Atasever, Cagan Bakirci, Alfredo Reina Corona, Keyan Azbijari, Jyotirmoy V. Deshmukh
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 96%
Last extracted: 7/5/2026, 9:08:44 AM
Summary
The paper introduces a framework for quadrupedal locomotion that uses Signal Temporal Logic (STL) to specify and shape rewards. Unlike traditional hand-crafted Markovian rewards, this approach uses parametric STL templates to define distinct gait behaviors (walking-trot, trot, and bound) across different speed regimes. The method utilizes a data-driven pipeline to extract parameters from expert trajectories, providing a dense, continuous, and interpretable reward landscape. The framework was instantiated on Google's Barkour robot in the MuJoCo XLA (MJX) simulator, demonstrating improved velocity tracking and training stability compared to heuristic baselines.
Entities (7)
Relation Signals (4)
Walking-Trot → isaregimeof → Quadruped Locomotion
confidence 100% · We define parametric STL templates for three speed regimes (walking-trot, trot, bound)
Barkour → simulatedin → MuJoCo XLA
confidence 100% · We instantiate the approach on Google's Barkour quadruped robot in MuJoCo XLA (MJX).
Signal Temporal Logic → specifies → Gait Behaviors
confidence 90% · distinct gaits are specified using parameterized constraints expressed in Signal Temporal Logic (STL).
Proximal Policy Optimization → uses → STL-shaped rewards
confidence 90% · The generated rewards can be used to provide shaped gradients compatible with Proximal Policy Optimization (PPO).
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Reinforcement learning (RL) for quadruped locomotion commonly depends on fixed, hand-crafted, and Markovian reward functions that limit both interpretability of learned policies and 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. We show that compared to a baseline of hand-crafted rewards, the STL-shaped rewards yield tighter velocity tracking and more stable training. Videos can be found on our project website: this https URL.
Tags
Links
- Source: https://arxiv.org/abs/2607.00442v1
- Canonical: https://arxiv.org/abs/2607.00442v1
Trouble viewing inline? Open PDF directly →
Full Text
62,154 characters extracted from source content.
Expand or collapse full text
Learning Gait-Aware Quadruped Locomotion with Temporal Logic Specifications Merve Atasever, Cagan Bakirci, Alfredo Reina Corona &Keyan Azbijari, Jyotirmoy V. Deshmukh Department of Electrical Engineering and Computer Sciences University of California Berkeley United States janedoe@berkeley.edu Merve Atasever Cagan Bakirci Alfredo Reina Corona Keyan Azbijari Jyotirmoy V. Deshmukh University of Southern California, Los Angeles, California, USA atasever,cbakirci,reinacor,azbijari,jdeshmuk@usc.edu Abstract Reinforcement learning (RL) for quadruped locomotion commonly depends on fixed, hand-crafted, and Markovian reward functions that limit both interpretability of learned policies and 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. We show that compared to a baseline of hand-crafted rewards, the STL-shaped rewards yield tighter velocity tracking and more stable training. Videos can be found on our project website: https://stl-locomotion.github.io/. Keywords: Quadrupedal Locomotion, Reinforcement Learning, STL 1 Introduction Legged robots, including both bipeds and quadrupeds, have made remarkable progress in recent years, with modern platforms exhibiting agile walking, crawling, running, and more in increasingly challenging settings [58, 36, 56, 41, 71, 1]. Despite this progress, achieving animal-level robustness across diverse speed regimes and gait patterns remains an open challenge. Classical model-based control approaches, such as differential dynamic programming (DDP) and model predictive control (MPC), have enabled impressive quadrupedal behaviors by explicitly optimizing trajectories under dynamics and contact constraints. However, their performance often depends on accurate system models and carefully designed cost functions, all of which can be difficult to obtain on real hardware. [37, 55, 16]. Reinforcement learning (RL) offers a complementary path by directly optimizing closed-loop policies in simulation, and recent advances in high-fidelity physics engines and standardized legged-locomotion platforms, such as MuJoCo, Isaac Gym, Google Barkour, Unitree A1/Go1, and ANYmal, have further accelerated progress in this direction.[67, 31, 49, 9]. A key requirement for quadrupedal locomotion is the ability to operate across multiple speed regimes by switching between distinct gait patterns. For example, walking, trotting, and bounding differ not only in velocity but also in their contact timing, duty factors, and employed support structures. Locomotion controllers must therefore satisfy several objectives simultaneously: accurate command tracking over a wide range of speeds, safety and stability under disturbances, and structured gait behavior whose contact patterns remain appropriate for the commanded regime. State-of-the-art deep RL pipelines address the first objective, and partially the second through carefully engineered reward terms, curriculum learning, and domain randomization [66, 31, 9]. However, these reward functions are often difficult to interpret, and they provide only indirect control over contact-sequence structure and speed-dependent gait transitions. This limitation becomes especially important in multi-gait locomotion. Heuristic rewards based on forward velocity, energy consumption, and posture regularization, can be sufficient for learning a single dominant gait such as trotting; yet, the same static rewards may fail to induce distinct gait regimes or smooth transitions. Existing approaches often address this issue through imitation learning or reference-based objectives, using motion-capture data, or hand-designed gait schedules to impose desired locomotion patterns. Figure 1: Overall Pipeline. Figure 2: Barkour vb robot in MJX. Formal specifications provide an alternative perspective: rather than expressing locomotion objectives through loosely coupled rewards, desired behaviors can be encoded as logical specifications. Signal Temporal Logic (STL) is a framework that has been used in robotics to express bounded-time constraints over real-valued signals. It admits quantitative or robustness semantics, i.e. signed margins indicating how well a trajectory satisfies a specification [50]. Prior work has demonstrated that robustness can be used as a reward to accelerate RL and improve interpretability [17, 44, 2, 34, 15, 10, 7, 75, 33, 27, 70, 32]. We build on this using STL robustness to encode multi-gait coordination and safety requirements. We target a key engineering challenge in quadrupedal locomotion: learning a single policy that adapts its gait structure across speed regimes (walking-trot → trot → bound). We specifically use mode-conditioned STL templates (where template parameters are mind from expert trajectories), and the shaped reward chooses the appropriate template based on the commanded speed regime. This design is motivated by: (1) many locomotion requirements, including footfall pattern and stability, are inherently temporal: they describe behavior over short trajectory segments rather than single states, and (2) switching between gait-specific objectives near speed thresholds can introduce reward discontinuities and destabilize learning unless the mode logic is designed carefully (e.g., hysteresis around regime boundaries). Our framework combines interpretable specification-based design with the scalability of deep RL. Each reward component corresponds to a human-readable requirement, active gait template changes with the commanded speed regime, and the robustness values provide diagnostic signals after training. Thus, beyond improving policy learning, the same STL structure enables failure attribution: poor rollouts can be analyzed in terms of violated predicates, such as insufficient support, actuator-limit violations, or poor orientation. This specification-level feedback is difficult to obtain from monolithic rewards and provides a practical tool for debugging multi-gait locomotion policies. Main Contributions. (1) Mode-aware logic-based rewards for quadruped locomotion, where different speeds activate different rewards/specifications. (2) Data-driven parameter learning pipeline that fits a set of parametric gait templates from expert trajectories, producing interpretable specs aligned with gait statistics. (3) A unified single policy enabling different gait patterns according to desired motion objectives that achieves lower errors in command-following relative to heuristic baselines. (4) Interpretable diagnostics for failure analysis through STL robustness signals by attributing policy errors to specific violated specifications. Related Work. Reward Shaping: As RL becomes standard in locomotion, reward design remains a key bottleneck [13, 19, 32]. Most work relies on hand-crafted weighted rewards with empirically tuned coefficients, justified through ablations rather than first principles [26, 19, 38]. Alternatives such as inverse RL and preference-based RL infer rewards from demonstrations or human feedback, but require expert trajectories or annotations and introduce additional optimization overhead [23, 54, 4, 11, 74, 43]. Prior work has explored logic-guided RL by converting logic objectives into quantitative rewards (e.g., LTL/STL reward shaping) and learning temporal logic specifications from demonstrations, often in navigation/manipulation settings [27, 44, 46, 45, 35, 57]. Formal specifications have also guided planning and control for legged robots, including locomotion over cluttered terrain and STL-informed MPC for bipedal push recovery [21, 77, 6, 24, 25]. However, comparable formulations for quadrupeds remain limited. Existing logic-driven gait learning for quadrupeds typically uses discrete logic rules or reward machines over foot-contact propositions, enabling structured gait sequencing but operating mainly on contact-level logic and step-wise signals [30, 14]. Quadruped Locomotion: Work in biology inspired locomotion focuses on gait expression and transitions emerging from structured interlimb coordination and speed-dependent dynamics rather than control outcomes [60, 12]. This has shaped research using central pattern generator (CPG) models and sensory-feedback frameworks used to encode rhythmic structure and transition behavior [59, 47, 29, 53, 65, 48, 8]. While effective, this work typically depends on accurate dynamic models, incurs computational cost, and needs carefully engineered optimization pipelines. More recent work focuses on hierarchical RL, phase-guided control, and unified multi-gait representations to achieve multi-gait locomotion and gait transitions [42, 28, 68, 64, 72, 69]. One hierarchical framework uses a high-level gait policy to specify footfall patterns with low-level MPC-based motion tracking, yielding energy-efficient gait transitions as speed increases [73]. Related work argues that single end-to-end locomotion policies often collapse to one dominant gait and instead proposes hierarchical controllers capable of generating pace, trot, and bound while tracking velocity commands [39]. Other approaches seek unified latent representations rather than explicit switching or hand-designed phase templates. These learn compact embeddings that capture shared structure across gait families and interpolate between them [51, 63]. These methods reduce the need for manually enumerated gait templates, but their learned representations can be less interpretable than structured controllers with explicit gait objectives. Overall, the literature reveals a trade-off: optimization-based, and contact-conditioned methods provide strong structure at the increased computation cost, while latent and morphology-general methods are flexible but less interpretable. Our work is complementary in this design space as it provides a structured, analyzable, mode-aware, specification-driven alternative to both black-box latent-representation methods and purely heuristic reward shaping. 2 Technical Background and Preliminaries Problem Setting. We consider a quadruped robot, specifically Google’s Barkour vb, with three (abduction, hip, and knee) joints on each of its legs [9]. The controller receives a command of linear and angular velocities (vx,tcmd,vy,tcmd,ωtcmd)(v_x,t^cmd,v_y,t^cmd, _t^cmd), primarily a forward velocity command vx,tcmdv_x,t^cmd. In our case, the goal is to learn a single policy πθ(at∣ot), _θ(a_t o_t), where θ,at,otθ,a_t,o_t denotes the current policy parameters, action, and observation respectively, that achieves accurate command tracking while exhibiting stable, interpretable, and mode-appropriate gait behavior across multiple speed regimes. The observation space includes user command (vxcmd,vycmd,ωcmdv_x^cmd,v_y^cmd,ω^cmd), robot proprioceptive information (g,ϕ,ωg,φ,ω), and previous action at−1a_t-1, where g is gravity projected in the body frame, ϕφ is joint angles, ω is the yaw velocity, and the mode flag (walk/trot/bound). We further include a observation history of 15 time steps (0.30.3 s) for the robot proprioception. The action space is absolute joint position with a default offset qdes,t=qdefault+kaatq_des,t=q_default+k_a\,a_t, where kak_a is the action scale. The desired joint position is mapped to torque via a PD controller [76]. Mode-Dependent Gait Selection. Using the same gait for low speed and high speed motion is not efficient and feasible for quadrupeds. Hence, the robots should follow different gait structure to reach high speed velocities and conserve their energy for low speed motions. To determine transition velocity thresholds between speed regimes, we leverage the Froude number which is used to characterize gait transition speeds of different-sized quadrupeds: Fr=v2gh,Fr= v^2gh, where Fr is the Froude number, v is the linear velocity of the robot’s torso, g is the acceleration due to gravity, and h is the maximum leg length [3]. Building on bio-inspired robotics gait design methodologies and reported gait structures that quadrupeds achieved to succeed, we use three speed regimes (modes): walking-trot (W), trot (T), and bound (B), selected based on commanded forward velocity |vxcmd(t)||v_x^cmd(t)|. Based on reported Froude numbers 0.15,0.74\0.15,0.74\ and Barkour’s leg length of 0.410.41m, we set gait transition velocity thresholds at 0.70.7m/s and 1.71.7m/s respectively [29]. To prevent mode chattering near transition boundaries, we incorporate hysteresis by defining separate enter and exit thresholds for each regime. We denote the active locomotion mode at time t as g(t)∈W,T,Bg(t)∈\W,T,B\, which also serves as the Boolean indicator for the corresponding gait mode. Signal Temporal Logic (STL) & Quantitative Robustness. Signal Temporal Logic (STL) specifies temporal properties over real-valued signals x(t)x(t) using Boolean and temporal operators [50]. Formulas are built from atomic predicates f(x(t))≥0f(x(t))≥ 0, Boolean connectives (∧,∨,¬ , , ), and time-bounded temporal operators [a,b]G_[a,b] (always) and [a,b]F_[a,b] (eventually). We use quantitative semantics of STL [18, 20]; for a given trace x, and each formula φ ρφ(t)ρ (t) assigns a real value capturing the degree of satisfaction. Positive values imply satisfaction; negative imply violation, and the magnitude measures the satisfaction margin. For atomic predicates, ρ(f(x)≥0,x,t)=f(x(t))ρ(f(x)≥ 0,x,t)=f(x(t)). For conjunction/disjunction, robustness uses min/max: ρφ∧ψ(t)=min(ρφ(t),ρψ(t))ρ ψ(t)= (ρ (t),ρ^ψ(t)), and ρφ∨ψ(t)=max(ρφ(t),ρψ(t)).ρ ψ(t)= (ρ (t),ρ^ψ(t)). For time-bounded operators, we have ρIφ(t)=inft′∈t+Iρφ(t′)ρ^G_I (t)= _t ∈ t+Iρ (t ), and ρIφ(t)=supt′∈t+Iρφ(t′)ρ^F_I (t)= _t ∈ t+Iρ (t ) for an arbitrary time interval I=[a,b]I=[a,b]. Parametric Signal Temporal Logic (PSTL) extends STL by allowing constants in predicates and intervals in temporal operators to be represented by parameters [5]. The specification mining problem seeks to infer parameter ranges where the template formula is satisfied providing a data-driven way to instantiate temporal specifications from expert-provided locomotion trajectories. 3 Methodology Data Collection & Feature Extraction. To capture diverse locomotion behaviors, we compile trajectory datasets from three specialized models corresponding to low-speed (walk-trot), mid-high speed (trot), high speed (bound) regimes. We adopt the base model from [9], introducing a revised reward formulation and a curriculum learning strategy for the different speed profiles. We demonstrate that a compact dataset of 50 expert trajectories per regime is sufficient for extracting PSTL parameters. Although these parameters could be estimated using heuristics from the literature, we opt for this data-driven approach to directly leverage the available expert trajectories. Each trajectory consists of 500500 simulation steps with timestep Δt=0.02s t=0.02\,s. To remove startup transients, we discard an initial warmup interval t∈[0,twarm]t∈[0,t_warm], where twarm=100t_warm=100 steps (∼2s 2\,s). All features are computed from the post-warmup trajectory and include signals describing tracking performance, stability, contact coordination, and gait structure: • Tracking features: |vx(t)−vxcmd(t)||v_x(t)-v_x^cmd(t)|, |vy−vycmd||v_y-\!v_y^cmd|, and |ωz−ωzcmd|| _z- _z^cmd|. • Safety/stability features: Center of mass (CoM) position pcom(t)p_com(t) and velocity vcom(t)v_com(t), a center of pressure (CoP) proxy pcop(t)p_cop(t), base roll/pitch (ϕ(t),θ(t))(φ(t),θ(t)), CoP-CoM distance ‖pcop(t)−pcomxy(t)‖2\|p_cop(t)-p_com^xy(t)\|_2, and slip proxy maxℓ∈(t)‖vℓxy(t)‖2 _ (t)\|v_ ^xy(t)\|_2. • Contact-pattern features: foot contacts cℓ(t)∈0,1c_ (t)∈\0,1\ for ℓ∈FL,FR,HL,HR ∈\FL,FR,HL,HR\, pair-synchronization errors (diagonal pairs for trot, front/hind pairs for bound). • Stride-level features: est. stride period T and duty factor DFDF from rising/falling edges of contact signals; diagonal phase error computed from timing difference between diagonal touch-downs. We define contact count nc(t)=∑ℓcℓ(t)n_c(t)= _ c_ (t) and foot tangential speed ‖vℓxy(t)‖2\|v_ ^xy(t)\|_2 in stance. For gait structure we compute windowed statistics such as stride period T¯(t) T(t), duty factor DF¯(t) DF(t), diagonal phase error ediag(t)e_diag(t), and the fraction of 2-contact states that correspond to diagonal pairs pdiag2(t)p_diag2(t). These windowed statistics are used as pSTL template terms. Data to STL Specifications. We define a family of PSTL templates. Each mode g∈W,T,Bg∈\W,T,B\ has: (i) a shared safety template φsafe,g _safe,g with mode-dependent thresholds, (i) a commanded velocity tracking template φtrack,g _track,g with mode-dependent thresholds, and (i) a gait-structure template φg _g capturing regime-specific contact patterns. We fit parameters of the fixed templates from data in a quantile-based approach. For each atomic predicate μk(t) _k(t) used in a template, we select thresholds based on empirical quantiles of the successful trajectories. For example, for a strict windowed-G implementation (min/softmin over time), we use tolerant high quantiles (e.g., 99th percentile for error magnitudes and a low percentile for floors) to reduce over-penalizing short transients. The thresholds and weights introduced in the next section are obtained empirically by fitting the reward components to expert demonstration datasets. For completeness, the full set of parameters, thresholds, and weights used in our work is reported in the Appendix. Mode-Dependent STL Specifications for Multi-Gait Locomotion. We consider three locomotion regimes parameterized by the commanded forward velocity vxcmdv_x^cmd: walking-trot for 0≤vxcmd≤0.70≤ v_x^cmd≤ 0.7 m/s, trot for 0.7<vxcmd≤1.70.7<v_x^cmd≤ 1.7 m/s, and bound for vxcmd>1.7v_x^cmd>1.7 m/s. For each mode g(t)∈W,T,Bg(t)∈\W,T,B\, we define a mode-specific STL specification composed of a shared safety, velocity tracking, and a gait-shape part. The reward is then derived from the quantitative robustness of the active specification over a finite horizon g=[t−Hg,t]W_g=[t-H_g,t]. HgH_g is the horizon for mode g, which is chosen to cover roughly one complete gait cycle, with a slightly longer window for slower walking-trot and shorter windows for faster trot/bound. For any Boolean event A(k)A(k), we define the window fraction pA(t)=1|g(t)|∑k∈g(t)A(k).p_A(t)= 1|W_g(t)| _k _g(t)1\A(k)\. Positive robustness indicates satisfaction, negative robustness indicates violation, and the magnitude gives the satisfaction/violation margin. Tables 1 and 2 summarize the predicates used in our reward. Table 1: Shared safety and tracking STL predicates. ID Predicate STL constraint Robustness S1 Torque limit g(|τj|≤τjmax),∀jG_W_g(| _j|≤τ _j),\ ∀ j ρτ(t)=minj(τjmax−|τj(k)|) _τ(t)= _j(τ _j-| _j(k)|) S2 Roll limit g(|ϕ|≤ϕmaxg)G_W_g(|φ|≤ _ ^g) ρϕ,g(t)=(ϕmaxg−|ϕ(k)|) _φ,g(t)=( _ ^g-|φ(k)|) S3 Pitch limit g(|θ|≤θmaxg)G_W_g(|θ|≤ _ ^g) ρθ,g(t)=(θmaxg−|θ(k)|) _θ,g(t)=( _ ^g-|θ(k)|) S4 CoM height g(zcom≥zming)G_W_g(z_com≥ z_ ^g) ρz,g(t)=(zcom(k)−zming) _z,g(t)=(z_com(k)-z_ ^g) S5 Support contacts g(nc≥nming)G_W_g(n_c≥ n_ ^g) ρc,g(t)=(nc(k)−nming) _c,g(t)=(n_c(k)-n_ ^g) T1 Linear velocity g(|vi−vicmd|≤ϵv,ig),i∈x,yG_W_g(|v_i-v_i^cmd|≤ _v,i^g),\ i∈\x,y\ ρvi,g(t)=(ϵv,ig−|vi(k)−vicmd(k)|) _v_i,g(t)=( _v,i^g-|v_i(k)-v_i^cmd(k)|) T2 Yaw-rate tracking g(|ωz−ωzcmd|≤ϵωg)G_W_g(| _z- _z^cmd|≤ _ω^g) ρω,g(t)=(ϵωg−|ωz(k)−ωzcmd(k)|) _ω,g(t)=( _ω^g-| _z(k)- _z^cmd(k)|) Table 2: Mode-dependent gait-structure STL predicates. ID Mode STL specifications Robustness G1 W,TW,T g(ediag≤ϵdiagg)G_W_g(e_diag≤ _diag^g) ρdiag,g(t)=ϵdiagg−ediag(t) _diag,g(t)= _diag^g-e_diag(t) G2 W,TW,T g(pdiag2≥ηdiag2g)G_W_g(p_diag2≥ _diag2^g) ρdiag2,g(t)=pdiag2(t)−ηdiag2g _diag2,g(t)=p_diag2(t)- _diag2^g G3 W W[0,K](nc≥3)G_W_WF_[0,K](n_c≥ 3) ρ3+event(t)=maxτ∈[t−K+1,t](nc(τ)−3) _3+event(t)= _τ∈[t-K+1,t](n_c(τ)-3) G4 T T(p2contact≥p2,min)G_W_T(p_2contact≥ p_2, ) ρ2contact(t)=p2contact(t)−p2,min _2contact(t)=p_2contact(t)-p_2, B1 B B(pflight≥pflight,min)G_W_B(p_flight≥ p_flight, ) ρflight(t)=pflight(t)−pflight,min _flight(t)=p_flight(t)-p_flight, B2 B B(pfront≥pfront,min)G_W_B(p_front≥ p_front, ) ρfront(t)=pfront(t)−pfront,min _front(t)=p_front(t)-p_front, B3 B B(phind≥phind,min)G_W_B(p_hind≥ p_hind, ) ρhind(t)=phind(t)−phind,min _hind(t)=p_hind(t)-p_hind, B4 B B(p4∈[p4,min,p4,max])G_W_B(p_4∈[p_4, ,p_4, ]) ρall4(t)=minp4(t)−p4,min,p4,max−p4(t) _all4(t)= \! \p_4(t)-p_4, ,p_4, -p_4(t) \ B5 B B(pdiag2≤pdiag2,max)G_W_B(p_diag2≤ p_diag2, ) ρdiag2,B(t)=pdiag2,max−pdiag2(t) _diag2,B(t)=p_diag2, -p_diag2(t) B6 B BEF∧BEHF_W_BE_F _W_BE_H ρbound_event(t)=minNF(t),NH(t)−1 _bound\_event(t)= \N_F(t),N_H(t)\-1 Using the predicate definitions in Tables 1-2, we obtain the following STL templates. Safety. Torque limits: For Barkour vb, the actuators provide a peak output torque of 18Nm at each, hence motor torque limits must be bounded by this limit. Roll & pitch limits: To not loose the balance, roll and pitch of the robot’s torso should be bounded. CoM height: Height of the torso should be lower-bounded to ensure no fall or tip over. Support contacts: We enhance the robot’s stability by specifying the number of legs in stance according in a desired gait mode. Walk/trot requires ≥2≥ 2 support contacts at all times (included only in the early curriculum stage and removed when training the bound gait.) The shared safety specification for mode g is φsafe,g=g(ρτ≥0∧ρϕ,g≥0∧ρθ,g≥0∧ρz,g≥0). _safe,g=G_W_g ( _τ≥ 0 _φ,g≥ 0 _θ,g≥ 0 _z,g≥ 0 ). Velocity Tracking. The objective is for the robot to follow the commanded linear velocity. Here, vx(t),vy(t),ωz(t)v_x(t),v_y(t), _z(t) denote linear and angular base velocities, and vxcmd(t),vycmd(t),ωzcmd(t)v_x^cmd(t),v_y^cmd(t), _z^cmd(t) are the corresponding target velocities. The velocity tracking specification for mode g is φtrack,g=g(ρvx,g≥0∧ρvy,g≥0∧ρω,g≥0). _track,g=G_W_g ( _v_x,g≥ 0 _v_y,g≥ 0 _ω,g≥ 0 ). Walk-Trot Gait. This is characterized by support-rich diagonal locomotion with no flight. We use the following mode-specific predicates: G1-Diagonal phase error: This predicate is applied to both walk-trot and trot gaits, and it quantifies the temporal synchronization of diagonal leg pairs. G2-Diagonal pair fraction: This predicate quantifies how strongly the gait exhibits trot-like diagonal contact structure. G3-Multi-support moment: This predicate encourages the walk gait to exhibit at least one recent multi-support phase (three or more feet are simultaneously in contact) by rewarding the existence of a timestep within the trailing K-step window. The walk-trot specification is φW=W(mW⇒(ρdiag,W≥0∧ρdiag2,W≥0∧ρ3+event≥0)), _W=G_W_W (m_W ( _diag,W≥ 0 _diag2,W≥ 0 _3+event≥ 0) ), Trot Predicates: While we have common predicates (G1 and G2) with walk-trot regime, trot is characterized by dominant diagonal 2-contact support and lower duty factor than walk-trot. G4-Two-leg support: This predicate is the fraction of timesteps in which exactly two feet are in contact with the ground. The trot specification is φT=T(mT⇒(ρdiag,T≥0∧ρdiag2,T≥0∧ρ2contact≥0)), _T=G_W_T (m_T ( _diag,T≥ 0 _diag2,T≥ 0 _2contact≥ 0) ), Bound Gait: This is a high-speed pair-synchronized running gait where the forelegs and hind legs move approximately in phase, the two leg pairs alternate in stance, and locomotion includes one or more aerial phases, yielding larger sagittal extension and higher speed than diagonal trot. B1-Minimum aerial-phase occupancy: This computes the time-fraction when no foot is in contact with the ground, and enforces the minimum aerial-phase occupancy for bounding. B2/3-Pair-only support states: This computes the fractions of times when only the fore or hind legs are in contact; robustness enforces the minimum pair-only support occupancy for bounding. B4-All four contact fraction: This constrains the time fraction where all four legs are in contact. B5-Trot suppression term: This predicate computes the fraction of 2-contact states that correspond to diagonal leg pairs; thus, for the bound mode, positive robustness favors suppression of trot-like diagonal support patterns in favor of pair-based fore/hind support. B6-Pair touchdown events: This predicate enforce that there should be at least one front-pair touchdown event and at least one hind-pair touchdown event within the current temporal window. The bound specification is φB=B(mB⇒(ρflight≥0∧ρfront≥0∧ρhind≥0∧ρall4≥0∧ρdiag2,B≥0∧ρbound_event≥0)). _B=G_W_B (m_B ( _flight≥ 0 _front≥ 0 _hind≥ 0 _all4≥ 0 _diag2,B≥ 0 _bound\_event≥ 0) ). Robustness Reward: We aggregate multiple robustness terms using the sign-preserving soft-min sminβsp(z1,…,zK):=∑k=1Kπkzksmin^sp_β(z_1,…,z_K):= _k=1^K _kz_k, where πk=e−βzk∑j=1Ke−βzj. _k= e^-β z_k _j=1^Ke^-β z_j. For the final reward shaping, each grouped robustness is normalized as tanh(ρ) (ρ) to map to a value in [−1,1][-1,1], preventing large robustness magnitudes from dominating the reward.111All scale factors and weight terms are obtained by fitting the templates to expert datasets. Details in the Appendix. We also include the torque-effort penalty for energy efficiency Jτ(t)=meanτ∈t(m)∑jτj(τ)2.J_τ(t)=mean_τ _t^(m) _j _j(τ)^2. The final scalar reward is: rt=wsafe(g)tanh(μsafety)+wtrack(g)tanh(μtrack)+wpattern(g)tanh(μpattern)−weffortJτ(t).r_t=w_safe^(g)\, ( _safety)+w_track^(g)\, ( _track)+w_pattern^(g)\, ( _pattern)-w_effortJ_τ(t). (1) 4 Experimental Results Robot and Simulation Setup. The locomotion controller is designed for the Barkour vb quadruped robot, modeled using the MuJoCo physics engine [9, 67]. The simulation leverages MuJoCo XLA (MJX), a JAX-based implementation of MuJoCo, which allows for highly parallelized simulation entirely on the GPU. We train the locomotion policy using the PPO algorithm with the hyperparameters listed in the Appendix [62, 40]. During training, a new velocity command is randomly sampled every 10 s. The initial command range is set to vx⋆∈[0.0, 1.7]m/sv_x ∈[0.0,\,1.7]\,m/s, vy⋆∈[−0.2, 0.2]m/sv_y ∈[-0.2,\,0.2]\,m/s, and ω˙⋆∈[−0.2, 0.2]rad/s ω ∈[-0.2,\,0.2]\,rad/s for the walk/trot regimes. The forward-velocity range is then gradually expanded to vx⋆∈[0.0, 1.9]m/sv_x ∈[0.0,\,1.9]\,m/s as part of the curriculum for learning the bound gait. Details of the training procedure and domain randomization are provided in the Appendix. The baseline is a hand-engineered reward function from [76], a de facto standard in recent quadrupedal RL. We evaluate two baseline configurations: heuristic-best, which utilizes the original optimized parameters and velocity ranges, and heuristic-default, which applies the same training structure within our specific experimental setup and velocity ranges to ensure a fair comparison. We evaluate each policy under forward velocity commands vxv_x ∈ 0.3,0.5,0.7,1.0,1.3,\0.3,0.5,0.7,1.0,1.3, 1.6,1.9,2.0,2.11.6,1.9,2.0,2.1\ m/s, with zero lateral and yaw commands. For each command, we run 2020 independent rollouts, each with a horizon of 500500 steps. For command-tracking performance, we ignore the first 5050 steps as a warm-up period and evaluate tracking only over the remaining trajectory. We leverage three evaluation metrics: cost of transportation (CoT), survival rate, and success rate. We measure energy efficiency using cost of transportation Emgd Em\,g\,d where E is the total energy consumed, m is the robot mass, g is gravitational acceleration, and d is the planar distance traveled during the rollout. Lower CoT indicates better transport efficiency. A rollout is counted as survived if the robot does not terminate early due to falling or violating the environment termination conditions. We define success based on velocity tracking accuracy after the warm-up phase. Let vx,cmdv_x,cmd be the commanded forward velocity, and let vx,loc(t)v_x,loc(t) denote the robot’s forward velocity in its local body frame. The average post-warm-up forward speed for rollout k is v¯x(k)=1T−50∑t=51Tvx,loc(k)(t). v_x^(k)= 1T-50 _t=51^Tv_x,loc^(k)(t). A rollout is considered successful if |v¯x(k)−vx,cmd|≤0.15|vx,cmd|, | v_x^(k)-v_x,cmd |≤ 0.15\,|v_x,cmd|, i.e., the average forward speed stays within ±15%± 15\% of the commanded velocity. Table 3: Benchmark comparison across commanded forward velocities. Each entry reports mean ± standard deviation over 20 rollouts. Lower CoT is better; higher survival and success are better. Success means the average post-warmup forward speed stays within ±15%± 15\% of the commanded speed. STL-based reward Heuristic-default Heuristic-best vxv_x CoT ↓ Survival ↑ Success ↑ CoT ↓ Survival ↑ Success ↑ CoT ↓ Survival ↑ Success ↑ 0.3 2.1 ± 0.1 1.0 ± 0.0 1.0 ± 0.0 2.1 ± 0.1 1.0 ± 0.0 0.0 ± 0.0 1.2 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 0.5 1.5 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.3 ± 0.0 1.0 ± 0.0 0.0 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 0.7 1.2 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.1 ± 0.0 1.0 ± 0.0 0.1 ± 0.2 1.0 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.0 1.2 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.5 ± 0.0 1.0 ± 0.0 0.8 ± 0.4 1.2 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.3 1.1 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.3 ± 0.1 1.0 ± 0.0 0.3 ± 0.5 1.3 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.6 1.0 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.2 ± 0.0 1.0 ± 0.2 0.3 ± 0.4 1.4 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.9 1.1 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.2 ± 0.1 0.5 ± 0.5 0.0 ± 0.0 1.4 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 2.0 1.1 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.3 ± 0.1 0.5 ± 0.5 0.0 ± 0.0 1.4 ± 0.0 1.0 ± 0.0 0.1 ± 0.2 2.1 1.1 ± 0.0 1.0 ± 0.0 1.0 ± 0.0 1.3 ± 0.1 0.3 ± 0.4 0.0 ± 0.0 1.4 ± 0.0 1.0 ± 0.0 0.0 ± 0.0 Table 3 shows that STL-based rewards achieve the most consistent performance across the full command range. The STL policy maintains perfect survival and success at every tested velocity, including the high-speed commands (vx∈1.9,2.0,2.1)(v_x∈1.9,2.0,2.1), where the heuristic baselines begin to degrade. This suggests that the mode-dependent STL reward provides a more reliable training signal for preserving command tracking and stability across gait regimes. At lower speeds, the heuristic-best baseline attains lower CoT than the STL policy, especially for (vx≤1.0)(v_x≤ 1.0). This indicates that the hand-tuned heuristic reward can be more energy efficient in the slower walking/trotting regimes. However, this advantage does not persist at higher speeds. From (vx=1.3)(v_x=1.3) onward, the STL-based policy achieves the lowest CoT while maintaining perfect survival and success. We attribute this high-speed advantage to the mode-dependent gait structure encoded by the STL reward: at high commanded velocities, the STL policy learns to transition to a bound-like gait, whereas the heuristic-best baseline continues to execute a trot-like gait induced by its static reward design. Since bounding is mechanically more suitable for fast forward locomotion, the STL policy can achieve lower CoT in the high-speed regime while preserving tracking accuracy. The heuristic-default baseline is the least reliable overall. Although it remains stable at low and moderate velocities, its success rate is poor for most commands, indicating that survival alone does not imply accurate velocity tracking. This result highlights a key limitation of static manually tuned rewards: their performance can be highly sensitive to implementation details and training procedure, and even small changes may substantially degrade their ability to sustain reliable locomotion performance. Overall, the table demonstrates the main benefit of the proposed STL-based reward: it provides a unified, mode-aware objective that maintains both stability and command-tracking success across slow, moderate, and high-speed locomotion. While the heuristic-best baseline can be more energy efficient at low speeds, the STL reward offers better robustness and scalability to high-speed regimes by explicitly encouraging the appropriate gait structure, including the transition to bound at high forward velocities. Limitations. Our study is conducted entirely in simulation (MJX). We employ domain randomization over friction and actuator parameters, but the results do not yet establish sim-to-real transfer. Thus, the present conclusions should be interpreted as evidence of improved simulation performance and reward design. The current formulation also models gait transitions primarily as speed-dependent without incorporating terrain information (slope, roughness) into the mode-selection mechanism. 5 Conclusion We presented a specification-driven reinforcement learning framework for quadruped locomotion in which the reward is synthesized from mode-dependent Signal Temporal Logic (STL) templates rather than from a purely heuristic Markovian objective. The resulting policy was trained as a single unified controller using PPO, which suggests that STL-based reward shaping is a practical middle ground between black-box reward tuning and explicitly scripted gait controllers. References [1] A. Agarwal, A. Kumar, J. Malik, and D. Pathak (2023) Legged locomotion in challenging terrains using egocentric vision. In Conference on robot learning, p. 403–415. Cited by: §1. [2] D. Aksaray, A. Jones, Z. Kong, M. Schwager, and C. Belta (2016) Q-learning for robust satisfaction of signal temporal logic specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC), p. 6565–6570. Cited by: §1. [3] R. M. Alexander and A. Jayes (1983) A dynamic similarity hypothesis for the gaits of quadrupedal mammals. Journal of zoology 201 (1), p. 135–152. Cited by: §2. [4] S. Arora and P. Doshi (2021) A survey of inverse reinforcement learning: challenges, methods and progress. Artificial Intelligence 297, p. 103500. Cited by: §1. [5] E. Asarin, A. Donzé, O. Maler, and D. Nickovic (2011) Parametric identification of temporal properties. In International Conference on Runtime Verification, p. 147–160. Cited by: §2. [6] H. Audren, A. Kheddar, and P. Gergondet (2016) Stability polygons reshaping and morphing for smooth multi-contact transitions and force control of humanoid robots. In 2016 IEEE-RAS 16th International Conference on Humanoid Robots (Humanoids), p. 1037–1044. Cited by: §1. [7] A. Balakrishnan and J. V. Deshmukh (2019) Structured reward shaping using signal temporal logic specifications. in 2019 ieee/rsj iros, 3481–3486. IEEE. Cited by: §1. [8] G. Bellegarda, M. Shafiee, and A. Ijspeert (2025) Allgaits: learning all quadruped gaits and transitions. In 2025 IEEE International Conference on Robotics and Automation (ICRA), p. 15929–15935. Cited by: §1. [9] K. Caluwaerts, A. Iscen, J. C. Kew, W. Yu, T. Zhang, D. Freeman, K. Lee, L. Lee, S. Saliceti, V. Zhuang, et al. (2023) Barkour: benchmarking animal-level agility with quadruped robots. arXiv preprint arXiv:2305.14654. Cited by: §1, §1, §2, §3, §4. [10] A. Camacho, R. T. Icarte, T. Q. Klassen, R. A. Valenzano, and S. A. McIlraith (2019) LTL and beyond: formal languages for reward function specification in reinforcement learning.. In IJCAI, Vol. 19, p. 6065–6073. Cited by: §1. [11] P. F. Christiano, J. Leike, T. Brown, M. Martic, S. Legg, and D. Amodei (2017) Deep reinforcement learning from human preferences. Advances in neural information processing systems 30. Cited by: §1. [12] S. M. Danner, S. D. Wilshin, N. A. Shevtsova, and I. A. Rybak (2016) Central control of interlimb coordination and speed-dependent gait expression in quadrupeds. The Journal of physiology 594 (23), p. 6947–6967. Cited by: §1. [13] P. Dayan and B. W. Balleine (2002) Reward, motivation, and reinforcement learning. Neuron 36 (2), p. 285–298. Cited by: §1. [14] D. DeFazio, Y. Hayamizu, and S. Zhang (2024) Learning quadruped locomotion policies using logical rules. In Proceedings of the International Conference on Automated Planning and Scheduling, Vol. 34, p. 142–150. Cited by: §1. [15] J. V. Deshmukh, A. Donzé, S. Ghosh, X. Jin, G. Juniwal, and S. A. Seshia (2017) Robust online monitoring of signal temporal logic. Formal Methods in System Design 51 (1), p. 5–30. Cited by: §1. [16] J. Di Carlo, P. M. Wensing, B. Katz, G. Bledt, and S. Kim (2018) Dynamic locomotion in the mit cheetah 3 through convex model-predictive control. In 2018 IEEE/RSJ international conference on intelligent robots and systems (IROS), p. 1–9. Cited by: §1. [17] X. Ding, S. L. Smith, C. Belta, and D. Rus (2014) Optimal control of markov decision processes with linear temporal logic constraints. IEEE Transactions on Automatic Control 59 (5), p. 1244–1257. Cited by: §1. [18] A. Donzé and O. Maler (2010) Robust satisfaction of temporal logic over real-valued signals. In International conference on formal modeling and analysis of timed systems, p. 92–106. Cited by: §2. [19] J. Eschmann (2021) Reward function design in reinforcement learning. Reinforcement learning algorithms: Analysis and Applications, p. 25–33. Cited by: §1. [20] G. E. Fainekos and G. J. Pappas (2009) Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410 (42), p. 4262–4291. Cited by: §2. [21] S. Feng, X. Xinjilefu, W. Huang, and C. G. Atkeson (2013) 3D walking based on online optimization. In 2013 13th IEEE-RAS International Conference on Humanoid Robots (Humanoids), p. 21–27. Cited by: §1. [22] C. D. Freeman, E. Frey, A. Raichuk, S. Girgin, I. Mordatch, and O. Bachem (2021) Brax–a differentiable physics engine for large scale rigid body simulation. arXiv preprint arXiv:2106.13281. Cited by: §A.2. [23] J. Fu, K. Luo, and S. Levine (2017) Learning robust rewards with adversarial inverse reinforcement learning. arXiv preprint arXiv:1710.11248. Cited by: §1. [24] Z. Gu, R. Guo, W. Yates, Y. Chen, Y. Zhao, and Y. Zhao (2024) Walking-by-logic: signal temporal logic-guided model predictive control for bipedal locomotion resilient to external perturbations. In 2024 IEEE International Conference on Robotics and Automation (ICRA), p. 1121–1127. Cited by: §1. [25] Z. Gu, Y. Zhao, Y. Chen, R. Guo, J. K. Leestma, G. S. Sawicki, and Y. Zhao (2025) Robust-locomotion-by-logic: perturbation-resilient bipedal locomotion via signal temporal logic guided model predictive control. IEEE Transactions on Robotics. Cited by: §1. [26] J. Hare (2019) Dealing with sparse rewards in reinforcement learning. arXiv preprint arXiv:1910.09281. Cited by: §1. [27] M. Hasanbeig, D. Kroening, and A. Abate (2020) Deep reinforcement learning with temporal logics. In International Conference on Formal Modeling and Analysis of Timed Systems, p. 1–22. Cited by: §1, §1. [28] B. Hu, S. Shao, Z. Cao, Q. Xiao, Q. Li, and C. Ma (2019) Learning a faster locomotion gait for a quadruped robot with model-free deep reinforcement learning. In 2019 IEEE International Conference on Robotics and Biomimetics (ROBIO), p. 1097–1102. Cited by: §1. [29] J. Humphreys, J. Li, Y. Wan, H. Gao, and C. Zhou (2023) Bio-inspired gait transitions for quadruped locomotion. IEEE Robotics and Automation Letters 8 (10), p. 6131–6138. Cited by: §1, §2. [30] J. Humphreys and C. Zhou (2025) Learning to adapt through bio-inspired gait strategies for versatile quadruped locomotion. Nature Machine Intelligence 7 (7), p. 1141–1153. Cited by: §1. [31] M. Hutter, C. Gehring, D. Jud, A. Lauber, C. D. Bellicoso, V. Tsounis, J. Hwangbo, K. Bodie, P. Fankhauser, M. Bloesch, et al. (2016) Anymal-a highly mobile and dynamic quadrupedal robot. In 2016 IEEE/RSJ international conference on intelligent robots and systems (IROS), p. 38–44. Cited by: §1, §1. [32] R. T. Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith (2022) Reward machines: exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research 73, p. 173–208. Cited by: §1, §1. [33] Y. Jiang, S. Bharadwaj, B. Wu, R. Shah, U. Topcu, and P. Stone (2021) Temporal-logic-based reward shaping for continuing reinforcement learning tasks. In Proceedings of the AAAI Conference on artificial Intelligence, Vol. 35, p. 7995–8003. Cited by: §1. [34] J. Kapinski, X. Jin, J. Deshmukh, A. Donze, T. Yamaguchi, H. Ito, T. Kaga, S. Kobuna, and S. Seshia (2016) ST-lib: a library for specifying and classifying model behaviors. Technical report SAE Technical Paper. Cited by: §1. [35] P. Kapoor, A. Balakrishnan, and J. V. Deshmukh (2020) Model-based reinforcement learning from signal temporal logic specifications. arXiv preprint arXiv:2011.04950. Cited by: §1. [36] B. Katz, J. Di Carlo, and S. Kim (2019) Mini cheetah: a platform for pushing the limits of dynamic quadruped control. In 2019 international conference on robotics and automation (ICRA), p. 6295–6301. Cited by: §1. [37] D. Kim, J. Di Carlo, B. Katz, G. Bledt, and S. Kim (2019) Highly dynamic quadruped locomotion via whole-body impulse control and model predictive control. arXiv preprint arXiv:1909.06586. Cited by: §1. [38] G. Kim, Y. Lee, and H. Park (2025) A learning framework for diverse legged robot locomotion using barrier-based style rewards. In 2025 IEEE International Conference on Robotics and Automation (ICRA), p. 10004–10010. Cited by: §1. [39] Y. Kim, B. Son, and D. Lee (2021) Learning multiple gaits of quadruped robot using hierarchical reinforcement learning. arXiv preprint arXiv:2112.04741. Cited by: §1. [40] N. Kohl and P. Stone (2004) Policy gradient reinforcement learning for fast quadrupedal locomotion. In IEEE International Conference on Robotics and Automation, 2004. Proceedings. ICRA’04. 2004, Vol. 3, p. 2619–2624. Cited by: §4. [41] J. Lee, J. Hwangbo, L. Wellhausen, V. Koltun, and M. Hutter (2020) Learning quadrupedal locomotion over challenging terrain. Science robotics 5 (47), p. eabc5986. Cited by: §1. [42] Y. H. Lee, D. T. Tran, J. Hyun, L. T. Phan, I. M. Koo, S. U. Yang, and H. R. Choi (2015) A gait transition algorithm based on hybrid walking gait for a quadruped walking robot. Intelligent Service Robotics 8 (4), p. 185–200. Cited by: §1. [43] T. Li, J. Won, J. Cho, S. Ha, and A. Rai (2023) Fastmimic: model-based motion imitation for agile, diverse and generalizable quadrupedal locomotion. Robotics 12 (3), p. 90. Cited by: §1. [44] X. Li, C. Vasile, and C. Belta (2017) Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), p. 3834–3839. Cited by: §1, §1. [45] X. Li, C. Vasile, and C. Belta (2017) Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), p. 3834–3839. Cited by: §1. [46] H. Liao (2020) A survey of reinforcement learning with temporal logic rewards. Cited by: §1. [47] C. Liu, Y. Chen, J. Zhang, and Q. Chen (2009) CPG driven locomotion control of quadruped robot. In 2009 IEEE International Conference on Systems, Man and Cybernetics, p. 2368–2373. Cited by: §1. [48] K. Liu, L. Dong, X. Tan, W. Zhang, and L. Zhu (2024) Optimization-based flocking control and mpc-based gait synchronization control for multiple quadruped robots. IEEE Robotics and Automation Letters 9 (2), p. 1929–1936. Cited by: §1. [49] V. Makoviychuk, L. Wawrzyniak, Y. Guo, M. Lu, K. Storey, M. Macklin, D. Hoeller, N. Rudin, A. Allshire, A. Handa, et al. (2021) Isaac gym: high performance gpu-based physics simulation for robot learning. arXiv preprint arXiv:2108.10470. Cited by: §1. [50] O. Maler and D. Nickovic (2004) Monitoring temporal properties of continuous signals. In International symposium on formal techniques in real-time and fault-tolerant systems, p. 152–166. Cited by: §1, §2. [51] A. L. Mitchell, W. Merkt, A. Papatheodorou, I. Havoutis, and I. Posner (2024) Gaitor: learning a unified representation across gaits for real-world quadruped locomotion. arXiv preprint arXiv:2405.19452. Cited by: §1. [52] V. Mnih, A. P. Badia, M. Mirza, A. Graves, T. Lillicrap, T. Harley, D. Silver, and K. Kavukcuoglu (2016) Asynchronous methods for deep reinforcement learning. In International conference on machine learning, p. 1928–1937. Cited by: §A.2. [53] M. Neunert, F. Farshidian, A. W. Winkler, and J. Buchli (2017) Trajectory optimization through contacts and automatic gait discovery for quadrupeds. IEEE Robotics and Automation Letters 2 (3), p. 1502–1509. Cited by: §1. [54] A. Y. Ng, S. Russell, et al. (2000) Algorithms for inverse reinforcement learning.. In Icml, Vol. 1, p. 2. Cited by: §1. [55] Q. Nguyen, M. J. Powell, B. Katz, J. Di Carlo, and S. Kim (2019) Optimized jumping on the mit cheetah 3 robot. In 2019 International Conference on Robotics and Automation (ICRA), p. 7448–7454. Cited by: §1. [56] X. Peng, E. Coumans, T. Zhang, T. Lee, J. Tan, and S. Levine Learning agile robotic locomotion skills by imitating animals. arxiv 2020. arXiv preprint arXiv:2004.00784. Cited by: §1. [57] A. Puranic, J. Deshmukh, and S. Nikolaidis (2021) Learning from demonstrations using signal temporal logic. In Conference on Robot Learning, p. 2228–2242. Cited by: §1. [58] M. Raibert, K. Blankespoor, G. Nelson, and R. Playter (2008) Bigdog, the rough-terrain quadruped robot. IFAC Proceedings Volumes 41 (2), p. 10822–10825. Cited by: §1. [59] L. Righetti and A. J. Ijspeert (2008) Pattern generators with sensory feedback for the control of quadruped locomotion. In 2008 IEEE International Conference on Robotics and Automation, p. 819–824. Cited by: §1. [60] G. Schöner, W. Y. Jiang, and J. S. Kelso (1990) A synergetic theory of quadrupedal gaits and gait transitions. Journal of theoretical Biology 142 (3), p. 359–391. Cited by: §1. [61] J. Schulman, S. Levine, P. Abbeel, M. Jordan, and P. Moritz (2015) Trust region policy optimization. In International conference on machine learning, p. 1889–1897. Cited by: §A.2. [62] J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov (2017) Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347. Cited by: §A.2, §4. [63] M. Shafiee, G. Bellegarda, and A. Ijspeert (2024) Manyquadrupeds: learning a single locomotion policy for diverse quadruped robots. In 2024 IEEE International Conference on Robotics and Automation (ICRA), p. 3471–3477. Cited by: §1. [64] Y. Shao, Y. Jin, X. Liu, W. He, H. Wang, and W. Yang (2021) Learning free gait transition for quadruped robots via phase-guided controller. IEEE Robotics and Automation Letters 7 (2), p. 1230–1237. Cited by: §1. [65] H. Sun, J. Yang, Y. Jia, and C. Wang (2024) Online hierarchical planning for multicontact locomotion control of quadruped robots. IEEE/ASME Transactions on Mechatronics 30 (3), p. 1718–1728. Cited by: §1. [66] J. Tan, T. Zhang, E. Coumans, A. Iscen, Y. Bai, D. Hafner, S. Bohez, and V. Vanhoucke (2018) Sim-to-real: learning agile locomotion for quadruped robots. arXiv preprint arXiv:1804.10332. Cited by: §1. [67] E. Todorov, T. Erez, and Y. Tassa (2012) Mujoco: a physics engine for model-based control. In 2012 IEEE/RSJ international conference on intelligent robots and systems, p. 5026–5033. Cited by: §1, §4. [68] V. Tsounis, M. Alge, J. Lee, F. Farshidian, and M. Hutter (2020) Deepgait: planning and control of quadrupedal gaits using deep reinforcement learning. IEEE Robotics and Automation Letters 5 (2), p. 3699–3706. Cited by: §1. [69] L. Wei, Y. Li, Y. Ai, Y. Wu, H. Xu, W. Wang, and G. Hu (2023) Learning multiple-gait quadrupedal locomotion via hierarchical reinforcement learning. International Journal of Precision Engineering and Manufacturing 24 (9), p. 1599–1613. Cited by: §1. [70] M. Wen, R. Ehlers, and U. Topcu (2015) Correct-by-synthesis reinforcement learning with temporal logic constraints. In 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), p. 4983–4990. Cited by: §1. [71] Z. Xie, X. Da, M. Van de Panne, B. Babich, and A. Garg (2021) Dynamics randomization revisited: a case study for quadrupedal locomotion. In 2021 IEEE International Conference on Robotics and Automation (ICRA), p. 4955–4961. Cited by: §1. [72] S. Xu, L. Zhu, and C. P. Ho (2022) Learning efficient and robust multi-modal quadruped locomotion: a hierarchical approach. In 2022 international conference on robotics and automation (ICRA), p. 4649–4655. Cited by: §1. [73] Y. Yang, T. Zhang, E. Coumans, J. Tan, and B. Boots (2022) Fast and efficient locomotion via learned gait transitions. In Conference on robot learning, p. 773–783. Cited by: §1. [74] D. Youm, H. Jung, H. Kim, J. Hwangbo, H. Park, and S. Ha (2023) Imitating and finetuning model predictive control for robust and symmetric quadrupedal locomotion. IEEE Robotics and Automation Letters 8 (11), p. 7799–7806. Cited by: §1. [75] L. Z. Yuan, M. Hasanbeig, A. Abate, and D. Kroening (2019) Modular deep reinforcement learning with temporal logic specifications. arXiv preprint arXiv:1909.11591. Cited by: §1. [76] K. Zakka, B. Tabanpour, Q. Liao, M. Haiderbhai, S. Holt, J. Y. Luo, A. Allshire, E. Frey, K. Sreenath, L. A. Kahrs, et al. (2025) Mujoco playground. arXiv preprint arXiv:2502.08844. Cited by: §2, §4. [77] Y. Zhao, U. Topcu, and L. Sentis (2016) High-level planner synthesis for whole-body locomotion in unstructured environments. In 2016 IEEE 55th Conference on Decision and Control (CDC), p. 6557–6564. Cited by: §1. Appendix A Appendix A.1 STL Specifications We additionally evaluated the two rules described below; however, given the constraints already established in the main text, they did not significantly contribute to the training process or improve overall model performance: • Prior literature frequently constrains the CoM or CoP within the support polygon, defined as the convex hull of all feet currently in contact with the ground. To ensure static or dynamic stability, the respective balance point (CoM or CoP) must remain inside this area. • Another common stability criterion is the enforcement of a slip bound, which limits the tangential motion of a foot during its stance phase. A.2 Proximal Policy Optimization Proximal Policy Optimization (PPO) is an on-policy policy-gradient algorithm that optimizes a clipped surrogate objective to constrain policy updates while enabling multiple epochs of minibatch SGD per rollout batch. PPO is commonly used in locomotion because it is relatively stable under noisy, high-dimensional continuous control, and provides sample-efficient training. The core intuition is to keep each update close to the behavior policy. PPO instantiates this trust-region idea by clipping the importance ratio rather than imposing a hard KL constraint as in TRPO, while retaining advantage-based updates in the spirit of A2C [61, 52, 62]. The surrogate objective function is L(s,a,θk,θ)= L(s,a, _k,θ)= min(πθ(a∣s)πθk(a∣s)Aπθk(s,a), ( _θ(a s) _ _k(a s)\,A _ _k(s,a), (2) clip(πθ(a∣s)πθk(a∣s), 1−ϵ, 1+ϵ)Aπθk(s,a)). \! ( _θ(a s) _ _k(a s),1-ε,1+ε )A _ _k(s,a) ). where θ denotes the current policy parameters and θk _k denotes the pre-update (behavior) policy, Aπθk(s,a)A _ _k(s,a) is the advantage estimate computed under πθk _ _k, and ϵε is the clipping hyperparameter that bounds how far the updated policy may deviate from πθk _ _k via the ratio range [1−ϵ, 1+ϵ][1-ε,\,1+ε]. The policy updates occur via θk+1=argmaxθ(s,a)∼πθk[L(s,a,θk,θ)]. _k+1= *arg\,max_θ\;E_(s,a) _ _k\! [\,L(s,a, _k,θ)\, ]. (3) We leverage Brax’s JAX-based PPO implementation as it is optimized for accelerator-parallel simulation [22]. Domain Randomization The goal of domain randomization is to prevent the reinforcement learning agent from relying too heavily on the exact, nominal parameters of the simulation. In our work, we randomize two critical sets of physical parameters: friction (chosen in the range (0.6,1.4)(0.6,1.4)) and actuator gain and bias (chosen in the range (−,)(-5,5)). This forces the learned policy to cope with slippery or sticky terrains and be robust to inaccurate torque control. Mode selection and hysteresis. A unified locomotion policy must change its preferred gait structure as the commanded forward speed changes. However, directly switching reward templates at a single threshold can cause chattering near the regime boundary. To address this, we use hysteresis in mode selection: the controller switches from walking-trot to trot only when the commanded forward velocity exceeds an upper threshold, and switches back only when it drops below a lower threshold. This separation introduces a buffer zone that prevents rapid back-and-forth mode changes and makes the reward landscape smoother around the transition region. Algorithm 1 Mode-dependent STL reward learning 1:Collect rollouts for low, mid, and high speed regimes; 2:Extract safety and gait-structure features (contacts, stride period, duty factor, phase error, CoM/CoP, slip). 3:Fit PSTL template parameters θW,θT,θB _W, _T, _B from the datasets. 4:for each PPO step do 5: Update mode g(t)g(t) from vxcmd(t)v_x^cmd(t) using hysteresis. 6: Update rolling buffers over horizon HgH_g. 7: Compute ρsafe,g(t)(t) _safe,g(t)(t), ρtrack,g(t)(t) _track,g(t)(t) and ρg(t)(t) _g(t)(t) via softmin windowed robustness. 8: Compute reward rtr_t from bounded robustness and optional effort penalty. 9: PPO policy update. 10:end for Table 4: PPO training hyperparameters used in our experiments. Hyperparameter Value Number of timesteps 200,000,000 Number of evaluations 10 Reward scaling 1 Episode length 1000 Normalize observations True Action repeat 1 Unroll length 30 Number of minibatches 32 Number of updates per batch 4 Discount factor 0.955 Learning rate 0.00015 Entropy cost 0.004 Number of environments 8192 Batch size 256 Table 5: Mode-dependent grouped reward weights and tanh saturation parameters. Parameter Walk Trot Bound wsafew_safe 1.0 1.0 1.0 wtrackw_track 1.0 1.0 1.15 wpatternw_pattern 1.1 1.1 1.3 αsafe _safe 0.9 0.6 0.8 αtrack _track 0.8 0.7 0.8 αpattern _pattern 1.2 0.4 0.7 Torque regularization coefficient weffortw_effort 1×10−61× 10^-6 A.3 Evaluation Under Mixed Velocity Commands Table 6 shows the evaluation results for the learned unified model with the heuristic-best baseline under commanded forward velocities vxv_x ∈ 0.3,0.5,0.7,1.0,1.3,1.6,1.9,2.0,2.1ms-1\0.3,0.5,0.7,1.0,1.3,1.6,1.9,2.0,2.1\\ ms -1, and additionally lateral-velocity and yaw-rate commands from (vy⋆∈[−0.4,0.4],m,s−1)(v_y ∈[-0.4,0.4],m,s^-1) and (ωz⋆∈[−0.4,0.4],rad,s−1)( _z ∈[-0.4,0.4],rad,s^-1), respectively. For each setting, we run 2020 independent rollouts, each with a horizon of 500500 time steps. Table 6: Evaluation under mixed velocity commands. We compare the learned unified model with the heuristic-best baseline across commanded forward velocities while additionally sampling lateral-velocity and yaw-rate commands from (vy⋆∈[−0.4,0.4],m,s−1)(v_y ∈[-0.4,0.4],m,s^-1) and (ωz⋆∈[−0.4,0.4],rad,s−1)( _z ∈[-0.4,0.4],rad,s^-1), respectively. This setting evaluates robustness beyond straight-line forward locomotion. Lower CoT is better; higher survival and success rates are better. STL-based unified model Heuristic-best vxv_x CoT ↓ Survival ↑ Success ↑ CoT ↓ Survival ↑ Success ↑ 0.30 1.87 ± 0.06 1.00 1.00 2.55 ± 0.21 1.00 0.00 0.50 1.46 ± 0.04 1.00 1.00 2.11 ± 0.11 1.00 0.35 0.70 1.24 ± 0.02 1.00 1.00 1.83 ± 0.07 1.00 1.00 1.00 1.21 ± 0.02 1.00 1.00 1.74 ± 0.06 1.00 1.00 1.30 1.10 ± 0.01 1.00 1.00 1.76 ± 0.05 1.00 1.00 1.60 1.07 ± 0.01 1.00 1.00 1.74 ± 0.05 1.00 1.00 1.90 1.11 ± 0.01 1.00 1.00 1.72 ± 0.05 1.00 0.00 2.00 1.12 ± 0.01 1.00 0.80 1.69 ± 0.06 1.00 0.00 2.10 1.13 ± 0.01 1.00 0.00 1.69 ± 0.15 0.90 0.00 Table 7: Mode-dependent STL predicate thresholds and related configuration. Parameter Walk Trot Bound Effective horizon HmH_m 30 24 24 Warm-up minimum valid steps 8 8 8 Aggregation sharpness β 0.5 0.5 0.1 Walk→ enter threshold on |vx||v_x| [m/s] 0.72 – Trot→ exit threshold on |vx||v_x| [m/s] 0.65 – Trot→ enter threshold on |vx||v_x| [m/s] – 1.75 Bound→ exit threshold on |vx||v_x| [m/s] – 1.45 Commanded vxv_x range [m/s] [0.0, 1.9] Commanded vyv_y range [m/s] [-0.2, 0.2] Commanded yaw range [rad/s] [-0.2, 0.2] Velocity tracking tolerance ϵvx _v_x [m/s] 0.55 0.60 0.60 Velocity tracking tolerance ϵvy _v_y [m/s] 0.05 0.05 0.05 Yaw-rate tracking tolerance ϵω _ω [rad/s] 0.05 0.05 0.05 Minimum required contacts 2 2 - Minimum CoM height [m] 0.18 0.22 0.16 Maximum roll magnitude [deg] 10.0 7.0 15.0 Maximum pitch magnitude [deg] 8.0 7.0 15.0 Maximum diagonal phase error 0.10 0.11 - Minimum diagonal 2-contact purity 0.92 0.99 - Maximum diagonal 2-contact purity - - 0.03 Minimum 2-contact fraction - 0.70 - Recent 3+ contact requirement window K 11 - - Minimum flight fraction - - 0.04 Minimum front-only fraction - - 0.18 Minimum hind-only fraction - - 0.16 Maximum all 4 contact fraction - - 0.30 Minimum all 4 contact fraction - - 0.10