Multiparty Motion Coordination: From Choreographies to Robotics Programs

TL;DR

This paper introduces a formal programming model with a type system for multi-robot coordination, ensuring safety, collision avoidance, and correct synchronization through static verification, implemented on ROS for complex robot scenarios.

Contribution

It presents a novel choreographic type system combining motion primitives and communication, enabling static verification of complex multi-robot behaviors.

Findings

Successfully verified complex multi-robot maneuvers.

Ensured collision freedom and communication safety.

Implemented on ROS for practical robotics applications.

Abstract

We present a programming model and typing discipline for complex multi-robot coordination programming. Our model encompasses both synchronisation through message passing and continuous-time dynamic motion primitives in physical space. We specify \emph{continuous-time motion primitives} in an assume-guarantee logic that ensures compatibility of motion primitives as well as collision freedom. We specify global behaviour of programs in a \emph{choreographic} type system that extends multiparty session types with jointly executed motion primitives, predicated refinements, as well as a \emph{separating conjunction} that allows reasoning about subsets of interacting robots. We describe a notion of \emph{well-formedness} for global types that ensures motion and communication can be correctly synchronised and provide algorithms for checking well-formedness, projecting a type, and local type checking. A well-typed program is \emph{communication safe}, \emph{motion compatible}, and \emph{collision free}. Our type system provides a compositional approach to ensuring these properties. We have implemented our model on top of the ROS framework. This allows us to program multi-robot coordination scenarios on top of commercial and custom robotics hardware platforms. We show through case studies that we can model and statically verify quite complex manoeuvres involving multiple manipulators and mobile robots---such examples are beyond the scope of previous approaches.