To enable the successful deployment of task-achieving multi-robot systems (MRS), coordination mechanisms must be utilized in order to effectively mediate the interactions between the robots and the task environment. Over the past decade, there have been a number of elegant experimentally demonstrated MRS coordination mechanisms. Most of these mechanisms have been task-specific in nature, typically providing only empirical insights into coordination design and little in the way of systematic techniques to assist in the design of coordinated MRS for new task domains. To fully realize the potentials of MRS, formally-grounded systematic techniques amenable to analysis are needed in order to facilitate the design of coordinated MRS. We address this problem by presenting a formal framework for describing and reasoning about coordination in a MRS. Using this principled foundation, we are developing a suite of general methods for automatically synthesizing the controllers of robots constituting a MRS such that the given task is performed in a coordinated fashion. This paper presents a method for the automatic synthesis of a specific type of controller, one that is stateless but capable of inter-robot communication. We also present a graph coloring-based approach for minimizing the number of necessary unique communication messages. The synthesis of such communicative controllers provides a means for assessing the uses and limitations of communication in MRS coordination. We present experimental validation of our formal approach of controller synthesis in a multi-robot construction domain through physically-realistic simulations and in real-robot demonstrations.