publications

preprints

2025

1. 

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

   Elizabeth Dietrich^*, Hanna Krasowski^*, Emir Cem Gezer, and 3 more authors

   2025

   Abs arXiv Video

   Real-world robotic systems must comply with safety requirements in the presence of uncertainty. To define and measure requirement adherence, Signal Temporal Logic (STL) offers a mathematically rigorous and expressive language. However, standard STL cannot account for uncertainty. We address this problem by presenting pacSTL, a framework that combines Probably Approximately Correct (PAC) bounded set predictions with an interval-extension of STL through optimization problems on the atomic proposition level. pacSTL provides PAC-bounded robustness intervals on the specification level that can be utilized in monitoring. We demonstrate the effectiveness of this approach through maritime navigation and analyze the efficiency and scalability of pacSTL through simulation and real-world experimentation on model vessels.

published

2025

1. 

   Data-Driven Reachability with Scenario Optimization and the Holdout Method

   Elizabeth Dietrich, Rosalyn Devonport, Stephen Tu, and 1 more author

   In Accepted for Proc. of the IEEE Conference on Decision and Control (CDC), 2025

   Abs arXiv

   Reachability analysis is an important method in providing safety guarantees for systems with unknown or uncertain dynamics. Due to the computational intractability of exact reachability analysis for general nonlinear, high-dimensional systems, recent work has focused on the use of probabilistic methods for computing approximate reachable sets. In this work, we advocate for the use of a general purpose, practical, and sharp method for data-driven reachability: the holdout method. Despite the simplicity of the holdout method, we show—on several numerical examples including scenario-based reach tubes—that the resulting probabilistic bounds are substantially sharper and require fewer samples than existing methods for data-driven reachability. Furthermore, we complement our work with a discussion on the necessity of probabilistic reachability bounds. We argue that any method that attempts to de-randomize the bounds, by converting the guarantees to hold deterministically, requires (a) an exponential in state-dimension amount of samples to achieve non-vacuous guarantees, and (b) extra assumptions on the dynamics.

2. 

   Symbolic Control for Autonomous Docking of Marine Surface Vessels

   Elizabeth Dietrich^*, Emir Cem Gezer^*, Bingzhuo Zhong, and 4 more authors

   In Accepted for Proc. of the IEEE Conference on Decision and Control (CDC), 2025

   Abs arXiv Video

   Docking marine surface vessels remains a largely manual task due to its safety-critical nature. In this paper, we develop a hierarchical symbolic control architecture for autonomous docking maneuvers of a dynamic positioning vessel, to provide formal safety guarantees. At the upper-level, we treat the vessel’s desired surge, sway, and yaw velocities as control inputs and synthesize a symbolic controller in real-time. The desired velocities are then transmitted to and executed by the vessel’s low-level velocity feedback control loop. Given a synthesized symbolic controller, we investigate methods to optimize the performance of the proposed control scheme for the docking task. The efficacy of this methodology is evaluated on a low-fidelity simulation model of a marine surface vessel in the presence of static and dynamic obstacles and, for the first time, through physical experiments on a scaled model vessel.

2024

1. 

   Nonconvex scenario optimization for data-driven reachability

   Elizabeth Dietrich, Alex Devonport, and Murat Arcak

   In Proceedings of the 6th Annual Learning for Dynamics & Control Conference, 2024

   Abs Bib PDF

   Many of the popular reachability analysis methods rely on the existence of system models. When system dynamics are uncertain or unknown, data-driven techniques must be utilized instead. In this paper, we propose an approach to data-driven reachability that provides a probabilistic guarantee of correctness for these systems through nonconvex scenario optimization. We pose the problem of finding reachable sets directly from data as a chance-constrained optimization problem, and present two algorithms for estimating nonconvex reachable sets: (1) through the union of partition cells and (2) through the sum of radial basis functions. Additionally, we investigate numerical examples to demonstrate the capability and applicability of the introduced methods to provide nonconvex reachable set approximations.

   @inproceedings{Dietrich2024,
     title = {Nonconvex scenario optimization for data-driven reachability},
     author = {Dietrich, Elizabeth and Devonport, Alex and Arcak, Murat},
     booktitle = {Proceedings of the 6th Annual Learning for Dynamics & Control Conference},
     year = {2024},
     url = {https://proceedings.mlr.press/v242/dietrich24a.html}
   }

* indicates equal contribution