Currently, the control software of swarm robotics systems is created by ad hoc development. This makes it hard to deploy these systems in real-world scenarios. In particular, it is difficult to maintain, analyse, or verify the 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. Also, there is cultural resistance to apply formal methods; they may be perceived as an additional step that does not add value to the final product. To address these problems, we propose supervisory control theory for the domain of swarm robotics. The advantages of supervisory control theory, and its associated tools, are a reduction in the amount of ad hoc development, the automatic generation of control code from modelled specifications, proofs of properties over generated control code, and the reusability of formally designed controllers between different robotic platforms. These advantages are demonstrated in four case studies using the e-puck and Kilobot robot platforms. Experiments with up to 600 physical robots are reported, which show that supervisory control theory can be used to formally develop state-of-the-art solutions to a range of problems in swarm robotics.

This paper faces the problem of coordinating equipment operation in a flexible manufacturing system consisting of several subsystems including robots, assembling machines, CNC lathes, and mills. There are two main problems in such a system. The first is controlling each individual subsystem considering its own sensors, actuators, and specialized controller to perform a certain sequence of activities. Due to their expertise and/or application of formal methods, programmable logic controller (PLC) practitioners and equipment manufacturers develop efficient and safe solutions to address this problem. The second problem is coordinating the concurrent operation of these subsystems with the goal of producing what is requested as efficiently as possible and guaranteeing the integrity and safety of the system. Supervisory control theory (SCT) is particularly suited to this problem. This paper presents a method that allows a designer to systematically convert SCT's results into a PLC application program. The resulting program conforms to IEC 61131-3 and preserves the natural modularity of the system to be controlled and control specifications. An extension of this method allows a designer to reuse existing PLC hardware and application programs designed for the control of equipment by easily integrating with the code corresponding to the SCT solution. A major portion of this code may even be automatically generated, reducing development time and minimizing editing errors.

In this article, we combine fault diagnosis and prognosis to generalize the notion of safe controllability of discrete-event systems. To do so, we reformulate the notions of safe diagnosability, prognosability, safe controllability by diagnosis, and safe controllability by prognosis in the context of strings. Moreover, we combine these notions to introduce the concept of safe controllability by diagnosis or prognosis, or simply DP-safe controllability. We show that a language can be DP-safe controllable even if it is not safe controllable either only by diagnosis or only by prognosis. Thus, the DP-safe controllability can be considered a generalization of the safe controllability concept found in the literature. If a DES is DP-safe controllable, to achieve fault tolerance using an active approach, reconfiguration actions could be forced based not only on online fault diagnosis, but also on online fault prognosis. Thus, our approach outperforms the previous ones, since it provides additional control options to keep the system away from forbidden zones and to switch from the nominal supervisor to a postfault-detection supervisor designed to achieve postfault performance objectives. Necessary and sufficient conditions for DP-safe controllability are presented and an example is used to illustrate the introduced concepts.