Supervisory control theory for controlling swarm robotics systems

Yuri Kaszubowski Lopes

Abstract

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 manufacturing 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.

Usage of Nadzoru

Nadzoru (Lopes et al. 2011), (Lopes et al. 2012 (PDF, 482KB)), and (Pinheiro et al. 2015) is an open-source development tool for supervisory control synthesis. With a user-friendly GUI, models can be created, analysed, and simulated.

The source code of controllers can be automatically generated. By changing the templates, this tool can generate code for different devices from the same model.

Watch a video showing the usage of Nadzoru.

Videos of physical experiments

The following videos show the conducted experiments.

Orbit case study (chapter 4)

This case study presents two robots where one robot is static and the other orbits counter-clockwise around it (Rubenstein et al. 2012).

The distance between those robots gets measured by sending/receiving an infra-red message from the static to the orbiting robot.

The orbiting robot modulates its behaviour according to its distance:

If it is too close, the robot turns clock-wise.
If it is too far away, the robot turns counter-clockwise.
If the robot is inside the boundary defined by thresholds it moves forward.

Kilobot: Trials 1-10: Trial 1

Trial 2

Trial 3

Trial 4

Trial 5

Trial 6

Trial 7

Trial 8

Trial 9

Trial 10
e-puck: Trials 1-10: Trial 1

Trial 2

Trial 3

Trial 4

Trial 5

Trial 6

Trial 7

Trial 8

Trial 9

Trial 10

Segregation case study (chapter 4)

This case studies separates robots into three distinct groups (indicated by three different colours) (Lopes et al. 2014) and (Lopes et al. 2016). In this study, we used red, green, and blue.

Each group has a leader, which sends out its identifier like a beacon. A follower robot tries to find a situation where it only receives messages of a single leader.

Kilobot: Trials 1-10: Trial 1

Trial 2

Trial 3

Trial 4

Trial 5

Trial 6

Trial 7

Trial 8

Trial 9

Trial 10
e-puck: Trials 1-10: Trial 1

Trial 2

Trial 3

Trial 4

Trial 5

Trial 6

Trial 7

Trial 8

Trial 9

Trial 10

Aggregation case study (chapter 4)

20 e-puck robots are randomly distributed and, with support of an on-board camera and the usage of one bit of information, the robots should aggregate. (Gauci et al. 2014a) and (Lopes et al. 2016).

Trial 1
Trial 2
Trial 3
Trial 4
Trial 5
Trial 6
Trial 7
Trial 8
Trial 9
Trial 10

Object clustering case study (chapter 4)

A group of five robots use a three-state sensor (pixels of the onboard camera) to cluster 20 objects that are initially dispersed in the environment.

Each robot can either detect an object, another robot, or nothing in its direct line of sight. (Gauci et al. 2014b) and (Lopes et al. 2016).

Trial 1
Trial 2
Trial 3
Trial 4
Trial 5
Trial 6
Trial 7
Trial 8
Trial 9
Trial 10

Group formation case study (chapter 4)

In this case study, leader robots (identified by a randomly chosen colour) accepts follower robots of two classes which we call green and blue.

Each leader tries to balance the amount of accepted green and blue robots and only accepts a robot of one class if the group has not an excess of this type.

By accepting one robot, the group also increases their communication area, because each accepted robot relays its leader messages. (Lopes et al. 2016).