Automatic Controller Code Generation for Swarm Robotics Using Probabilistic Timed Supervisory Control Theory (ptSCT)

The development of flexible swarm robotics systems capable of adapting to the task and environmental changes is a serious challenge. The main motivations of Swarm robotics are decentralized control, stability, adaptivity, and flexibility. Usually, ad-hoc approaches are employed to design a controller capable of meeting the problem specifications. However, these methods cannot be easily verified, and in some cases, it is not even shown that they meet the specifications. Moreover, the controller source code has to be developed separately, primarily when formal methods are employed; As a result, it cannot be guaranteed that the implementation matches the design. This paper proposes a new method - probabilistic timed supervisory control (ptSCT) - to formally design a controller from systems specifications. The proposed ptSCT has several advantages: 1) the automatic generation of the controller source code utilizable in ARGoS platform, 2) formal designing capability using the implemented software tool, 3) set of powerful design components like probabilistic decisions and time constraints, and 4) the reusability of formally designed modules among different scenarios and multiple robotic platforms. Two case studies are considered to investigate various aspects of the proposed system. Firstly, the synchronization case study is implemented for a comparison between SCT and ptSCT in terms of design capabilities and memory consumption. Secondly, the foraging case study as a complex and medium-sized problem is modeled using ptSCT step by step. More than 2400 experiments with a varying number of obstacles, targets, and robots are executed in ARGoS platform in order to show the performance of the automatically generated source code.