SAFE-SMART: Safety Analysis and Formal Evaluation using STL Metrics for Autonomous RoboTs

TL;DR

This work tackles the challenge of safely evaluating learning-based, black-box autonomous robots by introducing SAFE-SMART, a regulator-driven framework that translates human safety rules into STL specifications and uses rollout traces verified by TeLEx to compute TRV and LRV. The approach is model-agnostic and provides actionable feedback to designers for iterative retraining, demonstrated on two distinct domains: a virtual Mario Kart driving task and TurtleBot3 obstacle navigation, including real-world validation. Results show significant improvements in safety-rule adherence after retraining, with statistically robust gains across all rules in both scenarios and evidence of practical impact through real-world demonstrations. The study highlights the potential and limitations of regulator-guided STL verification for scalable, formal safety guarantees in learning-based autonomous robots.

Abstract

We present a novel, regulator-driven approach for post hoc safety evaluation of learning-based, black-box autonomous mobile robots, ensuring ongoing compliance with evolving, human-defined safety rules. In our iterative workflow, human safety requirements are translated by regulators into Signal Temporal Logic (STL) specifications. Rollout traces from the black-box model are externally verified for compliance, yielding quantitative safety metrics, Total Robustness Value (TRV) and Largest Robustness Value (LRV), which measure average and worst-case specification adherence. These metrics inform targeted retraining and iterative improvement by model designers. We apply our method across two different applications: a virtual driving scenario and an autonomous mobile robot navigating a complex environment, and observe statistically significant improvements across both scenarios. In the virtual driving scenario, we see a 177% increase in traces adhering to the simulation speed limit, a 1138% increase in traces minimizing off-road driving, and a 16% increase in traces successfully reaching the goal within the time limit. In the autonomous navigation scenario, there is a 300% increase in traces avoiding sharp turns, a 200% increase in traces reaching the goal within the time limit, and a 49% increase in traces minimizing time spent near obstacles. Finally, we validate our approach on a TurtleBot3 robot in the real world, and demonstrate improved obstacle navigation with safety buffers.

Figures (7)

• Figure 1: Overview of SAFE-SMART, an approach to incorporating human-defined safety rules into a learning-based robot navigation scenario. Rollout traces from an initial, unverified model are systematically checked for unsafe trajectories that violate formally defined safety specifications. Through iteration of the SAFE-SMART workflow, the retrained black-box model is able to produce safe trajectories that complies with safety specifications. We show the performance of the pre-analysis RL-based navigation algorithm at the top (pink) and the post-analysis RL algorithm with a different reward function at the bottom (green). The latter generates safer trajectories, as shown via different metrics.
• Figure 2: Overview of SAFE-SMART. Regulators construct safety requirements as formal verification specifications. Rollout traces from learning-based, black-box autonomous robots are checked for formal compliance, producing safety metrics that are fed back to Designers for iterative model improvement. Our compliance metrics are generated independently of model internals, without needing transparency or access to the black-box model.
• Figure 3: Role of the Regulator: Regulatory personnel translate human-defined safety rules into Signal Temporal Logic (STL) specifications. Using verification tools such as TeLEx Jha2017TeLExPS, we evaluate the compliance of learning-based controllers over rollout traces, and extract the robustness values for each rule. We use these robustness metrics to quantify the degree to which the system satisfies or violates the safety specification. The resulting information, indicating how well the system adheres to each requirement, is then communicated back to the model designers to guide further development and improvement of the autonomous robot system.
• Figure 4: Traces visualized on the Mario Kart (SNES) platform with red segments marking violations of the Global Speed Limit rule. Our approach significantly reduce the number of safety violations.
• Figure 5: TurtleBot3 scenarios in simulation (\ref{['subfig:gazebo']}) and real-world (\ref{['subfig:real']}). The red circles indicate approximate goal locations.