RACE-Nav: Refinable Occupancy Contracts and Prefix-Wide Runtime Assurance for Dynamic Mobile-Robot Navigation

Abstract

Modular navigation stacks permit predictors and controllers to be exchanged, but their uncertainty, timing, and braking assumptions rarely form one executable assurance argument. RACE-Nav introduces typed, refinable occupancy contracts whose guaranteed class, hazard scope, frame, horizon, risk allowance, and expiry are checked before command release. A model-conditional radial provider supplies the closed-loop conditional premise used by the risk ledger; marginal split conformal prediction is retained only as a diagnostic. Concrete trajectories are certified by finite sampled tests with Hausdorff-Lipschitz inter-sample margins and a prefix-wide recoverable-stop condition. A horizon-aware lease and downstream watchdog preserve the trusted-gate invariant under cancellation and provider substitution. We prove provider refinement, continuous-time separation, swept-stop safety, finite/anytime risk composition, stale-command exclusion, non-Zeno switching, and conditional release liveness. In a held-out paired-seed benchmark spanning eight dynamic interactions and six controllers (1,920 episodes), RACE-Nav produced 0/320 collisions (95% Wilson interval 0.00%-1.19%) and 97.5% goal success versus 12.2% collisions for the predictive time-to-collision/model predictive control comparator. The decision kernel recorded 0 and modelled 300-ms deadline misses. Stress and ablation results separate guaranteed behaviour from violations of the declared model and actuator bounds.