Sintesi Tecnica: Completamento degli Automi Emerson-Lei di tipo Elevator

Definizione del Problema

Il completamento degli $\omega$-automi è un'operazione fondamentale nei metodi formali, essenziale per compiti quali l'analisi della terminazione dei programmi, il model checking di logiche temporali (ad esempio, LTL, HyperLTL) e la decisione di teorie logiche (ad esempio, S1S). Tuttavia, il completamento di $\omega$-automi generici è notoriamente difficile, poiché spesso risulta in un'esplosione dello spazio degli stati che rende l'inverificabilità pratica.

Sebbene restrizioni strutturali come gli "elevator automata" (dove ogni componente fortemente connesso è o deterministico o intrinsecamente debole) abbiano dimostrato di consentire un completamento più efficiente per gli automi di Büchi, tali ottimizzazioni non sono state pienamente estese ad automi con condizioni di accettazione più ricche. Gli automi Emerson-Lei (ELA), che supportano combinazioni booleane arbitrarie di predicati Inf (infinitamente spesso) e Fin (frequentemente finito), offrono maggiore sinteticità e flessibilità, ma attualmente mancano di algoritmi di completamento efficienti che tengano conto della struttura. Gli algoritmi esistenti per gli ELA non ristretti soffrono di un'elevata complessità asintotica, e vi è una lacuna nei metodi pratici per completare gli ELA che presentano la struttura "elevator" tipica delle applicazioni reali.

Metodologia

Il documento introduce gli Emerson-Lei Elevator Automata (ELEA), una generalizzazione degli automi elevator di Büchi al framework di accettazione di Emerson-Lei. Gli autori propongono un nuovo algoritmo di completamento che sfrutta le proprietà strutturali degli ELEA per ottenere limiti di complessità significativamente migliori rispetto al completamento degli ELA generici.

La metodologia si articola in tre fasi principali:

1. Automi Semi-Deterministici (ELSA) con Condizioni Specifiche:
   Gli autori affrontano innanzitutto il completamento degli Emerson-Lei Semi-Deterministic Automata (ELSA), dove le corse entrano infine in una componente deterministica. Sviluppano costruzioni per due casi specifici:

   • Coppie di Rabin Generalizzate: L'algoritmo combina la costruzione di Miyano-Hayashi (per le condizioni Fin) e l'algoritmo NCSB (per le condizioni Inf). Utilizza una struttura di macrostato $(N, R, C, S_1, \dots, S_k, B)$ per tracciare le corse nella parte nondeterministica ($N$) e nella parte deterministica. La parte deterministica è suddivisa in insiemi per tracciare le violazioni di Fin ($R$) e le violazioni di Inf ($C$ e insiemi sicuri $S_i$). Un insieme di breakpoint globale $B$ assicura che tutte le corse siano ispezionate infinitamente spesso.
   • Coppie di Streett Generalizzate: Come duale del caso Rabin, questa costruzione utilizza un contatore di scheduling round-robin ($z$) per invalidare sequenzialmente tutte le condizioni nella coppia di Streett. Riutilizza gli insiemi tra un'istanza NCSB (per la condizione Inf) e molteplici istanze di Miyano-Hayashi (per le condizioni Fin).

2. Procedura Induttiva per Condizioni Emerson-Lei Arbitrarie:
   Per gestire combinazioni booleane arbitrarie di Inf e Fin, gli autori introducono un approccio basato su tree-macrostate. La condizione di accettazione negata $\psi = \neg Acc$ è rappresentata come un albero che rispecchia la sua struttura sintattica.

   • Modalità di Campionamento (Sampling Mode): Le corse che entrano nella componente deterministica sono assegnate nondeterministamente a sottoportanti corrispondenti ai disgiunti di $\psi$.
   • Modalità di Verifica (Checking Mode): L'algoritmo verifica che le corse soddisfino le sottoformule assegnate. Per le condizioni Inf, utilizza insiemi di breakpoint per garantire visite infinite; per le condizioni Fin, assicura che le corse evitino determinati colori.
   • Ottimizzazioni: Il documento dettaglia diverse ottimizzazioni per ridurre l'esplosione dello spazio degli stati:
     • Normalizzazione del Tree-Macrostate: Fusione del tracciamento delle corse ridondanti quando le corse si fondono.
     • Ottimizzazione del Breakpoint Condiviso: Utilizzo di un singolo breakpoint condiviso per più foglie Inf tramite scheduling round-robin.
     • Ottimizzazione OR-FIN: Propagazione sequenziale degli stati violanti attraverso le foglie Fin nelle disgiunzioni per evitare la ramificazione esponenziale.

3. Estensione agli Automi Elevator Completi e Non Ristretti:
   Le tecniche sviluppate per gli ELSA sono estese ai pieni ELEA. Gli autori osservano che, in pratica, molti automi non-elevator sono "quasi elevator" (contenenti solo poche componenti SCC non-elevator). La loro conversione tratta questi casi in modo efficiente, sfruttando il fatto che la maggior parte degli SCC negli automi pratici sono già componenti elevator.

Contributi Chiave e Risultati

• Definizione di ELEA: Il documento definisce formalmente gli Emerson-Lei Elevator Automata, generalizzando il concetto di automi elevator alle ricche condizioni di accettazione.
• Miglioramento dei Limiti di Complessità: L'algoritmo proposto raggiunge una complessità dello spazio degli stati asintoticamente molto inferiore per il complemento di un ELEA rispetto ai migliori algoritmi noti per gli ELA non ristretti.
  • Per una coppia di Rabin generalizzata con $k$ coppie, la dimensione del complemento è limitata da $(k+3)n$ (o $(5+k)n$ nel caso generale presentato nella Sezione 3), mentre gli ELA non ristretti hanno limiti come $O(n^{k}(0.76n)^{n})$.
  • La Tabella 1 nel documento fornisce un confronto esaustivo, mostrando miglioramenti esponenziali o polinomiali rispetto ai limiti non ristretti per varie condizioni (Büchi, Rabin, Streett, Parity e Emerson-Lei).
• Implementazione Pratica e Valutazione: L'algoritmo è implementato nello strumento Kofola. I confronti sperimentali con lo stato dell'arte, lo strumento Spot, dimostrano che Kofola produce spesso complementi di dimensioni molto minori. I benchmark includono ELA dalla letteratura, ELA generati casualmente come Generalized Rabin Automata ed ELA derivati da traduzioni LTL.

Significato e Rivendicazioni

Gli autori affermano che questo lavoro rappresenta il primo passo verso algoritmi pratici per il completamento, la determinizzazione e il test di universalità e inclusione per gli automi Emerson-Lei con ricche condizioni di accettazione.

La significanza risiede nel colmare il divario tra la sinteticità teorica (fornita dagli ELEA) e l'efficienza della verifica pratica. Sfruttando la prevalenza strutturale delle componenti elevator negli automi reali (come notato nel lavoro precedente [1]), gli autori forniscono un metodo che riduce drasticamente il problema dell'esplosione dello stato inerente al completamento. Il documento posiziona questo lavoro come un contributo fondamentale, abilitando workflow di verifica più efficienti per sistemi modellati con sofisticate condizioni di accettazione, senza inventare nuove applicazioni oltre quelle già stabilite nel campo (model checking LTL, verifica di hyperproprietà).

Il lavoro è modesto nel suo ambito, concentrandosi strettamente sul problema del completamento e sulle sue implicazioni immediate per la determinizzazione e il test di inclusione, pur riconoscendo che ulteriori lavori sono necessari per realizzare pienamente algoritmi pratici per tutte le operazioni sugli ELEA.