Verified Design of Robotic Autonomous Systems using Probabilistic Model Checking

• URL: http://arxiv.org/abs/2601.10720v1
• Date: Fri, 19 Dec 2025 13:01:08 GMT
• Title: Verified Design of Robotic Autonomous Systems using Probabilistic Model Checking
• Abstract summary: Safety and reliability play a crucial role when designing Robotic Autonomous Systems.<n>We propose a methodology to apply a formal method, namely Probabilistic Model Checking (PMC), to enable systematic evaluation and analysis of a given set of system design concepts.<n>We illustrate the application of the suggested methodology to a practical RAS concept selection use-case from robotics agriculture.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Safety and reliability play a crucial role when designing Robotic Autonomous Systems (RAS). Early consideration of hazards, risks and mitigation actions -- already in the concept study phase -- are important steps in building a solid foundations for the subsequent steps in the system engineering life cycle. The complex nature of RAS, as well as the uncertain and dynamic environments the robots operate within, do not merely effect fault management and operation robustness, but also makes the task of system design concept selection, a hard problem to address. Approaches to tackle the mentioned challenges and their implications on system design, range from ad-hoc concept development and design practices, to systematic, statistical and analytical techniques of Model Based Systems Engineering. In this paper, we propose a methodology to apply a formal method, namely Probabilistic Model Checking (PMC), to enable systematic evaluation and analysis of a given set of system design concepts, ultimately leading to a set of Verified Designs (VD). We illustrate the application of the suggested methodology -- using PRISM as probabilistic model checker -- to a practical RAS concept selection use-case from agriculture robotics. Along the way, we also develop and present a domain-specific Design Evaluation Criteria for agri-RAS.

Related papers

• Fundamentals of Building Autonomous LLM Agents [64.39018305018904]
  This paper reviews the architecture and implementation methods of agents powered by large language models (LLMs)<n>The research aims to explore patterns to develop "agentic" LLMs that can automate complex tasks and bridge the performance gap with human capabilities.
  arXiv  Detail & Related papers  (2025-10-10T10:32:39Z)
• A Verification Methodology for Safety Assurance of Robotic Autonomous Systems [0.1962656580942496]
  This paper presents a verification workflow for the safety assurance of an autonomous agricultural robot.<n>It covers the entire development life-cycle, from concept study and design to runtime verification.<n>Results show that the methodology can be effectively used to verify safety-critical properties and facilitate the early identification of design issues.
  arXiv  Detail & Related papers  (2025-06-24T13:39:51Z)
• Probabilistic modelling and safety assurance of an agriculture robot providing light-treatment [0.0]
  Continued adoption of agricultural robots postulates the farmer's trust in the reliability, robustness and safety of the new technology.<n>This paper considers a probabilistic modelling and risk analysis framework for use in the early development phases.
  arXiv  Detail & Related papers  (2025-06-24T13:39:32Z)
• An LLM-enabled Multi-Agent Autonomous Mechatronics Design Framework [49.633199780510864]
  This work proposes a multi-agent autonomous mechatronics design framework, integrating expertise across mechanical design, optimization, electronics, and software engineering.<n> operating primarily through a language-driven workflow, the framework incorporates structured human feedback to ensure robust performance under real-world constraints.<n>A fully functional autonomous vessel was developed with optimized propulsion, cost-effective electronics, and advanced control.
  arXiv  Detail & Related papers  (2025-04-20T16:57:45Z)
• A quantitative framework for evaluating architectural patterns in ML systems [49.1574468325115]
  This study proposes a framework for quantitative assessment of architectural patterns in ML systems.<n>We focus on scalability and performance metrics for cost-effective CPU-based inference.
  arXiv  Detail & Related papers  (2025-01-20T15:30:09Z)
• EARBench: Towards Evaluating Physical Risk Awareness for Task Planning of Foundation Model-based Embodied AI Agents [53.717918131568936]
  Embodied artificial intelligence (EAI) integrates advanced AI models into physical entities for real-world interaction.<n>Foundation models as the "brain" of EAI agents for high-level task planning have shown promising results.<n>However, the deployment of these agents in physical environments presents significant safety challenges.<n>This study introduces EARBench, a novel framework for automated physical risk assessment in EAI scenarios.
  arXiv  Detail & Related papers  (2024-08-08T13:19:37Z)
• A Methodology to Identify Physical or Computational Experiment Conditions for Uncertainty Mitigation [0.0]
  This paper introduces a methodology for designing computational or physical experiments for system-level uncertainty mitigation purposes. The proposed methodology is versatile enough to tackle uncertainty management across various design challenges.
  arXiv  Detail & Related papers  (2024-05-22T18:59:42Z)
• Toward Methodical Discovery and Handling of Hidden Assumptions in Complex Systems and Models [3.1771791275364194]
  external reviews can uncover undocumented built-in assumptions. We show that a variety of digital artifacts can be automatically checked against extensive reference knowledge. We believe that systematic handling of this aspect of system engineering can contribute significantly to the quality and safety of complex systems and models.
  arXiv  Detail & Related papers  (2023-12-27T10:33:12Z)
• Model-based Analysis and Specification of Functional Requirements and Tests for Complex Automotive Systems [0.19837121116620585]
  We propose a technique that starts with the early identification of validation concerns from a stakeholder perspective. We develop a Model-Based Systems Engineering (MBSE) methodology to ensure complete and consistent requirements and test specifications. Our study corroborates that our methodology is applicable and improves existing requirements and test specification processes.
  arXiv  Detail & Related papers  (2022-09-03T18:24:32Z)
• Multi Agent System for Machine Learning Under Uncertainty in Cyber Physical Manufacturing System [78.60415450507706]
  Recent advancements in predictive machine learning has led to its application in various use cases in manufacturing. Most research focused on maximising predictive accuracy without addressing the uncertainty associated with it. In this paper, we determine the sources of uncertainty in machine learning and establish the success criteria of a machine learning system to function well under uncertainty.
  arXiv  Detail & Related papers  (2021-07-28T10:28:05Z)
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification [81.32981236437395]
  We present a semi-formal verification approach for decision-making tasks based on interval analysis. Our method obtains comparable results over standard benchmarks with respect to formal verifiers. Our approach allows to efficiently evaluate safety properties for decision-making models in practical applications.
  arXiv  Detail & Related papers  (2020-10-19T11:18:06Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.