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, E-flow American Institute of Aeronautics and Astronautics (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 primitives 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 transformations (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 primitives 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 transformations (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=84973442614&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84973442614&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84973442614
T3 - AIAA Guidance, Navigation, and Control Conference 2015, MGNC 2015 - Held at the AIAA SciTech Forum 2015
BT - AIAA Guidance, Navigation, and Control Conference 2015, MGNC 2015 - Held at the AIAA SciTech Forum 2015
PB - American Institute of Aeronautics and Astronautics Inc.
T2 - AIAA Guidance, Navigation, and Control Conference 2015, MGNC 2015 - Held at the AIAA SciTech Forum 2015
Y2 - 5 January 2015 through 9 January 2015
ER -