Pith. sign in

REVIEW 3 major objections 7 minor 28 references

Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!

T0 review · 3 major / 7 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read Model checking can catch sensor-accuracy and step-size bugs before RL starts, and reward automata speed up multi-objective learning in autonomous driving.

desk verdict A genuinely useful workflow for using model checking in RL for AD, but the evidence is thin and the safety guarantee only holds for the discretized model, not the continuous dynamics. read the letter →

arxiv 2411.14375 v1 pith:IYJ75P3A submitted 2024-11-21 cs.LG cs.LO

Rong Gu (Mälardalen University) This is my paper · ORCID
classification cs.LGcs.LO
keywords modelcheckingreinforcementlearningautonomousdrivingrewardautomatasafetyshieldsensoraccuracymulti-objectiveUPPAAL
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

This paper argues that model checking can do much more for reinforcement learning in autonomous driving than the usual safety-shield job. It proposes new formal model templates that represent the vehicle's continuous dynamics with hybrid clocks and integer-scaled numbers, so that the UPPAAL model checker can symbolically analyze the system. Before training, the author runs model-checking queries to test whether sensor accuracy and the sensing/decision-making periods are adequate and whether a safe path to the goal exists at all. During training, reward automata, which accumulate separate rewards for safety, progress, and comfort, make multi-objective reward design explicit and verifiable, and the experiments show they greatly reduce reinforcement learning time. If the claims hold, model checking becomes a pre-training validation and reward-design tool for RL, not just a safety filter.

What carries the argument

The load-bearing device is a set of UPPAAL model templates (Timer, Controller, Action, Dynamics) that let continuous vehicle dynamics and discrete control coexist in a symbolically checkable model. Continuous variables such as x, y, v, acc, and head are hybrid clocks, whose derivatives are given by ordinary differential equations but whose values are abstracted from symbolic state-space exploration; all floating-point numbers are instead represented as integer significands with a fixed base and exponent, so the model stays finite while supporting a tunable granularity of "continuous" actions and numerical integration. Reward automata are the other central object: automata whose rates on hybrid clocks accumulate rewards for safety, progress, and comfort, and whose transitions encode priority (safety above progress above comfort), letting designers verify the reward structure with queries such as "unsafe reward cannot be compensated by other rewards" before learning.

What would settle it

Run the same scenario and the same learned strategy under a high-precision continuous ODE simulator (or a real test vehicle) with sensor noise within the assumed bounds; if the AD-obstacle distance ever falls below the unsafe threshold 3·TD while the UPPAAL model predicted it would stay above, the numerical-integration/integer-significand abstraction is too coarse and the pre-analysis guarantee is unsound.

Watch

Extended reading notes

Core claim

The paper's central claim is that model checking, applied through the CommonUppRoad toolchain, can strengthen reinforcement learning for autonomous driving in two ways beyond safety shields: an MC-based pre-analysis of the model can expose bugs in sensor accuracy and in the choice of sensing/decision-making periods and can certify whether a safe, goal-reaching motion plan exists before any learning is run; and reward automata give RL designers a verifiable, multi-objective structure for reward functions, which greatly improves learning performance. The pre-analysis queries Qa through Qd are presented as a recommended workflow: check the probability of sensor error, check existence of a safe path, check existence of a safe and reachable path, then synthesize a safety shield for RL. The experiments on an intersection left-turn scenario show that with inadequate precision (exponent one instead of four) or long sensing periods, the supposedly shielded vehicle still crosses the unsafe-distance threshold, while the correct settings pass the pre-analysis and the reward-automaton-guided learner reaches the goal in far fewer episodes.

Load-bearing premise

The discretized model, with hybrid clocks, integer-scaled floating-point representations, and the numerical integration in sense(), matches the real continuous vehicle dynamics closely enough that a safety shield or pre-analysis verdict computed on it remains valid on the physical vehicle.

Editorial extensions

If this is right

  • The Qa pre-analysis gives a quantitative bound on the sensor precision and sensing period a given RL task can tolerate, so RL engineers can choose these parameters before spending compute.
  • If Qb or Qc returns false, the model state space contains no safe or no goal-reaching plan, so running RL is pointless; the designer should change actions, periods, or scenario instead.
  • Reward automata make reward design a verification problem: queries can check that unsafe behavior is always punished more than all other rewards combined, and counterexamples guide fixes.
  • Safety shields synthesized before learning keep both the learning process and the learned strategy safe, so the RL result carries a correctness guarantee that pure RL lacks.
  • The same model supports finer action discretization and multiple sensing/decision periods, so the approach approximates continuous control while preserving symbolic analysis.

Reading between the lines

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

  • The same pre-analysis pattern should transfer to other cyber-physical RL settings with periodic sensing, such as robotics or drone navigation, where sensor period and precision can be checked before training.
  • Reward automata could be used as a formal specification artifact: model-checking properties of the automaton gives an audit trail for why a reward function has a particular shape, which may help with explainability and certification.
  • One testable extension is to automate reward-weight tuning by expressing the reward automaton constraints, such as safety punishment dominating progress reward, as parameter constraints and searching over weights with the model checker instead of manual trial and error.
  • The falsifier suggests a concrete benchmark: compare Algorithm 1's numerical integration against a high-precision ODE simulation of the same scenario to measure the largest error the integer-significand abstraction introduces, and check whether it stays below the safety margin.
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 / 7 minor

Summary. The paper proposes new UPPAAL model templates for autonomous-driving (AD) scenarios that combine symbolic and statistical model checking with reinforcement learning (RL). The templates represent continuous vehicle dynamics as hybrid clocks updated by Euler integration at discrete sensing instants, and represent floating-point values via integer significands. On this basis, the paper claims two contributions: (i) a model pre-analysis step that checks sensor accuracy and the existence of safe/reachable plans before RL is run, and (ii) reward automata that help design and verify multi-objective reward functions, allegedly leading to much faster learning. The claims are demonstrated on one intersection scenario using UPPAAL queries and simulations.

Significance. If the claims hold, the paper makes a useful step toward integrating formal methods into RL for AD: it exemplifies concrete model-checking queries for pre-training validation, and shows how reward automata can be verified before learning. The strengths include a concrete tool integration (CommonUppRoad), explicit model templates and queries, and a demonstration that model pre-analysis can detect inadequate sensor precision and sensing periods. However, the significance is limited by the fact that the experiments are confined to a single scenario, use a confounded comparison, and, most importantly, the safety guarantee is only established for a discretized, sampled model rather than for the continuous dynamics it is meant to approximate. The central promise that model checking makes RL 'safer' therefore rests on an unquantified abstraction gap.

major comments (3)
  1. [Section 3.1-3.2, Algorithm 1, Query (1)/Qd] The safety shield synthesized by Query (1) is only guaranteed for the sampled, discretized state space: the hybrid clocks x, y, v, acc, and head are excluded from the symbolic state space, and the integer significands iX, iY, iV, iAcc, iHead are updated only at sensing instants by the Euler integration in Algorithm 1. Hence A[] !collide() && !offroad() ensures safety for the discrete frames, not for the continuous trajectory between frames. Section 4.1 and Fig.7(a)-(b) explicitly show that under shields synthesized with exponent 1 or sensing period 2, simulated distances fall below the unsafe threshold. The proposed remedy, Qa, is a statistical query returning Pr[|cv - i2d(iv)| >= THD]; it provides no worst-case bound linking this discrepancy to collision distance, and the probability from Query (5) is not reported in the experiments. As the paper's central claim is that model checking can make RL for AD 'safer', this unquantified gap is load-bearing: a positive pre-analysis or a 100-run histogram is not a certificate that the shield is safe in the continuous model, nor that the chosen sensing period and step size are adequate.
  2. [Section 5, Table 3 and Equation (8)] The comparison between reward automata (RA) and reward functions (RF) is confounded. The weights in Equation (8) were hand-tuned by the author using the reward automaton and queries from Table 2, the learning episode counts differ by a factor of 25 (20 episodes for RA and SS&RA versus 500 for RF), and the results come from a single run with no error bars or variance information. Consequently, the claim that reward automata 'greatly improve' learning performance is suggestive but not established by the reported data. A fair comparison would fix episode counts, reward weights, and hyperparameters, or at least report multiple independent runs and statistical dispersion.
  3. [Section 5, Fig.7 and Query (5)] For the selected setting (c) (exponent 4, sensing period 1), the only reported support that this configuration is adequate is the 100 simulations from Query (6); the probability returned by Query (5) is not reported, and the value of THD used in Qa is not given. Without reporting the actual probability of sensor error and its relation to the 3*TD distance threshold, the choice of this setting is not quantitatively justified, and the claim that 'no cases exceeding the threshold' in 100 simulations demonstrates sufficiency is statistically weak.
minor comments (7)
  1. [Title / Header] The title in the workshop version contains a spacing artifact, 'Y ou Think!'; this should be corrected to 'You Think!'.
  2. [Section 2.2.3] The phrase 'safety-shield synthesis would have no actions to learn from' is imprecise; it should say that there would be no actions to choose from or to optimize over.
  3. [Section 4.2.1, Figure 5] The labels in Figure 5 are difficult to read, particularly the rates in states S2, S3, and S4; a larger font or a table listing the rates would improve readability.
  4. [Table 2] There is a typo in the explanation of Qg: 'non-negtive' should be 'non-negative'.
  5. [Section 5] The statement 'the exponent is decreased from four to one' is ambiguous. If the exponent refers to the power of 10 in Equation (4), changing from 10^-4 to 10^-1 increases the scale and reduces precision; it should be phrased as 'the scale is changed from 10^-4 to 10^-1'.
  6. [Section 5, Query (7)] The notation '{dv1,...}->{cv1,...}' in Query (7) is not explained in the text; a brief explanation of the variable lists would help the reader.
  7. [General] The paper repeatedly claims that 'all these findings are supported by experiments', but no statistical analysis, multiple seeds, or confidence intervals are provided; please consider adding at least a statement about the number of runs and variance.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the pre-analysis and reward-automaton claims are evaluated by independent UPPAAL queries and simulations, not by fitting parameters to the outcomes and renaming them predictions.

full rationale

The paper's central claims are that model checking can pre-analyze sensor accuracy and sensing periods, and that reward automata help design reward functions and improve multi-objective RL. These are supported by separate UPPAAL queries (Qa-Qd in Table 1, Qe-Qh in Table 2) and by simulation results (Fig.7, Table 3), rather than by parameters fitted to the experimental outcome and then reported as predictions. The self-citations to CommonUppRoad [13] and other prior work are background infrastructure, not load-bearing justifications of the new claims. The reward-automaton verification queries are conformance checks against the same guards used to build the automaton, but the paper presents them as design and debugging aids, not as independent predictions or derived facts. The abstraction gap between hybrid clocks and integer states is a soundness risk that the paper itself exposes in Fig.7, but exposing a limitation is not circularity.

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

The central claims rest on the faithfulness of the UPPAAL model abstractions (discretized actions, hybrid clocks, numerical integration) and on hand-chosen reward parameters. The reward weights and automaton rates are tuned by the author rather than derived from data, so the experimental demonstration is specific to these choices.

free parameters (5)
  • Reward weights in Equation (8) = 10 (safe), 5 (progress), 100 (goal), 1 (comfort)
    Hand-tuned by the author using reward automaton verification; they determine the RL reward function's balance between objectives and directly affect the reported learning times.
  • Reward automaton rates and penalties (Fig.5) = +1 per time unit per objective; -100 for collision; sa divided by 100 on collision
    These values define the reward automaton's behavior; the claimed learning improvement is relative to this specific reward structure, and no sensitivity analysis is provided.
  • Sensor accuracy exponent and sensing/decision periods = exponent 1 or 4; sensing period 1 or 2 time units
    The pre-analysis experiment varies these settings; the conclusion that one setting is adequate (exponent 4, period 1) is specific to these choices.
  • Distance thresholds TD and 3*TD = not numerically specified in the text
    These thresholds define collision and unsafe proximity in the scenario and in all queries (Table 2, Fig.7); without their values the experimental setting is under-specified.
  • Model constants C1, C2, G, D, U, MAXT = unspecified
    These constants define the sensing/decision periods, integration granularity, action range, and learning horizon; the paper does not give their values, which limits reproduction.
assumptions (4)
  • domain assumption UPPAAL's symbolic and statistical model checking are sound for the discretized timed-game model
    Used in Section 4.1 for Queries Qa-Qd and safety shield synthesis; the paper assumes the tool's exhaustive analysis is correct.
  • ad hoc to paper The integer-significand representation and numerical integration in sense() faithfully approximate the continuous vehicle dynamics
    Algorithm 1 in Section 3.2 uses Euler-style integration on hybrid clocks; safety shields and pre-analysis are computed on this abstraction, and no error bounds are given.
  • domain assumption Moving obstacles can be represented as predefined trajectories with instantaneous velocity and heading changes at waypoints
    Section 3.3 justifies this by the digital controller's periodic sensing; the verification and shield synthesis depend on this abstraction.
  • ad hoc to paper The reward automaton's rates, penalties, and priority order correctly encode the designer's multi-objective preferences
    Fig.5 assigns +1 per time unit for safety, progress, and comfort, and a collision penalty; the claimed learning improvements are measured under this specific encoding.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!." pith.science (2026). https://pith.science/paper/IYJ75P3A

@misc{pith2026241114375,
  author       = {Pith},
  title        = {Pith review of: Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IYJ75P3A}},
  note         = {Machine review of arXiv:2411.14375}
}
read the original abstract

Most reinforcement learning (RL) platforms use high-level programming languages, such as OpenAI Gymnasium using Python. These frameworks provide various API and benchmarks for testing RL algorithms in different domains, such as autonomous driving (AD) and robotics. These platforms often emphasise the design of RL algorithms and the training performance but neglect the correctness of models and reward functions, which can be crucial for the successful application of RL. This paper proposes using formal methods to model AD systems and demonstrates how model checking (MC) can be used in RL for AD. Most studies combining MC and RL focus on safety, such as safety shields. However, this paper shows different facets where MC can strengthen RL. First, an MC-based model pre-analysis can reveal bugs with respect to sensor accuracy and learning step size. This step serves as a preparation of RL, which saves time if bugs exist and deepens users' understanding of the target system. Second, reward automata can benefit the design of reward functions and greatly improve learning performance especially when the learning objectives are multiple. All these findings are supported by experiments.

Figures

Figures reproduced from arXiv: 2411.14375 by the authors.

Figure 1
Figure 1. CommonUppRoad, a platform for model-checking-based AD motion planning, verification, [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. UPPAAL model templates of AD vehicles. In (a), (b), and (c), [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Obstacle Moving obstacles in CommonRoad usually follow predefined trajecto￾ries (Fig.1), therefore the model template of moving obstacles is rel￾atively simple. Fig.3 is the model template, where xo and yo are the only two hybrid clocks because the velocity (iVo) and heading (iHo) of a moving obstacle immediately changes when it reaches a waypoint on the trajectory. One may argue that the model template is not faith… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: An illustration of potential problems when running RL without pre-analysis. [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 5
Figure 5. Figure 5: An example of reward automata. Hy￾brid clocks sa, co, and pr represent the rewards for safety, comfort, and progress, respectively. Fig.5 shows an example of reward automata, which considers the aforementioned three ob￾jectives in the following order of priority: safet…
Figure 6
Figure 6. Figure 6: Experimental AD scenario The experiments in this section aim to demonstrate the strengths of MC-enhanced RL in two aspects: i) the necessity of model pre-analysis, and ii) the benefits of MC in designing reward au￾tomata4 . The selected AD scenario is depicted in Fig.6…
Figure 7
Figure 7. Figure 7: Model pre-analysis result (Query (6)). The blue lines are the distances between the AD vehicle [PITH_FULL_IMAGE:figures/full_fig_p014_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

28 extracted references · 13 canonical work pages

  1. [1]

    arXiv preprint arXiv:2405.01440 , doi:10.48550/arXiv.2405.01440

    Ahmed Abouelazm, Jonas Michel & J Marius Zoellner (2024): A Review of Reward Functions for Reinforcement Learning in the context of Autonomous Driving . arXiv preprint arXiv:2405.01440 , doi:10.48550/arXiv.2405.01440

    work page doi:10.48550/arxiv.2405.01440 2024

  2. [2]

    In: 2017 IEEE Intelligent Vehicles Symposium (IV) , IEEE, pp

    Matthias Althoff, Markus Koschi & Stefanie Manzinger (2017): CommonRoad: Composable benchmarks for motion planning on roads . In: 2017 IEEE Intelligent Vehicles Symposium (IV) , IEEE, pp. 719–726, doi:10.1109/IVS.2017.7995802

    arXiv 2017

  3. [3]

    Information and Computation 261, pp

    Rajeev Alur, Salar Moarref & Ufuk Topcu (2018): Compositional and symbolic synthesis of reactive controllers for multi-agent systems . Information and Computation 261, pp. 616–633, doi:10.1016/j.ic.2018.02.021

    work page doi:10.1016/j.ic.2018.02.021 2018

  4. [4]

    https://www.bbc

    BBC (September 16th, 2020): Uber’s self-driving operator charged over fatal crash. https://www.bbc. com/news/technology-54175359

    work page 2020

  5. [5]

    In: Advanced Course on Petri Nets, Springer, pp

    Johan Bengtsson & Wang Yi (2003): Timed automata: Semantics, algorithms and tools . In: Advanced Course on Petri Nets, Springer, pp. 87–124, doi:10.1007/978-3-540-27755-2 3

    doi:10.1007/978-3-540-27755-2 2003

  6. [6]

    Formal Aspects of Computing 32(2), pp

    Marcello M Bersani, Matteo Soldo, Claudio Menghi, Patrizio Pelliccione & Matteo Rossi (2020): PuRSUE- from specification of robotic environments to synthesis of controllers. Formal Aspects of Computing 32(2), pp. 187–227, doi:10.1007/s00165-020-00509-0. Springer

    work page doi:10.1007/s00165-020-00509-0 2020

  7. [7]

    In: International Conference on Computer Aided Verification, Springer, doi:10.1007/978-3-642-14295-6 31

    Stefan Blom, Jaco van de Pol & Michael Weber (2010): LTSmin: Distributed and symbolic reachability. In: International Conference on Computer Aided Verification, Springer, doi:10.1007/978-3-642-14295-6 31

    doi:10.1007/978-3-642-14295-6 2010

  8. [8]

    In: International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, doi:10.1007/BFb0055357

    Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis & Sergio Yovine (1998): Kronos: A model-checking tool for real-time systems. In: International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, doi:10.1007/BFb0055357. 176 Model Checking for Reinforcement Learning in Autonomous Driving

    work page doi:10.1007/bfb0055357 1998

Show all 28 references
  1. [9]

    In: International Conference on Computer Aided Verification, Springer, doi:10.1007/978-3-642-22110-1 30

    Goran Frehse, Colas Le Guernic, Alexandre Donz ´e, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang & Oded Maler (2011):SpaceEx: Scalable verification of hybrid systems. In: International Conference on Computer Aided Verification, Springe...

    2011 doi

  2. [10]

    Annual Reviews in Control 57, p

    Kunal Garg, Songyuan Zhang, Oswin So, Charles Dawson & Chuchu Fan (2024): Learning safe control for multi-robot systems: Methods, verification, and open challenges. Annual Reviews in Control 57, p. 100948, doi:10.1016/j.arcontrol.2024.100948

    2024

  3. [11]

    ACM Trans

    Rong Gu, Eduard Baranov, Afshin Ameri, Cristina Seceleanu, Eduard Paul Enoiu, Baran C ¨ur¨ukl¨u, Axel Legay & Kristina Lundqvist (2024): Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions. ACM Trans. Softw. Eng. Methodol.33...

    2024 doi

  4. [12]

    Science of Computer Programming 224, p

    Rong Gu, Peter G Jensen, Cristina Seceleanu, Eduard Enoiu & Kristina Lundqvist (2022): Correctness- guaranteed strategy synthesis and compression for multi-agent autonomous systems . Science of Computer Programming 224, p. 102894, doi:10.1016/j.scico.2022.102894

    2022

  5. [13]

    Available at https://arxiv.org/abs/2408.01093

    Rong Gu, Kaige Tan, Andreas Holck Høeg-Petersen, Lei Feng & Kim Guldstrand Larsen (2024): Com- monUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Visualisation of Autonomous Vehicles. Available at https://arxiv.org/abs/2408.01093

    2024 arXiv

  6. [14]

    373–382, doi:10.1145/225058.225162

    Thomas A Henzinger, Peter W Kopke, Anuj Puri & Pravin Varaiya (1995): What’s decidable about hybrid automata? In: Proceedings of the twenty-seventh annual ACM symposium on Theory of computing , pp. 373–382, doi:10.1145/225058.225162

    1995

  7. [15]

    Journal of Artificial Intelligence Research 73, pp

    Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano & Sheila A McIlraith (2022): Reward machines: Exploiting reward function structure in reinforcement learning . Journal of Artificial Intelligence Research 73, pp. 173–208, doi:10.1613/jair.1.12440

    2022 doi

  8. [16]

    In: Eighth ACM/IEEE Interna- tional Conference on Formal Methods and Models for Codesign (MEMOCODE 2010) , IEEE, pp

    Franjo Ivan ˇci´c, Malay K Ganai, Sriram Sankaranarayanan & Aarti Gupta (2010): Numerical stability analysis of floating-point computations using software model checking . In: Eighth ACM/IEEE Interna- tional Conference on Formal Methods and Models for Codesign (MEMOCODE 2010) ...

    2010

  9. [17]

    In: 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), IEEE, pp

    Shivesh Khaitan & John M Dolan (2022): State dropout-based curriculum reinforcement learning for self- driving at unsignalized intersections. In: 2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), IEEE, pp. 12219–12224, doi:10.1109/IROS47612.2022.9981109

    2022

  10. [18]

    International journal on software tools for technology transfer 1, pp

    Kim G Larsen, Paul Pettersson & Wang Yi (1997): UPPAAL in a nutshell. International journal on software tools for technology transfer 1, pp. 134–152, doi:10.1007/s100090050010

    1997 doi

  11. [19]

    IEEE Transactions on Intelligent Vehicles, doi:10.1109/TIV .2023.3289580

    Irani Liu & Matthias Althoff (2023): Specification-compliant driving corridors for motion planning of auto- mated vehicles. IEEE Transactions on Intelligent Vehicles, doi:10.1109/TIV .2023.3289580

    2023

  12. [20]

    In: The 18th International Symposium on Theoretical Aspects of Software Engineering, Springer, doi:10.1007/978-3-031- 64626-3 21

    Naeem Muhammad, Gu Rong, Seceleanu Cristina, Guldstrand Larsen Kim, Nielsen Brian & Albano Michele (2024): Energy-Optimized Motion Planning for Autonomous Vehicles Using UPPAAL Stratego. In: The 18th International Symposium on Theoretical Aspects of Software Engineering, Sprin...

    2024 doi

  13. [21]

    In: International Symposium on Theoretical Aspects of Software Engineering , Springer, pp

    Muhammad Naeem, Rong Gu, Cristina Seceleanu, Kim Guldstrand Larsen, Brian Nielsen & Michele Albano (2024): Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal Stratego. In: International Symposium on Theoretical Aspects of Software Engineering , Springer, pp....

    2024 doi

  14. [22]

    In: 2019 IEEE Intelligent Vehicles Symposium (IV), IEEE, pp

    Maximilian Naumann, Hendrik Konigshof, Martin Lauer & Christoph Stiller (2019): Safe but not over- cautious motion planning under occlusions and limited sensor range . In: 2019 IEEE Intelligent Vehicles Symposium (IV), IEEE, pp. 140–145, doi:10.1109/IVS.2019.8814251

    2019

  15. [23]

    https://www.washingtonpost.com/technology/2023/06/10/ tesla-autopilot-crashes-elon-musk/

    The Washington Post (June 10th, 2023): 17 fatalities, 736 crashes: The shocking toll of Tesla’s Autopilot . https://www.washingtonpost.com/technology/2023/06/10/ tesla-autopilot-crashes-elon-musk/

    2023

  16. [24]

    https://www.es.mdh.se/dpac/

    KKS funded Project (2015 - 2023): DPAC - Dependable Platforms for Autonomous systems and Control . https://www.es.mdh.se/dpac/. Rong Gu 177

    2015

  17. [25]

    https://www.mdu.se/en/malardalen-university/research/research-projects/ holistic-synthesis-and-verification-for-safe-and-secure-autonomous-vehicles?

    KKS funded Project (2024 - 2026): Holistic Synthesis and Verification for Safe and Secure Autonomous Vehicles. https://www.mdu.se/en/malardalen-university/research/research-projects/ holistic-synthesis-and-verification-for-safe-and-secure-autonomous-vehicles?

    2024

  18. [26]

    In: 2022 IEEE Intelligent Vehicles Symposium (IV), IEEE, pp

    Jos ´e Manuel Gaspar S´anchez, Truls Nyberg, Christian Pek, Jana Tumova & Martin T¨orngren (2022): Foresee the unseen: Sequential reasoning about hidden obstacles for safe driving. In: 2022 IEEE Intelligent Vehicles Symposium (IV), IEEE, pp. 255–264, doi:10.1109/IV51971.2022.9827171

    2022

  19. [27]

    arXiv preprint arXiv:2307.14316, doi:10.3233/FAIA230598

    Qisong Yang, Thiago D Sim˜ao, Nils Jansen, Simon H Tindemans & Matthijs TJ Spaan (2023):Reinforcement Learning by Guided Safe Exploration. arXiv preprint arXiv:2307.14316, doi:10.3233/FAIA230598

    2023 arXiv

  20. [28]

    (2022): Finding critical sce- narios for automated driving systems: A systematic mapping study

    Xinhai Zhang, Jianbo Tao, Kaige Tan, Martin T ¨orngren, Jose Manuel Gaspar Sanchez, Muhammad Rusyadi Ramli, Xin Tao, Magnus Gyllenhammar, Franz Wotawa, Naveen Mohan et al. (2022): Finding critical sce- narios for automated driving systems: A systematic mapping study . IEEE Tra...

    2022

Pith tools

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