Riepilogo Tecnico: dtControl2+ε: Ottimalità del Trading per l'Esplicabilità negli MDP tramite Alberi di Decisione

Definizione del Problema

La sintesi di controller per i Processi Decisionali di Markov (MDP) produce spesso controller ottimali rappresentati come grandi tabelle stato-azione non strutturate. Sebbene queste tabelle siano matematicamente precise, sono impraticabili per l'implementazione su dispositivi con risorse limitate e mancano di esplicabilità, ostacolando la validazione e la certificazione. Strumenti esistenti, come dtControl2, tentano di rappresentare questi controller come Alberi di Decisione (DT) per migliorarne l'interpretabilità. Tuttavia, anche questi DT possono diventare troppo complessi per la comprensione umana quando si tratta di sistemi di grandi dimensioni o con molti casi limite.

Una sfida critica è che la riduzione della dimensione di un DT non è banale; rimuovere una singola decisione cruciale può rendere un controller errato. Inoltre, molti metodi di sintesi scalabili forniscono solo controller $\epsilon$-ottimali (prestazioni entro $\epsilon$ dal valore ottimale), mentre gli strumenti di costruzione DT esistenti mirano tipicamente a una rappresentazione esatta ($\epsilon=0$), non riuscendo a sfruttare l'imprecisione consentita per semplificare la spiegazione.

Metodologia

Il documento presenta dtControl2+ε, uno strumento che estende lo stato dell'arte dtControl2 introducendo una funzionalità "$\epsilon$". Il flusso di lavoro principale si integra strettamente con il model checker probabilistico Storm per costruire DT più piccoli ed esplicabili, garantendo al contempo che il controller risultante rimanga $\epsilon$-ottimale.

La metodologia procede in tre fasi:

1. Risoluzione del Modello e Costruzione del Dataset

Invece di partire da un controller ottimale deterministico, lo strumento genera un dataset iniziale che è permissivo (mappa gli stati a insiemi di azioni consentite) o combinato (restringe le azioni permissive agli stati raggiungibili).

• Strategie Permissive: Lo strumento identifica le azioni che sono ottimali o che producono lo stesso valore, permettendo al DT di "unificare" gli stati.
• Euristiche di Riduzione: Prima di apprendere il DT, lo strumento identifica e rimuove gli stati in cui la scelta specifica dell'azione non influisce sul risultato o in cui l'errore introdotto è limitato da $\epsilon$. Le principali tecniche di riduzione includono:
  • AllOpt: Rimozione degli stati in cui tutte le azioni disponibili sono ottimali.
  • Agency: Rimozione degli stati in cui la differenza tra il miglior e il peggior risultato possibile è inferiore a $\epsilon$.
  • Dominance: Rimozione degli stati raggiunti quasi certamente da altri stati indipendentemente dalla scelta effettuata.
  • Unreach: Rimozione degli stati non raggiungibili dallo stato iniziale sotto qualsiasi controller coerente.

2. Apprendimento dell'Albero di Decisione

Lo strumento impiega una versione modificata dello standard algoritmo di costruzione DT basato su euristiche (Algoritmo 1) con diversi miglioramenti:

• Estrazione dei Predicati: Estrae automaticamente i predicati rilevanti dalla descrizione del modello ad alto livello (es. guardie di transizione del linguaggio PRISM), migliorando l'approccio a template semi-automatico degli strumenti precedenti.
• Misure di Impurità: Introduce pesature specifiche del modello per il calcolo dell'impurità. Invece di una pesatura uniforme, utilizza:
  • Imp_Simulation: Pesa gli stati in base alla frequenza di visita (con un limite minimo di sicurezza per garantire l'$\epsilon$-ottimalità).
  • Imp_Agency: Pesa gli stati in base alla loro agency (potenziale errore).
  • Imp_CoE (Cost of Error): Pesa l'impatto della scelta della peggiore azione in quel determinato stato.
• Euristiche Aggressive con Verifica: Lo strumento utilizza l'Early-Stopping (termina le divisioni quando l'impurità è sotto una soglia) e il Greedy Pruning (collassa i sottotopologie). A differenza di altri approcci "aggressivi" che rischiavano la correttezza, dtControl2+ε usa Storm per verificare l'$\epsilon$-ottimalità del DT risultante dopo questi passaggi. Se il vincolo di precisione viene violato, lo strumento allenta le euristiche e riprova.

3. Ciclo di Verifica

Una caratteristica unica è il forte accoppiamento con Storm per la verifica post-costruzione. Lo strumento controlla la precisione del DT generato. Se la deviazione dal valore ottimale supera $\epsilon$, effettua un backtracking e riduce l'aggressività delle euristiche (ad esempio, aumentando la soglia di arresto o disabilitando il pruning), assicurando che l'output finale sia garantito come $\epsilon$-ottimale.

Contributi Chiave

1. Lo Strumento dtControl2+ε: Uno strumento autonomo che estende dtControl2 per costruire DT più piccoli sfruttando l'imprecisione consentita $\epsilon$.
2. Euristiche Safe vs. Aggressive: Un framework che separa chiaramente le riduzioni "safe" (che preservano l'$\epsilon$-ottimalità per definizione) dalle euristiche "aggressive" (che sono validate tramite model checking).
3. Estrazione Automatica dei Predicati: Un metodo per derivare i predicati decisionali direttamente dalle guardie di transizione del modello, eliminando la necessità di competenza manuale nella selezione dei predicati.
   {% end-block %}
4. Supporto per Diversi Obiettivi: L'approccio copre obiettivi standard (raggiungibilità, sicurezza, reach-avoid, basati su reward) e, unicamente, supporta le proprietà LTL (Linear Temporal Logic) gestendo i controller basati sulla memoria.

Risultati

Gli autori hanno valutato dtControl2+ε rispetto a dtControl2, dtPaynt, dtNESt e una reimplementazione dell'approccio CAV15 su 38 benchmark (inclusi modelli PRISM con fino a 500.000 stati).

• Riduzione delle Dimensioni: Anche per la rappresentazione esatta ($\epsilon=0$), dtControl2+ε produce DT ordini di grandezza più piccoli di dtControl2 grazie a dataset iniziali migliori e a euristiche sicure.
• Impatto di $\epsilon$: Quando viene consentito $\epsilon = 10^{-2}$, lo strumento ha prodotto DT a singolo nodo per quasi la metà dei benchmark, rivelando che un'unica azione (con un fallback casuale uniforme) è spesso sufficiente per l'$\epsilon$-ottimalità.
• Confronto:
  • vs. dtControl2: dtControl2+ε produce costantemente alberi più piccoli.
  • vs. dtPaynt: dtPaynt è andato in timeout nella maggior parte dei benchmark e ha prodotto alberi più grandi dove ha avuto successo.
  • vs. dtNESt: dtNESt è un forte concorrente per $\epsilon=0$, ma dtControl2+ε produce alberi al massimo della metà delle dimensioni di dtNESt in 23 di 38 benchmark e di un ordine di grandezza inferiore in 10. Notevolmente, dtNESt spesso fallisce o produce alberi più grandi quando $\epsilon > 0$, mentre dtControl2+ε eccelle nello sfruttare l'imprecisione.
• Scalabilità: Lo strumento ha risolto tutti i benchmark tranne uno entro un timeout di 20 minuti, dimostrando la fattibilità su modelli grandi e complessi.

Significato

Il documento afferma che dtControl2+ε rappresenta un significativo avanzamento nello stato dell'arte della sintesi di controller esplicabili. Scambiando una quantità controllabile di ottimalità con la compattezza, lo strumento consente la generazione di controller comprensibili dall'uomo che prima erano troppo complessi da interpretare. La capacità di derivare automaticamente intuizioni strutturali (ad esempio, identificare che una singola regola è sufficiente per l'$\epsilon$-ottimalità) e di supportare le proprietà LTL distingue questo strumento dagli altri. Gli autori sottolineano che il loro approccio fornisce garanzie di $\epsilon$-ottimalità, a differenza dei precedenti metodi di pruning basati su euristiche che potevano compromettere la correttezza.