Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement

1. Enunciato del Problema

I moderni sistemi intensivi di software (ad esempio, robotica autonoma, microservizi cloud, linee di prodotti software) si affidano ai Processi Decisionali di Markov (MDP) per modellare l'incertezza e sintetizzare politiche decisionali ottimali. Tuttavia, questi sistemi soffrono spesso del problema dell'esplosione dello spazio degli stati, dove il numero di stati e transizioni diventa troppo elevato perché gli algoritmi convenzionali di sintesi delle politiche (come l'Iterazione del Valore) possano gestirlo entro limiti ragionevoli di tempo e memoria.

Strumenti standard come PRISM e Storm spesso vanno in timeout su istanze di grandi dimensioni (ad esempio, modelli con $>10^6$ stati). Le tecniche esistenti di astrazione-raffinamento (come CEGAR) sono progettate principalmente per la verifica (controllo dei limiti) piuttosto che per la sintesi delle politiche (generazione di un controller eseguibile). L'aggregazione degli stati per l'astrazione può degradare la politica risultante se stati che richiedono azioni diverse vengono fusi. Inoltre, trattare tutte le regioni di un MDP con lo stesso livello di granularità è inefficiente, poiché molte regioni (ad esempio, spazi aperti in un magazzino) potrebbero non richiedere un'analisi fine per determinare una strategia ottimale.

2. Metodologia: SHARP

Gli autori propongono SHARP (Scalable Hierarchical Adaptive Refinement for Policy synthesis), un metodo che accelera la sintesi delle politiche raffinando dinamicamente l'MDP solo dove necessario.

Flusso di Lavoro Principale

SHARP opera secondo il principio "raffina dove serve" attraverso cinque fasi iterative:

1. Partizionamento (S1): Lo spazio degli stati viene inizialmente partizionato in blocchi grezzi (ad esempio, una griglia).
2. Costruzione della Gerarchia (S2): Questi blocchi formano un albero gerarchico in cui la radice è l'intero spazio degli stati e i figli rappresentano sottoblocchi.
3. Risoluzione Locale dei Sott-MDP (S3): Ogni nodo foglia (blocco) è trattato come un sotto-MDP.
   • Le transizioni che escono dal blocco sono collegate a "stati di confine".
   • Gli stati di confine sono resi assorbenti con valori fissi derivati dal vettore globale dei valori.
   • Un risolutore locale (Iterazione del Valore) calcola i valori ottimali e una politica parziale per il blocco.
4. Propagazione dei Valori (S4): Le soluzioni locali vengono propagate verso l'alto nell'albero per aggiornare le stime globali dei valori.
5. Raffinamento Adattivo (S5): Il sistema verifica se è necessario un raffinamento.
   • Criterio: Un blocco viene raffinato se la sua dispersione dei valori (differenza tra i valori massimo e minimo all'interno del blocco) supera una soglia adattata alla profondità ($\theta$).
   • Attivatore: Se i valori di confine di un blocco cambiano significativamente (superando $\eta_{thr}$) dall'ultima risoluzione, il blocco viene risolto nuovamente.
   • Azione: I blocchi selezionati vengono suddivisi in sottoblocchi figli più piccoli e il processo si ripete.

Meccanismi Tecnici Chiave

• Sotto-MDP Indotti: Per risolvere un blocco localmente, SHARP costruisce un sotto-MDP indotto che include gli stati del blocco e i successori a un passo (stati di confine). I valori di confine sono fissati alla stima globale corrente, consentendo aggiornamenti locali di Bellman senza fondere gli stati.
• Punto Fisso Asincrono: L'algoritmo utilizza una schedulazione asincrona in cui i blocchi vengono risolti nuovamente solo quando i cambiamenti di confine sono significativi, riducendo i calcoli non necessari.
• Composizione delle Politiche: La politica globale finale è costruita componendo le politiche locali dei nodi foglia. Poiché la partizione è disgiunta, ogni stato corrisponde esattamente a una politica locale.

3. Contributi Chiave

1. Algoritmo SHARP: Un nuovo framework di raffinamento gerarchico e adattivo specificamente progettato per la sintesi delle politiche (non solo per la verifica) che evita l'aggregazione degli stati per preservare l'ottimalità della politica.
2. Garanzie Formali: Gli autori forniscono prove teoriche che dimostrano che la politica globale composta è quasi-ottimale.
   • Il residuo di Bellman globale è limitato dalla tolleranza del risolutore locale ($\epsilon$) più il massimo disallineamento di confine ($\eta$).
   • Per gli obiettivi di Percorso Stocastico più Breve (SSP) e Probabilità di Raggiungimento Massima ($P_{max}$), il limite di errore è derivato esplicitamente (ad esempio, $\|V_{fin} - V^*\|_\infty \le (\epsilon + \eta)/\alpha$).
3. Implementazione: SHARP è implementato come un'estensione open-source del model checker PRISM (Java), integrandosi con il suo motore a stati espliciti.
4. Valutazione Estensiva: Valutazione su diversi benchmark, inclusi robotica di magazzino (fino a 1 milione di stati), arene sequenziali e protocolli di rete.

4. Risultati

La valutazione confronta SHARP con i motori espliciti di PRISM (Iterazione del Valore e Gauss-Seidel).

• Prestazioni (Accelerazione):
  • Su modelli di magazzino di grandi dimensioni (griglie $1024 \times 1024$, $\approx 1$M di stati), SHARP ottiene un'accelerazione da 1,2× a 2× rispetto a PRISM.
  • Per la minimizzazione dei costi ($R_{min}$) su modelli $1024 \times 1024$, SHARP ha ridotto il tempo da ~113s (PRISM-GS) a ~65s.
  • Su configurazioni casuali di muri, SHARP ha dimostrato non solo un'esecuzione più rapida ma anche una maggiore stabilità (varianza inferiore nel tempo di esecuzione) rispetto a PRISM.
• Scalabilità: Il tempo di esecuzione di SHARP scala più favorevolmente con la dimensione del modello rispetto a PRISM. Mentre il tempo di PRISM è aumentato di ~8× passando da $512^2$ a $1024^2$ stati, il tempo di SHARP è aumentato solo di ~5×.
• Generalizzazione:
  • Modelli Spaziali/Stadiati: SHARP eccelle su modelli con struttura spaziale (magazzini) o progressione a stadi (arene sequenziali), ottenendo fino a 2× di accelerazione sul modello dell'arena con 788k stati.
  • Modelli Fortemente Accoppiati: SHARP ha performato male (più lento di 5×–100×) su modelli di protocolli fortemente accoppiati (ad esempio, FireWire, WLAN) dove le dipendenze inter-blocco sono elevate, confermando che l'overhead della gestione gerarchica supera i benefici in questi casi.
• Accuratezza: La qualità delle politiche sintetizzate è trascurabile rispetto a PRISM. La massima deviazione nel valore è stata di $1,3 \times 10^{-4}$, confermando che l'approccio gerarchico non sacrifica la qualità della soluzione.
• Overhead di Memoria: SHARP richiede più memoria (ad esempio, ~18–20 GB per 1M di stati contro ~6 GB per PRISM) a causa dell'archiviazione dell'albero gerarchico e dei dati per foglia, ma questo rimane entro i limiti dell'hardware moderno.

5. Significato

• Impatto Pratico: SHARP abilita la verifica e la sintesi di politiche per sistemi reali su larga scala (come robot di magazzino autonomi) che in precedenza erano computazionalmente intrattabili o richiedevano tempi eccessivi per la verifica.
• Trade-off Efficienza vs. Accuratezza: Bilancia con successo efficienza e accuratezza concentrandosi sulle risorse computazionali solo sulle regioni "fragili" o ad alta incertezza dello spazio degli stati, invece di trattare l'intero modello in modo uniforme.
• Guida per i Pratici: Il documento fornisce linee guida attuabili, notando che SHARP è più efficace per modelli con dipendenze trans-blocco limitate (strutture spaziali o stadiate). Fornisce consigli sulla regolazione degli iperparametri (ad esempio, l'uso di partizioni iniziali più piccole come $8\times8$ e soglie di confine conservative) per massimizzare le prestazioni.
• Fondamento Teorico: Delimitando formalmente l'errore introdotto dai disallineamenti di confine, il lavoro colma il divario tra metodi euristici gerarchici e verifica formale dei modelli probabilistici, assicurando che l'approccio "dividi e conquista" rimanga matematicamente solido.

In conclusione, SHARP rappresenta un avanzamento significativo nella verifica probabilistica dei modelli scalabile, offrendo una soluzione robusta per la sintesi delle politiche in MDP di grandi dimensioni dove i risolutori piatti tradizionali non riescono a scalare.