Driven by both civilian and military applications, such as coordinated surveillance, search and rescue, underwater or space exploration, manipulation in hazardous environments, and rapid emergency response, cooperative actions by teams of robots has emerged as an important research area. However, the coordination strategies for such robot teams are still developed to a great extent by trial-and-error processes. Hence, the strategies cannot guarantee mission success. This award supports fundamental research to provide a provably correct formal design theory of multi-robot systems that guarantees mission success. Furthermore, results from the research can be extended to the design of more general cyber-physical systems (CPSs) consisting of distributed and coordinated subsystems, such as the national power grid, ground/air traffic networks, and manufacturing systems. These CPSs are critical components of the national civil infrastructure that must operate reliably to ensure public safety. The multidisciplinary approach taken will help broaden participation of underrepresented groups in research and positively impact engineering education. Focusing on multi-robot teams, the goal of the research is to build foundations for a provably correct formal design theory for CPSs. This design theory will guarantee a given global performance of multi-robot teams through designing local coordination rules and control laws. The basic idea is to decompose the team mission into individual subtasks such that the design can be reduced to a local synthesis problem for individual robots. Multidisciplinary approaches combining hybrid systems, supervisory control, regular inference and model checking will be utilized to achieve this goal. The developed theory will enable robots in the team to cooperatively learn their individual roles in a mission, and then automatically synthesize local supervisors to fulfill their subtasks. A salient feature of this method lies on its ability to handle environmental uncertainties and unmodeled dynamics, as there is no need for an explicit model of the transition dynamics of each agent/robot and their interactions with the environment. In addition, the design is online and reactive, enabling the robot team to adapt to changing environments and dynamic tasking. The derived theory will be implemented as software tools and will be demonstrated through real robotic systems consisting of unmanned ground and aerial vehicles in unstructured urban/rural areas.