9 papers
Expressiveness, Equivalence, and Uncertainty in Velocity Obstacles and Closest Point of Approach Metrics
Elizabeth Dietrich, Liam M. Imagawa, Hanna Krasowski +3
Time to Closest Point of Approach (TCPA), Distance to Closest Point of Approach (DCPA), and Velocity Obstacles (VOs), are widely used to assess and mitigate collision risk in auton…
Staying on Spec: Real-Time Monitoring under Uncertainty with a Maritime Case Study
Elizabeth Dietrich, Hanna Krasowski, Emir Cem Gezer +3
Robotic systems must operate under uncertainty while satisfying complex task and safety specifications. Monitoring such specifications under uncertainty remains challenging, as exi…
Finite-Step Invariant Sets for Hybrid Systems with Probabilistic Guarantees
Varun Madabushi, Elizabeth Dietrich, Hanna Krasowski +1
Poincare return maps are a fundamental tool for analyzing periodic orbits in hybrid dynamical systems, including legged locomotion, power electronics, and other cyber-physical syst…
Probably Approximately Correct Guarantees for Data-Driven Reachability Analysis: A Theoretical and Empirical Comparison
Elizabeth Dietrich, Hanna Krasowski, Murat Arcak
Reachability analysis evaluates system safety by identifying the set in which states may evolve over a time horizon. Data-driven reachability analysis estimates reachable sets and…
Importance Sampling for Statistical Certification of Viable Initial Sets
Elizabeth Dietrich, Hanna Krasowski, Vegard Flovik +1
We study the problem of statistically certifying viable initial sets (VISs)---sets of initial conditions whose trajectories satisfy a given control specification. While VISs can be…
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
Hanna Krasowski, Elizabeth Dietrich, Emir Cem Gezer +3
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…
Data-Driven Reachability with Scenario Optimization and the Holdout Method
Elizabeth Dietrich, Rosalyn Devonport, Stephen Tu +1
Reachability analysis is an important method in providing safety guarantees for systems with unknown or uncertain dynamics. Due to the computational intractability of exact reachab…
Symbolic Control for Autonomous Docking of Marine Surface Vessels
Elizabeth Dietrich, Emir Cem Gezer, Bingzhuo Zhong +4
We develop a hierarchical control architecture for autonomous docking maneuvers of a dynamic positioning vessel and provide formal safety guarantees. At the upper-level, we treat t…
A beginner guide to Iris, Coq and separation logic
Elizabeth Dietrich
Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are us…