Riepilogo Tecnico: Scalabilità della Pianificazione Consapevole delle Osservazioni in Domini Incerti

Definizione del Problema

Il documento affronta il Problema dell'Osservabilità Ottimale (OOP) nel contesto dei Processi Decisionali di Markov Parzialmente Osservabili (POMDP). La sfida ingegneristica fondamentale consiste nel determinare quali capacità di rilevamento (osservazioni) implementare su un agente in domini incerti per garantire che un compito sia realizzabile senza incorrere in costi hardware o di elaborazione proibitivi.

Formalmente, dato un Processo Decisionale di Markov (MDP) sottostante $M$, un budget $B$ e una soglia di ricompensa $\tau$, l'OOP chiede se esista una funzione di osservazione $obs$ (che mappa gli stati in un insieme di osservazioni con cardinalità $\le B$) tale che la ricompensa attesa minima del POMDP risultante sia $\le \tau$.

Sebbene l'OOP generale sia indecidibile, il documento si concentra su due frammenti decidibili:

1. Problema di Selezione dei Sensori (SSP): Una variante in cui le osservazioni sono binarie (acceso/spento) per sensori di posizione specifici.
2. Problema di Osservabilità Posizionale (POP): Una variante che considera strategie posizionali (le azioni dipendono solo dall'osservazione corrente, non dalla cronologia).

Lavori precedenti di Konsta et al. [19] hanno formalizzato questi problemi e li hanno ridotti a Catene di Markov Parametriche Tipizzate (tpMC), risolvendoli tramite sintesi dei parametri basata su SMT. Tuttavia, questo approccio fatica a scalare verso dimensioni di istanza più grandi.

Metodologia

Gli autori propongono un approccio a due fronti per scalare la soluzione dei frammenti OOP:

1. Miglioramenti alla Sintesi dei Parametri Basata su SMT

Costruendo sulla riduzione tpMC di [19], gli autori affinano la codifica SMT per migliorare le prestazioni del risolutore (in particolare utilizzando Z3):

• Codifica Booleana Nativa: Invece di utilizzare parametri a valore reale vincolati a $\{0,1\}$, gli autori li sostituiscono con variabili booleane native. Questo sfrutta la propagazione SAT e riduce l'overhead dell'aritmetica non lineare.
• Rilassamenti dei Vincoli:
  • Riparazione del Budget: Un approccio in due fasi "rilassa-e-ripara" in cui il risolutore trova prima una soluzione ignorando il vincolo di budget, quindi tenta di raffinarla per soddisfare il budget.
  • Limite Superiore Invariante: Sostituzione delle equazioni di Bellman esatte con disuguaglianze ($v_s \ge \text{Bellman}(v_s)$). Questo cerca una sovrastima conservativa della ricompensa attesa, sufficiente per i controlli di fattibilità dove la soglia $\tau$ non è necessariamente il minimo ottimale.
• Ordinamento delle Asserzioni: I test empirici hanno rivelato che l'ordine delle asserzioni SMT influisce significativamente sulle prestazioni; gli autori hanno identificato un ordinamento ottimale che domina altre permutazioni.

2. Decomposizione Basata su Euristiche tramite Oracoli POMDP

Riconoscendo che risolvere la codifica tpMC completa per ogni funzione di osservazione candidata è inefficiente, gli autori introducono un paradigma di decomposizione. Invece di risolvere direttamente il problema di ottimizzazione globale, esplorano lo spazio delle funzioni di osservazione utilizzando "oracoli" per valutare i candidati.

• Oracoli: Il documento utilizza due tipi di oracoli per valutare una funzione di osservazione candidata:
  1. Oracolo SMT: Una codifica tpMC semplificata in cui le variabili di osservazione sono fissate, riducendo la complessità.
  2. Oracolo PMC: Integrazione con il model checker probabilistico Storm per valutare le ricompense attese.
• Gruppi di Distinguibilità Atomica: Gli autori definiscono relazioni di equivalenza tra stati basate sulle loro "firme ottimali" (l'insieme delle azioni ottimali nell'MDP sottostante). Stati con firme ottimali identiche formano gruppi di distinguibilità atomica.
• Algoritmo AG (Enumerazione Euristiche):
  • L'algoritmo partiziona l'insieme dei gruppi di distinguibilità atomica in classi di osservazione.
  • Impiega un'euristica di classificazione basata su punteggi di equivalenza (quanti stati in una classe condividono un'azione ottimale comune) e vincoli di strategia (quante probabilità di azione possono essere fissate a 0 o 1).
  • L'algoritmo valuta i candidati in ordine decrescente di promessa. Se un candidato soddisfa la soglia, restituisce la soluzione; altrimenti, procede al successivo.
  • Questo approccio è corretto e completo per topologie specifiche (Linea, Labirinto, Griglia) sotto determinate condizioni di budget, sebbene sia generalmente incompleto poiché non divide i gruppi atomici.

Contributi Chiave

1. Codifiche SMT Ottimizzate: Gli autori hanno sviluppato codifiche booleane native e rilassamenti invarianti che migliorano le prestazioni dell'approccio originale di sintesi dei parametri di circa 3 ordini di grandezza nel tempo di esecuzione e permettono di risolvere istanze ~75 volte più grandi in termini di dimensioni.
2. Paradigma di Decomposizione: Hanno introdotto un nuovo metodo per risolvere istanze OOP decomponendo il problema nell'enumerazione di funzioni di osservazione valutate tramite oracoli, invece di risolvere un problema SMT monolitico.
3. Enumerazione Euristiche (Algoritmo AG): Un algoritmo specifico che sfrutta l'equivalenza degli stati e le firme delle azioni ottimali per dare priorità allo spazio di ricerca. Questo metodo migliora l'approccio SMT potenziato di 3 ordini di grandezza nel tempo di esecuzione e scala a istanze 100 volte più grandi.
4. Validazione Empirica: Ampie valutazioni su modelli standard (Griglia, Labirinto, Linea) dimostrano che i metodi proposti superano significativamente la linea di base di [19] e i miglioramenti SMT intermedi degli autori.

Risultati

Il documento presenta risultati sperimentali che confrontano l'approccio originale [19], l'approccio SMT potenziato (Sezione 3) e l'approccio di decomposizione euristica (Sezione 5):

• Tempo di Esecuzione: L'algoritmo AG riduce il tempo di risoluzione di fattori di $10^3$ rispetto al metodo SMT potenziato. Ad esempio, un'istanza di Griglia (G(20)) che ha superato il tempo limite o ha richiesto ~30 secondi con SMT è stata risolta in millisecondi da AG.
• Scalabilità:
  • Miglioramenti SMT: Ha risolto istanze con fino a ~10.000 stati (Linea) e ~1.296 stati (Griglia) per strategie deterministiche, rispetto a ~377 e ~96 rispettivamente nella linea di base.
  • Decomposizione AG: Ha risolto istanze con fino a 200.001 stati (Linea) e 160.801 stati (Griglia) per strategie deterministiche.
• Strategie Randomizzate: I miglioramenti sono significativi anche per le strategie randomizzate, sebbene le strategie deterministiche producano generalmente fattori di scala più grandi grazie all'efficacia della codifica booleana.

Significato e Affermazioni

Il documento afferma che combinando tecniche simboliche (SMT) e sub-simboliche (decomposizione euristica/basata su oracoli), è possibile scalare la soluzione di frammenti decidibili del Problema dell'Osservabilità Ottimale fino a dimensioni precedentemente considerate intrattabili.

Gli autori sottolineano che il loro lavoro sposta il focus dalla risoluzione dell'intera codifica tpMC alla ricerca intelligente nello spazio delle funzioni di osservazione. Affermano che il loro algoritmo di enumerazione basato su euristiche è corretto e, per le topologie specifiche studiate (Linea, Labirinto, Griglia), sembra essere completo per budget maggiori o uguali al budget posizionale minimo.

Il documento conclude con modestia, notando che, sebbene i risultati attuali siano significativi, il lavoro futuro potrebbe migliorare ulteriormente la prevedibilità tramite tattiche Z3, estendere gli strumenti di sintesi dei parametri e applicare tecniche di Apprendimento per Rinforzo inizializzate dalle euristiche proposte. Gli autori non affermano di aver risolto l'OOP generale indecidibile, ma di aver avanzato significativamente lo stato dell'arte per i suoi frammenti decidibili.