Pith. sign in

REVIEW 2 major objections 4 minor 79 references

pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis

T0 review · 2 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read pacSTL gives temporal-logic safety specs a probabilistic certificate: with confidence 1−β, an unseen trajectory's robustness lands inside the computed interval with probability at least 1−ε_R.

desk verdict A useful composition of PAC reachability and interval STL, but the central theorem has an unstated discrete-time assumption that conflicts with the continuous-time semantics; fixable but essential. read the letter →

arxiv 2511.00934 v3 pith:NH6C3SFF submitted 2025-11-02 cs.LO cs.RO

Hanna Krasowski , Elizabeth Dietrich , Emir Cem Gezer , Roger Skjetne , Asgeir Johan S{o}rensen , Murat Arcak This is my paper
classification cs.LOcs.RO
keywords SignalTemporalLogicPACboundsreachabilityanalysisscenariooptimizationintervalSTLruntimemonitoringmaritimenavigationprobabilisticguarantees
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

pacSTL is a framework for checking Signal Temporal Logic (STL) specifications on systems whose future behavior is uncertain. Instead of sampling many trajectories to estimate satisfaction probability, it builds a PAC-bounded reachable tube from sample data—a set that contains a new trajectory with probability at least 1−ε_R, with confidence 1−β—and then computes the narrowest interval of STL robustness values consistent with that tube. The key guarantee, Theorem 2, transfers the reachable tube's probabilistic containment to the specification level: with confidence 1−β, the probability that an unseen trajectory's STL robustness lies in the computed interval is at least 1−ε_R. A time-point refinement (Theorem 3) tightens the bound by using the typically better per-time-set accuracies at the characteristic time points that determine the robustness interval. The result is a real-time monitoring tool that avoids online re-sampling when atomic propositions or specification parameters change, demonstrated on maritime collision-avoidance rules in simulation and on physical model vessels.

What carries the argument

The central machinery is the composition of three ingredients: (1) PAC-bounded reachable tube estimates—convex sets (ellipsoids or zonotopes) fitted to sample trajectories via scenario optimization, with the holdout method and binomial tail inversion providing the accuracy ε_R and confidence β; (2) atomic robustness bounds computed by solving convex optimization problems that minimize and maximize the atomic robustness function h over each reachable set R_t, yielding interval inclusion functions [h_t, h_t]; and (3) Interval-STL (I-STL) semantics, which propagate these intervals through Boolean and temporal operators and can track the characteristic time points (the argmin/argmax of the lower

What would settle it

Run a new batch of real-world trajectories in an environment that includes disturbances not captured in the training distribution (e.g., waves or currents), and count the fraction of those trajectories whose measured STL robustness falls outside the pacSTL interval. If that fraction systematically exceeds the reported ε_R (beyond what the confidence β allows), the claimed probabilistic containment is falsified for that operational domain.

Watch

Extended reading notes

Core claim

The paper claims that PAC-bounded reachable set predictions can be composed with interval-valued STL semantics to yield a robustness interval with a formal probabilistic guarantee. Concretely, for any STL specification φ, if the atomic robustness bounds are obtained by solving min/max optimization problems of the robustness function h over each time-point reachable set R_t of a PAC-bounded reachable tube, and the I-STL semantics propagate these intervals through logical and temporal operators, then the resulting interval [h, h]^φ satisfies P( P( h^φ(δ) ∈ [h,h]^φ ) ≥ 1 − ε_R ) ≥ 1 − β. That is, the probability that an unseen trajectory's robustness lies in the computed interval is at least 1−

Load-bearing premise

The PAC guarantee holds only for the specific probability distributions over initial states and disturbances chosen by the user; if the real operational environment draws scenarios from a different distribution, the stated probability bound on the robustness interval may be violated.

Editorial extensions

If this is right

  • Runtime monitors can now certify STL specifications with a probability bound without online trajectory sampling; each evaluation reduces to a few convex optimizations, taking about 0.15–0.6 seconds on a laptop.
  • Changing atomic propositions or specification parameters (e.g., time horizons, rule thresholds) requires no re-calibration or re-sampling, because the reachable tube is computed once per agent and the robustness bounds are derived by optimization.
  • The guarantee holds for any PAC-bounded set predictor—scenario optimization is just one instance—so the framework can be combined with other data-driven reachability methods that provide (ε, β) bounds.
  • The time-point refinement (Theorem 3) gives a practical accuracy improvement: since per-time-set accuracies are often much better than the tube-level accuracy, the robustness interval's certificate can be stated with a tighter ε without additional data.
  • In real-world maritime trials, the estimated disturbance distribution (captured by the bias term b) made the sim-to-real transfer successful: robustness intervals and trigger times remained similar, and the evasive maneuvers avoided collisions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: because pacSTL inherits the reachable tube's distributional assumptions, the strongest testable extension is to stress the method under environmental conditions not represented in the lab-estimated disturbance distribution (e.g., wave tank waves or currents) and empirically measure how often the real robustness leaves the computed interval.
  • The characteristic-time-point tracking suggests a natural closed-loop application the paper only hints at: a controller that steers the reachable sets at those critical time points to maximize the lower robustness bound would inherit the same PAC certificate, turning pacSTL into a synthesis tool rather than only a monitor.
  • The comparison with direct scenario optimization on robustness values quantifies a trade-off that could be explored analytically: pacSTL is more conservative because it optimizes over the entire reachable set, not just the robustness distribution; deriving the gap between the two interval widths as a function of set volume and robustness curvature is an open problem.
  • Since the guarantee is one-sided (containment in the set implies containment in the robustness interval, not conversely), the interval can be tightened by shrinking the reachable tube—e.g., by conditioning the tube on the current ego trajectory—a modification that preserves the theorem's proof structure.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper introduces pacSTL, a framework that combines PAC-bounded reachable tubes obtained via scenario optimization with Interval Signal Temporal Logic (I-STL) to compute robustness intervals for STL specifications together with a probabilistic guarantee. Atomic robustness bounds are obtained by solving optimization problems over the reachable sets, and these bounds are propagated through I-STL operators. Theorem 2 claims that, with probability at least 1−β, an unseen trajectory's STL robustness lies in the computed interval with probability at least 1−ε_R. A second theorem (Theorem 3) attempts to give a tighter guarantee using characteristic time points. The method is evaluated on maritime COLREGS encounter monitoring in simulation and on physical model vessels, and the paper reports real-time feasibility and code release.

Significance. If the correctness issues are resolved, the paper would be a useful contribution: it decouples the expensive data-driven reachability computation from STL evaluation, supports changing atomic propositions without recalibration, and demonstrates real-time monitoring on a physical testbed. The compositional structure and the explicit probabilistic interface are appealing, and the release of code plus real-world experiments are concrete strengths. The distributional caveat—guarantees are relative to the user-chosen μ_X0 and μ_D—is inherent and acknowledged. However, as written, the central guarantee has a formal gap due to the finite sampling of the reachable tube versus the continuous-time I-STL semantics, and Theorem 3 is not correct as stated. These issues affect the main theorem and the experimental claims that rely on Theorem 3, so they must be fixed before the paper can be accepted.

major comments (2)
  1. [Theorem 3 (Eq. (30))] The proof of Theorem 3 relies on the assertion that P(h^φ(δ_t) ∧ h^φ(δ_t) ∈ [h,h]^φ) ≥ P(h^φ(δ) ∈ [h,h]^φ), but the robustness of the full trajectory is not determined by the two characteristic time points t and t of the computed interval. The final inequality P(h^φ(δ)∈[h,h]^φ) ≥ max(P(δ_t∈R_t), P(δ_t∈R_t)) does not follow. Consequently, the improved accuracies reported in Sec. VIII-C (e.g., ε_Rt = 0.039/0.038 at t_e) are not supported by a valid theorem. Either remove Theorem 3 or provide a correct proof under explicit assumptions, e.g. that the characteristic time points are fixed for all trajectories and that the specification robustness depends only on the value at those points.
  2. [Appendix A1 (Algorithm 1)] Algorithm 1 is presented as computing the exact lower and upper bounds for the nonlinear orientation-halfplane robustness, but no proof of exactness is given. Lemma 1 and Theorem 2 require the solutions of (21) and (22) to be exact; if Algorithm 1 only evaluates endpoint cases with a clipping rule, its correctness for a nonlinear, possibly non-monotonic function is not obvious. A correctness proof, or a reference containing one, is needed to substantiate the nonlinear atomic proposition experiments in Sec. VIII.
minor comments (4)
  1. [Eq. (8)] The formula for the binomial tail inversion is typeset confusingly ('max_e { n e: ... }'). Please clarify the notation and define the variables (e.g., the candidate violation probability and the empirical count) explicitly.
  2. [Sec. V, proof of Theorem 2] The notation 'i∈{1,...,K}, t∈{0,...,T}' should explicitly state that t ranges over the time grid of the reachable tube, consistent with the discrete-time interpretation that the framework apparently uses.
  3. [Sec. VI-A] The notation δ∈R^{6×T} for trajectories conflicts with the earlier continuous-time signal notation. State explicitly that the case study uses discrete-time trajectories with step Δt.
  4. [Fig. 6 caption] Please clarify which accuracy quantities are plotted: ε_R (tube accuracy) versus ε_Rt (time-point accuracy). The caption currently says 'minimal and maximal time-point accuracies' but the figure also shows tube accuracies.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the specification-level PAC guarantee is a monotone logical consequence of the PAC reachable-tube guarantee, and the same-author citations are to independent supporting results rather than to the paper's conclusion.

full rationale

The central derivation chain is: (i) Theorem 1 imports a holdout-based PAC bound on a reachable tube R and time-point sets R_t; (ii) Lemma 1 shows that if a trajectory point lies in R_t, then its atomic robustness lies in the min/max interval [h_t, hbar_t] over R_t — this is an implication by construction, not a circular reuse of the conclusion; (iii) Corollary 1 invokes the external I-STL soundness result [14] to propagate atomic inclusion intervals through the temporal operators; (iv) Theorem 2 then transfers the tube-level PAC guarantee to the specification interval, since containment in R implies containment in each atomic interval at the relevant time points. Each step is a conservative implication, not an equality with its input, and no parameter is fitted to the target robustness interval: epsilon_R and epsilon_Rt are estimated on independent holdout samples via binomial tail inversion, separate from the optimization problems that produce the intervals. The same-author citations [16] (holdout scenario-optimization theorem) and [66] (maritime predicate definitions) are load-bearing in a broad sense, but they are independent statistical/formal results with stated assumptions that do not already contain pacSTL's specification-level conclusion; under the review rules they therefore do not count as circularity. Separately, the paper has non-circular validity gaps: R is defined only at finitely many sampled time points (Sec. III-B), whereas I-STL temporal semantics such as Eq. (4) quantify over continuous intervals, so the proof of Theorem 2 should justify that sampled containment implies continuous-interval containment; and Theorem 3's proof lower-bounds an intersection probability by a maximum, which is not generally valid. These are correctness risks, not cases where a prediction reduces to its input by construction, so they do not raise the circularity score.

Assumptions & free parameters 3 free parameters · 6 assumptions · 0 invented entities

The central guarantee inherits the PAC reachability guarantee; the only fitted-to-data input is the disturbance interval. The paper relies on cited theorems (scenario-optimization PAC bound, I-STL soundness) and on a few domain assumptions about distribution matching, ego-state prediction, and the correctness of the nonlinear interval computation. The time-point refinement (Theorem 3) is a stated result with a flawed proof, not an input axiom.

free parameters (3)
  • Disturbance bias interval [b̄, b] = b=[-1.102,0.00764,0,0,0,-0.0941], b̄=[0.438,0.230,0,0,0,0.0263]
    Estimated from real-world experiments (Sec. VII-B) to define μ_D; the reachable tube and thus all robustness intervals depend on this fitted input.
  • Confidence parameter β = 1e-9
    Chosen by hand (Table I); all PAC guarantees are with respect to this confidence.
  • Training/testing sample sizes N, M = 1500, 1500
    Chosen by hand; affects the computed ε via (8).
assumptions (6)
  • standard math Theorem 1 (adapted from [16]): binomial tail inversion on holdout samples yields a 1−β confidence upper bound ε on the violation probability of the reachable tube/set.
    Invoked in Sec. III-B to convert empirical violation counts to PAC bounds; proved in a preprint by overlapping authors.
  • standard math I-STL quantitative semantics are sound interval inclusion functions (from [14, Thm. 1]).
    Invoked in Corollary 1 and Theorem 2; the paper does not re-prove it.
  • domain assumption Training/holdout samples are i.i.d. from μ_{X0} × μ_D and the holdout set is fresh.
    Required for the holdout PAC bound; stated in Sec. III-B.
  • domain assumption The real-world disturbance distribution is captured by the experimentally estimated interval [b̄, b].
    Stated in Sec. VII-B; if the true deployment distribution differs (waves, currents, other vessels), the PAC guarantees do not apply.
  • domain assumption The ego vessel's future state is known/perfectly predicted (constant speed and orientation).
    Sec. VII-C: 'we compute a trajectory that assumes constant speed and orientation'; uncertainty in this prediction is not included in the PAC guarantee.
  • ad hoc to paper Algorithm 1 computes the exact min/max of the nonlinear orientation robustness over the orientation interval.
    Sec. VI-D states the standard robustness function does not ensure true min/max, then asserts a case-wise computation without proof; the soundness of the atomic interval depends on it.

how reviews work

0 comments
Cite this review

Pith. "Pith review of pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis." pith.science (2026). https://pith.science/paper/NH6C3SFF

@misc{pith2026251100934,
  author       = {Pith},
  title        = {Pith review of: pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NH6C3SFF}},
  note         = {Machine review of arXiv:2511.00934}
}
read the original abstract

Signal Temporal Logic (STL) is an expressive language for specifying behaviors of dynamical systems from continuous signals. However, a limitation of standard STL is its inherently deterministic semantics, which prevents it from accommodating uncertainty. Existing approaches to overcome this limitation are computationally costly and limit real-time capability, requiring repeated trajectory sampling or redesign of probability distributions over atomic propositions whenever the atomic propositions or specifications change. We introduce pacSTL, a framework that combines Probably Approximately Correct (PAC)-bounded reachable set predictions with an interval extension of STL. pacSTL computes lower and upper bounds on atomic robustness values by solving optimization problems over PAC-bounded reachable sets and propagates the bounds through the temporal logic operators. The resulting evaluation yields a PAC-bounded robustness interval at the specification level. We demonstrate the efficiency and relevance of pacSTL by verifying a quadrotor flight scenario and runtime monitoring a maritime navigation encounter.

Figures

Figures reproduced from arXiv: 2511.00934 by the authors.

Figure 1
Figure 1. Example evaluation of a PAC-bounded Signal Temporal Logic [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Proposed pacSTL framework that combines PAC-bounded reachable tubes and optimization problems for lower and upper atomic robustness bounds [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Duffing Oscillator in R2 with reachable set estimates as an ellipsoid E (gold), a zonotope with 4 generators Z1 (dark pink), and a zonotope with 2 generators Z2 (light pink). To improve numerical stability, we replace this expression with log det(GG⊤), which does not change the minimizer. To solve (15), we set the initial centers c of the zonotope close to optimal using a k-means clustering algorithm and generate an… view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Minimal example of robustness bound calculations given PAC [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Reachable tubes for 5 time steps with time step size 0.5s, increasingly [PITH_FULL_IMAGE:figures/full_fig_p011_5.png]
Figure 6
Figure 6. Figure 6: Accuracies for zonotopic (pink) and ellipsoidal (gold) tubes and time [PITH_FULL_IMAGE:figures/full_fig_p011_6.png]
Figure 8
Figure 8. Figure 8: ?? Real-world initialization of experiments for head-on, crossing, and in-between situations (from left to right). ?? Simulation initialization of experiments for head-on, crossing, and in-between situations (from left to right). ?? h for real-world head-on (dark red),…
Figure 9
Figure 9. Figure 9: Successful maneuver, in which a head-on encounter is detected at [PITH_FULL_IMAGE:figures/full_fig_p013_9.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

79 extracted references · 9 linked inside Pith

  1. [16]

    Data-Driven Reachability with Scenario Optimization and the Holdout Method,

    E. Dietrich, R. Devonport, S. Tu, and M. Arcak, “Data-Driven Reachability with Scenario Optimization and the Holdout Method,” arXiv:2504.06541, 2025

    arXiv 2025

  2. [66]

    Falsification-Driven Reinforcement Learning for Maritime Motion Planning,

    M. M ¨uller, F. Finkeldei, H. Krasowski, M. Arcak, and M. Althoff, “Falsification-Driven Reinforcement Learning for Maritime Motion Planning,” arXiv:2510.06970, 2025

    arXiv 2025

  3. [1]

    Generalizing Safety Be- yond Collision-Avoidance via Latent-Space Reachability Analysis,

    A. B. Kensuke Nakamura, Lasse Peters, “Generalizing Safety Be- yond Collision-Avoidance via Latent-Space Reachability Analysis,” in Robotics: Science and Systems (RSS), 2025

    2025

  4. [2]

    Semantically Safe Robot Manipulation: From Semantic Scene Understanding to Motion Safeguards,

    L. Brunke, Y . Zhang, R. R ¨omer, J. Naimer, N. Staykov, S. Zhou, and A. P. Schoellig, “Semantically Safe Robot Manipulation: From Semantic Scene Understanding to Motion Safeguards,” IEEE Robotics and Automation Letters, vol. 10, no. 5, pp. 4810–4817, 2025

    2025

  5. [3]

    Autonomous COLREGs-compliant decision making using maritime radar tracking and model predictive control,

    D. K. M. Kufoalor, E. Wilthil, I. B. Hagen, E. F. Brekke, and T. A. Johansen, “Autonomous COLREGs-compliant decision making using maritime radar tracking and model predictive control,” in Proc. of the European Control Conf. (ECC), 2019, pp. 2536–2542

    2019

  6. [4]

    Seeing, Saying, Solving: An LLM-to-TL Framework for Cooperative Robots,

    D. B. Choe, S. V . Sangeetha, S. Emanuel, C.-Y . Chiu, S. Coogan, and S. Kousik, “Seeing, Saying, Solving: An LLM-to-TL Framework for Cooperative Robots,” arXiv: 2505.13376, 2025

    arXiv 2025

  7. [5]

    AutoTAMP: Autoregressive Task and Motion Planning with LLMs as Translators and Checkers,

    Y . Chen, J. Arkin, C. Dawson, Y . Zhang, N. Roy, and C. Fan, “AutoTAMP: Autoregressive Task and Motion Planning with LLMs as Translators and Checkers,” in 2024 IEEE International Conference on Robotics and Automation (ICRA), 2024, pp. 6695–6702

    2024

  8. [6]

    Continuous-Time Control Synthesis Under Nested Signal Temporal Logic Specifications,

    P. Yu, X. Tan, and D. V . Dimarogonas, “Continuous-Time Control Synthesis Under Nested Signal Temporal Logic Specifications,” IEEE Transactions on Robotics, vol. 40, pp. 2272–2286, 2024

    2024

Show all 79 references
  1. [7]

    Control of Mobile Robots Using Barrier Functions Under Temporal Logic Specifications,

    M. Srinivasan and S. Coogan, “Control of Mobile Robots Using Barrier Functions Under Temporal Logic Specifications,” IEEE Transactions on Robotics, vol. 37, no. 2, pp. 363–374, 2021

    2021

  2. [8]

    Reinforcement learning with temporal logic rewards,

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

    2017

  3. [9]

    Temporal-Logic-Based Reward Shaping for Continuing Reinforcement Learning Tasks,

    Y . Jiang, S. Bharadwaj, B. Wu, R. Shah, U. Topcu, and P. Stone, “Temporal-Logic-Based Reward Shaping for Continuing Reinforcement Learning Tasks,” in Proceedings of the AAAI Conference on Artificial Intelligence, 2021, pp. 7995–8003

    2021

  4. [10]

    Safe Control Under Uncertainty with Prob- abilistic Signal Temporal Logic,

    D. Sadigh and A. Kapoor, “Safe Control Under Uncertainty with Prob- abilistic Signal Temporal Logic,” in Proceedings of Robotics: Science and Systems XII, June 2016

    2016

  5. [11]

    Control with Probabilistic Signal Temporal Logic,

    C. Yoo and C. Belta, “Control with Probabilistic Signal Temporal Logic,” arXiv:1510.08474, 2015

    2015 arXiv

  6. [12]

    Confor- mal Prediction for STL Runtime Verification,

    L. Lindemann, X. Qin, J. V . Deshmukh, and G. J. Pappas, “Confor- mal Prediction for STL Runtime Verification,” in Proceedings of the ACM/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023), ser. ICCPS ’23. New York, NY , USA: Association for ...

    2023

  7. [13]

    A theory of the learnable,

    L. G. Valiant, “A theory of the learnable,” Commun. ACM, vol. 27, no. 11, p. 1134–1142, Nov. 1984

    1984

  8. [14]

    Interval Signal Tempo- ral Logic From Natural Inclusion Functions,

    L. Baird, A. Harapanahalli, and S. Coogan, “Interval Signal Tempo- ral Logic From Natural Inclusion Functions,” IEEE Control Systems Letters, vol. 7, pp. 3555–3560, 2023

    2023

  9. [15]

    Estimating Reachable Sets with Scenario Optimization,

    A. Devonport and M. Arcak, “Estimating Reachable Sets with Scenario Optimization,” in Proceedings of the 2nd Conference on Learning for Dynamics and Control, ser. Proceedings of Machine Learning Research, vol. 120. PMLR, 10–11 Jun 2020, pp. 75–84

    2020

  10. [17]

    Set Propagation Techniques for Reachability Analysis,

    M. Althoff, G. Frehse, and A. Girard, “Set Propagation Techniques for Reachability Analysis,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 4, no. V olume 4, 2021, pp. 369–395, 2021

    2021

  11. [18]

    Guarantees for Real Robotic Systems: Unifying Formal Controller Synthesis and Reachset- Conformant Identification,

    S. B. Liu, B. Sch ¨urmann, and M. Althoff, “Guarantees for Real Robotic Systems: Unifying Formal Controller Synthesis and Reachset- Conformant Identification,” IEEE Transactions on Robotics, vol. 39, no. 5, pp. 3776–3790, 2023

    2023

  12. [19]

    Data-Driven Reachability Analysis with Christoffel Functions,

    A. Devonport, F. Yang, L. El Ghaoui, and M. Arcak, “Data-Driven Reachability Analysis with Christoffel Functions,” in 2021 60th IEEE Conference on Decision and Control (CDC), 2021, pp. 5067–5072

    2021

  13. [20]

    NeuReach: Learning Reachability Functions from Simulations,

    D. Sun and S. Mitra, “NeuReach: Learning Reachability Functions from Simulations,” in Tools and Algorithms for the Construction and Analysis of Systems, D. Fisman and G. Rosu, Eds. Cham: Springer International Publishing, 2022, pp. 322–337

    2022

  14. [21]

    Data-Driven Reachability Analysis for Gaussian Process State Space Models,

    P. Griffioen and M. Arcak, “Data-Driven Reachability Analysis for Gaussian Process State Space Models,” in 2023 62nd IEEE Conference on Decision and Control (CDC), 2023, pp. 4100–4105

    2023

  15. [22]

    Reachability-based safe learning with Gaussian processes,

    A. K. Akametalu, J. F. Fisac, J. H. Gillula, S. Kaynama, M. N. Zeilinger, and C. J. Tomlin, “Reachability-based safe learning with Gaussian processes,” in 53rd IEEE Conference on Decision and Control, 2014, pp. 1424–1431

    2014

  16. [23]

    Nonconvex Scenario Op- timization for Data-Driven Reachability,

    E. Dietrich, A. Devonport, and M. Arcak, “Nonconvex Scenario Op- timization for Data-Driven Reachability,” in Proceedings of the 6th Annual Learning for Dynamics and Control Conference, ser. Proceed- ings of Machine Learning Research, vol. 242. PMLR, 15–17 Jul 2024, pp. 514–527

    2024

  17. [24]

    Verification of neural reachable tubes via scenario optimization and conformal prediction,

    A. Lin and S. Bansal, “Verification of neural reachable tubes via scenario optimization and conformal prediction,” in Proceedings of the 6th Annual Learning for Dynamics and Control Conference, ser. Proceedings of Machine Learning Research, A. Abate, M. Cannon, K. Margellos, a...

    2024

  18. [25]

    Scenario-Based Probabilistic Reach- able Sets for Recursively Feasible Stochastic Model Predictive Control,

    L. Hewing and M. N. Zeilinger, “Scenario-Based Probabilistic Reach- able Sets for Recursively Feasible Stochastic Model Predictive Control,” IEEE Control Systems Letters, vol. 4, no. 2, pp. 450–455, 2020

    2020

  19. [26]

    Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference,

    N. Hashemi, X. Qin, L. Lindemann, and J. V . Deshmukh, “Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference,” in 2023 62nd IEEE Conference on Decision and Control (CDC), 2023, pp. 3102–3109

    2023

  20. [27]

    Conformalized Reachable Sets for Obstacle Avoidance with Spheres,

    Y . Kwon, J. Michaux, S. Isaacson, B. Zhang, M. Ejakov, K. A. Skinner, and R. Vasudevan, “Conformalized Reachable Sets for Obstacle Avoidance with Spheres,” in 2025 IEEE International Conference on Robotics and Automation (ICRA), 2025, pp. 12 877–12 884

    2025

  21. [28]

    Data-driven Reachability using Christoffel Functions and Conformal Prediction,

    A. Tebjou, G. Frehse, and F. Chamroukhi, “Data-driven Reachability using Christoffel Functions and Conformal Prediction,” in Proceedings of the Twelfth Symposium on Conformal and Probabilistic Prediction with Applications, ser. Proceedings of Machine Learning Research, H. Papa...

    2023

  22. [29]

    Data-Driven Reachability Analysis Using Matrix Zonotopes,

    A. Alanwar, A. Koch, F. Allg ¨ower, and K. H. Johansson, “Data-Driven Reachability Analysis Using Matrix Zonotopes,” in Proceedings of the 3rd Conference on Learning for Dynamics and Control, vol. 144, 2021, pp. 163–175

    2021

  23. [30]

    Data- Driven Reachability Analysis From Noisy Data,

    A. Alanwar, A. Koch, F. Allg ¨ower, and K. H. Johansson, “Data- Driven Reachability Analysis From Noisy Data,” IEEE Transactions on Automatic Control, vol. 68, no. 5, pp. 3054–3069, 2023

    2023

  24. [31]

    Data-Driven Reachability Analysis for Nonlinear Systems,

    H. Park, V . Vijay, and I. Hwang, “Data-Driven Reachability Analysis for Nonlinear Systems,” IEEE Control Systems Letters, vol. 8, pp. 2661– 2666, 2024

    2024

  25. [32]

    Two Space-Time Obstacle Repre- sentations Based on Ellipsoids and Polytopes,

    A. B. Martinsen and A. M. Lekkas, “Two Space-Time Obstacle Repre- sentations Based on Ellipsoids and Polytopes,” IEEE Access, vol. 9, pp. 111 152–111 161, 2021

    2021

  26. [33]

    Safe Autonomy for Uncrewed Surface Vehicles Using Adaptive Control and Reachability Analysis,

    K. Mahesh, T. M. Paine, M. L. Greene, N. Rober, S. Lee, S. T. Monteiro, A. Annaswamy, M. R. Benjamin, and J. P. How, “Safe Autonomy for Uncrewed Surface Vehicles Using Adaptive Control and Reachability Analysis,” IEEE Transactions on Control Systems Technology, pp. 1– 16, 2025

    2025

  27. [34]

    A Tutorial on Conformal Prediction,

    G. Shafer and V . V ovk, “A Tutorial on Conformal Prediction,” J. Mach. Learn. Res., vol. 9, p. 371–421, Jun. 2008

    2008

  28. [35]

    Formal Verification and Control with Conformal Prediction,

    L. Lindemann, Y . Zhao, X. Yu, G. J. Pappas, and J. V . Desh- mukh, “Formal Verification and Control with Conformal Prediction,” arXiv:2409.00536, 2025

    2025 arXiv

  29. [36]

    A Gentle Introduction to Con- formal Prediction and Distribution-Free Uncertainty Quantification,

    A. N. Angelopoulos and S. Bates, “A Gentle Introduction to Con- formal Prediction and Distribution-Free Uncertainty Quantification,” arXiv:2107.07511, 2022

    2022 arXiv

  30. [37]

    V ovk, A

    V . V ovk, A. Gammerman, and G. Shafer, Algorithmic Learning in a Random World. Berlin, Heidelberg: Springer-Verlag, 2005

    2005

  31. [38]

    Scenario optimization,

    R. S. Dembo, “Scenario optimization,” Annals of Operations Research, vol. 30, pp. 63–80, 1991

    1991

  32. [39]

    A General Scenario Theory for Nonconvex Optimization and Decision Making,

    M. C. Campi, S. Garatti, and F. A. Ramponi, “A General Scenario Theory for Nonconvex Optimization and Decision Making,” IEEE Transactions on Automatic Control, vol. 63, no. 12, pp. 4067–4078, 2018

    2018

  33. [40]

    Non-convex scenario optimization,

    S. Garatti and M. C. Campi, “Non-convex scenario optimization,” Mathematical Programming, 2024

    2024

  34. [41]

    Conformal Predic- tion in the Loop: Risk-Aware Control Barrier Functions for Stochastic Systems With Data-Driven State Estimators,

    J. Zhang, B. Hoxha, G. Fainekos, and D. Panagou, “Conformal Predic- tion in the Loop: Risk-Aware Control Barrier Functions for Stochastic Systems With Data-Driven State Estimators,” IEEE Control Systems Letters, vol. 9, pp. 282–287, 2025

    2025

  35. [42]

    Safe Adaptive Cruise Control Under Perception Uncertainty: A Deep Ensemble and Conformal Tube Model Predictive Control Approach,

    X. Li, A. Girard, and I. Kolmanovsky, “Safe Adaptive Cruise Control Under Perception Uncertainty: A Deep Ensemble and Conformal Tube Model Predictive Control Approach,” arXiv:2412.03792, 2024

    2024 arXiv

  36. [43]

    Signal Temporal Logic Control Synthesis among Uncontrollable Dynamic Agents with Confor- mal Prediction,

    X. Yu, Y . Zhao, X. Yin, and L. Lindemann, “Signal Temporal Logic Control Synthesis among Uncontrollable Dynamic Agents with Confor- mal Prediction,” arXiv:2312.04242, 2025

    2025 arXiv

  37. [44]

    Safe Planning in Dynamic Environments Using Conformal Prediction,

    L. Lindemann, M. Cleaveland, G. Shim, and G. J. Pappas, “Safe Planning in Dynamic Environments Using Conformal Prediction,” IEEE Robotics and Automation Letters, vol. 8, no. 8, pp. 5116–5123, 2023

    2023

  38. [45]

    Safety-Critical Control with Un- certainty Quantification using Adaptive Conformal Prediction,

    H. Zhou, Y . Zhang, and W. Luo, “Safety-Critical Control with Un- certainty Quantification using Adaptive Conformal Prediction,” in 2024 American Control Conference (ACC), 2024, pp. 574–580

    2024

  39. [46]

    Uncer- tainty quantification and robustification of model-based controllers using conformal prediction,

    K. Y . Chee, T. C. Silva, M. A. Hsieh, and G. J. Pappas, “Uncer- tainty quantification and robustification of model-based controllers using conformal prediction,” in Proceedings of the 6th Annual Learning for Dynamics and Control Conference, ser. Proceedings of Machine Learnin...

    2024

  40. [47]

    The scenario approach to robust control design,

    G. Calafiore and M. Campi, “The scenario approach to robust control design,” IEEE Transactions on Automatic Control, vol. 51, no. 5, pp. 742–753, 2006

    2006

  41. [48]

    Non-convex scenario optimization,

    S. Garatti and M. C. Campi, “Non-convex scenario optimization,” Mathematical Programming, vol. 209, no. 1, pp. 557–608, 2025

    2025

  42. [49]

    Scenario-Based Trajectory Optimization in Uncertain Dynamic Envi- ronments,

    O. de Groot, B. Brito, L. Ferranti, D. Gavrila, and J. Alonso-Mora, “Scenario-Based Trajectory Optimization in Uncertain Dynamic Envi- ronments,” IEEE Robotics and Automation Letters, vol. 6, no. 3, pp. 5389–5396, 2021

    2021

  43. [50]

    Sample-based bounds for coherent risk measures: Applications to policy synthesis and verification,

    P. Akella, A. Dixit, M. Ahmadi, J. W. Burdick, and A. D. Ames, “Sample-based bounds for coherent risk measures: Applications to policy synthesis and verification,” Artificial Intelligence, vol. 336, p. 104195, 2024

    2024

  44. [51]

    Monitoring temporal properties of con- tinuous signals,

    O. Maler and D. Nickovic, “Monitoring temporal properties of con- tinuous signals,” in International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, 2004, pp. 152–166

    2004

  45. [52]

    Robustness of temporal logic spec- ifications for continuous-time signals,

    G. E. Fainekos and G. J. Pappas, “Robustness of temporal logic spec- ifications for continuous-time signals,” Theoretical Computer Science, vol. 410, no. 42, pp. 4262–4291, 2009

    2009

  46. [53]

    Incremental reasoning in probabilistic Signal Temporal Logic,

    M. Tiger and F. Heintz, “Incremental reasoning in probabilistic Signal Temporal Logic,” International Journal of Approximate Reasoning, vol. 119, pp. 325–352, 2020

    2020

  47. [54]

    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, no. 1, pp. 5–30, 2017

    2017

  48. [55]

    STL Model Check- ing of Continuous and Hybrid Systems,

    H. Roehm, J. Oehlerking, T. Heinz, and M. Althoff, “STL Model Check- ing of Continuous and Hybrid Systems,” in Automated Technology for Verification and Analysis, 2016, pp. 412–427

    2016

  49. [56]

    Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis,

    N. Kochdumper and S. Bak, “Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis,” Nonlinear Analysis: Hybrid Systems, vol. 53, no. 101491, 2024

    2024

  50. [57]

    Model Predictive Robustness of Signal Temporal Logic Predicates,

    Y . Lin, H. Li, and M. Althoff, “Model Predictive Robustness of Signal Temporal Logic Predicates,” IEEE Robotics and Automation Letters, vol. 8, no. 12, pp. 8050–8057, 2023

    2023

  51. [58]

    Neurosymbolic Motion and Task Planning for Linear Temporal Logic Tasks,

    X. Sun and Y . Shoukry, “Neurosymbolic Motion and Task Planning for Linear Temporal Logic Tasks,” IEEE Transactions on Robotics, vol. 40, pp. 2749–2768, 2024

    2024

  52. [59]

    Signal Temporal Logic Neural Predictive Control,

    Y . Meng and C. Fan, “Signal Temporal Logic Neural Predictive Control,” IEEE Robotics and Automation Letters, vol. 8, no. 11, pp. 7719–7726, 2023

    2023

  53. [60]

    SpaTiaL: monitoring and planning of robotic tasks using spatio-temporal logic specifications,

    C. Pek, G. F. Schuppe, F. Esposito, J. Tumova, and D. Kragic, “SpaTiaL: monitoring and planning of robotic tasks using spatio-temporal logic specifications,” Autonomous Robots, vol. 47, no. 8, pp. 1439–1462, 2023

    2023

  54. [61]

    Runtime Monitoring of Time Window Temporal Logic,

    E. Bonnah and K. A. Hoque, “Runtime Monitoring of Time Window Temporal Logic,” IEEE Robotics and Automation Letters, vol. 7, no. 3, pp. 5888–5895, 2022

    2022

  55. [62]

    Planning and Runtime Monitoring of Robotic Manipulator using Metric Interval Temporal Logic,

    Z. Lin and J. S. Baras, “Planning and Runtime Monitoring of Robotic Manipulator using Metric Interval Temporal Logic,” in IEEE International Systems Conference (SysCon), 2019, pp. 1–8

    2019

  56. [63]

    Sleep When Everything Looks Fine: Self-Triggered Monitoring for Signal Temporal Logic Tasks,

    C. Wang, X. Yu, J. Zhao, L. Lindemann, and X. Yin, “Sleep When Everything Looks Fine: Self-Triggered Monitoring for Signal Temporal Logic Tasks,” IEEE Robotics and Automation Letters, vol. 9, no. 10, pp. 8983–8990, 2024

    2024

  57. [64]

    Temporal Logics for Learning and Detection of Anomalous Behavior,

    Z. Kong, A. Jones, and C. Belta, “Temporal Logics for Learning and Detection of Anomalous Behavior,” IEEE Transactions on Automatic Control, vol. 62, no. 3, pp. 1210–1222, 2017

    2017

  58. [65]

    Automatic simulation-based testing of autonomous ships using Gaussian processes and temporal logic,

    T. R. Torben, J. A. Glomsrud, T. A. Pedersen, I. B. Utne, and A. J. Sørensen, “Automatic simulation-based testing of autonomous ships using Gaussian processes and temporal logic,” Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, ...

    2023

  59. [67]

    Past- time Signal Temporal Logic Hybrid Switching Control for Underwater Vehicles,

    M. Fossdal, A. H. Brodtkorb, M. Arcak, and A. J. Sørensen, “Past- time Signal Temporal Logic Hybrid Switching Control for Underwater Vehicles,” in IEEE/OES Autonomous Underwater Vehicles Symposium (AUV), 2024, pp. 1–6

    2024

  60. [68]

    Provable Traffic Rule Compliance in Safe Reinforcement Learning on the Open Sea,

    H. Krasowski and M. Althoff, “Provable Traffic Rule Compliance in Safe Reinforcement Learning on the Open Sea,” IEEE Transactions on Intelligent Vehicles, vol. 9, no. 12, pp. 7617–7634, 2024

    2024

  61. [69]

    Computation of Minimum-V olume Covering Ellipsoids,

    P. Sun and R. M. Freund, “Computation of Minimum-V olume Covering Ellipsoids,” Operations Research, vol. 52, no. 5, pp. 690–706, 2004

    2004

  62. [70]

    Computing the V olume of a Zonotope,

    H. L. Montgomery, “Computing the V olume of a Zonotope,” The American Mathematical Monthly, vol. 96, no. 5, pp. 431–432, 1989

    1989

  63. [71]

    Determinants and the volumes of paral- lelotopes and zonotopes,

    E. Gover and N. Krikorian, “Determinants and the volumes of paral- lelotopes and zonotopes,” Linear Algebra and its Applications, vol. 433, no. 1, pp. 28–40, 2010

    2010

  64. [72]

    Convention on the International Regulations for Preventing Collisions at Sea, 1972 (COLREGs),

    I. M. Organization, “Convention on the International Regulations for Preventing Collisions at Sea, 1972 (COLREGs),” 1972

    1972

  65. [73]

    Temporal Logic Formalization of Marine Traffic Rules,

    H. Krasowski and M. Althoff, “Temporal Logic Formalization of Marine Traffic Rules,” inProc. of the IEEE Intelligent VehiclesSymposium (IV), 2021, pp. 186–192

    2021

  66. [74]

    T. I. Fossen, Handbook of marine craft hydrodynamics and motion control. John Wiley and Sons, 2011

    2011

  67. [75]

    Line-of-sight guidance for path following of marine vehicles,

    A. M. Lekkas and T. I. Fossen, “Line-of-sight guidance for path following of marine vehicles,” Advanced in marine robotics, vol. 5, pp. 63–92, 2013

    2013

  68. [76]

    Provably Safe Reinforcement Learning: Conceptual Anal- ysis, Survey, and Benchmarking,

    H. Krasowski, J. Thumm, M. M ¨uller, L. Sch ¨afer, X. Wang, and M. Althoff, “Provably Safe Reinforcement Learning: Conceptual Anal- ysis, Survey, and Benchmarking,” Transactions on Machine Learning Research, 2023

    2023

  69. [77]

    Toward verified artificial intelligence,

    S. A. Seshia, D. Sadigh, and S. S. Sastry, “Toward verified artificial intelligence,” Commun. ACM, vol. 65, no. 7, pp. 46––55, 2022

    2022

  70. [78]

    Interval Signal Temporal Logic for Robust Optimal Control,

    L. Baird and S. Coogan, “Interval Signal Temporal Logic for Robust Optimal Control,” in IEEE Conference on Decision and Control (CDC), 2024, pp. 5197–5202

    2024

  71. [79]

    Digital-physical testbed for ship autonomy studies in the Marine Cybernetics Laboratory basin,

    E. C. Gezer, M. K. I. Moreau, A. S. Høgden, D. T. Nguyen, R. Skjetne, and A. Sørensen, “Digital-physical testbed for ship autonomy studies in the Marine Cybernetics Laboratory basin,” arXiv:2505.06787, 2025

    2025 arXiv

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.