Multiparty Motion Coordination: From Choreographies to Robotics Programs
summary
Combines multiparty session types with assume‑guarantee reasoning to avoid exponential state blowup and statically verify choreographies of robots; a Python implementation uses ROS for runtime and reduces compatibility checks to SMT queries solved by dReal4. Case study executes on 5 robots, exchanging 16 messages and running 53 motion primitives; motion primitives are specified as 7‑tuples (pre/assume/guarantee/post, footprint, duration, interruptibility) and composition checks disjoint footprints, compatible durations, and timed choice disambiguation. Verification artifact and hardware experiments are provided.
AI-written summary · about
chapters (11)
- 0:00Intro
- 1:02Programming & Verification of CPS
- 1:53State-space Explosion
- 2:15From Global to Local (and back) Multiparty session types (Communication) Global Spec.
- 4:54Assume-Guarantee Reasoning
- 5:49Motion Session Calculus
- 7:08Example Choreography
- 8:32Merge
- 10:17Evaluation: Sorting Example
- 11:13Eval.: Comparing to [ECOOP 19]
- 12:08Implementation
related talks
25mHigh-Level Mission Specification for Multiple Robots
40mCo-operative robots sharing the load
29mSynchronous Programming and Refinement Types in Robotics: From Verification to Implementation
09mTask-Consistent Signaling Motions for Improved Understanding in Human-Robot Interaction and ...
59mOn Human-robot Interactions via Multimodal Intent Modeling and Reachability-based Safety Assurance
20mPirouette: Higher-Order Typed Functional Choreographies
09mSituated Live Programming for Human-Robot Collaboration
18mRobotics: why now?