The goal of the project is to develop a formal foundation for the synthesis and analysis of implicit multi-robot coordination mechanisms. Such a formal understanding will allow the multi-robot community to move away from ad-hoc solutions and toward the principled design and analysis of coordinated multi-robot systems. This will be achieved by introducing a formal language to describe the entities interacting in a coordinated multi-robot system, and apply this framework to the principled synthesis of robot controllers using logic-based induction. At the same time, this project will develop a methodology for modeling the coupled robot-environment system and derive the equations describing dynamics of the system. Finally, these procedures will be combined, so that results of analysis can be used to drive performance-enhancing modifications in the robot controller. To validate the formal concepts of the proposed research, these methods will be applied to the design and analysis of multi-robot coordination methods for a real-world sensor/actuator network deployment and maintenance task. The proposed research is novel in that it combines formal techniques from Computer Science, Mathematics, and Physics. As such, the work will serve as a vehicle for raising the profile of mathematical analysis in the robotics community. Undergraduate and graduate robotics courses will benefit from the inclusion of the developed formal analysis techniques. In addition, twice a year demonstrations will be given at local high schools to teach the students the concepts of collective behavior and give them the skills to better understand and approach complex problems.
