Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion

Titolo

Verso l'uso di vincoli di conteggio a finestra nella sintesi di sistemi reattivi per ridurre l'esplosione dello spazio degli stati.

1. Il Problema

La sintesi reattiva mira a costruire automaticamente strategie per sistemi che interagiscono con un ambiente ostile o dinamico. Il problema fondamentale risiede nella complessità computazionale della traduzione di specifiche formali (come LTL - Linear Temporal Logic) in automati deterministici necessari per la costruzione della strategia.

• Complessità: La traduzione da LTL a un automa deterministico è doppiamente esponenziale rispetto alla lunghezza della specifica. Questo porta a un'esplosione dello spazio degli stati che rende la sintesi impraticabile per molte applicazioni reali.
• Limiti degli approcci attuali: Esistono sottoclassi di LTL (es. GR(1)) che permettono una sintesi efficiente ($O(N^3)$), ma molte specifiche reali, in particolare quelle che coinvolgono pattern di conteggio (es. "l'azione X deve avvenire almeno $k$ volte ogni $l$ mosse"), non rientrano in queste classi o richiedono automi troppo grandi.
• Obiettivo: Ridurre l'esplosione dello spazio degli stati durante la costruzione dell'automa per specifiche contenenti vincoli di conteggio, senza sacrificare la correttezza della strategia risultante.

2. Metodologia

Gli autori propongono un approccio di sintesi incrementale basato sulla proprietà di monotonicità intrinseca nei vincoli di conteggio.

Concetti Chiave:

• Vincoli di Conteggio a Finestra (Window Counting Constraints): Sono specifiche del tipo: "Il sistema esegue l'azione $act$ almeno $k$ volte (o al massimo $k$ volte) su $l$ delle proprie mosse".
  • Esempio: Un veicolo autonomo deve ricaricarsi almeno 2 volte ogni 10 mosse.
• Monotonicità:
  • Per vincoli di tipo "almeno" ($\ge k$ su $l$): Se una strategia soddisfa il vincolo per una finestra più piccola (es. $l-1$), soddisfa automaticamente anche il vincolo per una finestra più grande ($l$).
  • Per vincoli di tipo "al massimo" ($\le k$ su $l$): Se una strategia soddisfa il vincolo per una finestra più grande, soddisfa anche quello per una finestra più piccola.
  • Implicazione: È possibile iniziare la sintesi con vincoli "facili" (finestre piccole o restrizioni meno severe) e raffinarli progressivamente.

L'Algoritmo di Sintesi Incrementale:

L'approccio non costruisce l'intero grafo di gioco con la memoria completa fin dall'inizio. Procedura iterativa:

1. Inizializzazione: Si parte con un sottoinsieme di vincoli di conteggio con parametri ridotti (es. lunghezza della finestra $l$ minima).
2. Costruzione Parziale del Grafo delle Situazioni: Viene costruito un "situation graph" (un grafo di gioco esteso che include lo stato originale e la storia rilevante per i vincoli).
   • Se una situazione (stato + storia) è un'estensione di una situazione che appartiene già alla regione di vittoria calcolata in un'iterazione precedente, non è necessario espanderne i successori: viene direttamente marcata come vincente.
   • Le situazioni che violano i vincoli vengono scartate o indirizzate a un "sink" perdente.
3. Calcolo della Regione di Vittoria: Si utilizza un algoritmo di sintesi standard (adatto al tipo di gioco: sicurezza, raggiungibilità, Büchi, ecc.) sul grafo parziale per determinare la regione di vittoria.
4. Incremento: Se non è stata trovata una strategia vincente per lo stato iniziale, si aumentano i parametri dei vincoli (es. si aumenta $l$) e si ripete il processo.
5. Terminazione: L'algoritmo si ferma quando viene trovata una strategia vincente o quando si raggiunge la specifica completa senza successo.

Gestione dei Giochi a Somma Zero:

Il paper assume un setting a somma zero (gioco antagonista). Per gestire la razionalità dell'ambiente (ALTER), si assume che l'ambiente non possa essere forzato a violare i propri vincoli di conteggio. Questo evita soluzioni banali in cui il sistema vince solo costringendo l'ambiente a violare le proprie regole.

3. Contributi Chiave

1. Introduzione dei Vincoli di Conteggio a Finestra: Formalizzazione di pattern di specifica comuni (ricorrenza, limiti di frequenza) che non rientrano facilmente nelle classi sintetiche standard come GR(1).
2. Algoritmo di Sintesi Iterativa: Sviluppo di un metodo che sfrutta la monotonicità per costruire grafi di gioco parziali, riutilizzando le informazioni sulle regioni di vittoria delle iterazioni precedenti per "potare" (pruning) lo spazio degli stati.
3. Generalizzazione dei Giochi: Estensione dell'approccio (rispetto al lavoro precedente [FF24]) non solo ai giochi di sicurezza, ma anche a giochi di raggiungibilità, Büchi, co-Büchi e parità.
4. Gestione Ibrida dei Vincoli: Capacità di gestire contemporaneamente vincoli di tipo "almeno" e "al massimo" all'interno dello stesso processo di sintesi, trasformando i vincoli "al massimo" in equivalenti "almeno" tramite il Lemma 3.2 per uniformare l'approccio incrementale.
5. Implementazione e Validazione: Fornitura di un'implementazione in Python e risultati sperimentali che dimostrano la fattibilità dell'approccio.

4. Risultati Sperimentali

Gli autori hanno confrontato la sintesi incrementale con la sintesi classica (costruzione diretta dell'automa con vincoli completi) su diversi giochi di sicurezza sintetici.

• Efficienza: In quasi tutti i casi testati (7 esperimenti su 7, con alcune eccezioni in termini di overhead), l'approccio incrementale ha richiesto significativamente meno tempo di calcolo e memoria.
  • Esempio: Nell'esperimento 2, la sintesi incrementale (sequenziale) ha impiegato 11 secondi con ~90k stati, mentre la sintesi diretta ha richiesto 6102 secondi con ~6 milioni di stati.
  • Esempio: Nell'esperimento 3, la sintesi diretta ha fallito o richiesto risorse enormi, mentre quella incrementale ha completato il task in pochi secondi.
• Eccezioni: In alcuni casi (es. Esperimento 7), se la strategia vincente richiede necessariamente la finestra completa fin dall'inizio e le iterazioni precedenti non producono regioni di vittoria utili, l'approccio incrementale può introdurre un overhead non benefico rispetto alla sintesi diretta.
• Riduzione dello Spazio: La chiave del successo è che non è necessario memorizzare l'intero grafo espanso; basta memorizzare un insieme minimo di stati che coprono le regioni di vittoria precedenti, riducendo drasticamente la memoria necessaria.

5. Significato e Implicazioni

• Superamento delle Barriere di Scalabilità: Questo lavoro offre una via pratica per sintetizzare sistemi reattivi con specifiche complesse che coinvolgono conteggi, un'area dove gli algoritmi esistenti falliscono a causa dell'esplosione esponenziale.
• Euristiche per la Sintesi: Dimostra che non è necessario migliorare la classe di complessità teorica del problema (che rimane alta), ma è possibile migliorare l'efficienza euristica degli algoritmi esistenti sfruttando la struttura specifica delle richieste dell'utente.
• Applicabilità Reale: L'approccio è particolarmente rilevante per domini come la robotica (veicoli autonomi, magazzini automatizzati) dove i vincoli di frequenza e le finestre temporali sono comuni.
• Lavori Futuri: Gli autori identificano direzioni promettenti, tra cui:
  • Estensione a giochi cooperativi (non solo a somma zero).
  • Identificazione di nuovi pattern di specifica con proprietà di monotonicità.
  • Trasformazione dell'algoritmo in una versione simbolica (usando BDD o simili) per gestire spazi ancora più grandi.
  • Integrazione con algoritmi di sintesi on-the-fly.
  • Sintesi simmetrica per sistemi di sistemi (es. flotte di robot identici).

In conclusione, il paper presenta un metodo innovativo che trasforma un problema di complessità intrattabile in una serie di sottoproblemi gestibili, riducendo drasticamente i costi computazionali per la sintesi di controller reattivi complessi.