Receding Horizon Control for Signal Temporal Logic Using Robustness-Conserving Partial Formula Evaluation
Roland Ilyes, Lara Brudermüller, Nick Hawes, Bruno Lacerda
AI summary
Problem
Receding horizon control for Signal Temporal Logic typically requires unbounded memory of past trajectories or is limited to a narrow subset of unbounded specifications, hindering long-term operation in dynamic environments.
Approach
The method applies syntactic separation to partially evaluate STL formulas, extracting past robustness into new predicates. This allows a nonlinear program to optimize future control inputs over a finite horizon while conserving specification satisfaction with bounded memory.
Key results
- Bounded-memory receding horizon control formulation for arbitrary STL specifications
- Robustness-conserving formula rewriting technique via syntactic separation
- Online update equations for partially evaluated formulas during closed-loop execution
- Demonstrated scalability and effectiveness over state-of-the-art methods in dynamic environment case studies
Why it matters
Enables robots to reliably execute complex, long-horizon temporal logic tasks in unpredictable environments without memory overflow or computational bottlenecks.
Abstract
We present a bounded-memory receding horizon approach to robot control for complex specifications in dynamic environments. We use Signal Temporal Logic, a logic that quantifies how robustly trajectories satisfy the specification, to specify robot behavior. To handle unbounded specifications, we consider a short planning horizon, only searching for nonviolating trajectories. We identify the subset of Signal Temporal Logic for which this approach needs only a bounded memory of the past, and leverage syntactic separation to summarize the robust satisfaction of the trajectory as it evolves. We implement our ap- proach using receding horizon control in dynamic environments. We demonstrate the effectiveness and scalability of our approach compared to the state-of-the-art approach in several case studies.