Riepilogo Tecnico: Verifica Statistica Multi-Obiettivo mediante Campionamento di Strategie Leggere

Problema

La Verifica Statistica del Modello (SMC - Statistical Model Checking) è una tecnica consolidata per la verifica di sistemi probabilistici con spazi di stato ampi, dove la Verifica Probabilistica del Modello (PMC - Probabilistic Model Checking) esaustiva fallisce a causa dell'esplosione dello spazio degli stati. Tuttavia, gli approcci SMC esistenti sono limitati alla valutazione di proprietà singole alla volta. In molti scenari pratici, come il bilanciamento tra l'uso della batteria di un satellite e l'utilità o l'ottimizzazione del costo di una pompa di calore rispetto al comfort, i decisori richiedono il fronte di Pareto: l'insieme dei trade-off ottimali tra più obiettivi, spesso contrastanti.

Sebbene esistano algoritmi PMC multi-obiettivo (ad esempio, utilizzando la programmazione lineare o l'iterazione di valore), essi richiedono l'esplorazione completa dello spazio degli stati, rendendoli inapplicabili a modelli con miliardi di stati o spazi di obiettivi ad alta dimensionalità. Inoltre, strumenti esistenti come Uppaal Stratego gestiscono i problemi multi-obiettivo solo tramite ordinamento lessicografico o ottimizzazione monodimensionale, fallendo nel catturare i trade-off tra obiettivi di pari priorità. Attualmente non esiste un approccio SMC capace di calcolare i fronti di Pareto per query multi-obiettivo mantenendo al contempo l'impronta di memoria costante caratteristica della SMC.

Metodologia

Il documento propone il primo approccio SMC per query di Pareto multi-obiettivo, basato sul Campionamento di Strategie Leggere (LSS - Lightweight Strategy Sampling). La metodologia principale si compone dei seguenti elementi:

1. Campionamento di Strategie Leggere (LSS)

Per gestire l'indeterminismo nei Processi Decisionali di Markov (MDP) senza memorizzare informazioni sulla strategia per ogni stato, gli autori utilizzano la LSS. Inveve di memorizzare esplicitamente una strategia, la LSS utilizza un identificatore compatto (ad esempio, un intero a 32 bit) e una funzione hash per risolvere deterministicamente le scelte non deterministiche durante la simulazione. Ciò consente la simulazione di un numero vastissimo di strategie distinte utilizzando una memoria costante, indipendentemente dalla dimensione dello spazio degli stati del modello.

2. Approssimazione Statistica del Fronte di Pareto

L'approccio campiona strategie deterministiche e le valuta tramite SMC per ottenere intervalli di confidenza (CI - Confidence Intervals) per ogni obiettivo.

• Scatole di Confidenza (Confidence Boxes): Per una strategia $\sigma$ campionata, la SMC produce una scatola di confidenza $d$-dimensionale $B_\sigma$ attorno al vettore di media stimato $\hat{x}_\sigma$.
• Sottoapprossimazione e Sovraapprossimazione: L'inviluppo convesso degli angoli "più pessimistici" di queste scatole forma una sottoapprossimazione ($\underline{C}$) candidata dell'insieme raggiungibile. Al contrario, gli angoli "più ottimistici" formano una sovraapprossimazione ($\overline{C}$) candidata.
• Confronti Multipli: Per garantire la correttezza simultanea di tutte le scatole di confidenza con una probabilità $\gamma$, gli autori applicano la correzione di Bonferroni (unione di eventi) per distribuire il budget di errore tra le strategie e le dimensioni.

3. Algoritmi

Il documento introduce due categorie di algoritmi:

A. Campionamento Incrementale con Convergenza
Questo schema campiona in modo indefinito batch di strategie. Regola dinamicamente il budget di errore per batch (usando un fattore $f$) per garantire che, nel limite, le sotto e sovraapprossimazioni convergano a una banda di confidenza simultanea attorno al vero fronte di Pareto. Ciò fornisce una garanzia teorica di convergenza quasi certa dato un LSS ideale.

B. Campionamento a Budget Fisso
Riconoscendo che le applicazioni pratiche hanno tempi finiti, vengono proposti tre algoritmi euristici per trovare la migliore approssimazione entro un budget di simulazione fisso:

1. Raffinamento del Vettore di Peso (WVR - Weight Vector Refinement): Adatta le tecniche PMC multi-obiettivo attraverso la scalarizzazione lineare degli obiettivi. Raffina iterativamente i vettori di peso in base alla distanza tra le attuali approssimazioni e scarta le strategie subottimali.
2. Budget di Iterazione Fisso (FIB - Fixed Iteration Budget): Campiona un set iniziale di strategie ed esegue iterativamente sessioni di simulazione, scartando le strategie con prestazioni peggiori in ogni iterazione per concentrare il budget sui candidati promettenti.
3. Budget di Strategia Fisso (FSB - Fixed Strategy Budget): Simile a FIB, ma assicura che il set finale di strategie superstiti riceva un numero uniforme di sessioni di simulazione, sostituendo le strategie scartate con nuove strategie campionate.

Euristiche di Selezione della Strategia:
Per filtrare le strategie, gli autori definiscono diverse regole basate sulle medie campionarie e sugli intervalli di confidenza (ad esempio, "Simple", "Far Enough", "Conservatively Far"). Queste regole determinano se una strategia è dominata da un'altra con sufficiente confidenza statistica per essere scartata.

Contributi Chiave

1. Primo SMC Multi-Obiettivo: Il documento presenta il primo framework SMC capace di approssimare i fronti di Pareto per $d$ obiettivi di pari priorità.
2. Memoria Costante: L'approccio mantiene il vantaggio principale della SMC: l'uso della memoria è costante rispetto alla dimensione dello spazio degli stati del modello, consentendo l'analisi di modelli con miliardi di stati.
3. Garanzie Statistiche: Lo schema incrementale fornisce una garanzia teorica di convergenza verso una banda di confidenza attorno al vero fronte di Pareto. Gli algoritmi a budget fisso fornis드로 limiti inferiori statisticamente solidi (sottoapprossimazioni) con un livello di confidenza specificato.
4. Implementazione e Valutazione: Le tecniche sono implementate nel simulatore modes all'interno del Modest Toolset. Gli autori valutano l'approccio su 40 istanze benchmark dalla letteratura della verifica quantitativa e dell'apprendimento per rinforzo, confrontando i risultati con lo strumento PMC Storm.

Risultati Sperimentali

Gli esperimenti dimostrano che il proposto approccio SMC può gestire istanze in cui gli strumenti PMC (Storm) falliscono a causa dell'esplosione dello spazio degli stati o del timeout.

• Scalabilità: Per modelli grandi (ad esempio, fruit_tree con $2.7 \times 10^9$ stati, varianti di puddle_world con centinaia di milioni di stati), l'approccio SMC calcola con successo approssimazioni del fronte di Pareto in secondi o minuti, mentre gli strumenti PMC sono andati in timeout o non sono riusciti a completare l'esecuzione.
• Accuratezza: Per modelli più piccoli dove i risultati PMC sono disponibili, le approssimazioni SMC corrispondono spesso da vicino al vero fronte di Pareto (ad esempio, i modelli deep_sea e fruit_tree con $\epsilon$ moltiplicativo vicino a 1). Tuttavia, l'accuratezza varia; per alcuni modelli come breakable_bottles, l'approssimazione può essere più distante dal fronte reale, evidenziando la natura stocastica del campionamento.
• Prestazioni degli Algoritmi: Tra gli algoritmi a budget fisso, FSB (Fixed Strategy Budget) combinato con l'euristica Simple e una configurazione che favorisce un alto numero di strategie iniziali con meno sessioni per strategia, ha generalmente prodotto i migliori risultati in termini di ipervolume.
• Impatto delle Euristiche: La regola "Simple" (scartare le strategie basandosi puramente sulle medie campionarie) ha spesso performato meglio, suggerendo che lo scarto precoce delle strategie non promettenti sia benefico nel set di benchmark testato.

Significato e Rivendicazioni

Gli autori affermano che questo lavoro colma una lacuna critica tra la scalabilità della SMC e la complessità dell'ottimizzazione multi-obiettivo. Sfruttando il campionamento di strategie leggere, l'approccio consente la verifica dei trade-off in sistemi che sarebbero altrimenti intrattabili per i metodi esaustivi.

Il documento riconosce modestamente alcuni limiti:

• Sovraapprossimazione: Sebbene lo schema incrementale converga verso una banda di confidenza, gli algoritmi a budget fisso non possono garantire una sovraapprossimazione valida in tempo finito perché potrebbero mancare completamente la strategia ottimale.
• Spazio delle Strategie: Il metodo assume uno spazio di strategie finito (tramite identificatori di dimensione fissa). Sebbene pratico, questo è un limite rispetto allo spazio teorico infinito di strategie nei modelli MDP generali.
• Classe di Modelli: Sebbene dimostrato sugli MDP, l'approccio è direttamente applicabile a qualsiasi classe di modelli supportata dalla LSS, come gli automi di Markov e gli automi temporizzati probabilistici, a condizione che le esecuzioni terminino quasi certamente.

Il lavoro è presentato come un passo fondamentale, offendo uno strumento pratico per la verifica multi-obiettivo in sistemi su larga scala dove i metodi esaustivi tradizionali non sono disponibili.