pith. sign in

arxiv: 2603.29868 · v2 · pith:DBYXJSMOnew · submitted 2026-01-28 · 💻 cs.AI · cs.LO

Spatiotemporal Robustness of Temporal Logic Tasks using Multi-Objective Reasoning

Oliver Sch\"on , Lars Lindemann This is my paper

Pith reviewed 2026-05-21 14:59 UTC · model grok-4.3

classification 💻 cs.AI cs.LO
keywords spatiotemporal robustnesstemporal logicmulti-objective optimizationrobust semanticsmonitoring algorithmsautonomous systemspartial orderPareto optimality
0
0 comments X

The pith

Spatiotemporal robustness captures joint spatial and temporal perturbations for temporal logic specifications using multi-objective reasoning.

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

The paper proposes spatiotemporal robustness (STR) to measure how well a discrete-time signal satisfies a temporal logic specification under both spatial and temporal changes at once. This matters for autonomous and interacting systems such as multi-agent robotics, smart cities, and air traffic control, where both the position and the timing of events affect whether a task is met. STR is defined as a multi-objective reasoning problem that uses a partial order over pairs of spatial and temporal perturbations. The resulting Pareto-optimal set describes every admissible perturbation that still keeps the specification satisfied. To keep the idea practical, the authors introduce sound robust semantics that under-approximate the true STR while remaining computationally tractable and supply monitoring algorithms built on those semantics.

Core claim

We define STR as a multi-objective reasoning problem, formalized via a partial order over spatial and temporal perturbations. This perspective has two key advantages: STR can be interpreted as a Pareto-optimal set that characterizes all admissible spatiotemporal perturbations, and STR can be computed using tools from multi-objective optimization. To navigate computational challenges, we propose robust semantics for STR that are sound in the sense of suitably under-approximating STR while being computationally tractable. Finally, we present monitoring algorithms for STR using these robust semantics.

What carries the argument

Spatiotemporal robustness (STR) formalized as a multi-objective reasoning problem over a partial order on spatial and temporal perturbation pairs.

If this is right

  • STR can be interpreted as a Pareto-optimal set that characterizes all admissible spatiotemporal perturbations.
  • STR can be computed using tools from multi-objective optimization.
  • Robust semantics under-approximate STR in a sound manner while staying computationally tractable.
  • Monitoring algorithms can be built on the robust semantics without losing essential guarantees.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Adoption could allow verification tools to jointly account for position and timing errors in multi-agent settings.
  • The same multi-objective view might later be applied to continuous-time or hybrid-system specifications.
  • Integration with existing temporal-logic monitors could improve robustness analysis for traffic or urban systems.

Load-bearing premise

The proposed robust semantics suitably under-approximate the true STR while remaining computationally tractable.

What would settle it

A concrete signal and temporal logic formula where the value returned by the robust semantics differs from the actual joint spatial-temporal distance to the nearest violation.

Figures

Figures reproduced from arXiv: 2603.29868 by Lars Lindemann, Oliver Sch\"on.

Figure 1
Figure 1. Figure 1: Motivation for spatiotemporal robustness. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: F-16 fighter jet flight path (nominal and 10 perturbed paths), no-fly zone [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Left panel: Two Pareto optimal sets D1 (red line) and D2 (blue line) and their downward closures D1 ↓ (red shaded area) and D2 ↓ (blue shaded area). Middle panel: The minimum of D1 and D2 , i.e., min{D1 , D2} := max{D1 ↓∩D2 ↓ }. Right panel: The maximum of D1 and D2 , i.e., max{D1 , D2} := max{D1 ∪D2}. The downward closure is used for the definition of min{D1 , D2}, while it is not needed for the definitio… view at source ↗
Figure 4
Figure 4. Figure 4: Parse tree of the fighter-jet benchmark specification. [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Spatiotemporal robustness of the fighter jet example. [PITH_FULL_IMAGE:figures/full_fig_p017_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Spatiotemporal robustness of the robotaxi example. [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗
read the original abstract

The reliability of autonomous systems depends on their robustness, i.e., their ability to meet their objectives under uncertainty. In this paper, we study spatiotemporal robustness of temporal logic specifications evaluated over discrete-time signals. Existing work has proposed robust semantics that capture not only Boolean satisfiability, but also the geometric distance from unsatisfiability, corresponding to admissible spatial perturbations of a given signal. In contrast, we propose spatiotemporal robustness (STR), which captures admissible spatial and temporal perturbations jointly. This notion is particularly informative for interacting systems, such as multi-agent robotics, smart cities, and air traffic control. We define STR as a multi-objective reasoning problem, formalized via a partial order over spatial and temporal perturbations. This perspective has two key advantages: (1) STR can be interpreted as a Pareto-optimal set that characterizes all admissible spatiotemporal perturbations, and (2) STR can be computed using tools from multi-objective optimization. To navigate computational challenges, we propose robust semantics for STR that are sound in the sense of suitably under-approximating STR while being computationally tractable. Finally, we present monitoring algorithms for STR using these robust semantics. To the best of our knowledge, this is the first work to deal with robustness across multiple dimensions via multi-objective reasoning.

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 proposes spatiotemporal robustness (STR) for temporal logic specifications over discrete-time signals. STR is defined as a multi-objective reasoning problem via a partial order on joint spatial and temporal perturbations, yielding a Pareto-optimal set of admissible perturbations. The authors introduce robust semantics that under-approximate the true STR in a computationally tractable manner and present monitoring algorithms based on these semantics. The work targets applications in multi-agent robotics, smart cities, and air traffic control, claiming to be the first to address multi-dimensional robustness through multi-objective optimization.

Significance. If the soundness of the under-approximating semantics holds for general formulas and the monitoring algorithms scale, the framework could meaningfully extend existing robust semantics (which treat space and time separately) to joint perturbations. This would be particularly useful for systems where spatial and temporal deviations interact, such as in coordinated multi-agent tasks. The multi-objective Pareto perspective is a natural and potentially reusable modeling choice.

major comments (1)
  1. [§4] §4 (Robust Semantics): The central claim that the proposed robust semantics suitably under-approximate the true STR (Pareto set over joint perturbations) while remaining tractable is load-bearing but not fully established for general formulas. For operators such as 'until', where spatial and temporal aspects couple through the signal dynamics, combining spatial and temporal robustness separately before applying the partial order risks missing admissible trade-offs (e.g., a larger spatial deviation enabled by a small temporal shift). A concrete counter-example or inductive proof sketch addressing this coupling is needed to confirm the under-approximation property.
minor comments (2)
  1. [Abstract / §1] The abstract and introduction would benefit from a brief comparison table contrasting STR with prior robust semantics (e.g., those in Fainekos et al. or Donzé et al.) to clarify the precise novelty of the multi-objective formulation.
  2. [§3] Notation for the partial order and Pareto front should be introduced with an explicit example in §3 to aid readability before the general definition.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their constructive and insightful review of our manuscript. We address the major comment on the robust semantics below and will incorporate revisions to strengthen the justification of the under-approximation property.

read point-by-point responses

  1. Referee: [§4] §4 (Robust Semantics): The central claim that the proposed robust semantics suitably under-approximate the true STR (Pareto set over joint perturbations) while remaining tractable is load-bearing but not fully established for general formulas. For operators such as 'until', where spatial and temporal aspects couple through the signal dynamics, combining spatial and temporal robustness separately before applying the partial order risks missing admissible trade-offs (e.g., a larger spatial deviation enabled by a small temporal shift). A concrete counter-example or inductive proof sketch addressing this coupling is needed to confirm the under-approximation property.

    Authors: We appreciate the referee highlighting this key aspect of our framework. The robust semantics are defined recursively following the syntax of the temporal logic formula, with the Pareto partial order applied to combine spatial and temporal robustness values at each operator. For the 'until' operator specifically, the definition computes the supremum over admissible temporal shifts in the interval while evaluating the corresponding spatial robustness on the shifted signal segments; the resulting set of (spatial, temporal) pairs is then filtered under the partial order. This recursive construction is intended to under-approximate the true joint Pareto set of admissible perturbations. To address the concern directly, we will add a concise inductive proof sketch in the revised Section 4, proceeding by induction on formula structure and explicitly verifying the coupling for 'until' (and other binary operators) by showing that any joint perturbation admissible under the true STR is captured (or conservatively bounded) by the recursive combination. We believe this addition will confirm soundness while preserving the tractability of the monitoring algorithms. revision: yes

Circularity Check

0 steps flagged

No significant circularity; new definition and under-approximation are independent of inputs

full rationale

The paper defines spatiotemporal robustness (STR) as a fresh multi-objective partial order over joint spatial-temporal perturbations, then introduces sound under-approximating robust semantics and monitoring algorithms derived from that definition. No equation reduces to a fitted parameter renamed as a prediction, no self-citation chain bears the central claim, and the soundness argument is presented as a separate proof obligation rather than a tautology. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard assumptions from temporal logic and multi-objective optimization; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption Robust semantics for temporal logic can be defined over discrete-time signals to capture geometric distance from unsatisfiability.
    This is the foundation explicitly contrasted with the new spatiotemporal extension.
  • domain assumption Multi-objective optimization tools can be applied to characterize Pareto-optimal sets of perturbations.
    Invoked to obtain the two key advantages listed in the abstract.

pith-pipeline@v0.9.0 · 5750 in / 1316 out tokens · 41759 ms · 2026-05-21T14:59:10.702280+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Runtime Monitoring of Perception-Based Autonomous Systems via Embedding Temporal Logic

    cs.LG 2026-05 unverdicted novelty 7.0

    Embedding Temporal Logic enables runtime monitoring of temporally extended perceptual behaviors by defining predicates via distances between observed and reference embeddings in learned spaces, with conformal calibrat...

  2. Runtime Monitoring of Perception-Based Autonomous Systems via Embedding Temporal Logic

    cs.LG 2026-05 unverdicted novelty 7.0

    Embedding Temporal Logic (ETL) performs runtime monitoring directly in learned embedding spaces using distance-based predicates composed with temporal operators, supported by conformal calibration for reliable predica...

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages · cited by 1 Pith paper · 1 internal anchor

  1. [1]

    ACM Transactions on Embedded Computing Systems (TECS)12(2s), 1–30 (2013)

    Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Probabilis- tic temporal logic falsification of cyber-physical systems. ACM Transactions on Embedded Computing Systems (TECS)12(2s), 1–30 (2013)

    work page 2013

  2. [2]

    Do As I Can, Not As I Say: Grounding Language in Robotic Affordances

    Ahn, M., Brohan, A., Brown, N., Chebotar, Y., Cortes, O., David, B., Finn, C., Fu, C., Gopalakrishnan, K., Hausman, K., et al.: Do as I can, not as I say: Grounding language in robotic affordances. arXiv preprint arXiv:2204.01691 (2022)

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  3. [3]

    Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification.In:InternationalConferenceonComputerAidedVerification.pp.356–

    work page

  4. [4]

    Journal of the ACM (JACM)43(1), 116–146 (1996)

    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM (JACM)43(1), 116–146 (1996)

    work page 1996

  5. [5]

    In: 2019 18th European control conference (ECC)

    Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: Theory and applications. In: 2019 18th European control conference (ECC). pp. 3420–3431. IEEE (2019)

    work page 2019

  6. [6]

    IEEE Transactions on Automatic Control62(8), 3861–3876 (2016)

    Ames, A.D., Xu, X., Grizzle, J.W., Tabuada, P.: Control barrier function based quadratic programs for safety critical systems. IEEE Transactions on Automatic Control62(8), 3861–3876 (2016)

    work page 2016

  7. [7]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: A tool for temporal logic falsification for hybrid systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 254–257. Springer (2011)

    work page 2011

  8. [8]

    Acta Cybernetica24(1), 17–28 (2019)

    Bálint, C., Valasek, G., Gergó, L.: Operations on signed distance functions. Acta Cybernetica24(1), 17–28 (2019)

    work page 2019

  9. [9]

    In: Lectures on Runtime Verification: Introductory and Advanced Topics, pp

    Bartocci, E., Deshmukh, J., Donzé, A., Fainekos, G., Maler, O., Ničković, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In: Lectures on Runtime Verification: Introductory and Advanced Topics, pp. 135–175. Springer (2018)

    work page 2018

  10. [10]

    Belta, C., Yordanov, B., Gol, E.A.: Formal methods for discrete-time dynamical systems, vol. 15. Springer

    work page

  11. [11]

    In: 26th ACM International Conference on Hybrid Systems: Computation and Control (2023)

    Bortolussi, L., Cairoli, F., Paoletti, N.: Conformal quantitative predictive moni- toring of STL requirements for stochastic processes. In: 26th ACM International Conference on Hybrid Systems: Computation and Control (2023)

    work page 2023

  12. [12]

    IEEE Robotics and Au- tomation Letters (2025)

    Buyukkocak, A.T., Aksaray, D.: Resilient online planning for mobile robots with minimal relaxation of signal temporal logic specifications. IEEE Robotics and Au- tomation Letters (2025)

    work page 2025

  13. [13]

    In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control

    Chen, H., Smolka, S.A., Paoletti, N., Lin, S.: An STL-based approach to resilient control for cyber-physical systems. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control. pp. 1–12 (2023)

    work page 2023

  14. [14]

    In: Proceedings of the 2023 Con- ference on Empirical Methods in Natural Language Processing

    Chen, Y., Gandhi, R., Zhang, Y., Fan, C.: NL2TL: Transforming natural languages to temporal logics using large language models. In: Proceedings of the 2023 Con- ference on Empirical Methods in Natural Language Processing. pp. 15880–15903 (2023)

    work page 2023

  15. [15]

    Formal Methods in System Design 51(1), 5–30 (2017)

    Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Ro- bust online monitoring of signal temporal logic. Formal Methods in System Design 51(1), 5–30 (2017)

    work page 2017

  16. [16]

    arXiv preprint arXiv:2110.00339 (2021) 20 Oliver Schön and Lars Lindemann

    Dhonthi, A., Schillinger, P., Rozo, L., Nardi, D.: Study of signal temporal logic robustness metrics for robotic tasks optimization. arXiv preprint arXiv:2110.00339 (2021) 20 Oliver Schön and Lars Lindemann

    work page arXiv 2021

  17. [17]

    In: International Conference on Runtime Verification

    Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: International Conference on Runtime Verification. pp. 231–246. Springer (2014)

    work page 2014

  18. [18]

    In: Inter- national conference on computer aided verification

    Donzé, A., Ferrere, T., Maler, O.: Efficient robust monitoring for STL. In: Inter- national conference on computer aided verification. pp. 264–279. Springer (2013)

    work page 2013

  19. [19]

    In: Formal Modeling and Analysis of Timed Systems: 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010

    Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Formal Modeling and Analysis of Timed Systems: 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings 8. pp. 92–106. Springer (2010)

    work page 2010

  20. [20]

    In: 1988 American control conference

    Doyle, J., Glover, K., Khargonekar, P., Francis, B.: State-space solutions to stan- dardH 2 andH ∞ control problems. In: 1988 American control conference. pp. 1691–1696. IEEE (1988)

    work page 1988

  21. [21]

    Springer (2005)

    Ehrgott, M.: Multicriteria optimization. Springer (2005)

    work page 2005

  22. [22]

    Theoretical Computer Science410(42), 4262–4291 (2009)

    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science410(42), 4262–4291 (2009)

    work page 2009

  23. [23]

    Springer Science & Business Media (2008)

    Freeman, R., Kokotovic, P.V.: Robust nonlinear control design: state-space and Lyapunov techniques. Springer Science & Business Media (2008)

    work page 2008

  24. [24]

    Springer (2014)

    Fridman, E.: Introduction to time-delay systems. Springer (2014)

    work page 2014

  25. [25]

    https://apnews.com/article/dc-crash-investigation- american-airlines-helicopter-ntsb-acc8bf751427eb6824d9d1fad30895b8 (2025)

    Funk, J.: What is known about the deadly January air crash between a passenger jet and US Army helicopter. https://apnews.com/article/dc-crash-investigation- american-airlines-helicopter-ntsb-acc8bf751427eb6824d9d1fad30895b8 (2025)

    work page 2025

  26. [26]

    IEEE Control Systems Letters5(1), 241–246 (2020)

    Gilpin, Y., Kurtz, V., Lin, H.: A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Systems Letters5(1), 241–246 (2020)

    work page 2020

  27. [27]

    In: 2019 IEEE 58th Conference on Decision and Control (CDC)

    Haghighi, I., Mehdipour, N., Bartocci, E., Belta, C.: Control from signal temporal logic specifications with smooth cumulative quantitative semantics. In: 2019 IEEE 58th Conference on Decision and Control (CDC). pp. 4361–4366. IEEE (2019)

    work page 2019

  28. [28]

    ARCH@ ADHS2018 (2018)

    Heidlauf, P., Collins, A., Bolender, M., Bak, S.: Verification challenges in F-16 ground collision avoidance and other automated maneuvers. ARCH@ ADHS2018 (2018)

    work page 2018

  29. [29]

    In: Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design

    Hekmatnejad, M., Yaghoubi, S., Dokhanchi, A., Amor, H.B., Shrivastava, A., Karam, L., Fainekos, G.: Encoding and monitoring responsibility sensitive safety rules for automated vehicles in signal temporal logic. In: Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design. pp. 1–11 (2019)

    work page 2019

  30. [30]

    The International Journal of Robotics Research39(7), 812–836 (2020)

    Kantaros, Y., Zavlanos, M.M.: Stylus*: A temporal logic optimal control syn- thesis algorithm for large-scale multi-robot systems. The International Journal of Robotics Research39(7), 812–836 (2020)

    work page 2020

  31. [31]

    Real-time systems2(4), 255–299 (1990)

    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-time systems2(4), 255–299 (1990)

    work page 1990

  32. [32]

    IEEE Transactions on Robotics25(6), 1370–1381 (2009)

    Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mis- sion and motion planning. IEEE Transactions on Robotics25(6), 1370–1381 (2009)

    work page 2009

  33. [33]

    In: 2023 18th Conference on Computer Science and Intelligence Systems (FedCSIS)

    Kwiatkowska, M., Zhang, X.: When to trust AI: Advances and challenges for cer- tification of neural networks. In: 2023 18th Conference on Computer Science and Intelligence Systems (FedCSIS). pp. 25–37. IEEE (2023)

    work page 2023

  34. [34]

    In: 2024 Amer- ican Control Conference (ACC)

    Le, N.K., Noorani, E., Hirche, S., Baras, J.S.: Time-robust path planning with piece-wise linear trajectory for signal temporal logic specifications. In: 2024 Amer- ican Control Conference (ACC). pp. 4133–4140. IEEE (2024)

    work page 2024

  35. [35]

    The International Journal of Robotics Research42(6), 356–370 (2023) Spatiotemporal Robustness using Multi-Objective Reasoning 21

    Leung, K., Aréchiga, N., Pavone, M.: Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods. The International Journal of Robotics Research42(6), 356–370 (2023) Spatiotemporal Robustness using Multi-Objective Reasoning 21

    work page 2023

  36. [36]

    In: 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)

    Li, X., Vasile, C.I., Belta, C.: Reinforcement learning with temporal logic rewards. In: 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). pp. 3834–3839. IEEE (2017)

    work page 2017

  37. [37]

    IEEE control systems letters3(1), 96–101 (2018)

    Lindemann, L., Dimarogonas, D.V.: Control barrier functions for signal temporal logic tasks. IEEE control systems letters3(1), 96–101 (2018)

    work page 2018

  38. [38]

    MIT Press (2025)

    Lindemann, L., Dimarogonas, D.V.: Formal Methods for Multi-Agent Feedback Control Systems. MIT Press (2025)

    work page 2025

  39. [39]

    In: Proceedings of the ACM/IEEE 14th International Con- ference on Cyber-Physical Systems (with CPS-IoT Week 2023)

    Lindemann, L., Qin, X., Deshmukh, J.V., Pappas, G.J.: Conformal prediction for stl runtime verification. In: Proceedings of the ACM/IEEE 14th International Con- ference on Cyber-Physical Systems (with CPS-IoT Week 2023). pp. 142–153 (2023)

    work page 2023

  40. [40]

    In: 25th ACM International Conference on Hybrid Systems: Computation and Control

    Lindemann, L., Rodionova, A., Pappas, G.: Temporal robustness of stochastic sig- nals. In: 25th ACM International Conference on Hybrid Systems: Computation and Control. pp. 1–11 (2022)

    work page 2022

  41. [41]

    IEEE Control Systems45(6), 72–122 (2025)

    Lindemann, L., Zhao, Y., Yu, X., Pappas, G.J., Deshmukh, J.V.: Formal verifi- cation and control with conformal prediction: Practical safety guarantees for au- tonomous systems. IEEE Control Systems45(6), 72–122 (2025)

    work page 2025

  42. [42]

    The International Journal of Robotics Research43(9), 1409–1424 (2024)

    Luo, R., Zhao, S., Kuck, J., Ivanovic, B., Savarese, S., Schmerling, E., Pavone, M.: Sample-efficient safety assurances using conformal prediction. The International Journal of Robotics Research43(9), 1409–1424 (2024)

    work page 2024

  43. [43]

    In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp

    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp. 152–166. Springer (2004)

    work page 2004

  44. [44]

    In: 2019 American Control Con- ference (ACC)

    Mehdipour, N., Vasile, C.I., Belta, C.: Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In: 2019 American Control Con- ference (ACC). pp. 1690–1695. IEEE (2019)

    work page 2019

  45. [45]

    IEEE Transactions on Automatic Control (2024)

    Mehdipour, N., Vasile, C.I., Belta, C.: Generalized mean robustness for signal temporal logic. IEEE Transactions on Automatic Control (2024)

    work page 2024

  46. [46]

    In: Conference on Formal Methods in Computer-Aded Design (FMCAD)

    Mendoza, D., Hahn, C., Trippel, C.: Translating natural language to temporal logics with large language models and model checkers. In: Conference on Formal Methods in Computer-Aded Design (FMCAD). p. 119 (2024)

    work page 2024

  47. [47]

    Miettinen, K.: Nonlinear multiobjective optimization, vol. 12. Springer Science & Business Media (1999)

    work page 1999

  48. [48]

    Niculescu,S.I.:Delayeffectsonstability:arobustcontrolapproach.Springer(2002)

    work page 2002

  49. [49]

    In: 2017 IEEE Conference on Control Tech- nology and Applications (CCTA)

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

    work page 2017

  50. [50]

    In: 53rd IEEE Conference on Decision and Control

    Raman, V., Donzé, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli, A., Seshia, S.A.: Model predictive control with signal temporal logic specifications. In: 53rd IEEE Conference on Decision and Control. pp. 81–87. IEEE (2014)

    work page 2014

  51. [51]

    In: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems

    Rino, N., Foughali, M., Asarin, E.: Efficiently computable distance-based robust- ness for a practical fragment of STL. In: International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. pp. 179–195. Springer (2024)

    work page 2024

  52. [52]

    Rodionova, A., Lindemann, L., Morari, M., Pappas, G.J.: Time-robust control for STLspecifications.In:202160thIEEEConferenceonDecisionandControl(CDC). pp. 572–579. IEEE (2021)

    work page 2021

  53. [53]

    IEEE Control Systems Letters7, 619–624 (2022) 22 Oliver Schön and Lars Lindemann

    Rodionova, A., Lindemann, L., Morari, M., Pappas, G.J.: Combined left and right temporal robustness for control under STL specifications. IEEE Control Systems Letters7, 619–624 (2022) 22 Oliver Schön and Lars Lindemann

    work page 2022

  54. [54]

    In: 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton)

    Sadraddini, S., Belta, C.: Robust temporal logic model predictive control. In: 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton). pp. 772–779. IEEE (2015)

    work page 2015

  55. [55]

    In: Proceedings of the 15th ACM inter- national conference on Hybrid Systems: Computation and Control

    Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the 15th ACM inter- national conference on Hybrid Systems: Computation and Control. pp. 125–134 (2012)

    work page 2012

  56. [56]

    Com- munications of the ACM65(7), 46–55 (2022)

    Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Com- munications of the ACM65(7), 46–55 (2022)

    work page 2022

  57. [57]

    In: 2020 American Control Conference (ACC)

    Varnai, P., Dimarogonas, D.V.: On robustness metrics for learning stl tasks. In: 2020 American Control Conference (ACC). pp. 5394–5399. IEEE (2020)

    work page 2020

  58. [58]

    In: IROS (2017)

    Vasile, C., Raman, V., Karaman, S.: Sampling-based synthesis of maximally- satisfying controllers for temporal logic specifications. In: IROS (2017)

    work page 2017

  59. [59]

    In: 2024 IEEE International Conference on Robotics and Automation (ICRA)

    Wang, S., Li, S., Yin, L., Yin, X.: Synthesis of temporally-robust policies for signal temporal logic tasks using reinforcement learning. In: 2024 IEEE International Conference on Robotics and Automation (ICRA). pp. 10503–10509. IEEE (2024)

    work page 2024

  60. [60]

    Springer (2006)

    Zhong, Q.C.: Robust control of time-delay systems. Springer (2006)

    work page 2006

  61. [61]

    Zhou, K., Doyle, J.C.: Essentials of robust control, vol. 104. Prentice hall Upper Saddle River, NJ (1998) A Robust Semantics for Spatial Robustness For the convenience of the reader, we recall the robust semantics for spatial robustness from [22] which will structurally resemble the robust semantics for spatiotemporal robustness. Definition 6 (STL Robust...

    work page 1998