Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Engenharia de Automação e SistemasO problema da coordenação de um sistema multi-robôs, que pode realizar atividades mais complexas e de forma mais rápida e eficiente que um único robô, é um tema complexo que apresenta um importante desafio de pesquisa. O planejamento de trajetórias e de tarefas são alguns dos problemas fundamentais dos sistemas multi-robôs e se referem a encontrar caminhos livres de colisão para cada robô determinado a realizar uma dada tarefa. Obviamente, para alcançar estes caminhos livres de colisão, algum tipo de coordenação é indispensável. Para garantir propriedades de segurança e alcançabilidade, este trabalho se interessa em estudar o uso de técnicas de modelagem e de verificação formal na solução deste tipo de problema. Para tal, duas diferentes técnicas para a solução do planejamento e coordenação de sistemas multi-robôs foram abordadas. Na primeira técnica, Teoria de Controle Supervisório, o problema consiste em calcular o supervisor ótimo que representa a lógica de controle utilizada para o planejamento de tarefas. Na segunda técnica, Autômato Jogo-Temporizado, uma estratégia é sintetizada para o planejamento de tarefas dos robôs que considera um jogo entre o ambiente e o controlador evidenciando a reatividade destes sistemas e a constante busca da vitória por parte do controlador em termos de segurança e alcançabilidade. Por fim, uma arquitetura genérica para a implementação de sistemas multi-robôs foi desenvolvida para fornecer desde o planejamento de tarefas ao controle contínuo dos robôs. Desta maneira, este trabalho avalia diferentes métodos formais para o desenvolvimento do planejamento e coordenação de sistemas multi-robôs, além de reproduzir os resultados das técnicas em um ambiente real.The coordination problem of a multi-robot system to accomplish complex activities and in a faster and more effcient way than a single robot is a complex issue that presents a major research challenge. The path and task planning are some of the fundamental problems of multi-robot systems and corresponds to and collision-free paths for each robot to accomplish an individual given task. Obviously, to achieve these collision-free paths, some kind of coordination is essential. For this purpose, two different techniques for solving the planning and the coordination of multi-robot systems have been tackled. In the frst technique, the Supervisory Control Theory, the problem consists to calculate the optimal supervisor representing the control logic used for task planning. In the second technique, Timed Game tomata, a strategy is synthesized for the robot task planning that take account a game between the environment and the controller showing the reactivity of these systems and the constant seek for the victory by the controller in terms of safety and reachability. Finally, a generic architecture for the implementation of a multi-robot system is designed to provide resources from task planning to the continuous control. Thus, this work evaluates different formal methods for the development of planning and coordination of multi-robots systems, besides to reproduce the results of the techniques in a real environment.