Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

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

T0 review · 3 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read SanDRA proposes to verify LLM-generated driving actions by translating them into temporal-logic formulas and checking that a specification-compliant reachable set stays non-empty over the decision horizon, executing only verified actions an

desk verdict A genuinely useful integration of LLM action selection with reachability-based safety verification, weakened by a closed-loop evaluation that never shows the executed trajectories live inside the verified reachable sets. read the letter →

arxiv 2510.06717 v2 pith:F6X3HZ3L submitted 2025-10-08 cs.RO

Yuanfei Lin , Sebastian Illing , Matthias Althoff This is my paper
classification cs.RO
keywords LLMdecision-makingreachabilityanalysistemporallogicautonomousdrivingsafetyverificationtrafficruleformalizationset-basedpredictionfail-safeplanning
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Large language models can reason about traffic context, but they hallucinate, ignore vehicle dynamics, and know traffic laws only implicitly. SanDRA's bet is that you don't have to trust the model's answer — you only need its proposals. The paper claims to close the safety gap by converting each ranked action pair the LLM suggests into a temporal-logic formula, conjoining it with formalized traffic rules, and proving with reachability analysis that a compliant trajectory exists over the whole decision horizon. If such a certificate exists, the action is executed; if not, the vehicle falls back to a fail-safe plan. A sympathetic reader should care because this is a concrete route to making knowledge-driven, LLM-based driving decisions formally safe rather than merely plausible.

What carries the argument

The central object is the specification-compliant reachable set R_k(φ): an overapproximation of all ego states reachable at step k while avoiding forbidden states (the set-based predicted occupancies of other traffic participants) and satisfying the LTLf formula φ. LTLf is linear temporal logic over finite traces, used here to express both driving actions (e.g., STOP becomes "eventually always in standstill") and traffic rules (e.g., the safe-distance rule) as finite-horizon specifications. The framework combines reachability analysis with model checking to compute these sets; non-emptiness of R_k(φ) for every step in the horizon is the safety certificate. The same reachable sets are handed

What would settle it

Run a closed-loop scenario in which a surrounding vehicle performs a maneuver outside its set-based prediction envelope (an emergency brake harder than the assumed a_obs,min, or a sudden cut-in) while the check R_k(φ)≠∅ has passed; if the ego follows the verified action into a collision or rule violation, the certificate's predictive assumption is falsified. More directly, record real trajectories and check whether every observed occupancy lies inside the predicted O_k at every timestep; any frame outside the envelope breaks the premise of the proof.

Watch

Extended reading notes

Core claim

SanDRA is presented as the first framework that combines LLM-based driving decisions with reachability-based formal verification. At each decision cycle, a prompt describing the scenario makes the LLM return ranked longitudinal–lateral action pairs; each pair is translated into an LTLf formula, conjoined with formalized traffic rules, and checked by reachability analysis combined with model checking. The check computes an overapproximated specification-compliant reachable set R_k(φ) for every step k of the horizon: if R_k(φ) is non-empty for all k, the action is verified safe and executed (its reachable sets also constrain the trajectory planner); otherwise the vehicle takes a fail-safe plan

Load-bearing premise

The safety certificate is conditional: it holds only if the set-based prediction O_k truly encloses every possible future occupancy of every traffic participant and the ego dynamics model f is exact, since a participant leaving that envelope — or an inaccurate dynamics model — can falsify the non-empty reachable set; the paper concedes this dependence in Sec. II-C and falls back to an external safety concept otherwise.

Editorial extensions

If this is right

  • LLM outputs become proposals, not commands: a ranked action pair is executed only if its LTLf formula, conjuncted with formalized traffic rules, yields non-empty specification-compliant reachable sets over the entire decision horizon.
  • Using set-based prediction of other traffic, rather than only most-likely trajectories, is what closes the safety gap; in the paper's closed-loop tests, the set-based variants achieve 100% success across the three tested density settings, while most-likely-only variants can still collide.
  • Conjoining formalized traffic rules with the action formulas measurably improves rule compliance, especially the safe-distance rule, and yields trajectory robustness values that stay positive on average.
  • The reachable sets computed during verification can be handed directly to a trajectory planner, so the verified action and the executable trajectory share the same safety certificate.
  • If no action verifies, or the LLM fails to respond, the fail-safe planner takes the vehicle to an invariably safe state, making the finite-horizon check part of an infinite-horizon safety argument.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the verification gate treats the LLM as an action proposer, so the same action-to-LTLf-to-reachability pipeline could be attached to any generative planner — a diffusion policy, a reinforcement-learning controller, or a rule-based proposer — not just to language models.
  • Editorial inference: because the certificate is only as strong as the occupancy prediction, a runtime monitor that checks whether each traffic participant stays inside its predicted envelope O_k, switching to fail-safe the moment one leaves it, would turn the conditional guarantee into an enforced one.
  • Editorial inference: the paper's own ablation shows that adding traffic rules to the prompt alone barely changes LLM accuracy; the safety gain comes from formalizing rules into the verification step, suggesting that progress on safe LLM driving should focus on the verification layer rather than on better prompting.
  • Editorial inference: the formalized rules used here simplify some real-world cases — the safe-distance formalization omits the prior-cut-in case — so legal-safety claims inherit that simplification until the full formalization is plugged in; a natural testable extension is multimodal input (cameras or lidar tokenized as vision tokens), which the paper names as future work.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes SanDRA, a decision-making framework in which an LLM proposes ranked longitudinal/lateral action pairs; these are automatically translated into LTLf formulas, conjoined with formalized traffic rules, and checked by computing specification-compliant reachable sets. An action is considered verified if the reachable set is non-empty for every step of the horizon; otherwise the next action is tried or a fail-safe plan is triggered. The evaluation includes open-loop ablation on highD/MONA and closed-loop highway-env comparisons against DiLu, and the code is released.

Significance. The paper addresses a timely problem and has several strengths: the action-to-LTLf mapping is a useful contribution; the verification is independent of the LLM's output (no fitted constants enter the safety check); the open-loop ablations with off-the-shelf and finetuned models are extensive; and the code/benchmarks are public. If the formal guarantee were established, this would be a valuable integration of LLM-based decision making with formal methods. However, the central verification condition as stated is not sound because it checks non-emptiness of an overapproximation, and the closed-loop experiments do not connect executed trajectories to the verified reachable corridor. These issues must be resolved before the 'provably safe' claim is justified.

major comments (3)
  1. [Sec. II-B, Eq. (3), and Sec. II-C] The verification condition ∀k R_k(φ)≠∅ is insufficient to certify an action. Eq. (3) defines the exact specification-compliant reachable set R^e_k, and the text then states that R_k(φ)⊇R^e_k is a tight overapproximation. Non-emptiness of a superset does not imply non-emptiness of the exact set: R_k can contain spurious states even when no real safe trajectory exists. Thus the algorithm as written may accept an action for which no collision-free, spec-compliant trajectory exists. To prove existence, one needs an underapproximation of R^e_k, or a concrete trajectory whose tube is verified against the forbidden states; using an overapproximation as an emptiness certificate provides only a necessary condition.
  2. [Sec. IV-D, Tabs. III-IV] The closed-loop evaluation does not demonstrate that the executed trajectories are the ones verified. The verified action pairs are mapped to highway-env meta-actions, and the simulator's default controller executes them; the paper does not show that the resulting states lie inside the R_k(φ) computed for Eq. (1), nor that the executed inputs belong to the U_k used in the reachability computation. The fail-safe behavior ('stronger SLOWER') is likewise not verified to reach an invariably safe state. Consequently, the 100% success rates in Tab. IV show only that this particular LLM+controller combination did not collide; they do not show that the reachability certificate was the cause of safety. Please add a coupling: either execute a trajectory synthesized inside an inner approximation of R_k and report tracking error, or verify the actual controller online.
  3. [Sec. III-E and Sec. IV-D] The infinite-horizon fail-safe guarantee described in Sec. III-E relies on reaching an invariably safe state, but the closed-loop implementation replaces this with an ad hoc 'stronger SLOWER' meta-action whose braking parameters are stated in a footnote. No evidence is provided that this adapted behavior satisfies the requisite safe-state condition or even remains within the verified reachable corridor. The paper should either implement the fail-safe concept from [30, Sec. X] in the simulation or explicitly state that the closed-loop results are not backed by the formal fail-safe guarantee.
minor comments (4)
  1. [Fig. 7 and Sec. IV-C] The model name is inconsistent: Fig. 7(c) refers to 'Qwen3-0.6B' while the text in Sec. IV-C uses 'Qwen3-0.8B'. Please unify.
  2. [Sec. II-A] The notation 'X_k ∈ R^{n_x}' and 'U_k ∈ R^{n_u}' should be sets, not elements; e.g., X_k ⊆ R^{n_x} and U_k ⊆ R^{n_u}.
  3. [Sec. III-B3] The prompt includes 'concretized traffic rules' in natural language, while the verification uses separately formalized LTLf versions. The paper should clarify whether the prompt wording and the formalized rule are guaranteed to be semantically identical; otherwise the LLM may be influenced by a different rule statement than the one verified.
  4. [Fig. 6e and Sec. IV-B] The caption says 'fail-safe trajectory when no verified action is available', but the case study shows that no *legally safe* action is available; the fail-safe trajectory may itself violate R_G2. Suggest clarifying that fail-safe guarantees collision safety but not rule compliance.

Circularity Check

0 steps flagged · score 1.0 of 10

No material circularity: the reachability gate is a genuine existential certificate, and the self-cited tooling is independent support rather than a definitional loop.

full rationale

The central derivation is not circular. In Eq. (3), R^e_k(phi) is defined as ego states reachable from X0 with inputs avoiding forbidden states X^F_tau and satisfying the action/traffic-rule formula phi; checking R_k(phi) != empty therefore establishes existence of a collision-avoiding, rule-compliant behavior consistent with the LLM's candidate action. The LLM output enters only through the formula phi, and the safety predicate comes from X^F_k and the formalized rules, so the prediction is not equal to its input by construction. The action-to-LTLf translations in Tab. II (e.g., KEEP -> G(|a| <= a_lim), STOP -> FG(in_standstill(x))) are threshold definitions, not fits to the outcomes being predicted. The finetuning/labeling step explicitly withholds the ego's final state from the LLM ('the final state recorded in the dataset is withheld from the LLM'), and the ablation safety metric uses recorded trajectories of other obstacles, so Safe@k is not a self-scored label. The heavy use of prior work by the same authors ([30], [34], [35], [41], [42], [58]) supplies rule formalization, overapproximative reachability, and set-based prediction; these are previously published, code-available components and are not invoked as a uniqueness theorem that forbids alternatives, so the self-citations are supporting rather than circular. The paper also explicitly conditions the guarantee on prediction accuracy and on a fail-safe concept from [30, Sec. X]; that is a stated soundness assumption, not a hidden definitional loop. The main weakness is a validation gap, not circularity: in the closed-loop evaluation the verified reachable set is not shown to contain the trajectory actually executed by the highway-env meta-action controller, and the adapted SLOWER fail-safe behavior is not itself verified. This affects whether the empirical 100% success rates demonstrate the formal gate, but it is not a reduction of the derivation to its inputs.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The central derivation is an integration of established formal-method tools. The only new mathematical content is the action-to-LTLf mapping; the listed parameters and domain assumptions are what the safety claim imports.

free parameters (4)
  • alim = 0.2 m/s^2
    Hand-chosen acceleration threshold separating KEEP, ACCELERATE, and DECELERATE in Tab. II; changes which trajectories satisfy the action formula.
  • v_err = 0.1 m/s
    Tolerance defining in_standstill(x) for the STOP action; hand-chosen and affects verification semantics.
  • safe-distance parameters = t_d = 0.4 s; a_min = -6 m/s^2; a_obs,min = -12 m/s^2
    Parameters of the safe-distance rule R_G1 in Eq. (4), imported from the previous formalization and set by hand rather than fitted.
  • kappa = 3
    Number of ranked action candidates requested from the LLM; directly affects Safe@kappa and runtime, chosen as a trade-off (Sec. IV-C).
assumptions (5)
  • domain assumption Ego dynamics f in Eq. (1) with input bounds U_k accurately model the vehicle, and obstacle occupancy O_k encloses all possible future positions of other traffic participants.
    The non-emptiness certificate R_k(phi) is only as strong as the model and predictive envelope; the paper acknowledges this in Sec. II-C.
  • domain assumption The LTLf action semantics in Tab. II accurately capture the natural-language action labels (e.g., ACCELERATE is equivalent to G(a > a_lim)).
    This mapping is the bridge from LLM output to verification; if the LLM or a human means something different by the same word, the verification checks the wrong property.
  • domain assumption The formalized traffic rules from [30], [34], [35] faithfully encode German traffic law, and the LTLf rewrites preserve their meaning.
    The 'legally compliant' part of the claim inherits the correctness of these prior formalizations.
  • standard math The reachability-analysis overapproximation from CommonRoad-Reach [61]/[42] is tight enough that non-emptiness of R_k(phi) indicates existence of a safe specification-compliant trajectory.
    The paper imports soundness of the reachability algorithm from prior work rather than proving it (Sec. II-B, III-E).
  • standard math LTLf finite-trace semantics and the model-checking performed by Spot [56] are sound.
    Standard formal-methods background relied upon by the verification pipeline.

how reviews work

0 comments
Cite this review

Pith. "Pith review of SanDRA: Safe Large-Language-Model-Based Decision Making for Automated Vehicles Using Reachability Analysis." pith.science (2026). https://pith.science/paper/F6X3HZ3L

@misc{pith2026251006717,
  author       = {Pith},
  title        = {Pith review of: SanDRA: Safe Large-Language-Model-Based Decision Making for Automated Vehicles Using Reachability Analysis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/F6X3HZ3L}},
  note         = {Machine review of arXiv:2510.06717}
}
read the original abstract

Large language models (LLMs) have been widely applied to knowledge-driven decision-making for automated vehicles due to their strong generalization and reasoning capabilities. However, the safety of the resulting decisions cannot be ensured due to possible hallucinations and the lack of integrated vehicle dynamics. To address this issue, we propose SanDRA, the first safe large-language-model-based decision making framework for automated vehicles using reachability analysis. Our approach starts with a comprehensive description of the driving scenario to prompt LLMs to generate and rank feasible driving actions. These actions are translated into temporal logic formulas that incorporate formalized traffic rules, and are subsequently integrated into reachability analysis to eliminate unsafe actions. We validate our approach in both open-loop and closed-loop driving environments using off-the-shelf and finetuned LLMs, showing that it can provide provably safe and, where possible, legally compliant driving actions, even under high-density traffic conditions. To ensure transparency and facilitate future research, all code and experimental setups are publicly available at github.com/CommonRoad/SanDRA.

Figures

Figures reproduced from arXiv: 2510.06717 by the authors.

Figure 1
Figure 1. An example usage of SANDRA, where the LLM is prompted to generate a ranked list of longitudinal and lateral action pairs ordered from best to worst. The action pair corresponding to stopping while staying on the current lane is verified as safe using reachability analysis and then executed. mated vehicles. a) LLMs as Decision Makers: LLMs are trained on vast and diverse internet-scale data, enabling them to understa… view at source ↗
Figure 2
Figure 2. Exemplary road network with lanes defined by lanelets. The ego vehicle [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. SANDRA overview diagram. Our tool SANDRA takes planning and environmental information as inputs and processes them to generate a structured description of the current scenario. The description is then used to prompt the LLM to produce a ranked sequence of longitudinal and lateral action pairs, ordered from best to worst. After converting the actions and traffic rules into LTLf formulas, we take their conjunction and… view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: LLM prompt design. Automatically generated content in the prompt [PITH_FULL_IMAGE:figures/full_fig_p004_4.png]
Figure 5
Figure 5. Figure 5: Prediction of other traffic participants and reachable set of the ego [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: CommonRoad scenarios4 in which the ego vehicle approaches a signalized intersection. (6b) and (6c) use the most likely predictions of other obstacles, while (6d) employs set-based predictions. When formalized traffic rules are incorporated in (6e), no safe action is fo…
Figure 7
Figure 7. Figure 7: Ablation studies on the effectiveness of the main components of [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]
Figure 8
Figure 8. Figure 8: Action distribution of the ego vehicle in the highway-env simulation, [PITH_FULL_IMAGE:figures/full_fig_p010_8.png]
Figure 9
Figure 9. Figure 9: Illustrative comparison in highway-env10 under setting ⃝2 , in which the past occupancies of vehicles are shown for the previous five time steps. a high degree of violations from the very beginning, ultimately leading to a collision. In contrast, safety verification us…

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Language-Driven Cost Optimization for Autonomous Driving

    cs.RO 2026-06 unverdicted novelty 4.0 of 10

    LLM interprets user language to set parameters of a risk-aware MPPI controller, with human-in-the-loop validation for adaptive autonomous driving behavior.

Reference graph

Works this paper leans on

69 extracted references · 8 linked inside Pith · cited by 1 Pith paper

  1. [1]

    A survey of motion planning and control techniques for self-driving urban vehicles,

    B. Paden, M. ˇC´ap, S. Z. Yong, D. Yershov, and E. Frazzoli, “A survey of motion planning and control techniques for self-driving urban vehicles,” vol. 1, no. 1, pp. 33–55, 2016

    2016

  2. [2]

    Safe reinforcement learning for autonomous lane changing using set-based prediction,

    H. Krasowski, X. Wang, and M. Althoff, “Safe reinforcement learning for autonomous lane changing using set-based prediction,” inProc. of the IEEE Int. Conf. on Intell. Transp. Syst., 2020, pp. 1–7

    2020

  3. [3]

    A survey on multimodal large language models for autonomous driving,

    C. Cui, Y . Ma, X. Cao, W. Ye, Y . Zhou, K. Liang, J. Chen, J. Lu, Z. Yang, K.-D. Liao,et al., “A survey on multimodal large language models for autonomous driving,” inProc. of the IEEE/CVF Winter Conf. on Applications of Computer Vision, 2024, pp. 958–979

    2024

  4. [4]

    A survey on large language model based autonomous agents,

    L. Wang, C. Ma, X. Feng, Z. Zhang, H. Yang, J. Zhang, Z. Chen, J. Tang, X. Chen, Y . Lin,et al., “A survey on large language model based autonomous agents,”Frontiers of Computer Science, vol. 18, no. 6, p. 186345, 2024

    2024

  5. [5]

    SurrealDriver: Designing LLM-powered generative driver agent framework based on human drivers’ driving-thinking data,

    Y . Jin, R. Yang, Z. Yi, X. Shen, H. Peng, X. Liu, J. Qin, J. Li, J. Xie, P. Gao,et al., “SurrealDriver: Designing LLM-powered generative driver agent framework based on human drivers’ driving-thinking data,” in Proc. of the IEEE/RSJ Int. Conf. on Intell. Robots and Syst., 2024, pp. 966–971

    2024

  6. [6]

    Driving with regulation: Interpretable decision-making for autonomous vehicles with retrieval-augmented reasoning via LLM,

    T. Cai, Y . Liu, Z. Zhou, H. Ma, S. Z. Zhao, Z. Wu, and J. Ma, “Driving with regulation: Interpretable decision-making for autonomous vehicles with retrieval-augmented reasoning via LLM,”arXiv preprint arXiv:2410.04759, 2024

    arXiv 2024

  7. [7]

    DiLu: A knowledge-driven approach to autonomous driving with large language models,

    L. Wen, D. Fu, X. Li, X. Cai, T. Ma, P. Cai, M. Dou, B. Shi, L. He, and Y . Qiao, “DiLu: A knowledge-driven approach to autonomous driving with large language models,” inProc. of the Int. Conf. on Learning Representations, 2024

    2024

  8. [8]

    Reflexion: Language agents with verbal reinforcement learning,

    N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao, “Reflexion: Language agents with verbal reinforcement learning,”Proc. of the Advances in Neural Information Processing Syst., vol. 36, pp. 8634–8652, 2023

    2023

Show all 69 references
  1. [9]

    KoMa: Knowledge-driven multi-agent framework for autonomous driving with large language models,

    K. Jiang, X. Cai, Z. Cui, A. Li, Y . Ren, H. Yu, H. Yang, D. Fu, L. Wen, and P. Cai, “KoMa: Knowledge-driven multi-agent framework for autonomous driving with large language models,”IEEE Trans. on Intell. Veh., pp. 1–15, 2024, early Access

    2024

  2. [10]

    SafeDrive: Knowledge-and data-driven risk-sensitive decision-making for autonomous vehicles with large language models,

    Z. Zhou, H. Huang, B. Li, S. Zhao, Y . Mu, and J. Wang, “SafeDrive: Knowledge-and data-driven risk-sensitive decision-making for autonomous vehicles with large language models,”arXiv preprint arXiv:2412.13238, 2024

    2024 arXiv

  3. [11]

    Large language model guided deep reinforcement learning for decision making in autonomous driving,

    H. Pang, Z. Wang, and G. Li, “Large language model guided deep reinforcement learning for decision making in autonomous driving,” arXiv preprint arXiv:2412.18511, 2024

    2024 arXiv

  4. [12]

    PADriver: Towards personalized autonomous driving,

    G. Kou, F. Jia, W. Mao, Y . Liu, Y . Zhao, Z. Zhang, O. Yoshie, T. Wang, Y . Li, and X. Zhang, “PADriver: Towards personalized autonomous driving,”arXiv preprint arXiv:2505.05240, 2025

    2025 arXiv

  5. [13]

    DriveMLM: Aligning multi-modal large language models with behavioral planning states for autonomous driving,

    W. Wang, J. Xie, C. Hu, H. Zou, J. Fan, W. Tong, Y . Wen, S. Wu, H. Deng, Z. Li,et al., “DriveMLM: Aligning multi-modal large language models with behavioral planning states for autonomous driving,”arXiv preprint arXiv:2312.09245, 2023

    2023

  6. [14]

    GPT-driver: Learning to drive with GPT,

    J. Mao, Y . Qian, H. Zhao, and Y . Wang, “GPT-driver: Learning to drive with GPT,”arXiv preprint arXiv:2310.01415, 2023

    2023 arXiv

  7. [15]

    DriveLM: Driving with graph visual question answering,

    C. Sima, K. Renz, K. Chitta, L. Chen, H. Zhang, C. Xie, P. Luo, A. Geiger, and H. Li, “DriveLM: Driving with graph visual question answering,” inProc. of the European Conf. on Computer Vision, 2024, pp. 256–274

    2024

  8. [16]

    LMDrive: Closed-loop end-to-end driving with large language models,

    H. Shao, Y . Hu, L. Wang, S. L. Waslander, Y . Liu, and H. Li, “LMDrive: Closed-loop end-to-end driving with large language models,” inProc. of the IEEE/CVF Conf. on Computer Vision and Pattern Recognition, 2024, pp. 15 120–15 130

    2024

  9. [17]

    DrPlanner: Diagnosis and repair of motion planners for automated vehicles using large language models,

    Y . Lin, C. Li, M. Ding, M. Tomizuka, W. Zhan, and M. Althoff, “DrPlanner: Diagnosis and repair of motion planners for automated vehicles using large language models,”IEEE Robot. and Automation Letters, vol. 9, no. 10, pp. 8218–8225, 2024

    2024

  10. [18]

    Enhancing autonomous driving systems with on-board deployed large language models,

    N. Baumann, C. Hu, P. Sivasothilingam, H. Qin, L. Xie, M. Magno, and L. Benini, “Enhancing autonomous driving systems with on-board deployed large language models,” inProc. of Robot.: Science and Syst., 2025

    2025

  11. [19]

    LanguageMPC: Large language models as deci- sion makers for autonomous driving,

    H. Sha, Y . Mu, Y . Jiang, L. Chen, C. Xu, P. Luo, S. E. Li, M. Tomizuka, W. Zhan, and M. Ding, “LanguageMPC: Large language models as deci- sion makers for autonomous driving,”arXiv preprint arXiv:2310.03026, 2025

    2025 arXiv

  12. [20]

    Personalized autonomous driving with large language models: Field experiments,

    C. Cui, Z. Yang, Y . Zhou, Y . Ma, J. Lu, L. Li, Y . Chen, J. Panchal, and Z. Wang, “Personalized autonomous driving with large language models: Field experiments,” inProc. of the IEEE Int. Conf. on Intell. Transp. Syst., 2024, pp. 20–27

    2024

  13. [21]

    Driving with LLMs: Fusing object- level vector modality for explainable autonomous driving,

    L. Chen, O. Sinavski, J. H ¨unermann, A. Karnsund, A. J. Willmott, D. Birch, D. Maund, and J. Shotton, “Driving with LLMs: Fusing object- level vector modality for explainable autonomous driving,” inProc. of the IEEE Int. Conf. on Robot. and Autom., 2024, pp. 14 093–14 100

    2024

  14. [22]

    DriveGPT4: Interpretable end-to-end autonomous driving via large language model,

    Z. Xu, Y . Zhang, E. Xie, Z. Zhao, Y . Guo, K.-Y . K. Wong, Z. Li, and H. Zhao, “DriveGPT4: Interpretable end-to-end autonomous driving via large language model,”IEEE Robot. and Automation Letters, vol. 9, no. 10, pp. 8186–8193, 2024

    2024

  15. [23]

    Drive as you speak: En- abling human-like interaction with large language models in autonomous vehicles,

    C. Cui, Y . Ma, X. Cao, W. Ye, and Z. Wang, “Drive as you speak: En- abling human-like interaction with large language models in autonomous vehicles,” inProc. of the IEEE/CVF Winter Conf. on Applications of Computer Vision, 2024, pp. 902–909

    2024

  16. [24]

    Traffic regulation-aware path planning with regulation databases and vision-language models,

    X. Han, Z. Wu, X. Xia, and J. Ma, “Traffic regulation-aware path planning with regulation databases and vision-language models,” in Proc. of the IEEE Int. Conf. on Robot. and Autom., 2025

    2025

  17. [25]

    EMMA: End-to-end multimodal model for autonomous driving,

    J.-J. Hwang, R. Xu, H. Lin, W.-C. Hung, J. Ji, K. Choi, D. Huang, T. He, P. Covington, B. Sapp,et al., “EMMA: End-to-end multimodal model for autonomous driving,”arXiv preprint arXiv:2410.23262, 2024

    2024 arXiv

  18. [26]

    Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges,

    N. Mehdipour, M. Althoff, R. D. Tebbens, and C. Belta, “Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges,”Automatica, vol. 152, no. 110692, 2023

    2023

  19. [27]

    Online verification of automated road vehicles using reachability analysis,

    M. Althoff and J. M. Dolan, “Online verification of automated road vehicles using reachability analysis,”IEEE Trans. on Robot., vol. 30, no. 4, pp. 903–918, 2014

    2014

  20. [28]

    Using online verification to prevent autonomous vehicles from causing accidents,

    C. Pek, S. Manzinger, M. Koschi, and M. Althoff, “Using online verification to prevent autonomous vehicles from causing accidents,” Nature Machine Intell., vol. 2, no. 9, pp. 518–528, 2020

    2020

  21. [29]

    Reachability-based decision-making for autonomous driving: Theory and experiments,

    H. Ahn, K. Berntorp, P. Inani, A. J. Ram, and S. Di Cairano, “Reachability-based decision-making for autonomous driving: Theory and experiments,”IEEE Trans. on Control Syst. Technology, vol. 29, no. 5, pp. 1907–1921, 2020

    1907

  22. [30]

    No more traffic tickets: A tutorial to ensure traffic-rule compliance of automated vehicles,

    M. Althoff, S. Maierhofer, G. W ¨ursching, Y . Lin, F. Lercher, and R. Stolz, “No more traffic tickets: A tutorial to ensure traffic-rule compliance of automated vehicles,”Proc. of the IEEE, pp. 1–30, 2025, early Access

    2025

  23. [31]

    Specifying safety of autonomous vehicles in signal temporal logic,

    N. Ar ´echiga, “Specifying safety of autonomous vehicles in signal temporal logic,” inProc. of the IEEE Intell. Veh. Symp., 2019, pp. 58–63

    2019

  24. [32]

    Encoding and monitoring responsi- bility sensitive safety rules for automated vehicles in signal temporal logic,

    M. Hekmatnejad, S. Yaghoubi, A. Dokhanchi, H. B. Amor, A. Shrivas- tava, L. Karam, and G. Fainekos, “Encoding and monitoring responsi- bility sensitive safety rules for automated vehicles in signal temporal logic,” inProc. of the ACM/IEEE Int. Conf. on Formal Methods and Model...

    2019

  25. [33]

    Formalizing traffic rules for machine interpretability,

    K. Esterle, L. Gressenbuch, and A. Knoll, “Formalizing traffic rules for machine interpretability,” inProc. of the IEEE Connected and Automated Veh. Symp., 2020, pp. 1–7

    2020

  26. [34]

    Formal- ization of interstate traffic rules in temporal logic,

    S. Maierhofer, A.-K. Rettinger, E. C. Mayer, and M. Althoff, “Formal- ization of interstate traffic rules in temporal logic,” inProc. of the IEEE Intell. Veh. Symp., 2020, pp. 752–759

    2020

  27. [35]

    Formalization of intersection traffic rules in temporal logic,

    S. Maierhofer, P. Moosbrugger, and M. Althoff, “Formalization of intersection traffic rules in temporal logic,” inProc. of the IEEE Intell. Veh. Symp., 2022, pp. 1135–1144

    2022

  28. [36]

    Interpretable safety validation for autonomous vehicles,

    A. Corso and M. J. Kochenderfer, “Interpretable safety validation for autonomous vehicles,” inProc. of the IEEE Int. Conf. on Intell. Transp. Syst., 2020, pp. 1–6

    2020

  29. [37]

    Autonomous vehicle decision-making and monitoring based on signal temporal logic and mixed-integer programming,

    Y . E. Sahin, R. Quirynen, and S. Di Cairano, “Autonomous vehicle decision-making and monitoring based on signal temporal logic and mixed-integer programming,” inProf. of the American Control Conf., 2020, pp. 454–459

    2020

  30. [38]

    Synthesizing traffic scenarios from formal specifications for testing automated vehicles,

    M. Klischat and M. Althoff, “Synthesizing traffic scenarios from formal specifications for testing automated vehicles,” inProf. of the IEEE Intell. Veh. Symp., 2020, pp. 2065–2072. JOURNAL OF XX, VOL. XX, NO. X, MONTH YEAR xii

    2020

  31. [39]

    Motion planning with temporal-logic spec- ifications: Progress and challenges,

    E. Plaku and S. Karaman, “Motion planning with temporal-logic spec- ifications: Progress and challenges,”AI communications, vol. 29, no. 1, pp. 151–162, 2016

    2016

  32. [40]

    Traffic-rule-compliant trajec- tory repair via satisfiability modulo theories and reachability analysis,

    Y . Lin, Z. Xing, X. Han, and M. Althoff, “Traffic-rule-compliant trajec- tory repair via satisfiability modulo theories and reachability analysis,” IEEE Trans. on Robot., pp. 1–18, 2025, early Access

    2025

  33. [41]

    Specification-compliant driving corridors for motion planning of automated vehicles,

    E. Irani Liu and M. Althoff, “Specification-compliant driving corridors for motion planning of automated vehicles,”IEEE Trans. on Intell. Veh., vol. 8, no. 9, pp. 4180–4197, 2023

    2023

  34. [42]

    Specification-compliant reachability analysis for autonomous vehicles using on-the-fly model checking,

    F. Lercher and M. Althoff, “Specification-compliant reachability analysis for autonomous vehicles using on-the-fly model checking,” inProc. of the IEEE Intell. Veh. Symp., 2024, pp. 1484–1491

    2024

  35. [43]

    A formal methods approach to interpretable reinforcement learning for robotic planning,

    X. Li, Z. Serlin, G. Yang, and C. Belta, “A formal methods approach to interpretable reinforcement learning for robotic planning,”Science Robot., vol. 4, no. 37, p. eaay6276, 2019

    2019

  36. [44]

    Provable traffic rule compliance in safe reinforcement learning on the open sea,

    H. Krasowski and M. Althoff, “Provable traffic rule compliance in safe reinforcement learning on the open sea,”IEEE Trans. on Intell. Veh., vol. 9, no. 12, pp. 7617–7634, 2024

    2024

  37. [45]

    Lanelets: Efficient map represen- tation for autonomous driving,

    P. Bender, J. Ziegler, and C. Stiller, “Lanelets: Efficient map represen- tation for autonomous driving,” inProc. of the IEEE Intell. Veh. Symp., 2014, pp. 420–425

    2014

  38. [46]

    Robust and efficient curvilinear coordi- nate transformation with guaranteed map coverage for motion planning,

    G. W ¨ursching and M. Althoff, “Robust and efficient curvilinear coordi- nate transformation with guaranteed map coverage for motion planning,” inProc. of the IEEE Intell. Veh. Symp., 2024, pp. 2694–2701

    2024

  39. [47]

    Linear temporal logic and linear dynamic logic on finite traces

    G. De Giacomo, M. Y . Vardi,et al., “Linear temporal logic and linear dynamic logic on finite traces.” inProc. of the Int. Joint Conf. on Artificial Intell., vol. 13, 2013, pp. 854–860

    2013

  40. [48]

    Baier and J.-P

    C. Baier and J.-P. Katoen,Principles of model checking. MIT press, 2008

    2008

  41. [49]

    The image computation problem in hybrid systems model checking,

    A. Platzer and E. M. Clarke, “The image computation problem in hybrid systems model checking,” inProc. of the Int. Workshop on Hybrid Systems: Computation and Control. Springer, 2007, pp. 473–486

    2007

  42. [50]

    Convention on road traffic,

    United Nations Economic Commission for Europe, “Convention on road traffic,” United Nations Conference on Road Traffic, 1968, (consolidated version of 2006). [Online]. Available: https://www.unece. org/fileadmin/DAM/trans/conventn/Conv road traffic EN.pdf

    1968

  43. [51]

    Learning transferable visual models from natural language supervision,

    A. Radford, J. W. Kim, C. Hallacy, A. Ramesh, G. Goh, S. Agarwal, G. Sastry, A. Askell, P. Mishkin, J. Clark,et al., “Learning transferable visual models from natural language supervision,” inProf. of the Int. Conf. on Machine Learning, 2021, pp. 8748–8763

    2021

  44. [52]

    Chain-of-thought prompting elicits reasoning in large language models,

    J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V . Le, D. Zhou,et al., “Chain-of-thought prompting elicits reasoning in large language models,”Proc. of the Advances in Neural Info. Processing Syst., vol. 35, pp. 24 824–24 837, 2022

    2022

  45. [53]

    Commonroad-RL: A con- figurable reinforcement learning environment for motion planning of autonomous vehicles,

    X. Wang, H. Krasowski, and M. Althoff, “Commonroad-RL: A con- figurable reinforcement learning environment for motion planning of autonomous vehicles,” inProc. of the IEEE Int. Conf. on Intell. Transp. Syst., 2021, pp. 466–472

    2021

  46. [54]

    CommonRoad-CriMe: A toolbox for criticality measures of autonomous vehicles,

    Y . Lin and M. Althoff, “CommonRoad-CriMe: A toolbox for criticality measures of autonomous vehicles,” inProc. of the IEEE Intell. Veh. Symp., 2023, pp. 1–8

    2023

  47. [55]

    LoRA: Low-rank adaptation of large language models,

    E. J. Hu, Y . Shen, P. Wallis, Z. Allen-Zhu, Y . Li, S. Wang, L. Wang, W. Chen,et al., “LoRA: Low-rank adaptation of large language models,” Proc. of the Int. Conf. on Learning Representations, vol. 1, no. 2, p. 3, 2022

    2022

  48. [56]

    Spot 2.0 – a framework for LTL andω-automata manipulation,

    A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu, “Spot 2.0 – a framework for LTL andω-automata manipulation,” inProc. of the Int. Symposium on Automated Technology for Verification and Analysis, 2016, pp. 122–129

    2016

  49. [57]

    A survey on motion prediction and risk assessment for intelligent vehicles,

    S. Lef `evre, D. Vasquez, and C. Laugier, “A survey on motion prediction and risk assessment for intelligent vehicles,”ROBOMECH J., vol. 1, no. 1, pp. 1–14, 2014

    2014

  50. [58]

    Set-based prediction of traffic participants considering occlusions and traffic rules,

    M. Koschi and M. Althoff, “Set-based prediction of traffic participants considering occlusions and traffic rules,”IEEE Trans. on Intell. Veh., vol. 6, no. 2, pp. 249–265, 2020

    2020

  51. [59]

    Efficient computation of invariably safe states for motion planning of self-driving vehicles,

    C. Pek and M. Althoff, “Efficient computation of invariably safe states for motion planning of self-driving vehicles,” inProc. of the IEEE/RSJ Int. Conf. on Intell. Robot. and Syst., 2018, pp. 3523–3530

    2018

  52. [60]

    CommonRoad: Composable benchmarks for motion planning on roads,

    M. Althoff, M. Koschi, and S. Manzinger, “CommonRoad: Composable benchmarks for motion planning on roads,” inProc. of the IEEE Intell. Veh. Symp., 2017, pp. 719–726

    2017

  53. [61]

    CommonRoad-Reach: A toolbox for reachability analysis of automated vehicles,

    E. Irani Liu, G. W ¨ursching, M. Klischat, and M. Althoff, “CommonRoad-Reach: A toolbox for reachability analysis of automated vehicles,” inProc. of the IEEE Int. Intell. Transp. Systems Conf., 2022, pp. 2313–2320

    2022

  54. [62]

    An environment for autonomous driving decision-making,

    E. Leurent, “An environment for autonomous driving decision-making,” https://github.com/eleurent/highway-env, 2018

    2018

  55. [63]

    GPT-4o system card,

    A. Hurst, A. Lerer, A. P. Goucher, A. Perelman, A. Ramesh, A. Clark, A. Ostrow, A. Welihinda, A. Hayes, A. Radford,et al., “GPT-4o system card,”arXiv preprint arXiv:2410.21276, 2024

    2024 arXiv

  56. [64]

    Qwen3 technical report,

    A. Yang, A. Li, B. Yang, B. Zhang, B. Hui, B. Zheng,et al., “Qwen3 technical report,”arXiv preprint arXiv:2505.09388, 2025

    2025 arXiv

  57. [65]

    The highD dataset: A drone dataset of naturalistic vehicle trajectories on German highways for validation of highly automated driving systems,

    R. Krajewski, J. Bock, L. Kloeker, and L. Eckstein, “The highD dataset: A drone dataset of naturalistic vehicle trajectories on German highways for validation of highly automated driving systems,” inProc. of the IEEE Int. Conf. on Intell. Transp. Syst., 2018, pp. 2118–2125

    2018

  58. [66]

    MONA: The Munich motion dataset of natural driving,

    L. Gressenbuch, K. Esterle, T. Kessler, and M. Althoff, “MONA: The Munich motion dataset of natural driving,” inProc. of the IEEE Int. Conf. on Intell. Transp. Syst., 2022, pp. 2093–2100

    2022

  59. [67]

    Rule-compliant trajectory repairing using satisfiability modulo theories,

    Y . Lin and M. Althoff, “Rule-compliant trajectory repairing using satisfiability modulo theories,” inProc. of the IEEE Intell. Veh. Symp., 2022, pp. 449–456

    2022

  60. [68]

    Sampling-based optimal trajectory generation for autonomous vehicles using reachable sets,

    G. W ¨ursching and M. Althoff, “Sampling-based optimal trajectory generation for autonomous vehicles using reachable sets,” inProc. of the IEEE Int. Intell. Transp. Syst. Conf., 2021, pp. 828–835

    2021

  61. [69]

    Model predictive robustness of signal temporal logic predicates,

    Y . Lin, H. Li, and M. Althoff, “Model predictive robustness of signal temporal logic predicates,”IEEE Robot. and Automation Letters, vol. 08, no. 12, pp. 8050–8057, 2023. Yuanfei Linreceived his B.Eng. degree in Auto- motive Engineering from Tongji University, China, in 2018,...

    2023

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.