Multiparty Motion Coordination: From Choreographies to Robotics Programs
Tue 17 Nov 2020 03:40 - 04:00 at SPLASH-I - M-5 Chair(s): Bernardo Toninho, Xiangzhe Xu
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 <i>continuous-time motion primitives</i> in an assume-guarantee
logic that ensures compatibility of motion primitives as well as collision freedom.
We specify global behaviour of programs in a <i>choreographic</i> type system that extends
multiparty session types with jointly executed motion primitives, predicated refinements,
as well as a <i>separating conjunction</i> that allows reasoning about subsets of interacting
We describe a notion of <i>well-formedness</i> 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 <i>communication safe</i>, <i>motion compatible</i>, and <i>collision free</i>.
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.
Mon 16 NovDisplayed time zone: Central Time (US & Canada) change
Tue 17 NovDisplayed time zone: Central Time (US & Canada) change
03:00 - 04:20
M-5OOPSLA at SPLASH-I
Chair(s): Bernardo Toninho Nova University of Lisbon / NOVA-LINCS, Xiangzhe Xu Nanjing University
|CAMP: Cost-Aware Multiparty Session Protocols|
David Castro-Perez Imperial College London, Nobuko Yoshida Imperial College LondonLink to publication DOI Media Attached
|Counterexample-Guided Correlation Algorithm for Translation Validation|
Shubhani Gupta IIT Delhi, Abhishek Rose IIT Delhi, Sorav Bansal IIT Delhi and CompilerAI LabsLink to publication DOI Media Attached
|Multiparty Motion Coordination: From Choreographies to Robotics Programs|
Rupak Majumdar MPI-SWS, Nobuko Yoshida Imperial College London, Damien Zufferey MPI-SWSLink to publication DOI Media Attached
|On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers|
Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH ZurichLink to publication DOI Media Attached