Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Ro-To-Go! Robust Reactive Control with Signal Temporal Logic

Roland Ilyes, Lara Brudermüller, Nick Hawes, Bruno Lacerda

TL;DR

Ro-To-Go introduces a suffix-focused robustness-to-go $\rho^{\looparrowright}$ for Signal Temporal Logic (STL) to improve reactive model-predictive control in robotics. The approach proves a formal link between Ro-To-Go and STL formula progression, enabling efficient online computation by progressively updating the specification. In simulations with dynamic disturbances, Ro-To-Go outperforms traditional STL robustness by yielding higher task success rates and safer trajectories, validating its practical value for real-time MPC. The work lays a theoretical and algorithmic foundation for suffix-based robustness and points to future work connecting Ro-To-Go with Robust Satisfaction Interval (RoSI) and related concepts.

Abstract

Signal Temporal Logic (STL) robustness is a common objective for optimal robot control, but its dependence on history limits the robot's decision-making capabilities when used in Model Predictive Control (MPC) approaches. In this work, we introduce Signal Temporal Logic robustness-to-go (Ro-To-Go), a new quantitative semantics for the logic that isolates the contributions of suffix trajectories. We prove its relationship to formula progression for Metric Temporal Logic, and show that the robustness-to-go depends only on the suffix trajectory and progressed formula. We implement robustness-to-go as the objective in an MPC algorithm and use formula progression to efficiently evaluate it online. We test the algorithm in simulation and compare it to MPC using traditional STL robustness. Our experiments show that using robustness-to-go results in a higher success rate.

Ro-To-Go! Robust Reactive Control with Signal Temporal Logic

TL;DR

Ro-To-Go introduces a suffix-focused robustness-to-go for Signal Temporal Logic (STL) to improve reactive model-predictive control in robotics. The approach proves a formal link between Ro-To-Go and STL formula progression, enabling efficient online computation by progressively updating the specification. In simulations with dynamic disturbances, Ro-To-Go outperforms traditional STL robustness by yielding higher task success rates and safer trajectories, validating its practical value for real-time MPC. The work lays a theoretical and algorithmic foundation for suffix-based robustness and points to future work connecting Ro-To-Go with Robust Satisfaction Interval (RoSI) and related concepts.

Abstract

Signal Temporal Logic (STL) robustness is a common objective for optimal robot control, but its dependence on history limits the robot's decision-making capabilities when used in Model Predictive Control (MPC) approaches. In this work, we introduce Signal Temporal Logic robustness-to-go (Ro-To-Go), a new quantitative semantics for the logic that isolates the contributions of suffix trajectories. We prove its relationship to formula progression for Metric Temporal Logic, and show that the robustness-to-go depends only on the suffix trajectory and progressed formula. We implement robustness-to-go as the objective in an MPC algorithm and use formula progression to efficiently evaluate it online. We test the algorithm in simulation and compare it to MPC using traditional STL robustness. Our experiments show that using robustness-to-go results in a higher success rate.

Paper Structure

This paper contains 18 sections, 88 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Problem Formulation
  5. Ro-To-Go!
  6. Formula Progression for STL Ro-To-Go
  7. Experiments
  8. Results
  9. Conclusion and Future Work
  10. Proofs
  11. Proof of Theorem \ref{['thm: RoToGoSound']}
  12. When $\hat{t}$ is less than $t_k$
  13. Pointwise supremum of a function of a signal
  14. When $\hat{t}$ is equal to $t_k$
  15. When $\hat{t}$ is greater than $t_k$
  16. ...and 3 more sections

Figures (3)

  • Figure 1: This examples shows a robot planning a path to the goal while avoiding the human. With regular robustness, the proximity to the obstacles at the beginning limits the overall robustness, so there is no value in going further away from the human. With robustness-to-go, the robot has forgotten about its past proximity to the obstacles and can find trajectories that are more robust to human movement.
  • Figure 2: Control Block Diagram for Ro-To-Go MPC with Formula Progression
  • Figure 3: Sample trajectories for both formulas, simulated with a static environment