  This study proposes a novel planning framework based on a model predictive
control formulation that incorporates signal temporal logic (STL)
specifications for task completion guarantees and robustness quantification.
This marks the first-ever study to apply STL-guided trajectory optimization for
bipedal locomotion push recovery, where the robot experiences unexpected
disturbances. Existing recovery strategies often struggle with complex task
logic reasoning and locomotion robustness evaluation, making them susceptible
to failures caused by inappropriate recovery strategies or insufficient
robustness. To address this issue, the STL-guided framework generates optimal
and safe recovery trajectories that simultaneously satisfy the task
specification and maximize the locomotion robustness. Our framework outperforms
a state-of-the-art locomotion controller in a high-fidelity dynamic simulation,
especially in scenarios involving crossed-leg maneuvers. Furthermore, it
demonstrates versatility in tasks such as locomotion on stepping stones, where
the robot must select from a set of disjointed footholds to maneuver
successfully.
