Formal design of a provably safe robotic roundabout system

In this paper, we show how to design a provably safe robotic roundabout system comprised of three vehicles. This is accomplished by combining two-vehicle collision avoidance primitives, which are each computationally light given the natural partial order structure on which the system evolves. We show how to design the system parameters in order to prevent conflicts among the control primitives, and to thus ensure the safety and liveness of the system as a whole. We implement our design on a multi-vehicle test-bed involving three vehicles continuously running on three intersecting roundabouts, and provide experimental results demonstrating the system is collision free and live.