Efficiently Obtaining Reachset Conformance for the Formal Analysis of Robotic Contact Tasks

TL;DR

This paper introduces a method for creating simplified, conformant models of robotic contact tasks that accurately capture system uncertainties, enabling safer and more efficient verification of robotic behaviors.

Contribution

It presents the first approach to generate reachset conformant models for hybrid robotic contact tasks, integrating non-determinism and optimal parameter identification.

Findings

Successfully applied to 3-DOF robots

Effectively captures uncertainties in system behavior

Reduces testing effort in industrial settings

Abstract

Formal verification of robotic tasks requires a simple yet conformant model of the used robot. We present the first work on generating reachset conformant models for robotic contact tasks considering hybrid (mixed continuous and discrete) dynamics. Reachset conformance requires that the set of reachable outputs of the abstract model encloses all previous measurements to transfer safety properties. Aiming for industrial applications, we describe the system using a simple hybrid automaton with linear dynamics. We inject non-determinism into the continuous dynamics and the discrete transitions, and we optimally identify all model parameters together with the non-determinism required to capture the recorded behaviors. Using two 3-DOF robots, we show that our approach can effectively generate models to capture uncertainties in system behavior and substantially reduce the required testing effort in industrial applications.