Using progress sets on non-deterministic transition systems for multiple UAV motion planning

<p>In this demonstration, two Aerial Robotic Workers are given a surveillance task where the first drone (red circle) starts in the blue area, the second drone (blue circle) starts in the red area, and the drones need to infinitely often exchange their positions while avoiding collisions and avoiding leaving the flying area. A controller for the multi-agent system guaranteeing the satisfaction of this high-level task is synthesized by first considering a non-deterministic and finite abstraction of the dynamical system, and then using the notion of progress sets corresponding to sets of state-control pairs for which eventual progress towards the desired goal is guaranteed.</p>