Riepilogo Tecnico: Una Procedura di Decisione per una Teoria degli Insiemi Finiti con Intervalli Interi Finiti

Enunciato del Problema

Nel contesto della verifica formale e dell'analisi, gli strumenti di ragionamento automatico sono essenziali per esonerare le condizioni di verifica. Sebbene gli strumenti esistenti basati sulla teoria degli insiemi (ad esempio B, ProB) siano efficaci, spesso mancano di procedure di decisione per specifici frammenti della teoria degli insiemi che combinano insiemi finiti con intervalli interi. Nello specifico, l'algebra booleana degli insiemi finiti estesa con vincoli di cardinalità (denotata come $L|\cdot|$) è decidibile, ma non può esprimere o ragionare nativamente su intervalli interi finiti (range) in cui i limiti possono essere variabili illimitate. Questa limitazione ostacola la verifica automatica di proprietà che coinvolgono operazioni sugli insiemi, come la ricerca del minimo o del massimo di un insieme, la partizione di insiemi basata su soglie intere, o il ragionamento su domini di array definiti da intervalli. Il problema centrale affrontato è la decidibilità di una teoria che integra insiemi finiti, vincoli di cardinalità e intervalli interi finiti (denotata come $L[\ ]$) all'interno di una logica libera da quantificatori.

Metodologia

Gli autori propongono una procedura di decisione, SAT $[\ ]$, che estende il risolutore esistente SAT $|\cdot|$ (per $L|\cdot|$) per gestire intervalli interi. La metodologia si basa su una teoria di base degli insiemi ereditariamente finiti implementata all'interno del linguaggio di Programmazione Logica con Vincoli (CLP) CLP($SET$) e dello strumento {log}.

Componenti Tecnici Chiave:

1. Estensione del Linguaggio ($L[\ ]$):

   • Il linguaggio è esteso per includere termini di insieme della forma $[k, m]$, che rappresentano l'insieme $\{p \in \mathbb{Z} \mid k \le p \le m\}$.
   • I limiti dell'intervallo ($k, m$) possono essere termini lineari interi, incluse variabili.
   • La logica rimane libera da quantificatori, utilizzando congiunzioni e disgiunzioni di vincoli che coinvolgono appartenenza all'insieme, unione, disgiunzione, cardinalità e appartenenza all'intervallo.

2. Identità Centrale e Strategia di Riduzione:

   • La intuizione teorica centrale è l'identità: $k \le m \implies (A = [k, m] \iff A \subseteq [k, m] \land |A| = m - k + 1)$.
   • Questa identità permette alla procedura di trasformare vincoli che coinvolgono l'uguaglianza con un intervallo in vincoli che coinvolgono relazioni di sottoinsieme e cardinalità.
   • Il risolutore riscrive le formule in una congiunzione di una formula standard $L|\cdot|$ ($\Phi_{|\cdot|}$) e un insieme di vincoli di sottoinsieme che coinvolgono intervalli ($\Phi_{\subseteq[\ ]}$), tipicamente della forma $X \subseteq [p, q]$ dove $X$ è una variabile.

3. L'Algoritmo SAT $[\ ]$:

   • Regole di Riscrittura: Il risolutore impiega un insieme di regole di riscrittura (STEPS$[\ ]$) che riducono la complessità sintattica. Queste regole gestiscono vincoli di uguaglianza, appartenenza, unione, disgiunzione e cardinalità che coinvolgono intervalli.
   • Riduzione all'Aritmetica Interi: Molte regole riscrivono i vincoli sugli insiemi che coinvolgono intervalli direttamente in vincoli di aritmetica lineare intera (LIA).
   • Controllo della Soluzione Minima: Quando rimangono vincoli irriducibili della forma $X \subseteq [p, q]$, la procedura non fallisce semplicemente. Invece, sfrutta la proprietà che se una formula è soddisfacibile, deve avere una "soluzione minima" (una soluzione in cui gli insiemi hanno la cardinalità minima possibile).
     • Il risolutore calcola la soluzione minima per la parte $L|\cdot|$ ($\Phi_{|\cdot|}$).
     • Successivamente, verifica se questa soluzione minima soddisfa i vincoli di intervallo ($\Phi_{\subseteq[\ ]}$).
     • Gli autori dimostrano che se nessuna soluzione minima soddisfa l'intera formula, allora nemmeno una soluzione più grande lo farà, rendendo la formula insoddisfacibile.

4. Implementazione in {log}:

   • La procedura è implementata in {log} (setlog), uno strumento basato su Prolog.
   • L'implementazione include uno schema di memorizzazione (memoizing schema) per tracciare le sostituzioni di variabili per gli intervalli, prevenendo riscritture ridondanti e migliorando l'efficienza.
   • I vincoli derivati (ad esempio, intersezione, differenza) sono definiti in termini di vincoli primitivi per mantenere la coerenza.

Contributi Chiave

1. Dimostrazione di Decidibilità: Il documento fornisce la prima dimostrazione che l'algebra booleana degli insiemi finiti estesa con vincoli di cardinalità e intervalli interi finiti ($L[\ ]$) è decidibile.
2. Procedura di Decisione (SAT $[\ ]$): Viene presentato un algoritmo completo che decide la soddisfacibilità delle formule $L[\ ]$. La procedura è dimostrata essere corretta, completa e terminante.
3. Integrazione di Intervalli e Insiemi: A differenza di approcci che trattano gli intervalli come un dominio separato o richiedono limiti costanti, questo lavoro integra senza soluzione di continuità intervalli interi con limiti variabili nella teoria degli insiemi, permettendo l'espressione di operatori non banali (ad esempio, l'$i$-esimo elemento più piccolo, partizionamento per una soglia) in una logica libera da quantificatori.
4. Implementazione e Strumentazione: La procedura di decisione è implementata come estensione dello strumento {log}, fornendo una doppia capacità come linguaggio di programmazione logica con vincoli e come risolutore di soddisfacibilità.

Risultati e Valutazione

Il documento presenta evidenze empiriche e uno studio di caso per dimostrare l'utilità pratica dell'approccio:

• Valutazione sui Benchmark: Un insieme di 60 formule $L[\ ]$, che rappresentano proprietà di operatori definiti nel documento (ad esempio, minimo, massimo, $i$-esimo elemento), è stato risolto. {log} ha risolto tutti i problemi in una media di 0,51 secondi per problema, con solo uno che ha richiesto oltre 5 secondi.
• Studio di Caso (Algoritmo dell'Ascensore): Gli autori hanno modellato un sistema di controllo di un ascensore in cui l'ascensore deve soddisfare le richieste in una direzione specifica. Il modello ha utilizzato intervalli interi per definire i piani e le richieste.
  • Il sistema includeva 7 operazioni (ad esempio, aggiunta di richieste, servizio della prossima richiesta).
  • {log} è stato utilizzato per esonerare automaticamente 49 lemmi di invarianza (dimostrando che le operazioni sullo stato preservano 7 invarianti di stato) e 7 controlli dello stato iniziale.
  • Tutte le dimostrazioni sono state completate in circa 0,5 secondi su un laptop standard.
  • Lo strumento ha generato con successo controesempi quando gli invarianti sono stati intenzionalmente indeboliti, dimostrando le sue capacità di debug.

Significato e Affermazioni

Gli autori affermano che questo lavoro rappresenta un passo significativo in avanti nel ragionamento automatico per la verifica formale. Estendendo il frammento decidibile della teoria degli insiemi per includere intervalli interi finiti con limiti variabili, l'approccio permette la verifica automatica di proprietà che erano precedentemente difficili o impossibili da esprimere senza quantificatori.

Il documento sottolinea che l'approccio è radicato nella teoria degli insiemi, distinguendosi da altri strumenti di ragionamento sugli intervalli (come quelli basati sull'algebra degli intervalli di Allen o sui reticoli di analisi statica) che spesso mancano della capacità di combinare intervalli con operazioni generali sugli insiemi. L'integrazione del ragionamento sugli intervalli nel framework {log} permette agli utenti di scrivere programmi e dimostrare le loro proprietà utilizzando lo stesso codice e lo stesso strumento, sfruttando la dualità tra formula e programma. Gli autori notano modestamente che, sebbene l'approccio sia generale e coerente, potrebbe comportare costi di efficienza rispetto a risolutori specializzati per problemi specifici solo sugli intervalli, ma il compromesso è la capacità di ragionare su complesse strutture ibride insieme-intervallo.