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

Toward formal models and languages for verifiable multi-robot systems

Inverso O
2018

Abstract

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
multi-robot systems, languages, communication, collective behavior, automated reasoning
File in questo prodotto:
File Dimensione Formato  
2018_FrontRobotAI_DeNicola.pdf

accesso aperto

Tipologia: Versione Editoriale (PDF)
Licenza: Accesso gratuito
Dimensione 589.34 kB
Formato Adobe PDF
589.34 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.12571/7113
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? ND
social impact