Verified planar formation control algorithms by composition of primitives

Leonardo Bobadilla, Taylor T. Johnson, Amy Laviers, Umer Huzaifa

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationAIAA Guidance, Navigation, and Control Conference
PublisherAmerican Institute of Aeronautics and Astronautics Inc, AIAA
ISBN (Print)9781624103391
StatePublished - 2015
EventAIAA Guidance, Navigation, and Control Conference, 2015 - Kissimmee, United States
Duration: Jan 5 2015Jan 9 2015

Publication series

NameAIAA Guidance, Navigation, and Control Conference, 2013


OtherAIAA Guidance, Navigation, and Control Conference, 2015
Country/TerritoryUnited States

ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Aerospace Engineering
  • Control and Systems Engineering


Dive into the research topics of 'Verified planar formation control algorithms by composition of primitives'. Together they form a unique fingerprint.

Cite this