pith. sign in

arxiv: 2604.07414 · v1 · submitted 2026-04-08 · 💻 cs.LO · cs.RO· cs.SE· cs.SY· eess.SY

Formally Guaranteed Control Adaptation for ODD-Resilient Autonomous Systems

Gricel V\'azquez , Calum Imrie , Sepeedeh Shahbeigi , Nawshin Mannan Proma , Tian Gan , Victoria J Hodge , John Molloy , Simos Gerasimou This is my paper

Pith reviewed 2026-05-10 17:07 UTC · model grok-4.3

classification 💻 cs.LO cs.ROcs.SEcs.SYeess.SY
keywords autonomous systemsoperational design domainprobabilistic modelsformal guaranteescontrol adaptationresilienceout-of-ODDverification
0
0 comments X

The pith

Adapting probabilistic system models dynamically extends their coverage to out-of-ODD scenarios while providing quantitative formal guarantees for autonomous system behavior.

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

The paper introduces a method to adapt probabilistic models of autonomous systems so they can handle situations outside the original Operational Design Domain. This adaptation runs alongside verification steps that supply quantitative guarantees on the new behavior. A sympathetic reader would care because autonomous systems routinely encounter real conditions their designers never anticipated, and current approaches often leave them without safety assurances in those cases. The work shows preliminary evidence that reliability improves when the model is extended on the fly instead of requiring a complete redesign.

Core claim

We explore the challenge of ensuring reliable performance in situations outside the Operational Design Domain (ODD) by introducing an approach for adapting probabilistic system models to handle out-of-ODD scenarios while, in parallel, providing quantitative guarantees. Our approach dynamically extends the coverage of existing system situation capabilities, supporting the verification and adaptation of the system's behaviour under unanticipated situations. Preliminary results demonstrate that our approach effectively increases system reliability by adapting its behaviour and providing formal guarantees even under unforeseen out-of-ODD situations.

What carries the argument

Dynamic extension of probabilistic system models that adds coverage for out-of-ODD situations while preserving the ability to compute quantitative formal guarantees on adapted control actions.

Load-bearing premise

Probabilistic system models can be dynamically extended to out-of-ODD scenarios while still allowing quantitative formal guarantees to be provided on the adapted behavior.

What would settle it

A concrete out-of-ODD scenario in which the adapted model produces a control policy that violates the stated quantitative guarantee or leads to unsafe system behavior.

Figures

Figures reproduced from arXiv: 2604.07414 by Calum Imrie, Gricel V\'azquez, John Molloy, Nawshin Mannan Proma, Sepeedeh Shahbeigi, Simos Gerasimou, Tian Gan, Victoria J Hodge.

Figure 1
Figure 1. Figure 1: SAVE approach overview: pre-deployment (A,B) and deployment (M,A,P,E) phases with shared knowledge. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: SAVE execution times to get criticality scores. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
read the original abstract

Ensuring reliable performance in situations outside the Operational Design Domain (ODD) remains a primary challenge in devising resilient autonomous systems. We explore this challenge by introducing an approach for adapting probabilistic system models to handle out-of-ODD scenarios while, in parallel, providing quantitative guarantees. Our approach dynamically extends the coverage of existing system situation capabilities, supporting the verification and adaptation of the system's behaviour under unanticipated situations. Preliminary results demonstrate that our approach effectively increases system reliability by adapting its behaviour and providing formal guarantees even under unforeseen out-of-ODD situations.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The manuscript introduces an approach for dynamically extending probabilistic system models of autonomous systems to cover out-of-ODD scenarios, enabling behavior adaptation and verification under unanticipated situations while claiming to provide quantitative formal guarantees; preliminary results are asserted to demonstrate increased reliability.

Significance. If the model-extension construction can be shown to preserve soundness of quantitative bounds (e.g., PCTL probabilities), the work would address a practically important gap in resilient autonomous systems. At present the significance is potential rather than demonstrated, given the preliminary character of the reported results.

major comments (2)
  1. [Abstract] Abstract and preliminary-results description: the central claim that dynamic extension 'provides formal guarantees even under unforeseen out-of-ODD situations' is not accompanied by any explicit construction, theorem, or argument showing how new states/transitions receive probability values while preserving the soundness assumptions of the original quantitative verification procedure.
  2. [Preliminary results] Preliminary results: no data, methods, error bars, verification details, or comparison baselines are supplied, so the assertion that the approach 'effectively increases system reliability' cannot be evaluated and remains unsupported.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address the major comments point by point below and will incorporate revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract and preliminary-results description: the central claim that dynamic extension 'provides formal guarantees even under unforeseen out-of-ODD situations' is not accompanied by any explicit construction, theorem, or argument showing how new states/transitions receive probability values while preserving the soundness assumptions of the original quantitative verification procedure.

    Authors: We agree the abstract is too concise on this point. The manuscript body describes the dynamic extension procedure for assigning probabilities to new states and transitions in out-of-ODD cases. To make the soundness preservation explicit (e.g., for PCTL bounds), we will add a dedicated theorem and argument in the revised version showing how the extension maintains the original verification assumptions. revision: yes

  2. Referee: [Preliminary results] Preliminary results: no data, methods, error bars, verification details, or comparison baselines are supplied, so the assertion that the approach 'effectively increases system reliability' cannot be evaluated and remains unsupported.

    Authors: We acknowledge the preliminary results section lacks the requested supporting details. In the revision we will expand it with the underlying data, methods, error bars, verification specifics, and baseline comparisons to allow proper evaluation of the reliability claims. revision: yes

Circularity Check

0 steps flagged

No circularity detected; approach described at high level without equations or self-referential reductions.

full rationale

The abstract and provided description introduce a dynamic extension of probabilistic models for out-of-ODD scenarios with formal guarantees, but contain no equations, derivations, fitted parameters, or load-bearing self-citations. Claims rest on preliminary results and the assumption that extensions preserve quantitative bounds, yet no specific construction (e.g., probability assignment or model-checking soundness proof) is shown that reduces to its own inputs by definition. This is a standard high-level proposal without the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no concrete parameters, axioms, or invented entities; all content remains at the level of general approach description.

pith-pipeline@v0.9.0 · 5426 in / 959 out tokens · 42039 ms · 2026-05-10T17:07:05.634854+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

40 extracted references · 40 canonical work pages

  1. [1]

    https://github.com/Gricel-lee/RV-OutOfODD/tree/main- v1-SEAMS26

    Project’s GitHub. https://github.com/Gricel-lee/RV-OutOfODD/tree/main- v1-SEAMS26

    work page

  2. [2]

    Abeywickrama, Michael Fisher, Frederic Wheeler, and Louise Dennis

    Dhaminda B. Abeywickrama, Michael Fisher, Frederic Wheeler, and Louise Dennis. 2025. Towards Patterns for a Reference Assurance Case for Autonomous Inspection Robots . In2025 IEEE/ACM 22nd International Conference on Software and Systems Reuse (ICSR). IEEE Computer Society, 95–100. doi:10.1109/ICSR66718.2025.00016

    work page doi:10.1109/icsr66718.2025.00016 2025

  3. [3]

    Naif Alasmari, Radu Calinescu, Colin Paterson, and Raffaela Mirandola

    work page

  4. [4]

    Quantitative verification with adaptive uncertainty reduction.Journal of Systems and Software188 (2022), 111275

    work page 2022

  5. [5]

    Rob Alexander, Heather Rebecca Hawkins, and Andrew John Rae. 2015. Situation coverage–a coverage criterion for testing autonomous robots. (2015)

    work page 2015

  6. [6]

    Héctor Avilés, Marco Negrete, Alberto Reyes, Rubén Machucho, Karelly Rivera, Gloria de-la Garza, and Alberto Petrilli. 2024. Autonomous Behavior Selection For Self-driving Cars Using Probabilistic Logic Factored Markov Decision Processes.Applied Artificial Intelligence38, 1 (2024), 2304942

    work page 2024

  7. [7]

    2008.Principles of model checking

    Christel Baier and Joost-Pieter Katoen. 2008.Principles of model checking. MIT press

    work page 2008

  8. [8]

    Radu Calinescu, Simos Gerasimou, Kenneth Johnson, and Colin Pater- son. 2018. Using runtime quantitative verification to provide assurance evidence for self-adaptive software: advances, applications and research challenges. InSoftware Engineering for Self-Adaptive Systems III. Assur- ances: International Seminar, Dagstuhl Castle, Germany, December 15-19, ...

    work page 2018

  9. [9]

    Radu Calinescu, Sinem Getir Y aman, Simos Gerasimou, Gricel Vázquez, and Micah Bassett. 2025. Verification and External Parameter Inference for Stochastic World Models.2026 IEEE/ACM 48th IEEE International Conference on Software Engineering(2025). https://arxiv.org/abs/2503. 16034

    work page 2025

  10. [10]

    Radu Calinescu, Carlo Ghezzi, Kenneth Johnson, Mauro Pezzé, Y asmin Rafiq, and Giordano Tamburrelli. 2015. Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE transactions on reliability65, 1 (2015), 107–125

    work page 2015

  11. [11]

    Radu Calinescu, Calum Imrie, Ravi Mangal, Genaína Nunes Rodrigues, Corina P ˘as˘areanu, Misael Alpizar Santana, and Gricel Vázquez. 2022. Discrete-event controller synthesis for autonomous systems with deep- learning perception components.arXiv preprint arXiv:2202.03360(2022)

    work page arXiv 2022

  12. [12]

    Javier Cámara, David Garlan, Bradley Schmerl, and Ashutosh Pandey

    work page

  13. [13]

    InProceedings of the 30th annual ACM symposium on applied computing

    Optimal planning for architecture-based self-adaptation via model checking of stochastic games. InProceedings of the 30th annual ACM symposium on applied computing. 428–435

    work page

  14. [14]

    Nicolás Cardozo and Ivana Dusparic. 2021. Adaptation to Unknown Situa- tions as the Holy Grail of Learning Based Self-Adaptive Systems: Research Directions. In16th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS@ICSE 2021, Madrid, Spain, May 18-24, 2021. IEEE, 252–253. doi:10.1109/SEAMS51251.2021. 00041

    work page doi:10.1109/seams51251.2021 2021

  15. [15]

    Shang Gao, Zhixin Huang, Ghassan Al-Falouji, Bernhard Sick, and Sven Tomforde. 2025. Towards Cognitive Situational Awareness in Maritime Traf- fic Using Federated Evidential Learning. In2025 IEEE Conference on Cog- nitive and Computational Aspects of Situation Management (CogSIMA). 9–16. doi:10.1109/CogSIMA64436.2025.11079521

    work page doi:10.1109/cogsima64436.2025.11079521 2025

  16. [16]

    Simos Gerasimou, Radu Calinescu, and Alec Banks. 2014. Efficient runtime quantitative verification using caching, lookahead, and nearly- optimal reconfiguration. InProceedings of the 9th international symposium on software engineering for adaptive and self-managing systems. 115– 124

    work page 2014

  17. [17]

    Victoria J Hodge and Matt Osborne. 2025. Agile Development for Safety Assurance of Machine Learning in Autonomous Systems (AgileAMLAS). Array27 (2025), 100482

    work page 2025

  18. [18]

    J., Paterson, C., and Habli, I

    Victoria J. Hodge, Colin Paterson, and Ibrahim Habli. 2025. Out-of- Distribution Detection for Safety Assurance of AI and Autonomous Systems. arXiv:2510.21254 [cs.AI] https://arxiv.org/abs/2510.21254

    work page arXiv 2025

  19. [19]

    Calum Imrie, Rhys Howard, Divya Thuremella, Nawshin Mannan Proma, Tejas Pandey, Paulina Lewinska, Ricardo Cannizzaro, Richard Hawkins, Colin Paterson, Lars Kunze, et al. 2024. Aloft: self-adaptive drone controller testbed. InProceedings of the 19th International Symposium on Software Engineering for Adaptive and Self-Managing Systems. 70–76

    work page 2024

  20. [20]

    Erblin Isaku, Hassan Sartaj, and Shaukat Ali. 2025. Digital Twin-based Out-of-Distribution Detection in Autonomous Vessels. arXiv:2504.19816 [cs.RO] https://arxiv.org/abs/2504.19816

    work page arXiv 2025

  21. [21]

    Marta Kwiatkowska, Gethin Norman, and David Parker. 2007. Stochastic model checking. InInternational School on Formal Methods for the Design of Computer, Communication and Software Systems. Springer, 220–270

    work page 2007

  22. [22]

    Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. InComputer Aided Verification: 23rd International Conferenc (CAV). Proceedings 23. Springer, 585–591

    work page 2011

  23. [23]

    Lee et al

    J. Lee et al. 2025. Enhancing Safety in Autonomous Maritime Transporta- tion Systems with Real-Time AI Agents.Applied Sciences15, 9 (2025),

    work page 2025

  24. [24]

    doi:10.3390/app15094986

    work page doi:10.3390/app15094986

  25. [25]

    Gabriel A Moreno, Javier Cámara, David Garlan, and Bradley Schmerl

    work page

  26. [26]

    InProceedings of the 2015 10th joint meeting on foundations of software engineering

    Proactive self-adaptation under uncertainty: a probabilistic model checking approach. InProceedings of the 2015 10th joint meeting on foundations of software engineering. 1–12

    work page 2015

  27. [27]

    Society of Automotive Engineers. 2018. Taxonomy and Definitions for Terms Related to Driving Automation Systems for On-Road Motor Vehi- cles. https://www.sae.org/standards/j3016_201806-taxonomy-definitions- terms-related-driving-automation-systems-road-motor-vehicles

    work page 2018

  28. [28]

    Nawshin Mannan Proma and Rob Alexander. 2023. Systematic Situ- ation Coverage versus Random Situation Coverage for Safety Testing in an Autonomous Car Simulation. InProcs of the 12th Latin-American Symposium on Dependable and Secure Computing(<conf-loc>, <city>La Paz</city>, <country>Bolivia</country>, </conf-loc>)(LADC ’23). 208–213. https://doi.org/10.1...

    work page doi:10.1145/3615366.3625077 2023

  29. [29]

    Nawshin Mannan Proma, Gricel Vazquez Flores, Sepeedeh Shahbeigi Roudposhti, Arjun Badyal, and Victoria J Hodge. 2025. Probabilistic Safety Verification for an Autonomous Ground Vehicle: A Situation Coverage Grid Approach. In2025 IEEE International Conference on Vehicular Electronics and Safety. IEEE

    work page 2025

  30. [30]

    Hodge, and Rob Alexander

    Nawshin Mannan Proma, Victoria J. Hodge, and Rob Alexander. 2025. SCALOFT: An Initial Approach for Situation Coverage-Based Safety Analy- sis of an Autonomous Aerial Drone in a Mine Environment. InAccepted for, 44th International Conference on Computer Safety, Reliability and Security (safecomp 2025). https://arxiv.org/abs/2505.20969

    work page arXiv 2025

  31. [31]

    Salil Purandare, Urjoshi Sinha, Md Nafee Al Islam, Jane Cleland-Huang, and Myra B. Cohen. 2023. Self-Adaptive Mechanisms for Misconfigurations in Small Uncrewed Aerial Systems. In2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS). 169–180. doi:10.1109/SEAMS59076.2023.00030

    work page doi:10.1109/seams59076.2023.00030 2023

  32. [32]

    Y asmin Rafiq, Gricel Vázquez, Radu Calinescu, Sanja Dogramadzi, and Robert M Hierons. 2025. Symbolic Runtime Verification and Adaptive Decision-Making for Robot-Assisted Dressing. InEuromicro Conference on Software Engineering and Advanced Applications. Springer, 290–308

    work page 2025

  33. [33]

    Zaid Tahir and Rob Alexander. 2021. Intersection focused situation coverage-based verification and validation framework for autonomous vehicles implemented in Carla. InInternational Conference on Modelling and Simulation for Autonomous Systems. Springer, 191–212

    work page 2021

  34. [34]

    Tobias Rye Torben. 2023. Formal approaches to design and ver- ification of safe control systems for autonomous vessels.PhD Thesis, NTNU: Norwegian University of Science and Technology, https://hdl.handle.net/11250/3059350(2023)

    work page 2023

  35. [35]

    Gricel Vázquez, Alexandros Evangelidis, Sepeedeh Shahbeigi, and Simos Gerasimou. 2025. Adaptive Human-Robot Collaborative Missions using Hybrid Task Planning. In2025 IEEE/ACM 20th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS). IEEE, 73–84

    work page 2025

  36. [36]

    2020.An introduction to self-adaptive systems: A contem- porary software engineering perspective

    Danny Weyns. 2020.An introduction to self-adaptive systems: A contem- porary software engineering perspective. John Wiley & Sons

    work page 2020

  37. [37]

    Danny Weyns and Jesper Andersson. 2023. From self-adaptation to self- evolution leveraging the operational design domain. In2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS). IEEE, 90–96

    work page 2023

  38. [38]

    Danny Weyns, Radu Calinescu, Raffaela Mirandola, Kenji Tei, Maribel Acosta, Nelly Bencomo, Amel Bennaceur, Nicolas Boltz, Tomas Bures, Javier Camara, et al. 2023. Towards a research agenda for understand- ing and managing uncertainty in self-adaptive systems.ACM SIGSOFT Software Engineering Notes48, 4 (2023), 20–36

    work page 2023

  39. [39]

    Xingyu Zhao, Radu Calinescu, Simos Gerasimou, Valentin Robu, and David Flynn. 2020. Interval change-point detection for runtime probabilis- tic model checking. InProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering. 163–174

    work page 2020

  40. [40]

    Xingyu Zhao, Simos Gerasimou, Radu Calinescu, Calum Imrie, Valentin Robu, and David Flynn. 2024. Bayesian learning for the robust verification of autonomous robots.Communications Engineering3, 1 (2024), 18

    work page 2024