Physically-Feasible Reactive Synthesis for Terrain-Adaptive Locomotion via Trajectory Optimization and Symbolic Repair

TL;DR

The paper presents a hybrid planning framework for terrain-adaptive locomotion that combines GR(1) reactive synthesis with MICP-based motion primitives to guarantee safety and feasibility on dynamic terrains. Offline, it builds a strategy by solving gait-fixed MICPs for a predefined set of terrains and uses symbolic repair to fill unrealizable gaps, then extends to gait-free MICPs to adapt gaits. Online, it re-solves MICPs with real terrain data and performs online symbolic repair to handle unseen conditions, complemented by an NMPC-WBC tracking stack for precise execution. The approach demonstrates robust performance in simulation and hardware on unstructured terrains and rebar environments, offering a scalable path toward safe, adaptable legged locomotion with formal guarantees. The work advances terrain-aware locomotion by tightly integrating symbolic planning with continuous feasibility checks and online adaptation, enabling safe and responsive behaviors in safety-critical settings.

Abstract

We propose an integrated planning framework for quadrupedal locomotion over dynamically changing, unforeseen terrains. Existing approaches either rely on heuristics for instantaneous foothold selection--compromising safety and versatility--or solve expensive trajectory optimization problems with complex terrain features and long time horizons. In contrast, our framework leverages reactive synthesis to generate correct-by-construction controllers at the symbolic level, and mixed-integer convex programming (MICP) for dynamic and physically feasible footstep planning for each symbolic transition. We use a high-level manager to reduce the large state space in synthesis by incorporating local environment information, improving synthesis scalability. To handle specifications that cannot be met due to dynamic infeasibility, and to minimize costly MICP solves, we leverage a symbolic repair process to generate only necessary symbolic transitions. During online execution, re-running the MICP with real-world terrain data, along with runtime symbolic repair, bridges the gap between offline synthesis and online execution. We demonstrate, in simulation, our framework's capabilities to discover missing locomotion skills and react promptly in safety-critical environments, such as scattered stepping stones and rebars.

Figures (12)

• Figure 1: Terrain abstraction and skill definition. (a) Top-down view of the real-world terrain before abstraction. The red polygons denote the segmented terrain polygons. (b) Abstraction of the terrain and robot's skills (pink) moving from one location to another. (c) Repair process to find a new skill (blue).
• Figure 2: System architecture overview. The solid lines indicate online communication, while dashed lines represent offline processes.$\bm{\epsilon}$
• Figure 3: Demonstration of decision variables and polygons when solving MICP for skill $a_0$ in Example \ref{['example:1']} using a trotting locomotion gait.
• Figure 4: System overview for offline synthesis and online execution modules. During the offline synthesis (pink solid arrows), an initial set of motion primitives is given and symbolic skills are iteratively generated by solving MICP. When the task specifications are unrealizable, a symbolic repair is triggered to seek missing skills. During the online execution (black solid arrows), MICP is solved again taking online terrain segments and the symbolic state only advances when a solution is found. Online repair is triggered (blue solid arrows) when a solving failure or an unseen terrain is detected.
• Figure 5: Demonstrations of (a) offline MICP for a skill transitioning from a flat terrain to a high terrain with predefined polygons; (b) online MICP for the same skill but with online terrain polygons.