Pith. sign in

REVIEW 2 major objections 5 minor 35 references

Staying on Spec: Real-Time Monitoring under Uncertainty with a Maritime Case Study

T0 review · 2 major / 5 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read Monitoring formal safety rules under uncertainty can be done in real time if the heavy computation is moved offline into reachable tubes calibrated by a small number of real-world trials.

desk verdict Solid, honest application of pacSTL to maritime COLREG monitoring with real hardware evidence, but the PAC guarantees are conditional on a disturbance-support assumption that the paper itself concedes is imperfect. read the letter →

arxiv 2608.02811 v1 pith:PD7NYBHD submitted 2026-08-03 cs.RO cs.SYeess.SY

Elizabeth Dietrich , Hanna Krasowski , Emir Cem Gezer , Roger Skjetne , Asgeir Johan S{o}rensen , Murat Arcak This is my paper
classification cs.ROcs.SYeess.SY
keywords signaltemporallogicPACguaranteesreachablesetsdata-drivenreachabilitymaritimenavigationcollisionavoidanceCOLREGreal-timemonitoring
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

This paper tries to establish that a robotic system can monitor complex safety specifications in real time under uncertainty without an explicit probabilistic model or large datasets. The trick is to pair pacSTL, a probably-approximately-correct extension of signal temporal logic, with reachable tubes that are computed offline from high-fidelity simulations and calibrated to reality using roughly 100 experimental trials. On a physical maritime testbed with two vessels, the resulting monitor detects COLREG head-on and crossing encounters earlier than standard STL and TCPA monitors and, in the tested wave trials, achieves zero collisions and 100% detection where the baselines miss encounters or collide. The paper also reports reachable-tube accuracy bounds around 0.03 to 0.05 and an online evaluation rate near 1.4 Hz, making the approach a candidate for full-scale deployment.

What carries the argument

pacSTL (Probably Approximately Correct Signal Temporal Logic) is the central object: it takes a PAC-bounded reachable tube R_t and computes lower and upper robustness bounds for atomic predicates by optimizing the robustness function over R_t, then propagates these intervals through interval-STL semantics. The supporting mechanism is the data-driven reachable-tube pipeline: disturbance support S_D is built from extrema of the measured load term b over about 100 trials, a uniform distribution is placed on that support, simulated trajectories generate reachable tubes via scenario optimization, and the holdout method certifies them with epsilon-beta guarantees. Two practical devices carry the d

What would settle it

Collect a new set of trials in a different wave condition (e.g., larger wave height or a different spectrum), compute the measured disturbance b for each trial, and count how many fall outside the offline support S_D; then compare collision and detection rates of pacSTL against the epsilon bounds. If a substantial fraction of trials violate the support, or if any collision occurs in configurations the paper reports as collision-free, the claimed PAC guarantees and the zero-collision result do not generalize to that environment.

Watch

Extended reading notes

Core claim

The central claim is that pacSTL monitoring over data-driven reachable sets is a viable real-time way to evaluate temporal-logic specifications under realistic disturbances. The paper constructs reachable tubes for a six-degree-of-freedom vessel model from simulated trajectories, with the disturbance distribution estimated from the component-wise extrema of a measured load term b across about 100 physical trials and modeled as uniform over that support. Those tubes carry PAC guarantees: with confidence beta = 1e-9, an unseen trajectory lies in the tube with probability at least 1-epsilon, where epsilon ranges from 0.026 to 0.045 in still water and 0.029 to 0.044 in waves. The hardware experi

Load-bearing premise

The guarantees collapse if the box built from the extremes of about 100 disturbance measurements does not contain the disturbances the vessel actually meets at deployment; the paper assumes no distribution shift and reports that 2 of 60 wave trials already fell outside that box.

Editorial extensions

If this is right

  • Offline-computed reachable tubes make the online monitor cheap: evaluation ran at about 1.4 Hz on hardware, and the optimization problems admit parallelization or closed forms for linear predicates.
  • The monitor's robustness intervals widen under waves, reflecting uncertainty instead of hiding it, yet decision quality improves: pacSTL had 0 collisions and 100% detection in the tested wave trials, while STL and TCPA had nonzero miss or collision rates.
  • The sim-to-real calibration can be validated a posteriori: over 60 wave trials, only 2 measured disturbance samples fell outside the offline support, suggesting the tube remains valid under the tested conditions.
  • Because the dynamics are invariant under translation and equivariant under rotation, one set of reachable tubes serves multiple scenarios and vessel pairs, reducing offline computation.
  • pacSTL handles more expressive specifications: a transition-based formula (not encounter then G encounter) still detects 100% of encounters at an average time to evasion close to the simple formula, while STL detects only sporadically.

Reading between the lines

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

  • A natural extension is to carry the same support-calibration recipe into other relative-state monitoring problems, such as aerial or ground collision avoidance, whenever a high-fidelity simulator and a handful of real-world trials can bound an additive disturbance; the open step is deriving PAC guarantees when both agents' reachable sets are uncertain.
  • If the disturbance support is misspecified, the epsilon-PAC guarantee degrades silently; a cheap stress test would be to rerun support estimation at a different wave height or spectrum and watch how the fraction of out-of-support test trials and the empirical collision rate move.
  • The factor-of-two sampling mismatch between disturbance and control signals implies an implicit bandwidth assumption on the environment; faster-varying disturbances than the pool trials would require finer disturbance sampling or a different reachable-set parameterization.
  • The motion-capture setup removes ego-state uncertainty, which is unlikely at full scale; folding ego reachable sets into the other-vessel tubes, as the authors suggest, would let the same framework handle noisy GPS and compass observations.
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 / 5 minor

Summary. The paper proposes a real-time monitoring framework for maritime navigation that combines pacSTL, a probabilistic signal temporal logic with PAC bounds, with data-driven reachable sets. The authors characterize a disturbance distribution from roughly 100 physical trials, embed it in a 6-DOF simulation, compute PAC-bounded reachable tubes via scenario optimization with holdout verification, and define COLREG-inspired encounter predicates. They report hardware experiments with waves showing earlier detection and lower collision rates than STL and TCPA baselines, plus ablation studies on specification complexity, time horizon, and vessel type.

Significance. If the claims hold, the paper offers a practical template for uncertainty-aware temporal logic monitoring with modest data requirements: offline simulation plus limited experimental calibration, online evaluation at about 1.4 Hz. The hardware experiments, a posteriori disturbance checks, ablations, and anonymous code release are concrete strengths. The main risk is that the probabilistic guarantees are only proven with respect to a simulation distribution whose support is inferred from limited trials; the paper itself concedes distribution shift is neglected and reports 2/60 deployment trials outside the assumed support. This makes the headline quantitative claims conditional on an unverified extrapolation.

major comments (2)
  1. [Sec. III and Sec. VI-C] The disturbance support S_D is defined in Sec. III as the component-wise extrema of b (Eq. 17) from approximately 100 trials, and the distribution is modeled as uniform over that box. The PAC accuracies reported in Sec. V-B (epsilon in [0.026,0.045] for tubes) are computed with respect to this simulation distribution, i.e., i.i.d. samples from U(S_D). The a posteriori check in Sec. VI-C shows 2 of 60 wave trials fall outside S_D. The paper argues informally that occasional support violations need not imply reachable-set violations, but no quantitative sensitivity analysis is given. Since every downstream pacSTL robustness interval inherits the reachable-tube guarantee only for trajectories under the assumed disturbance distribution, the deployment-time validity of the claimed 0.00 collision rate and 1.00 detection rate under waves is not established. This is load-bearing for the main exp
  2. [Table II (Sec. VI-A)] The claim that pacSTL 'reduces collision rates' under waves relies on very small counts. In the head-on wave condition, pacSTL has 0 collisions out of 8 observed encounters, STL has 3 out of 8, and TCPA has 1 out of 10. With n=8, the difference between 0/8 and 3/8 is within ordinary sampling variability, and no confidence intervals or hypothesis tests are reported. Similarly, detection-rate differences (e.g., 0.75 vs 1.00 for head-on waves) are based on a handful of events. This does not invalidate the framework, but the experimental evidence for the central quantitative comparison is weaker than the text suggests. Additional trials or a statistical treatment (e.g., Wilson intervals, Fisher's exact test) are needed to support the headline performance gap.
minor comments (5)
  1. [Sec. V-B] Typo: 'JONSW AP' should be 'JONSWAP'; also the reference formatting in [35] is inconsistent.
  2. [Fig. 6] The axes are labeled only as 'bu (surge)' and 'bv (sway)'; it would be helpful to state explicitly that the teal box is the projection of the four-dimensional b-support S_D and that the other disturbance components are omitted for visualization.
  3. [Eq. (9)] The notation [ψ O_t, ψ O_t] is ambiguous because both lower and upper bounds are typeset with the same overline/underline as the interval endpoints. The case-wise definition of the orientation_halfplane function should be written more explicitly, especially the handling of angles more than π/2 from the threshold.
  4. [Sec. V-C] There are a few formatting issues: 'v destturn', 'd turn = v destturn', and 't turn = 30 s' are not clearly defined as equations; 'v des' appears in the text but not in Table I.
  5. [Fig. 4] The caption says 'worst-case robustness' but the plotted quantity is not defined. State whether this is the lower robustness bound, the upper bound, or a minimum over trials of one of these.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the framework builds on prior formal results and is validated against independent baselines.

full rationale

The paper's derivation chain is: (i) estimate disturbance support S_D from physical trials; (ii) simulate trajectories with uniform disturbances on S_D; (iii) construct ellipsoidal reachable tubes using scenario optimization and holdout verification from prior work [12], [31]; (iv) evaluate pacSTL atomic propositions over these tubes using interval semantics from prior work [15]; (v) measure detection/collision outcomes on hardware against STL and TCPA baselines. No step redefines its conclusion as an input. The pacSTL semantics and scenario-optimization guarantees are cited from prior, peer-reviewed formal work; they are not fitted values from this paper's experiments, and the paper's experiments provide external evidence via the baseline comparison and the a posteriori disturbance check. The acknowledged assumption of no distribution shift between characterization and deployment (Sec. V-B) and the observation that 2/60 wave trials fall outside S_D (Sec. VI-C) are validity/extrapolation concerns, not circularity: reachable-set validity under a different true disturbance distribution would degrade, but that is a limitation of the support estimate, not an equation reducing a prediction to its input. The reliance on self-cited prior methods is real but does not make the central claim tautological.

Assumptions & free parameters 5 free parameters · 5 assumptions · 2 invented entities

The paper's new conceptual contribution is the pipeline that maps limited real-world disturbance trials into a uniform bounded support, injects it into simulation, and generates PAC-bounded reachable sets for pacSTL. The load-bearing free parameters are the support extrema and the uniform distribution choice, while the main axioms are the absence of distribution shift and the validity of the 6-DOF model plus b. The invented entities are procedural (the calibrated support and the maritime predicates) rather than new physical objects.

free parameters (5)
  • Disturbance support S_D from component-wise extrema of b over ~100 trials = Set by extrema of measured b
    The support of the disturbance distribution is estimated directly from limited physical trials; this is a fitted quantity on which the reachable sets and PAC guarantees depend.
  • Uniform distribution assumption on S_D = Uniform over extrema box
    With no prior distribution, the paper assumes mu_D = Uniform(S_D), which is an ad hoc modeling choice affecting reachable set construction.
  • Global translation/rotation invariance of reachable sets = Used to partition initial surge velocity into four intervals
    The paper exploits system invariance to reduce offline computation by only computing reachable tubes for a few initial velocity intervals.
  • Time horizon t_h for collision risk = Default 10, tested 20
    The horizon parameter is user-chosen and materially affects detection time t_e (6.8 s vs 4.0 s), showing the metric is sensitive to this choice.
  • Initial-state velocity intervals U_i = 4 intervals spanning experimental operating speeds
    The initial state distribution is a modeling choice based on the operating conditions, affecting the reachable sets.
assumptions (5)
  • domain assumption Disturbance support S_D is exactly captured by component-wise extrema of ~100 experimental trials
    The paper states 'we assume no distribution shift between disturbance characterization and deployment' and validates with only 2/60 wave trials outside support; this is a load-bearing domain assumption.
  • ad hoc to paper The disturbance distribution is uniform over the identified support
    Modeling mu_D as uniform is justified in the absence of additional distributional information; it is an assumption introduced to enable sampling-based reachability.
  • standard math The 6-DOF vessel model (16) plus b captures all relevant disturbances
    The paper computes b from (17) and treats it as the full disturbance; any unmodeled dynamics are implicitly assumed negligible.
  • standard math Holdout-based scenario optimization yields PAC-bounded reachable sets (methods of [12], [31])
    The paper builds on scenario optimization and the holdout method from prior work; the guarantees hold only under i.i.d. sampling from the assumed distributions.
  • domain assumption Reachable tubes for the other vessel are independent and the ego vessel's state uncertainty is neglected
    The paper confines uncertainty to the ego vessel's predicted trajectory and the other vessel's reachable set; the motion capture system provides accurate ego state, but full-scale applications would need joint multi-agent reachable sets.
invented entities (2)
  • Sim-to-real calibrated disturbance support S_D independent evidence
    purpose: Bridges the sim-to-real gap by injecting measured vessel disturbance into a 6-DOF simulator for reachable set computation
    The support is grounded in physical trials and is checked a posteriori against 60 wave trials (2/60 violations), providing a falsifiable handle outside the paper itself.
  • pacSTL maritime monitoring predicates (pos encounter, ori encounter, collision risk)
    purpose: Specialized atomic propositions for head-on and crossing encounters, derived from COLREG, enabling real-time pacSTL evaluation
    These are a reformulation of COLREG rules; they are not a new physical entity, but a new specification vocabulary. They are internally validated via experiments but lack an external benchmark.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Staying on Spec: Real-Time Monitoring under Uncertainty with a Maritime Case Study." pith.science (2026). https://pith.science/paper/PD7NYBHD

@misc{pith2026260802811,
  author       = {Pith},
  title        = {Pith review of: Staying on Spec: Real-Time Monitoring under Uncertainty with a Maritime Case Study},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PD7NYBHD}},
  note         = {Machine review of arXiv:2608.02811}
}
read the original abstract

Robotic systems must operate under uncertainty while satisfying complex task and safety specifications. Monitoring such specifications under uncertainty remains challenging, as existing formulations typically require extensive data or explicit uncertainty distributions. In this paper, we propose a real-time monitoring framework that reduces data requirements by leveraging data-driven reachable sets for specification evaluation. We instantiate the framework for maritime navigation, where complex specifications arise from traffic rules. We develop a data-efficient pipeline for constructing reachable sets and derive a monitoring formulation suitable for real-time deployment. Simulation and hardware experiments demonstrate robust monitoring under realistic disturbances, achieving improved risk detection compared to state-of-the-art metrics.

Figures

Figures reproduced from arXiv: 2608.02811 by the authors.

Figure 1
Figure 1. Offline: We use experimental data to characterize the disturbance dis [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Illustrative computation of three orientation halfplane robust￾ness intervals. The colored sectors represent orientation intervals projected from reachable sets, and the blue line denotes the robustness satisfaction boundary. The yellow example illustrates an orientation interval that overlaps the satisfaction boundary. The purple example shows the case in which the lower and upper robustness bounds are reversed. In… view at source ↗
Figure 3
Figure 3. Example evaluation pacSTL specification ϕ, which is based on the example atomic proposition encounter. The resulting robustness interval of ϕ, here [−1.0, 2.4], is endowed with a probabilistic guarantee on the robust￾ness value of an unseen trajectory being contained within the interval. The robustness intervals are used to monitor critical encounters and, consequently, trigger an evasive maneuver reliably for still… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Worst-case robustness over time for head-on encounters, comparing [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Smoothed mean of pacSTL robustness intervals over time (dark, inner [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: Measured disturbance btest in surge and sway from 60 wave trials (purple points), plotted against the b-component of the support SD used for offline, reachable-set computation (teal box) [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

35 extracted references · 30 canonical work pages

  1. [1]

    Reinforcement learning with temporal logic rewards,

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

    work page 2017

  2. [2]

    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

    work page 2021

  3. [3]

    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

  4. [4]

    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 Insti- tution of Mechanical Engineers, Part O: Journal of Risk and Reliability, vol. 237, no. 2, pp. 293–313, 2023

    work page 2023

  5. [5]

    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

    work page Pith review arXiv 2025

  6. [6]

    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,” inIEEE/OES Autonomous Underwater Vehicles Symposium (AUV), 2024, pp. 1–6

    work page 2024

  7. [7]

    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

    work page 2024

  8. [8]

    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

    work page 2025

Show all 35 references
  1. [9]

    Online data- driven reachability analysis using zonotopic recursive least squares,

    A. N. Akhormeh, A. Hegazy, and A. Alanwar, “Online data- driven reachability analysis using zonotopic recursive least squares,” arXiv:2509.17058, 2025

    2025

  2. [10]

    Enhancing data-driven reachability analysis using temporal logic side information,

    A. Alanwar, F. J. Jiang, M. Sharifi, D. V . Dimarogonas, and K. H. Johansson, “Enhancing data-driven reachability analysis using temporal logic side information,” in2022 International Conference on Robotics and Automation (ICRA), 2022, pp. 6793–6799

    2022

  3. [11]

    Reachset-conformant system identification,

    L. L ¨utzow and M. Althoff, “Reachset-conformant system identification,” IEEE Transactions on Automatic Control, vol. 71, no. 5, pp. 3014–3029, 2026

    2026

  4. [12]

    Estimating reachable sets with scenario optimization,

    A. Devonport and M. Arcak, “Estimating reachable sets with scenario optimization,” inLearning for Dynamics & Control Conference (L4DC), 2020, pp. 75–84

    2020

  5. [13]

    Pick-to-learn for systems and control: theoretical review with a showcase in reachability analysis,

    D. Paccagnan, D. Marks, M. C. Campi, and S. Garatti, “Pick-to-learn for systems and control: theoretical review with a showcase in reachability analysis,” inIEEE Conference on Decision and Control (CDC), 2025, pp. 1980–1985

    2025

  6. [14]

    Nonconvex Scenario Opti- mization for Data-Driven Reachability,

    E. Dietrich, A. Devonport, and M. Arcak, “Nonconvex Scenario Opti- mization for Data-Driven Reachability,” inLearning for Dynamics & Control Conference (L4DC), 2024, pp. 514–527

    2024

  7. [15]

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

    H. Krasowski, E. Dietrich, E. C. Gezer, R. Skjetne, A. J. Sørensen, and M. Arcak, “pacSTL: PAC-Bounded Signal Temporal Logic from Data- Driven Reachability Analysis,”IEEE Control Systems Letters, 2026

    2026

  8. [16]

    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,” inProceedings of Robotics: Science and Systems XII, June 2016

    2016

  9. [17]

    Control with Probabilistic Signal Temporal Logic,

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

    2015 arXiv

  10. [18]

    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

  11. [19]

    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

  12. [20]

    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

  13. [21]

    Interval Signal Temporal Logic From Natural Inclusion Functions,

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

    2023

  14. [22]

    Data-Driven Reachability Analysis with Christoffel Functions,

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

    2021

  15. [23]

    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

  16. [24]

    Hamilton–Jacobi reachability: Some recent theoretical advances and applications in unmanned airspace manage- ment,

    M. Chen and C. J. Tomlin, “Hamilton–Jacobi reachability: Some recent theoretical advances and applications in unmanned airspace manage- ment,”Annual Review of Control, Robotics, and Autonomous Systems, vol. 1, no. 1, pp. 333–358, 2018

    2018

  17. [25]

    Information theory and statistical mechanics,

    E. T. Jaynes, “Information theory and statistical mechanics,”Phys. Rev., vol. 106, pp. 620–630, May 1957

    1957

  18. [26]

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

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

    1972

  19. [27]

    Temporal Logic Formalization of Marine Traffic Rules,

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

    2021

  20. [28]

    Formalizing testing of collision avoidance systems using signal temporal logic,

    T. A. Pedersen, C. Vasanthan, M. Hemrich, K. B. Karolius, and S. Kemna, “Formalizing testing of collision avoidance systems using signal temporal logic,” inProceedings of the European Safety and Reliability conference (ESREL), 2025

    2025

  21. [29]

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

    2011

  22. [30]

    Data-driven reachability and support estimation with Christoffel functions,

    A. Devonport, F. Yang, L. E. Ghaoui, and M. Arcak, “Data-driven reachability and support estimation with Christoffel functions,”IEEE Transactions on Automatic Control, vol. 68, no. 9, pp. 5216–5229, 2023

    2023

  23. [31]

    Data-Driven Reach- ability with Scenario Optimization and the Holdout Method,

    E. Dietrich, R. Devonport, S. Tu, and M. Arcak, “Data-Driven Reach- ability with Scenario Optimization and the Holdout Method,” inIEEE Conference on Decision and Control (CDC), 2025, pp. 3925–3931

    2025

  24. [32]

    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

  25. [33]

    Unmanned aircraft systems in the national airspace system: a formal methods perspective,

    C. A. Mu ˜noz, A. Dutle, A. Narkawicz, and J. Upchurch, “Unmanned aircraft systems in the national airspace system: a formal methods perspective,” vol. 3, no. 3, pp. 67—-76, 2016

    2016

  26. [34]

    Path planning and collision avoidance for autonomous surface vehicles i: a review,

    A. Vagale, R. Oucheikh, R. T. Bye, O. L. Osen, and T. I. Fossen, “Path planning and collision avoidance for autonomous surface vehicles i: a review,”Journal of Marine Science and Technology, vol. 26, no. 4, pp. 1292–1306, 2021

    2021

  27. [35]

    Measurements of wind-wave growth and swell decay during the joint north sea wave project (JONSW AP),

    K. Hasselmann, T. P. Barnett, E. Bouws, H. Carlson, D. E. Cartwright, K. Enke, J. A. Ewing, H. Gienapp, D. E. Hasselmann, P. Kruseman, A. Meerburg, P. M¨uller, D. J. Olbers, K. Richter, W. Sell, and H. Walden, “Measurements of wind-wave growth and swell decay during the joint ...

    1973

Pith tools

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