Motion Session Types for Robotic Interactions
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning.
We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time.
We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision.
We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.
Thu 18 JulDisplayed time zone: Belfast change
15:40 - 17:00
Concurrency and ParallelismResearch Papers at Mancy
Chair(s): Stephen Kell University of Kent
|DynaSOAr: A Parallel Memory Allocator for Object-oriented Programming on GPUs with Efficient Memory Access|
Matthias Springer Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of TechnologyDOI Pre-print Media Attached
|Reliable State Machines: A Framework for Programming Reliable Cloud Services|
Suvam Mukherjee Microsoft Research India, Nitin John Raj International Institute of Information Technology, Hyderabad, Krishnan Govindraj Microsoft Research, Pantazis Deligiannis Microsoft Research, Chandramouleswaran Ravichandran Microsoft Azure, Akash Lal Microsoft Research India, Aseem Rastogi Microsoft Research, Raja Krishnaswamy Microsoft AzureDOI Media Attached
|Transferring Obligations Through Synchronizations|
Jafar Hamin imec-DistriNet, Depatrmant of Computer Science, KU Leuven, Belgium, Bart Jacobs KU LeuvenDOI Media Attached
|Motion Session Types for Robotic Interactions|
Rupak Majumdar MPI-SWS, Germany, Marcus Pirron MPI-SWS, Nobuko Yoshida Imperial College London, Damien Zufferey MPI-SWSDOI Media Attached