Toward formal models and languages for verifiable multi-robot systems

Incorrect operation of a multi-robot system (MRS) may not only lead to unsatisfactory results, but it can also cause economic losses and jeopardize safety. These risks may not always be evident, since they may arise as unforeseen consequences of interactions between different components of the system. Thus, tools and techniques that can help in providing guarantees about the behavior of MRSs are on demand; whenever possible, these guarantees should be backed up by formal proofs complementing the traditional approaches based on testing and simulation. Tailored linguistic support to specify MRSs is a major step toward this goal. In fact, reducing the gap between typical features of an MRS and the linguistic primitives used to model them would simplify both the specification of these systems and their verification. With the aim of reducing this gap, we identified some key features of MRSs in this work. Subsequently, we considered the selection of three specification languages oriented toward MRSs, which are representative of wider categories of languages with similar aims. Finally, we assessed the extent to which the considered languages captured the key features in an adequate and intuitive way by using them to implement multi-robot systems case studies.