This study investigates formal-method-based trajectory optimization (TO) for bipedal locomotion, focusing on scenarios where the robot encounters external perturbations at unforeseen times. Our key research question centers around the assurance of task specification correctness and the maximization of specification robustness for a bipedal robot in the presence of external perturbations. Our contribution includes the design of an optimization-based task and motion planning framework that generates optimal control sequences with formal guarantees of external perturbation recovery. As a core component of the framework, a model predictive controller (MPC) encodes signal temporal logic (STL)-based task specifications as a cost function. In particular, we investigate challenging scenarios where the robot is subjected to lateral perturbations that increase the risk of failure due to leg self-collision. To address this, we synthesize agile and safe crossed-leg maneuvers to enhance locomotion stability. This work marks the first study to incorporate formal guarantees offered by STL into a TO for perturbation recovery of bipedal locomotion. We demonstrate the efficacy of the framework via perturbation experiments in simulations.

翻译：本研究探索了基于形式化方法的双足行走轨迹优化（TO），重点关注机器人在未知时刻遭遇外部扰动的场景。核心研究问题围绕在存在外部扰动的情况下，如何确保双足机器人的任务规范正确性并最大化规范鲁棒性。我们的贡献在于设计了一个基于优化的任务与运动规划框架，该框架能够生成具有外部扰动恢复形式化保证的最优控制序列。作为该框架的核心组件，模型预测控制器（MPC）将基于信号时态逻辑（STL）的任务规范编码为代价函数。特别地，我们研究了机器人遭受横向扰动的挑战性场景——此类扰动因腿部自碰撞风险增加而易导致失败。为此，我们综合运用了敏捷且安全的交叉步态来增强运动稳定性。本研究首次将STL的形式化保证纳入双足行走扰动恢复的轨迹优化中。我们通过仿真中的扰动实验验证了该框架的有效性。