Towards formal models and languages for verifiable Multi-Robot Systems

TL;DR

This paper explores formal models and languages tailored for specifying and verifying Multi-Robot Systems to ensure safety and correctness, emphasizing the importance of formal proofs and linguistic support for system guarantees.

Contribution

It reviews agent-oriented languages for MRSs, implements case studies using these languages, and evaluates their effectiveness in expressing complex behaviors.

Findings

Formal verification can enhance MRS safety guarantees.

Linguistic support simplifies specifying complex multi-robot behaviors.

Surveyed languages vary in expressiveness and verification capabilities.

Abstract

Incorrect operations of a Multi-Robot System (MRS) may not only lead to unsatisfactory results, but can also cause economic losses and threats to safety. These threats may not always be apparent, since they may arise as unforeseen consequences of the interactions between elements of the system. This call for tools and techniques that can help in providing guarantees about MRSs behaviour. We think that, whenever possible, these guarantees should be backed up by formal proofs to complement traditional approaches based on testing and simulation. We believe that tailored linguistic support to specify MRSs is a major step towards this goal. In particular, reducing the gap between typical features of an MRS and the level of abstraction of the linguistic primitives would simplify both the specification of these systems and the verification of their properties. In this work, we review different agent-oriented languages and their features; we then consider a selection of case studies of interest and implement them useing the surveyed languages. We also evaluate and compare effectiveness of the proposed solution, considering, in particular, easiness of expressing non-trivial behaviour.