Real-Time Model Checking for Closed-Loop Robot Reactive Planning

Definizione del Problema
I metodi di evitamento reattivo degli ostacoli, come quelli utilizzati nei veicoli Braithead o nei robot per la pulizia commerciale, spesso si basano su un ragionamento a singolo step (stimolo-risposta). Sebbene efficaci per riflessi semplici, questi metodi causano frequentemente l'intrappolamento degli agenti in minimi locali, in particolare all'interno di ambienti concavi come angoli o vicoli ciechi. Ciò accade perché l'agente non è in grado di prevedere le conseguenze delle sue azioni immediate sugli stati futuri. In contesti critici per la missione, come l'esplorazione spaziale remota o la guida autonoma, questa limitazione può portare a fallimenti catastrofici. Inoltre, i popolari metodi di IA "black-box" come il Deep Reinforcement Learning (DRL) mancano spesso di trasparenza e si affidano a generalizzazioni rigide che possono fallire in ambienti non strutturati e imprevisti. Sebbene il Model Checking (MC) sia una tecnica robusta per la verifica di sistemi critici per la sicurezza, la sua applicazione alla pianificazione in tempo reale su robot fisici è stata limitata dagli elevati costi computazionali, dai ritardi di compilazione e dal problema dell' "esplosione dello spazio degli stati". I tenti esistenti di MC in tempo reale si affidano spesso a strumenti standard (ad esempio, SPIN) che introducono latenze inaccettabili (secondi) per la navigazione ad alta velocità.

Metodologia
Gli autori propongono un algoritmo di model checking su misura, semplificato e integrato direttamente nel codice del robot, per consentire una pianificazione reattiva multi-step in tempo reale. L'approccio si basa sul concetto biologico di "vicarious trial and error" (tentativo ed errore vicario), in cui un agente simula azioni future per prevederne gli esiti.

• Architettura e Astrazione: Il sistema utilizza una prospettiva egocentrica, trattando gli ostacoli come "disturbi" che interrompono un'azione predefinita preferita (andare dritto). Invece di mantenere una mappa globale, il robot costruisce istantanee astratte temporanee del suo ambiente immediato. Queste istantanee si concentrano strettamente sulle relazioni spaziali rilevanti per evitare l'esplosione dello spazio degli stati.
• Sistema di Transizione Focalizzato sui Disturbi (DTS): Il nucleo del metodo è un sistema di transizione finito con 15 stati che rappresentano possibili configurazioni future rispetto al frame locale del robot. Gli stati codificano la conoscenza "core" sull'evoluzione temporale di compiti a ciclo chiuso (ad esempio, ruotare a sinistra/destra, andare dritto). Il sistema modella sequenze di compiti (piani a 2, 3 e 4 step) per determinare se un robot possa tornare in sicurezza al proprio stato predefinito dopo aver evitato un disturbo.
• Pianificazione basata su LTL: Invece di verificare un sistema rispetto a una proprietà, gli autori utilizzano una proprietà di percorso di Logica Temporale Lineare (LTL) negata. Definiscono una proprietà $\varphi = \neg(\text{safe} \mathcal{U} (\text{safe} \land \text{horizon}))$. Cercando contro-esempi a questa proprietà negata, il model checker genera "percorsi di soluzione" validi (sequenze sicure di compiti) che portano a uno stato in cui il robot può guidare indefinitamente senza disturbi.
• Esecuzione Runtime: L'algoritmo viene eseguito su hardware a bassa potenza (ad esempio, Raspberry Pi 3). Utilizza una ricerca in profondità in avanti (f-DFS) sul prodotto del sistema di transizione e di un Automa a Stati Finiti Non Deterministico (NFA) derivato dalla proprietà LTL. Il sistema privilegia piani più brevi (2 step) e si espande solo a piani a 3 o 4 step se le sequenze più brevi sono ritenute insicure (ad esempio, se il robot è "incastrato" da ostacoli su entrambi i lati).

Contributi Chiave

1. Algoritmo di Model Checking Su Misura: Sviluppo di un algoritmo di model checking leggero e personalizzato, progettato specificamente per l'esecuzione in tempo reale su dispositivi con risorse limitate, evitando l'overhead dei checker general-purpose.
2. Integrazione Diretta: Integrazione riuscita del model checker direttamente nel loop di controllo del robot (C++), eliminando i ritardi di pre-compilazione e consentendo prestazioni hard real-time.
3. Mitigazione dello Spazio degli Stati: Una strategia di astrazione innovativa che utilizza istantanee ambientali temporanee e un rigoroso focus attentivo sui disturbi per prevenire l'esplosione dello spazio degli stati.
4. Pianificazione tramite Contro-Esempi: Utilizzo di proprietà LTL negate per generare piani di evitamento ostacoli multi-step come contro-esempi, contrastando con gli approcci di verifica tradizionali.
5. Validazione Empirica: Dimostrazione dell'approccio su un robot fisico in ambienti non strutturati, mostrando prestazioni superiori rispetto ai baseline reattivi a singolo step.

Risultati
Gli autori hanno valutato il loro metodo rispetto a un controller reattivo di base in due scenari: un vicolo cieco e un ambiente playground con un ostacolo isolato.

• Scenario Cul-de-sac (Quantitativo): In uno studio di 90 corse, l'approccio di model checking ha generato traiettorie significativamente più brevi (confronto del rango mediano, $p < .001$) e ha prodotto zero collisioni, mentre il metodo di base ha subito 3 collisioni e si è spesso incagliato. La latenza di elaborazione per l'approccio di model checking è variata da 5,58 ms a 18,76 ms (media ~10,1 ms), ampiamente entro il limite di 100 ms del tempo reale. L'uso della memoria è stato minimo (372 byte per il checker stesso).
• Scenario Playground (Qualitativo): Nei test di movimento libero, il metodo di base ha rivisitato ripetutamente e si è incagliato nel vicolo cieco (per un totale di 89–168 secondi di intrappolamento tra le varie corse) e ha causato 6 collisioni. L'approccio di model checking ha evitato con successo il vicolo cieco, con zero collisioni e zero tempo trascorso intrappolato.
• Validazione Cross-Platform: Il metodo è stato testato con successo su una seconda piattaforma robotica (Radxa Rock 5B) con hardware LiDAR differente, confermando la sua portabilità.
• Garanzie Teoriche: Gli autori forniscono prove informali che dimostrano come, sotto ipotesi di ambiente statico e rumore sensoriale limitato, il metodo impedisca strutturalmente al robot di alternare indefinitamente tra rotazioni a sinistra e destra (incagliandosi in un angolo) e assicuri che i disturbi non entrino nella zona sicura definita durante l'esecuzione del moto rettilineo.

Significatività e Rivendicazioni
Il documento sostiene che questo approccio offre un "sostituto diretto" per l'evitamento reattivo degli ostacoli puramente basato su reazioni in applicazioni critiche per la sicurezza come i veicoli autonomi e i robot mobili. A differenza del DRL, che si affida a un addestramento opaco e intensivo di dati e fatica con gli ambienti non strutturati, questo metodo fornisce un processo di ragionamento spiegabile e basato su regole che simula gli esiti futuri sulla base dell'input sensoriale immediato. Gli autori sottolineano che il loro metodo raggiunge vincoli hard real-time su hardware a bassa potenza, rendendolo efficiente dal punto di vista energetico e adatto alla distribuzione dove non è disponibile hardware accelerato costoso. Sebbene l'implementazione attuale si concentri sull'evitamento locale degli ostacoli piuttosto che sulla navigazione orientata a un obiettivo, gli autori la pongono come un passo fondamentale verso l'integrazione della verifica formale con la decomposizione gerarchica per una navigazione autonoma sicura, affidabile e trasparente.