Leveraging automata learning for strategy synthesis in socially-aware autonomous systems

Emergency response efficiency is a critical factor in reducing casualties during large-scale evacuations. This thesis explores the integration of socially-aware autonomous systems with formal verification techniques to enhance search and rescue (SAR) operations. The study builds upon the FormIDEAble framework, refining its decision-making model through the use of automata learning and strategy synthesis. By leveraging Priced Timed Markov Decision Processes (PTMDPs) and agent-based simulations in NetLogo, the research aims to optimize the role of SAR robots in coordinating evacuations. A core focus of this work is the adaptive-support strategy, designed to dynamically assess the willingness of zero responders (untrained civilians) to assist victims, thereby reducing reliance on first responders. Experimental results obtained through extensive simulations highlight the potential and limitations of this approach. The comparative analysis with existing evacuation strategies, including the original FormIDEAble model, reveals that while the adaptive-support strategy improves flexibility, it does not always lead to better evacuation times due to suboptimal decision-making in responder engagement. Findings suggest that refinements in decision logic, machine learning integration, and enhanced real-world validation are necessary for further improving SAR efficiency. Future directions include hybrid evacuation strategies, improved environmental awareness, and human-robot cooperation frameworks to maximize emergency response effectiveness.

L'efficienza nella gestione delle emergenze è un fattore cruciale per ridurre il numero di vittime durante evacuazioni su larga scala. Questa tesi esplora l’integrazione di sistemi autonomi socialmente consapevoli con tecniche di verifica formale per migliorare le operazioni di ricerca e soccorso (SAR). Lo studio si basa sul framework FormIDEAble, affinando il suo modello decisionale attraverso l’uso di apprendimento automatico degli automi e sintesi strategica. Grazie all’utilizzo di Priced Timed Markov Decision Processes (PTMDPs) e simulazioni ad agenti in NetLogo, la ricerca mira a ottimizzare il ruolo dei robot SAR nel coordinamento delle evacuazioni. Il cuore di questo lavoro è l’adaptive-support strategy, una strategia progettata per valutare dinamicamente la disponibilità dei zero responders (civili non addestrati) ad assistere le vittime, riducendo così la dipendenza dai soccorritori professionisti. I risultati sperimentali, ottenuti attraverso simulazioni su larga scala, mettono in evidenza sia il potenziale che i limiti di questa strategia. L’analisi comparativa con le strategie di evacuazione preesistenti, incluso il modello FormIDEAble originale, mostra che, sebbene l’adaptive-support strategy migliori la flessibilità decisionale, non sempre garantisce tempi di evacuazione inferiori a causa di scelte subottimali nell’assegnazione degli aiuti. I risultati suggeriscono la necessità di affinare la logica decisionale, integrare tecniche di apprendimento automatico e convalidare il modello in scenari reali per migliorare l’efficacia dei sistemi SAR. Le direzioni future includono lo sviluppo di strategie di evacuazione ibride, un miglioramento della consapevolezza ambientale e l’integrazione di modelli avanzati di cooperazione uomo-robot per massimizzare l’efficacia degli interventi di emergenza.