pith. sign in

arxiv: 2503.05792 · v3 · pith:QCVVQC4Pnew · submitted 2025-02-28 · 📡 eess.SY · cs.SY

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

Roland Ilyes , Lara Bruderm\"uller , Nick Hawes , Bruno Lacerda This is my paper

Pith reviewed 2026-05-23 01:12 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords signal temporal logicrobustness semanticsmodel predictive controlformula progressionrobot controlreactive control
0
0 comments X

The pith

A new Signal Temporal Logic semantics called robustness-to-go isolates future trajectory contributions to enable better decisions in model predictive control.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Standard STL robustness depends on the entire history of a trajectory, which restricts how robots can replan in model predictive control loops. The paper defines robustness-to-go to measure only the contribution of the remaining suffix trajectory after formula progression. This new measure is shown to depend solely on the suffix and the progressed formula, allowing online use inside MPC without carrying history forward. When implemented as the MPC objective, the approach produces higher task success rates than standard STL robustness in the reported simulations.

Core claim

Robustness-to-go is a quantitative semantics for Signal Temporal Logic that isolates the contributions of suffix trajectories, depends only on the suffix and the progressed formula, and yields higher success rates when used as the objective inside model predictive control compared with traditional STL robustness.

What carries the argument

robustness-to-go semantics for STL, which measures suffix contributions and is computed online via formula progression

Load-bearing premise

That replacing standard STL robustness with robustness-to-go inside an MPC loop will produce measurably higher task success rates under the tested conditions.

What would settle it

A side-by-side simulation run of the same MPC controller and tasks where robustness-to-go achieves the same or lower success rate than standard STL robustness.

Figures

Figures reproduced from arXiv: 2503.05792 by Bruno Lacerda, Lara Bruderm\"uller, Nick Hawes, Roland Ilyes.

Figure 1
Figure 1. Figure 1: This examples shows a robot planning a path to the [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Control Block Diagram for Ro-To-Go MPC with [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces Signal Temporal Logic robustness-to-go (Ro-To-Go), a new quantitative semantics isolating suffix trajectory contributions. It proves the relationship to Metric Temporal Logic formula progression, shows dependence only on the suffix and progressed formula, implements Ro-To-Go as the objective in an MPC algorithm using progression for online evaluation, and reports simulation experiments with higher task success rates than MPC using traditional STL robustness.

Significance. If the claims hold, the work provides a useful refinement for STL-based optimal control by enabling purely forward-looking decisions in MPC, which may improve reactivity in robotic applications. The explicit proof connecting Ro-To-Go to MTL progression and the empirical validation constitute clear strengths supporting the approach's potential.

major comments (1)
  1. [Experiments] Experiments section: The baseline is described only as 'MPC using traditional STL robustness' without stating whether it also employs formula progression (or equivalent suffix-only evaluation). Because the proposed method relies on progression to evaluate Ro-To-Go, observed gains in success rate cannot be unambiguously attributed to the new semantics rather than the progression technique itself. This directly affects the central experimental claim.
minor comments (2)
  1. [Abstract] Abstract: The construction 'use[s]' is a typographical artifact and should read 'uses'.
  2. [Definition of Ro-To-Go] Ensure that all definitions of robustness measures are accompanied by explicit notation for the time interval and signal suffix to avoid ambiguity when comparing Ro-To-Go to standard STL robustness.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their detailed review and constructive comment. We address the major point on the experimental baseline below and will revise the manuscript to improve clarity.

read point-by-point responses

  1. Referee: [Experiments] Experiments section: The baseline is described only as 'MPC using traditional STL robustness' without stating whether it also employs formula progression (or equivalent suffix-only evaluation). Because the proposed method relies on progression to evaluate Ro-To-Go, observed gains in success rate cannot be unambiguously attributed to the new semantics rather than the progression technique itself. This directly affects the central experimental claim.

    Authors: We agree that the baseline description should be clarified to support unambiguous attribution of the observed gains. In the reported experiments, the baseline implements MPC with standard STL robustness computed over the full predicted trajectory and does not employ formula progression. Progression is applied specifically to enable efficient, suffix-only evaluation of Ro-To-Go. We will revise the Experiments section to state this distinction explicitly and to discuss how the comparison isolates the contribution of the new semantics. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper defines a new quantitative semantics (Ro-To-Go) for STL that isolates suffix contributions, states a proof relating it to MTL formula progression, and implements the semantics via progression in MPC for online evaluation. The experimental comparison is to MPC using traditional STL robustness (an external baseline). No equations or claims reduce a derived quantity to a fitted input by construction, no load-bearing self-citations are invoked to justify uniqueness or ansatzes, and the central result does not rename a known pattern or import uniqueness from prior author work. The derivation chain is therefore independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no concrete free parameters, axioms, or invented entities; ledger left empty pending full text.

pith-pipeline@v0.9.0 · 5665 in / 1014 out tokens · 42248 ms · 2026-05-23T01:12:24.064201+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

  1. [1]

    Rescher and A

    N. Rescher and A. Urquhart, Temporal logic. Springer Science & Business Media, 2012, vol. 3

    work page 2012

  2. [2]

    The temporal logic of programs,

    A. Pnueli, “The temporal logic of programs,” in 18th annual symposium on foundations of computer science (sfcs 1977) . ieee, 1977, pp. 46–57

    work page 1977

  3. [3]

    Specifying real-time properties with metric temporal logic,

    R. Koymans, “Specifying real-time properties with metric temporal logic,” Real-time systems, vol. 2, no. 4, pp. 255–299, 1990

    work page 1990

  4. [4]

    The benefits of relaxing punctuality,

    R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing punctuality,” Journal of the ACM (JACM) , vol. 43, no. 1, pp. 116–146, 1996

    work page 1996

  5. [5]

    Monitoring temporal properties of continuous signals,

    O. Maler and D. Nickovic, “Monitoring temporal properties of continuous signals,” in International symposium on formal techniques in real-time and fault-tolerant systems . Springer, 2004, pp. 152–166

    work page 2004

  6. [6]

    Robust satisfaction of temporal logic over real-valued signals,

    A. Donz ´e and O. Maler, “Robust satisfaction of temporal logic over real-valued signals,” in International Conference on Formal Modeling and Analysis of Timed Systems . Springer, 2010, pp. 92–106

    work page 2010

  7. [7]

    Model predictive control with signal temporal logic specifications,

    V . Raman, A. Donz´e, M. Maasoumy, R. M. Murray, A. Sangiovanni- Vincentelli, and S. A. Seshia, “Model predictive control with signal temporal logic specifications,” in 53rd IEEE Conference on Decision and Control, 2014, pp. 81–87

    work page 2014

  8. [8]

    Arithmetic-geometric mean robustness for control from signal temporal logic specifications,

    N. Mehdipour, C.-I. Vasile, and C. Belta, “Arithmetic-geometric mean robustness for control from signal temporal logic specifications,” in 2019 American Control Conference (ACC) . IEEE, 2019, pp. 1690– 1695

    work page 2019

  9. [9]

    Formal methods for control synthesis: An optimization perspective,

    C. Belta and S. Sadraddini, “Formal methods for control synthesis: An optimization perspective,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, no. 1, pp. 115–140, 2019

    work page 2019

  10. [10]

    Smooth operator: Control using the smooth robustness of temporal logic,

    Y . V . Pant, H. Abbas, and R. Mangharam, “Smooth operator: Control using the smooth robustness of temporal logic,” in 2017 IEEE Conference on Control Technology and Applications (CCTA) . IEEE, 2017, pp. 1235–1240

    work page 2017

  11. [11]

    Planning for temporally extended goals,

    F. Bacchus and F. Kabanza, “Planning for temporally extended goals,” Annals of Mathematics and Artificial Intelligence , vol. 22, pp. 5–27, 1998

    work page 1998

  12. [12]

    Optimization-based trajectory generation with linear temporal logic specifications,

    E. M. Wolff, U. Topcu, and R. M. Murray, “Optimization-based trajectory generation with linear temporal logic specifications,” in 2014 IEEE International Conference on Robotics and Automation (ICRA) . IEEE, 2014, pp. 5319–5325

    work page 2014

  13. [13]

    Computing descent direction of mtl robust- ness for non-linear systems,

    H. Abbas and G. Fainekos, “Computing descent direction of mtl robust- ness for non-linear systems,” in 2013 American Control Conference . IEEE, 2013, pp. 4405–4410

    work page 2013

  14. [14]

    Fly-by-logic: Control of multi-drone fleets with temporal logic objectives,

    Y . V . Pant, H. Abbas, R. A. Quaye, and R. Mangharam, “Fly-by-logic: Control of multi-drone fleets with temporal logic objectives,” in 2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 2018, pp. 186–197

    work page 2018

  15. [15]

    A smooth robustness measure of signal temporal logic for symbolic control,

    Y . Gilpin, V . Kurtz, and H. Lin, “A smooth robustness measure of signal temporal logic for symbolic control,” IEEE Control Systems Letters, vol. 5, no. 1, pp. 241–246, 2020

    work page 2020

  16. [16]

    Continuous optimization- based task and motion planning with signal temporal logic specifications for sequential manipulation,

    R. Takano, H. Oyama, and M. Yamakita, “Continuous optimization- based task and motion planning with signal temporal logic specifications for sequential manipulation,” in 2021 IEEE international conference on robotics and automation (ICRA) . IEEE, 2021, pp. 8409–8415

    work page 2021

  17. [17]

    Generalized mean robustness for signal temporal logic,

    N. Mehdipour, C.-I. Vasile, and C. Belta, “Generalized mean robustness for signal temporal logic,” IEEE Transactions on Automatic Control , 2024

    work page 2024

  18. [18]

    Robust control for signal temporal logic specifications using discrete average space robustness,

    L. Lindemann and D. V . Dimarogonas, “Robust control for signal temporal logic specifications using discrete average space robustness,” Automatica, vol. 101, pp. 377–387, 2019

    work page 2019

  19. [19]

    Model checking real-time systems,

    P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, J. Ouaknine, and J. Worrell, “Model checking real-time systems,” Handbook of model checking, pp. 1001–1046, 2018

    work page 2018

  20. [20]

    Temporal logic robustness for general signal classes,

    H. Abbas, Y . V . Pant, and R. Mangharam, “Temporal logic robustness for general signal classes,” in Proceedings of the 22nd ACM Interna- tional Conference on Hybrid Systems: Computation and Control , 2019, pp. 45–56

    work page 2019

  21. [21]

    Ro-to-go! robust reactive control with signal temporal logic,

    Ilyes, R. et al., “Ro-to-go! robust reactive control with signal temporal logic,” arXiv preprint, 2025

    work page 2025

  22. [22]

    Breach, a toolbox for verification and parameter synthesis of hybrid systems,

    A. Donz ´e, “Breach, a toolbox for verification and parameter synthesis of hybrid systems,” in Computer Aided Verification, T. Touili, B. Cook, and P. Jackson, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 167–170

    work page 2010

  23. [23]

    Vp-sto: Via-point-based stochastic trajectory optimization for reactive robot behavior,

    J. Jankowski, L. Bruderm ¨uller, N. Hawes, and S. Calinon, “Vp-sto: Via-point-based stochastic trajectory optimization for reactive robot behavior,” in 2023 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2023, pp. 10 125–10 131

    work page 2023

  24. [24]

    The cma evolution strategy: A tutorial

    N. Hansen, “The cma evolution strategy: A tutorial.”

    work page

  25. [25]

    Donz ´e, Decyphir et

    A. Donz ´e, Decyphir et. al. Stlrom. [Online]. Available: https: //github.com/decyphir/STLRom

    work page

  26. [26]

    Robotic operating system

    Stanford Artificial Intelligence Laboratory et al. Robotic operating system. [Online]. Available: https://www.ros.org

    work page

  27. [27]

    Robust online monitoring of signal temporal logic,

    J. V . Deshmukh, A. Donz´e, S. Ghosh, X. Jin, G. Juniwal, and S. A. Seshia, “Robust online monitoring of signal temporal logic,” Formal Methods in System Design , vol. 51, pp. 5–30, 2017. APPENDIX I PROOFS A. Proof of Theorem 1 A signal s satisfies an STL formula if and only if it has a positive robustness to go, i.e. (s, t) ⊨ φ ⇐ ⇒ ρ↬(s, t, ˆt, φ) > 0 Pr...

    work page 2017