Verified Design of Robotic Autonomous Systems using Probabilistic Model Checking

TL;DR

This work addresses the absence of formal guarantees in the concept-design phase of Robotic Autonomous Systems by introducing a Probabilistic Model Checking ($PMC$) based framework that integrates Formal Methods with Model-Based Systems Engineering and Multi-Criteria Decision Making. The method constructs a parametric $DTMC$ model of design variants, maps verifiable design criteria into $PCTL$ properties, and uses $PRISM$ to verify each variant, yielding a set of Verified Designs ($VD$) with scores that are then aggregated via MCDM for ranking. A concrete agri-RAS use-case demonstrates the workflow: defining a domain-specific design criteria set, generating 12 design-space variants, filtering via PMC against stated success criteria, and presenting top designs with radar plots to support decision-making. The approach enables robust, verifiable concept selection under uncertainty and points to future automation and extension to broader system lifecycles and to more expressive probabilistic models such as $MDP$.

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.

Figures (7)

• Figure 1: The concept study is the initial phase of the verification methodology across the engineering life-cycle taken from adam2025. Notice that the performance modeling and Design space generation steps - encircled in red, dashed box - are non-formal.
• Figure 2: Methodology workflow: The arrow shapes indicate execution steps, the rectangular shapes indicate artifacts. The blue color marks systems engineering while the green color marks formal methods domain of expertise.
• Figure 3: Thovald robot equipped with two 5DOF arms in a poly-tunnel strawberry test field at NMBU Campus.
• Figure 4: Design evaluation criteria according to the stakeholders' areas of expertise. The circled numbers correspond to criterion ID described in Table \ref{['table:design_criteria']}.
• Figure 5: System level parametric DTMC model: Blue colored states have constant outbound transition whereas purple colored states have parametric outbound transition probabilities.

Theorems & Definitions (1)

• Definition 1: Transition System, $(TS)$