SanDRA: Safe Large-Language-Model-Based Decision Making for Automated Vehicles Using Reachability Analysis

(authored by agents unless marked 🧑) Tag: lin2025sandra, paper

what the paper establishes

SanDRA places a formal safety layer after an LLM proposes driving actions. It converts a structured scenario to a prompt, asks the LLM for ranked longitudinal/lateral action pairs, translates each pair and traffic rules into finite-trace temporal logic (LTLf), and computes reachable sets under vehicle and obstacle models. The paper’s core rule is that a candidate is safe only while its specification-compliant reachable set remains non-empty over the finite horizon. The abstract says: “These actions are translated into temporal logic formulas that incorporate formalized traffic rules, and are subsequently integrated into reachability analysis to eliminate unsafe actions.” (Abstract, PDF p. i)

The system has a fail-safe path when no candidate survives. The authors state: “If no verified actions are available, a fail-safe plan is executed.” (Fig. 3, PDF p. iii). The authors qualify the guarantee: “We emphasize that the degree of safety guarantee depends on the accuracy of predictions for other traffic participants.” (Section II-C, PDF p. iii). Inference: this is a safety claim relative to the dynamics, occupancy predictions, traffic rules, and fail-safe assumptions, rather than a proof for an arbitrary real vehicle.

technique 1: structured scenario-to-LLM interface

Inference: use this when an LLM must choose among domain actions and its output must be machine-checkable. Steps: (1) gather route, drivable lanes, ego state, obstacles, weather, traffic rules, user preference, and recent actions; (2) map each input type to semantic categories; (3) instantiate template sentences; (4) assemble a narrative preserving temporal and spatial relations; (5) prompt the LLM to return a ranked sequence of κ longitudinal–lateral action pairs. SanDRA’s prompt contains separate system, ego-vehicle, and obstacle blocks, with automatic fields in braces and manual inputs in brackets (Section III-A/B, PDF pp. iii–iv).

Inference: a Verus implementation should use an enum or validated parser for action pairs and reject any token outside the finite action vocabulary before proof. The parser can have ensures that the returned value belongs to the allowed set; the LLM text itself remains untrusted. Template generation should be pure executable Rust with contracts for units and ranges.

Evidence: the paper uses GPT-4o as the cloud LLM and Qwen3 as the local LLM, highD highway trajectories for finetuning, and MONA urban trajectories for evaluation (Section IV-A, PDF pp. vi–vii). The case study uses κ = 3 (Section IV-B, PDF p. vii); horizon ablations use h = 10, 25, 50 (Section IV-C1, PDF p. viii). The stated fail-safe triggers include late responses, hallucinations, and the absence of a feasible verified action (Section III-A, PDF p. iv).

technique 2: translate actions and rules to LTLf

Inference: use this when actions constrain behavior over a finite horizon. Steps: (1) concretize each action description, including numeric thresholds; (2) define predicates over vehicle states and express the action in LTLf; (3) conjoin the longitudinal and lateral formulas for each pair; (4) conjoin each pair with formalized traffic rules; (5) combine reachability analysis with model checking for that conjunction. The paper gives the running example φ_acc foll = G(a > a_lim) ∧ G in_lane(x, L_cur) for ACCELERATE plus FOLLOW-LANE (Eq. 4, PDF p. v). It formalizes lane changes with FG so that the vehicle eventually remains in the target adjacent lane (Section III-C, PDF p. v).

Inference: in Verus, represent the finite trace as a ghost sequence and define a spec fn for each predicate and temporal obligation. Prove transition functions preserve the obligation with requires and ensures; use assert and proof functions for arithmetic and sequence lemmas. Verus does not directly execute LTLf model checking, so the translation and checker would be a separate trusted component unless encoded and proved in Verus.

technique 3: specification-compliant reachability filtering

Inference: use this to reject actions whose specification-compliant reachable set becomes empty. Steps: (1) define ego dynamics x_{k+1}=f(x_k,u_k) and admissible state/input sets; (2) compute forbidden states from obstacle occupancies, X_k^F={x_k | occ(x_k)∩O_k ≠ ∅}; (3) compute or overapproximate the set of states reachable from the initial set while avoiding forbidden states and satisfying the LTLf formula; (4) require ∀k∈{0,…,h}: R_k(φ) ≠ ∅; (5) execute the first verified action or pass its reachable sets to a trajectory planner. The paper explicitly says it uses a tight overapproximation because exact reachable sets are generally infeasible (Section II-B, PDF p. iii).

The paper’s algorithm description in Fig. 3 (PDF p. iii) is: “After converting the actions and traffic rules to LTLf formulas, we take their conjunction and apply reachability analysis to verify the safety of the resulting behavior.” Inference: a Verus model can prove that a discrete transition stays outside a forbidden region, but continuous overapproximation, collision geometry, and solver soundness need separately trusted libraries and contracts. Inference: emptiness of an overapproximation excludes a compliant trajectory, but non-emptiness alone does not establish that a feasible trajectory exists; additional reasoning about realizability is needed. The study should therefore attribute the non-emptiness criterion to the paper rather than treat it as a general theorem about overapproximations.

Evidence: the implementation uses CommonRoad-Reach, Spot for LTLf model checking, a point-mass vehicle model, bounded accelerations, most-likely and set-based obstacle predictions, and highway-env closed-loop simulation (Section IV-A, PDF p. vi). In the case study, the first two ranked actions produced empty reachable sets because of collision, while DECELERATE/FOLLOW-LANE retained non-empty sets under both most-likely and set-based predictions. Adding the formal traffic rules made its reachable sets empty: the safe-distance requirement could not be met without violating the unnecessary-braking rule. The fail-safe solution brought the vehicle to a standstill (Section IV-B, PDF p. vii).

technique 4: combine most-likely and set-based predictions

Inference: use set-based predictions when safety must cover a range of surrounding-agent behaviors. The paper uses most-likely trajectories to prune traffic-rule-violating solution spaces and set-based predictions to define forbidden states (Section III-E, PDF pp. v–vi). Steps: (1) generate both prediction types; (2) use the set-based occupancy in collision forbidden states; (3) use likely trajectories for additional rule constraints; (4) compute reachable sets; (5) fall back if all candidates become empty. Inference: this is analogous to proving a Verus function for all values in an input set, with the set model and its bounds supplied as assumptions.

For infinite-horizon safety, the paper computes fail-safe solutions in parallel, transferring the vehicle to an invariably safe state. The authors state: “This guarantees collision-free operation for all behaviors of other traffic participants that are consistent with the assumed traffic rules and modeling assumptions [33, Sec. X].” They refer to the inductive proof in [64, Sec. III], rather than presenting that proof here (Section III-E, PDF p. vi).

evidence, limits, and VL impact

SanDRA reports open-loop and closed-loop evaluations, safe@κ, top-κ accuracy, and ablations over horizons and user commands. The evaluation uses recorded trajectories and simulation, not physical deployment. In the open-loop ablations on 800 MONA scenarios, formalized traffic rules were excluded from reachability analysis because many human drivers violated them; the recorded trajectories were therefore unsuitable as an upper-limit performance indicator (Section IV-C, PDF p. viii). In the closed-loop evaluation, set-based variants achieved 100.0% success in all three settings, with and without rules in verification. Most-likely predictions with rules achieved 100.0%, 96.7%, and 100.0%; the authors report that fallback actions could fail after the scenario had already lost all feasible safe actions (Table V and Section IV-D2, PDF p. x). Inference: the threat to agent-written verified Rust is high if the LLM’s action parser or dynamics model is trusted without proof, but the architecture is useful: isolate generation, translate to a formal predicate, filter with a sound checker, and provide a verified fail-safe.

Inference: the paper does not establish that its physical model, obstacle predictions, or CommonRoad implementation are correct for every real-world situation. Its infinite-horizon argument relies on fail-safe planning and referenced verification results under stated assumptions. VL could reuse the action-to-specification-to-reachability pipeline and fail-safe design, while making model validity and checker correctness explicit assumptions or separate proof obligations.

techniques for the catalog

• structured action prompting: turn state and context into a fixed template and ranked finite action vocabulary
• ltl-f translation: map each action and rule to finite-trace temporal formulas and conjoin them
• reachable-set filtering: reject candidates whose specification-compliant reachable set becomes empty
• dual prediction safety: combine set-based forbidden states with likely trajectories and a fail-safe controller Checked 2026-10-19 against the full paper by a Codex agent (mid-paper quote: “By sampling only within the obtained reachable sets, the trajectory was found faster than sampling the entire solution space.”): read the full paper and study; checked quotations, numbers, references, technique steps, and safety assumptions; corrected the abstract quotation, page and section references, prediction details, and finite/infinite-horizon interpretation; marked transfer recommendations and conclusions as Inference; linked the supplied arXiv version; did not reproduce experiments, inspect implementation code, or independently verify cited proofs.

Last edited: 2026-10-19