Movement primitives and formal methods have been proposed for many robotic applications. In this paper, we discuss work-in-progress utilizing formal methods for synthesizing high-level specifications written in linear temporal logic (LTL) realized with low-level prim- itives that ensure these specifications produce physically feasible swarm behaviors. The methodology synthesizes higher-level, choreographed behaviors for virtual kinematic chains of planar mobile robots that are realized with primitives consisting of (a) a one-dimensional distributed flocking algorithm with verified properties and (b) planar homogeneous trans- formations (rotations and translations). We show how to use the methodology to construct verified distributed algorithms for higher-dimensional (planar) shape formation. The existing one-dimensional algorithm has two main properties: (safety) avoidance of collisions between swarm members, and (progress) eventual flock (platoon) formation, which in one dimension is a roughly equal spacing between adjacent robots. By combining this one- dimensional flocking algorithm with other simple local operations, namely rotations and other distributed consensus (averaging) algorithms, we show how to create planar formations with planar safety and progress properties.
