We present an integrated planning framework for quadrupedal locomotion over discrete, unforeseen terrain configurations revealed at runtime. Existing methods often depend on heuristics for real-time foothold selection—limiting robustness and adaptability—or rely on computationally intensive trajectory optimization across complex terrains and long horizons. In contrast, our approach combines reactive synthesis for generating correct-by-construction symbolic-level controllers with mixed-integer convex programming (MICP) for physically feasible footstep planning during each symbolic transition. To reduce the reliance on costly MICP solves and accommodate specifications that may be violated due to physical infeasibility, we adopt a symbolic repair mechanism that selectively generates only the required symbolic transitions. During execution, real-time MICP replanning based on actual terrain data, runtime symbolic repair, kinematic-feasibility re-targeting, and a delay-aware coordination scheme enable seamless bridging between offline synthesis and online operation. Through extensive simulation and hardware experiments, we validate the framework's ability to identify missing locomotion skills and respond effectively in safety-critical environments, including scattered stepping stones and rebar scenarios.
Approach Summary
Fig. 1 System architecture overview. Solid lines indicate online communication; dashed lines represent offline processes. Request goals are user-defined in the offline phase and provided by a global planner in the online phase.
We manage complexity at both the symbolic and physical levels. At the symbolic level, reactive synthesis decomposes local navigation into manageable subproblems whose solutions are reusable across scenarios; each subproblem is a short-horizon symbolic transition. At the physical level, each transition is validated by a mixed-integer convex program (MICP) that certifies dynamic and kinematic feasibility. This symbolic guidance limits the planning horizon and the number of terrain features any single MICP must consider, mitigating the poor scaling of pure mixed-integer planning.
Offline, gait-free MICP precomputes a diverse set of locomotion skills (e.g., trotting and leaping gaits) for predefined terrain states and goals. A high-level manager fixes the local terrain/goal context and retains only the skills relevant to the current environment, while symbolic repair—equipped with dynamic-feasibility checks—generates only the missing transitions that need to be verified. Online, a lightweight gait-fixed MICP is re-solved against the actually perceived terrain at each transition. Runtime symbolic repair handles previously unseen terrain, kinematic-feasibility re-targeting adjusts the desired pose to match real geometry, and a delay-aware coordination scheme keeps the discrete strategy automaton and the continuous-time tracking controller consistent under variable MICP solve times.
Key contributions
- Integrated reactive-synthesis + MICP framework bridging high-level symbolic reasoning with low-level physical feasibility.
- Scalable offline synthesis. The high-level manager reduces the symbolic state space by 80.9–90.1%; symbolic repair with gait-free MICP feasibility checks generates only necessary skills, cutting costly gait-free MICP solves by 71.6–97.6% versus exhaustive enumeration.
- Online execution module with delay-aware coordination, kinematic-feasibility re-targeting, online collision-avoidance constraints, and runtime symbolic repair.
- Comprehensive validation across four simulated terrain scenarios, benchmarks against pure-MIP and heuristic planners, and hardware deployment on two robots (Unitree Go2 and SkyMul Chotu).
