Verified planar formation control algorithms by composition of primitives Conference

Bobadilla, L, Johnson, TT, Laviers, A et al. (2015). Verified planar formation control algorithms by composition of primitives .

cited authors

  • Bobadilla, L; Johnson, TT; Laviers, A; Huzaifa, U

abstract

  • 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.

publication date

  • January 1, 2015

International Standard Book Number (ISBN) 13