ROVER: Regulator-Driven Robust Temporal Verification of Black-Box Robot Policies

I. INTRODUCTION

• Temporal verification is needed because aggregate failure rates and single-state checks can miss persistence, sequencing, oscillation, and gradual drift in robot behavior.STL captures safety requirements spanning time intervals and event sequences rather than only isolated states or trajectory statistics.Source: §I · p. 1
• ROVER evaluates opaque autonomy stacks through formal, trajectory-level STL assessments of rollout traces without internal controller access.The specifications cover behaviors such as lane keeping, acceleration, and turning, while robustness metrics summarize satisfaction and violation severity.Source: §I · p. 1
• ROVER evaluates reinforcement-learning rollout traces in a virtual racing game and an autonomous mobile-robot platform using TRV, LRV, and AVRV.These metrics guide targeted reward restructuring and retraining, producing post-verification models with higher satisfaction rates in both domains.Source: §I · pp. 1–2
• 43.8% average satisfaction-rate improvement across six STL specifications followed regulator-guided retraining over two scenarios.The approach also improved TRV for all specifications and produced better LRV and AVRV in three of six specifications.Source: §I · p. 2

II. BACKGROUND AND RELATED WORKS

• Formal-methods research includes policy synthesis, but ROVER instead verifies existing policies whose internal training and controller structure are unavailable.This distinction places the work in black-box policy verification rather than synthesis-oriented methods.Source: §II · p. 2

A. White-Box Verification

• White-box verification methods use internal models for reachability, model checking, certificates, or STL-based analysis, limiting their applicability to opaque controllers.These methods can also struggle with high-dimensional learning-based controllers and may not provide actionable retraining feedback.Source: A. White-Box Verification · p. 2

B. Black-Box Verification

• Black-box validation commonly relies on finite-state surrogates, runtime assurance, scenario testing, or statistical failure estimates rather than formal temporal trajectory analysis.A cited Bayesian approach still assumes restricted gray-box visibility, limiting applicability to high-dimensional nonlinear black-box controllers.Source: B. Black-Box Verification · pp. 2–3
• ROVER addresses a gap in formally grounded, trajectory-level verification of temporal behavior for learning-based black-box robot policies.It complements policy synthesis and simulation-based testing by applying STL specifications and robustness measures to observed executions.Source: B. Black-Box Verification · p. 3, §III · p. 3

III. OUR APPROACH: ROVER

• ROVER uses an iterative regulator–designer loop in which safety evaluation produces recommendations for policy updates and improved specification satisfaction.The regulator evaluates the black-box system, then the designer revises the policy to better satisfy temporal requirements.Source: §III · p. 3

A. Modeling The System

• The robot is modeled as a discrete-time dynamical system whose policy maps states to control inputs and induces rollout trajectories.For an initial condition, the policy generates traces collected into a possibly random trace set Tπ.Source: A. Modeling The System · p. 3

B. Regulator Specifications

• The Regulator specifies a finite set of STL requirements while remaining external to and unable to inspect the internal policy.Each specification can encode safety, social-compliance, or mission constraints.Source: B. Regulator Specifications · p. 3
• STL robustness ρ(ϕi, τ) is positive for robust satisfaction, zero at exact satisfaction, and negative for violation.Its absolute value measures the margin of satisfaction or violation for a trace with respect to a specification.Source: B. Regulator Specifications · p. 3

• ROVER computes an N × m matrix of robustness scores by evaluating each rollout trace against each STL specification.Source: C. Robustness Evaluation · p. 3
• TRV aggregates robustness across all rollout traces to represent the model’s average safety margin.Higher TRV indicates that most scenarios maintain a comfortable safety margin under normal operating conditions.Source: C. Robustness Evaluation · p. 3
• LRV captures the single most critical violation among rollout traces, while AVRV measures average violation severity across failing traces.Source: C. Robustness Evaluation · p. 3
• Robustness is interpreted per rule: large negative values indicate severe violations, values near zero indicate borderline outcomes, and positive values indicate comfortable satisfaction margins.The analysis focuses on negative robustness when quantifying violation severity.Source: C. Robustness Evaluation · p. 3

1) Domain Experts:

• Domain experts assign positive weights to specifications to encode their relative criticality and define a safety score for comparing candidate policies.Designers can use the score to guide reward shaping or retraining.Source: 1) Domain Experts · p. 4

2) Recommendations:

• Policies with TRV, LRV, and AVRV near zero receive no recommendation because they satisfy the specification with small robustness dispersion.Source: 2) Recommendations · p. 4

2. Recommend policy improvement (systematic viola-

• Large-magnitude negative TRV, LRV, and AVRV indicate frequent or severe violations and trigger policy-improvement recommendations.Source: §2 · p. 4

3. Recommend edge-case analysis (rare but severe

• When LRV is much lower than AVRV, regulators flag rare but catastrophic failures and recommend targeted edge-case analysis.Source: §3 · p. 4
• Recommendation categories are communicated alongside the safety score to provide quantitative scores and qualitative guidance for subsequent model updates.Source: §3 · p. 4

D. Designer Formulation

• Designers optimize task reward and safety adherence, then decide whether to keep, retrain, or replace the black-box policy using regulator recommendations.Source: D. Designer Formulation · p. 4
• ROVER is positioned for regulators evaluating deployed opaque policies rather than policy synthesis, coverage optimization, or rare-event simulation.The approach addresses temporal robustness-based verification of exercised behaviors.Source: D. Designer Formulation · p. 4, E. Verification using STL · p. 4

E. Verification using STL

• The application uses PPO for the RL policy, while ROVER remains agnostic to the specific black-box learning algorithm.Source: E. Verification using STL · p. 4
• Human-defined safety rules are translated into STL, and rollout robustness values are aggregated into TRV, LRV, AVRV, safety scores, and recommendations.Source: E. Verification using STL · p. 4
• The workflow evaluates a pre-verification model, updates its reward structure from compliance metrics, and reevaluates a post-verification model.Source: E. Verification using STL · p. 4

IV. VIRTUAL RACING GAME

• The Mario Kart case study uses a controlled, reproducible simulation with a trained driving policy and STL-defined safety rules.Source: §IV · p. 4
• Evaluation uses fixed goal and environmental conditions, but generates 100 distinct rollout traces because the policy is probabilistic.Source: §IV · pp. 4–5

• The Mario Kart specification set contains three scenario-specific safety requirements represented as individual STL formulas.Source: A. Mario Kart STL Rules · p. 5
• The Global Speed Limit rule requires the car to remain below 90 kph.Source: A. Mario Kart STL Rules · p. 5
• The Stay on Track rule requires an off-track car to return to the track within 60 timesteps.Its STL form specifies globally that leaving the track implies eventual track recovery within the bounded window.Source: A. Mario Kart STL Rules · p. 5
• The Wait to Accelerate rule forbids acceleration after a sharp turn begins until the turn rate has substantially stabilized.The rule uses ˙ψ > 1 for sharp turning and requires waiting until ˙ψ < 0.04.Source: A. Mario Kart STL Rules · p. 5
• Figure 1 marks Global Speed Limit violations with red trace segments and reports fewer safety violations after retraining.Source: Figure 1 · p. 5

• Satisfaction percentage measures Boolean pass/fail frequency across traces, while TRV, LRV, and AVRV quantify robustness and violation severity.Positive STL robustness indicates satisfaction; negative values indicate violation.Source: B. Model Evaluation and Discussion · p. 5
• 53% compliance improvement followed a specification with frequent, severe violations and strongly negative AVRV and LRV.Source: Table I · p. 5
• 91% compliance improvement followed a specification with almost-constant severe violations and low TRV, LRV, and AVRV.Source: Table II · p. 5
• The largely satisfied specification had mild or moderate violations, so regulators recommended prioritizing other rules.Source: Table III · p. 5, B. Model Evaluation and Discussion · p. 5
• Reward restructuring increased penalties for extended track departures and speeding, shifting the balance between task reward and the safety score S(π).Source: B. Model Evaluation and Discussion · pp. 5–6

V. MOBILE ROBOT NAVIGATION

• The TurtleBot3 must reach a randomly selected target while avoiding obstacles, using five discrete angular velocities, constant linear speed, and 24 lidar points over 180 degrees.Source: §V · p. 6
• The pre-verification reward combines goal-alignment yaw reward, obstacle-proximity penalty, and a terminal success-or-failure reward.Source: §V · p. 6
• The pre-verification model was trained for 500 episodes and exhibited unsafe behavior as an under-trained black-box controller.Source: §V · p. 6
• Figure 2 shows simulation and real-world TurtleBot3 scenarios, with red circles marking approximate goal locations.Source: Figure 2 · p. 6

A. TurtleBot STL Rules

• No Sharp Turns requires reducing turning rate from above 0.2 within 50 timesteps and maintaining the gentle rate for at least 5 timesteps.Source: A. TurtleBot STL Rules · p. 6
• Timed Completion requires reaching the goal within 800 timesteps.Source: A. TurtleBot STL Rules · p. 6
• Don’t Linger Near an Obstacle requires moving away within 50 timesteps after approaching within 0.5 meters.Source: A. TurtleBot STL Rules · p. 6

B. Model Evaluation and Discussion

• 53% compliance increase followed regulator recommendations for a rule with frequent but mild pre-verification violations.The pre-verification model had negative but small TRV, LRV, and AVRV values.Source: Table IV · p. 6
• 36% compliance increase followed policy improvement for a rule whose negative TRV and AVRV indicated systematic failure to finish on time.The table characterized the pre-verification model as having low satisfaction and clear negative aggregate robustness.Source: Table V · p. 6
• Regulators de-prioritized a rule with balanced pass/fail outcomes and non-catastrophic violations.The rule’s robustness profile did not indicate the same urgency as the more problematic specifications.Source: Table VI · p. 7
• Designers added an angular-acceleration penalty and increased obstacle-proximity penalties to encourage smoother turns and less lingering near obstacles.These reward changes were an explicit response to regulator feedback on poor adherence.Source: B. Model Evaluation and Discussion · pp. 6–7
• After a few hundred additional training episodes, post-verification traces showed more direct paths to goals and improved adherence to all three specifications.The navigation evaluation used per-rule robustness bands because robustness lacks a canonical cross-environment scale.Source: B. Model Evaluation and Discussion · pp. 6–7

C. Real World Experiments

• The real-world test scaled the simulation scenario to 25% and halved robot speed to accommodate indoor area restrictions and safer navigation.Both pre- and post-verification models were deployed in the resulting proxy environment.Source: C. Real World Experiments · p. 7
• Both TurtleBot3 policies reached the goal, but the post-verification policy demonstrated a comparatively smoother path in the real-world experiment.The demonstration was manually annotated and the post-verification path remained less smooth than simulation trajectories.Source: C. Real World Experiments · p. 7, Figure 4 · p. 7
• The real robot made more frequent turns than simulation trajectories, indicating a sim-to-real gap despite the post-verification improvement.The reported improvement concerns observed behavior in the real-world demonstration rather than simulation-level smoothness.Source: C. Real World Experiments · p. 7

VI. CONCLUSIONS, LIMITATIONS, AND FUTURE WORK

• ROVER evaluates opaque autonomy stacks from rollout traces by formalizing time-dependent safety requirements as STL specifications.This preserves the black-box certification setting while allowing domain experts to express temporal requirements.Source: §VI · p. 7
• TRV, LRV, and AVRV provide safety scores summarizing average performance, worst-case behavior, and violation severity for targeted retraining recommendations.Experiments across two domains and six specifications reported increased satisfaction and improved robustness metrics.Source: §VI · p. 7
• The approach remains limited by lengthy regulator–designer iteration and ambiguous human translation of specifications.It also does not yet address coverage or rare-event analysis.Source: §VI · p. 7