TY - GEN
T1 - Verified planar formation control algorithms by composition of primitives
AU - Bobadilla, Leonardo
AU - Johnson, Taylor T.
AU - Laviers, Amy
AU - Huzaifa, Umer
N1 - Publisher Copyright:
© 2015, American Institute of Aeronautics and Astronautics Inc, AIAA. All rights reserved.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85027294588&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85027294588&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:85027294588
SN - 9781624103391
T3 - AIAA Guidance, Navigation, and Control Conference, 2013
BT - AIAA Guidance, Navigation, and Control Conference
PB - American Institute of Aeronautics and Astronautics Inc, AIAA
T2 - AIAA Guidance, Navigation, and Control Conference, 2015
Y2 - 5 January 2015 through 9 January 2015
ER -