Generating Local Shields for Decentralised Partially Observable Markov Decision Processes

1. Il Problema

I sistemi multi-agente operanti in ambienti con osservazione parziale (Dec-POMDP - Decentralised Partially Observable Markov Decision Processes) e senza comunicazione affrontano sfide critiche per la sicurezza. Il problema fondamentale risiede nel fatto che l'azione locale di un singolo agente non determina univocamente l'azione congiunta risultante. Di conseguenza, garantire che ogni agente selezioni un'azione concreta che sia sicura (evitando collisioni, deadlock o livelock) è estremamente complesso.

Le tecniche di shielding (schermatura) esistenti, che filtrano le azioni basandosi sullo stato corrente, presentano limitazioni significative in questo contesto:

• Assumono spesso l'accesso a uno stato globale centralizzato condiviso.
• Utilizzano filtri locali senza memoria (memoryless), incapaci di considerare la storia delle interazioni.
• Si basano su costruzioni rigide (es. DFA da specifiche LTL) che non catturano la complessità informativa introdotta dall'osservazione parziale.

2. Metodologia

Gli autori propongono una pipeline completa che parte da una specifica formale e genera shield locali eseguibili senza comunicazione tra agenti.

A. Algebra dei Processi di Shield (Shield Process Algebra)

Viene introdotta un'algebra dei processi compatta con scelta protetta (guarded choice) e ricorsione per specificare il comportamento globale sicuro. La grammatica include:

• idle / fail: terminazione riuscita o fallita.
• µX.P: ricorsione (assunta protetta).
• Sh.P: continuazione che asserisce che il prossimo stato globale deve appartenere all'insieme sicuro Sh, continuando poi con P.
• P1 ∥g P2: scelta protetta; il processo si comporta come P1 se lo stato corrente s è in g, altrimenti come P2.

B. Pipeline di Compilazione

Il processo di compilazione trasforma la specifica dell'algebra in shield locali attraverso tre fasi principali:

1. Automata del Processo di Shield: La specifica dell'algebra viene tradotta in un automa deterministico che interpreta il processo di shield.
2. Macchina di Mealy Globale (Global Shield Mealy Machine):
   • Viene costruita una macchina di Mealy globale che prende in input lo stato del Dec-POMDP.
   • Gli stati della macchina globale combinano l'insieme degli stati Dec-POMDP raggiungibili con lo stato corrente dell'automa del processo.
   • L'output è una rappresentazione decentralizzata degli insiemi di azioni congiunte sicure.
   • Viene applicata una decomposizione deterministica (Dec) per trasformare un insieme di azioni congiunte in insiemi di azioni locali sicuri per ogni agente, garantendo che la scelta indipendente di un'azione da parte di ogni agente porti a un'azione congiunta sicura.
3. Macchine di Mealy Locali (Local Shield Mealy Machines):
   • Per ogni agente, la macchina globale viene proiettata in una macchina locale.
   • Gli stati locali sono sottoinsiemi di credenza (belief-style subsets) degli stati della macchina globale coerenti con l'osservazione parziale dell'agente.
   • L'output locale è l'intersezione degli output delle macchine globali corrispondenti agli stati nella credenza corrente. Se l'intersezione è vuota (o tutti gli stati sono fail), l'output è ⊥ (fallimento dello shield).

C. Implementazione e Analisi

• La pipeline è implementata in Rust.
• Viene integrata con PRISM (Probabilistic Symbolic Model Checker) per calcolare le probabilità di sicurezza (migliore e peggiore caso) indipendentemente dalla politica degli agenti, senza fissare una strategia specifica.

3. Contributi Chiave

1. Algebra dei Processi di Shield: Una nuova algebra con ricorsione e scelta protetta specifica per ambienti decentralizzati, parzialmente osservabili e privi di comunicazione.
2. Pipeline di Compilazione: Un metodo sistematico che, data una specifica di processo, genera automi, macchine di Mealy globali e le proietta in macchine di Mealy locali eseguibili basate su osservazioni parziali.
3. Implementazione e Verifica: Un'implementazione in Rust con integrazione PRISM che permette di analizzare le probabilità di fallimento dello shield e di raggiungere stati non sicuri senza dover definire una politica a priori.

4. Risultati

Lo studio di caso si basa su un problema di Multi-Agent Path Finding (MAPF) su griglie, confrontando diverse specifiche di shield (P1 e P2) rispetto a una baseline non schermata e a politiche casuali o apprese (Q-learning).

• Sicurezza: Tutti gli shield proposti eliminano completamente le collisioni (conflitti sui vertici) in tutte le configurazioni testate, a differenza della baseline non schermata che mostra tassi di collisione elevati.
• Performance (Raggiungimento Target):
  • Lo shield P2 (meno conservativo, basato su una struttura di ramificazione che minimizza la perdita di azioni) dimostra prestazioni superiori rispetto a P1 (conservativo, che tende a mantenere gli agenti fermi).
  • P2 permette agli agenti di esplorare più stati e raggiungere i target con successo in una percentuale molto più alta di casi, pur mantenendo la sicurezza.
• Impatto dell'Osservazione: Un raggio di osservazione (R) più grande migliora le prestazioni di P2, riducendo i fallimenti dello shield (shield failure) grazie a aggiornamenti di credenza più precisi.
• Apprendimento (Q-learning): Quando combinati con agenti che apprendono (Q-learning), gli shield garantiscono zero collisioni durante tutto l'addestramento. La combinazione "Qreach + P2" ottiene il miglior compromesso tra sicurezza e successo nel raggiungimento dell'obiettivo.

5. Significato e Implicazioni

Questo lavoro è significativo perché risolve il problema della sicurezza nei sistemi multi-agente decentralizzati senza richiedere comunicazione o uno stato globale condiviso, che sono spesso irrealistici in scenari reali.

• Generalità: La metodologia non è limitata al MAPF, ma si applica a qualsiasi Dec-POMDP privo di comunicazione dove le condizioni di sicurezza possono essere rappresentate tramite stati e contatori finiti.
• Flessibilità: L'uso di un'algebra dei processi permette di specificare comportamenti sicuri complessi e ricorsivi, superando la rigidità degli approcci basati su DFA tradizionali.
• Robustezza: L'integrazione con PRISM fornisce garanzie probabilistiche formali sulla sicurezza, indipendentemente dalla politica di controllo scelta dagli agenti.

In sintesi, il paper offre un framework teorico e pratico per generare shield locali "intelligenti" che bilanciano sicurezza e libertà di azione in ambienti complessi e parzialmente osservabili.