Swarm robotics systems have the potential to tackle many interesting problems. Their control software is mostly created by ad-hoc development. This makes it hard to deploy
swarm robotics systems in real-world scenarios as it is difficult to analyse, maintain, or extend these systems. Formal methods can contribute to overcome these problems.
However, they usually do not guarantee that the implementation matches the specification because the system’s control code is typically generated manually.
This thesis studies the application of the supervisory control theory (SCT) framework in swarm robotics systems. SCT is widely applied and well established in the man-
ufacturing context. It requires the system and the desired behaviours (specifications) to be defined as formal languages. In this thesis, regular languages are used. Regular languages, in the form of deterministic finite state automata, have already been widely applied for controlling swarm robotics systems, enabling a smooth transition from the ad-hoc development currently in practice. This thesis shows that the control code for
swarm robotics systems can be automatically generated from formal specifications.
Several case studies are presented that serve as guidance for those who want to learn how to specify swarm behaviours using SCT formally. The thesis provides the tools for
the implementation of controllers using formal specifications. Controllers are validated on swarms of up to 600 physical robots through a series of systematic experiments.
It is also shown that the same controllers can be automatically ported onto different robotics platforms, as long as they offer the required capabilities. The thesis extends and incorporates techniques to the supervisory control theory framework; specifically, the concepts of global events and the use of probabilistic generators. It can be seen as a step towards making formal methods a standard practice in swarm robotics.
