User-friendly controller synthesis for multi-agent robotic applications in presence of agents with unknown behavior

Developing robotic applications is a complex task that requires skills that are usually possessed by highly qualified robotic developers. We believe that, while formal methods techniques that support developers in the creation and design of robotic applications exist, they must be explicitly customized to be impactful in the robotic domain and to effectively support the growth of the robotic market. Specifically, the robotic market is asking for techniques that: (i) support a systematic and rigorous design of robotic applications though high-level languages; and (ii) enable the automatic synthesis of low-level controllers that allow robots to achieve their missions. To address those problems we present the PuRSUE (Planner for RobotS in Uncontrollable Environments) approach, which aims at supporting developers in the rigorous and systematic design of high-level run-time control strategies for robotic applications. The approach introduces PuRSUE-ML, a high-level language that allows modeling the environment, the agents deployed therein, and their missions. PuRSUE is able to automatically check whether a controller that allows robots to achieve their missions exist and synthesize it. We evaluated if PuRSUE offers a more compact way than Timed Game Automata (TGA) for modeling robotic applications, the effectiveness of its automatic computation of controllers, as well as whether it helped designers in reasoning on real-time properties of the scenarios, and how the approach supports the deployment of controllers on actual robots. To answer those questions we considered 13 scenarios coming from 3 different robotic applications presented in the literature. The results show that: (1) PuRSUE-ML does offer designers a more compact way for formal modeling of robotic applications compared to a direct encoding of the latter in low-level modeling formalisms; (2) PuRSUE effectively supports designers in the generation of controllers, compared to their manual development and supports them in reasoning on their temporal properties; and (3) the plans generated with PuRSUE are indeed effective when deployed on actual robots.

Negli ultimi anni le applicazioni robotiche sono diventate parte integrante delle nostre vite. Piattaforme mobili e manipolatori vengono sempre più utilizzati nella nostra società per eseguire azioni ripetitive, alienanti o pericolose per un essere umano. I robot, fianco a fianco con i lavoratori, sono utilizzati in ogni settore industriale, dalla meccanica, chimica al settore manifatturiero, per il trasporto di materiali e persone. Grazie alla loro flessibilità, personalizzabilità e vasta gamma di scelta nel mercato globale, questo genere di prodotto è in grado di soddisfare richieste e bisogni di molte tipologie. Per questo motivo le aziende che si affidano ad applicazioni robotiche necessitano di strumenti di programmazione sempre aggiornati in modo da rendere i loro prodotti sempre più disponibili per necessità di tipologie differenti. Gli sviluppatori di software hanno il compito di garantire strumenti flessibili e riutilizzabili in modo da soddisfare ogni necessità del consumatore. Il progetto Co4robots [44] all’interno del quale questa tesi è stata sviluppata, ha l’obiettivo di fornire strumenti che agevolano la programmazione nel contesto di applicazioni robotiche. Co4robots mira ad introdurre nel campo della robotica principi e tecniche caratteristiche dell’ingegneria del software per fornire un approccio ingegneristico alla programmazione di robot. Il progetto analizza principalmente applicazioni multi-robot nelle quali un team di robot collabora al fine di raggiungere il soddisfacimento di una data missione, che risulterebbe non eseguibile da un singolo robot. Per esempio, una missione potrebbe richiedere al team di robot di caricare e muovere oggetti o rifornimenti in un determinato ambiente p.e. uffici, alberghi od ospedali. L’ obiettivo finale del team di robot è descritto e assegnato come una missione definita da un linguaggio di alto livello. Co4robots progetta di elaborare un approccio sistematico per lo sviluppo di applicazioni robotiche. Questo approccio include tecniche che riguardano diversi aspetti tra cui (i) la possibilità di lavorare con agenti eterogenei, tra cui lavoratori e supervisori, (ii) lo sviluppo di algoritmi per la computazione delle azioni che i vari agenti devono eseguire per raggiungere la missione assegnata, (iii) un controllo decentralizzato che permette ai robot di interagire con l’ambiente circostante attraverso l’utilizzo di sensori e la comunicazione tra i componenti del team, (iv) facile integrazione con i diversi sistemi presenti sul mercato, (v) l’utilizzo di un linguaggio di alto livello per la definizione delle missioni, in modo da non richiedere all’utente particolari nozioni di robotica. Questa tesi tratta uno dei vari aspetti considerati all’interno del progetto Co4robot: la generazione di controllori partendo da un linguaggio di alto livello. La nostra analisi dello stato dell’arte ha sottolineato richiesta nell’ambito robotico di strumenti che (i) diano la possibilità di descrivere ad alto livello, attraverso una grammatica strutturata, un’applicazione robotica e (ii) gener- ino un controllore per i robot coinvolti nell’applicazione. In particolare, ci focalizziamo sul fornire tali funzioni in situazioni in cui il designer desidera descrivere ad alto livello agenti controllabili e non controllabili e di considerare una rappresentazione esplicita del tempo. Questo lavoro propone PuRSUE, un framework mirato al risolvere i problemi sopra citati. PuRSUE fornisce: • Un Domain Specific Language (DSL) chiamato PuRSUE-ML. PuRSUE- ML offre la possibilità di descrivere applicazioni robotiche in termini di descrizione dell’ambiente e degli agenti che interagiscono in questo ambiente, includendo rappresentazione esplicita del tempo. • Una traduzione automatica del modello definito con PuRSUE-ML in un modello nel formalismo dei Timed Game Automata (TGA). La traduzione in questo formalismo permettere di usare tecniche di model- checking esistenti per generare un controllore per l’applicazione robotica presa in considerazione. Per valutare PuRSUE, abbiamo preso in considerazione i seguenti punti: se PuRSUE offre un modo più compatto dei TGA per modellare un applicazione robotica, se PuRSUE supporta i designer nella generazione di controller i robot negli scenari considerati e nel ragionare su proprietà temporali e se i controller generati da PuRSUE sono efficaci se utilizzati su un robot reale. Sono state prese in considerazione alcune varianti di scenari robotici ispirati dalla letteratura, per un totale di 13 scenari totali. I risultati mostrano che (1) PuRSUE-ML offre un modo più compatto di modellare formalmente un’applicazione robotica, (2) PuRSUE è efficace nel supportare i designer nella generazione di un controllore per applicazioni robotiche e nel ragionare su proprietà temporali del sistema descritto e (3) i controller generati da PuRSUE sono efficaci quando utilizzati per comandare robot reali.