机器人系统往往面临的是复杂而多变的任务需求以及外部不确定环境,多机器人分布式系统的协同配合以及安全地控制多机器人系统在外部环境下完成任务是严峻而又急迫的研究内容。在传统方法上,开发人员手工设计任务规划方案、运动规划方案以及机器人系统之间的消息通信方案,接着手工编写软件代码将开发人员所设计的控制器实现并且部署到机器人系统上对系统进行控制,最后通过手工地协同多机器人分布式系统让多机器人最后能够协同完成给定的任务。手工的流程是繁琐且非常容易出错的过程,在上个世纪丘奇就提出能否根据逻辑规约来自动地合成满足该逻辑规约的系统模型、程序或者电路,后续提出了很多解决方案,但是由于复杂度过高导致难以和软件工程相结合。近年来,Pnueli等人提出了基于GR（1）（一种线性时序逻辑的片段）的反应式系统综合,由于其高效的算法使得系统综合与实际软件工程相结合成为可能。与此同时,分布式系统的综合也得到深入的研究。本文运用GR（1）的自动控制器合成技术以及分布式系统综合来解决针对多变的任务需要以及的外部环境,能够自动地合成多机器人系统的控制器模型,以及自动地合成多机器人之间为了协同完成任务而相互通信的通信策略。更具体地说,本文将反应系统综合与分布式系统综合相结合,新颖地提出一种多机器人控制器生成方法,其工作内容分成如下三点:1.本文首先基于GR（1）规约,为开发人员提供便捷而又易于理解与书写的多机器人规约语言。2.基于本文提出的规约,自动地综合多机器人系统每个机器人的局部行为,同时,在局部行为综合的过程中帮助设计人员自动地合成多机器人系统的通信策略。3.为了避免运行过程种机器人之间的死锁问题,本文提出了相应的机器人运行同步方法,同时基于该方法提出两种实现方式。设计者只需要关心怎么将外部环境以及任务刻画为本文的规约语言,而无需操心机器人控制器的设计,以及机器人之间的通信设计。本文的多机器人控制器生成方法解决了分布式多机器人系统协同完成全局任务的问题。从全局任务规约综合得出的局部行为策略可以用作机器人的高层的任务规划。