An Efficient Reachability-Based Framework for Provably Safe Autonomous Navigation in Unknown Environments

TL;DR

This work addresses safe autonomous navigation in unknown environments by leveraging Hamilton-Jacobi reachability to compute a backward reachable set (BRS) and a least-restrictive safety controller, treating unseen areas as obstacles to guarantee collision avoidance. It introduces real-time BRS updates via two innovations: a warm-start scheme that reuses prior value functions and a local update method that confines computation to a small region, enabling near real-time performance. The framework is sensor- and planner-agnostic and is demonstrated across multiple sensors (LiDAR, camera) and planners (e.g., RRT, spline-based) in both simulation and hardware (TurtleBot 2), including a safety demonstration around a learning-based RGB planner. The results show that the approach provides provable safety with only modest conservatism early in exploration and achieves practical online update speeds, enabling safe integration with diverse autonomous systems. This work thus offers a scalable, provably safe method for autonomous navigation in unknown static environments and lays groundwork for extensions to imperfect perception and dynamic multi-agent settings.

Abstract

Real-world autonomous vehicles often operate in a priori unknown environments. Since most of these systems are safety-critical, it is important to ensure they operate safely in the face of environment uncertainty, such as unseen obstacles. Current safety analysis tools enable autonomous systems to reason about safety given full information about the state of the environment a priori. However, these tools do not scale well to scenarios where the environment is being sensed in real time, such as during navigation tasks. In this work, we propose a novel, real-time safety analysis method based on Hamilton-Jacobi reachability that provides strong safety guarantees despite environment uncertainty. Our safety method is planner-agnostic and provides guarantees for a variety of mapping sensors. We demonstrate our approach in simulation and in hardware to provide safety guarantees around a state-of-the-art vision-based, learning-based planner.

Figures (6)

• Figure 1: Overview: We consider the problem of safe navigation from an initial state to a goal state in an a priori unknown environment. Our approach treats the unsensed environment as an obstacle, and uses a HJ reachability framework to compute a safe controller for the vehicle, which is updated in real-time as the vehicle explores the environment. We show an application of our approach on a Turtlebot using a vision-based planner. When the robot is at risk of colliding, the safe controller ($u^{*}$) keep the system safe.
• Figure 2: The initial setup for the running example. The goal is to safely reach the goal (center of the green area) from the initial position (black marker) in the presence of an unknown obstacle (the grey square). We also show the initial sensing region for the LiDAR and camera sensors.
• Figure 3: The vehicle trajectories for the problem setting in Figure \ref{['fig:initial_setup_running_example']} for both planners (RRT and Spline planners) and both sensors (LiDAR and Camera sensors) with the safety controller computed from each of the three candidate safety approaches. The proposed framework is able to safely navigate the vehicle to the goal in all cases. When the planner makes unsafe decisions, the safety controller intervenes (the states marked in red) to ensure safety.
• Figure 4: (a) The sensed region by the vehicle at different states in time for the camera sensor. (b) The overall free space sensed by the vehicle and the corresponding safe set (interior of the red boundary). Since the vehicle is at the boundary of the safe set, the safety controller $u^{*}$ is applied to steer the robot inside the safe set and ensure collision avoidance.
• Figure 5: The proposed framework can be exploited to provide safety guarantees around vision-based planners that incorporate learning in the loop. The vision-based planner plans a path through the doorway. Without safety control (a) this results in collision, however with safety (b) the robot avoids collision and reaches the goal.

Theorems & Definitions (2)

• Lemma 1
• proof