Formal Verification of Robotic Contact Tasks via Reachability Analysis

TL;DR

This paper introduces a formal verification method for robotic contact tasks using reachability analysis, enabling comprehensive safety checks in complex hybrid systems with contacts.

Contribution

It extends reachability analysis for hybrid automata with a novel guard intersection approach, allowing scalable verification of contact-rich robot behaviors.

Findings

Successfully verified safe human-robot interactions with contact constraints.

Demonstrated scalability and reliability of the approach in complex contact scenarios.

Outperformed existing methods in verifying hybrid contact dynamics.

Abstract

Verifying the correct behavior of robots in contact tasks is challenging due to model uncertainties associated with contacts. Standard methods for testing often fall short since all (uncountable many) solutions cannot be obtained. Instead, we propose to formally and efficiently verify robot behaviors in contact tasks using reachability analysis, which enables checking all the reachable states against user-provided specifications. To this end, we extend the state of the art in reachability analysis for hybrid (mixed discrete and continuous) dynamics subject to discrete-time input trajectories. In particular, we present a novel and scalable guard intersection approach to reliably compute the complex behavior caused by contacts. We model robots subject to contacts as hybrid automata in which crucial time delays are included. The usefulness of our approach is demonstrated by verifying safe human-robot interaction in the presence of constrained collisions, which was out of reach for existing methods.