Abstract
Summary form only given. As robotic systems are getting cheaper and easier to produce in mass, more and more applications envision future systems in which groups of simple robots are expected to self-organize and cooperate to perform complex tasks. While earlier developments have mostly emphasized an empiric approach, observing the emergence of collective behavior under given circumstances, there has been a call for a more formal approach based on rigorous problem definitions, formally stated algorithms, and detailed proofs of correctness. The rigorous definition of a system model for cooperative mobile robots is a necessary foundation for a formal study of algorithms and their proofs. The first definition of such a model, proposed by Suzuki and Yamashita and called SYm, appeared for the first time in a journal publication a decade ago. A weaker model, called CORDA, with full asynchrony between robots has been later defined by Prencipe et al. In this tutorial, we will introduce the two main system models, namely SYm and CORDA, as well as many of the variants that have been considered in the literature. We will discuss some of the tradeoffs and illustrate the difference between the two main system models through the example of the gathering problem. The attendant will have a good grasp of the main issues and the terminology used in this area of research.