Riepilogo Tecnico: Risultati di Decidibilità per Frammenti della Logica del Primo Ordine tramite una Proprietà di Modello Simbolico

Enunciato del Problema

La logica del primo ordine (FOL) è un formalismo potente per specificare condizioni di verifica per sistemi con domini illimitati, come quelli che coinvolgono liste collegate o strutture dati a forma di albero. Tuttavia, la FOL è generalmente indecidibile. Sebbene la proprietà del modello finito (dove ogni formula soddisfacibile ammette un modello finito) implichi la decidibilità, molti frammenti utili della FOL non possiedono questa proprietà; possono ammettere solo modelli infiniti. Di conseguenza, gli strumenti di verifica basati sulla FOL potrebbero non riuscire a trovare contro-modelli per formule non valide, lasciando gli utenti senza feedback azionabili.

I frammenti decidibili esistenti, come il frammento delle Formule Stratificate (SF) (una variante a molti tipi di EPR), impongono vincoli di aciclicità rigorosi sui grafi di alternanza dei quantificatori per garantire la proprietà del modello finito. Questi vincoli sono spesso troppo restrittivi per la modellazione di sistemi complessi, richiedendo un notevole sforzo da parte dell'utente per adattare le specifiche. Questo lavoro affronta la sfida di stabilire la decidibilità per frammenti della FOL che non godono della proprietà del modello finito, in particolare quelli che consentono cicli di auto-connessione nel grafo di alternanza dei quantificatori su un tipo specifico, a condizione che siano rispettate determinate restrizioni di ordine.

Metodologia

Gli autori propongono una generalizzazione delle strutture simboliche, introdotte originariamente in [15] utilizzando l'Aritmetica Interale Lineare (LIA), a teorie di base arbitrarie che ammettono un modello standard.

1. Strutture Simboliche Generalizzate

Una struttura simbolica è una rappresentazione finita di una struttura del primo ordine potenzialmente infinita. È composta da:

• Nodi: Un insieme finito di nodi che rappresentano sottoinsiemi del dominio di un modello standard di una teoria di base $T$.
• Formule Vincolate: Ogni nodo è associato a una formula nel linguaggio di $T$ che definisce l'insieme di elementi che rappresenta.
• Interpretazioni Simboliche: Le interpretazioni di costanti, funzioni e relazioni sono definite simbolicamente utilizzando termini e formule di $T$.

La proprietà chiave delle strutture simboliche è che il controllo dei modelli (determinare se una struttura soddisfa una formula) si riduce alla validità di una formula nella teoria di base $T$. Se $T$ è decidibile, il controllo dei modelli per le strutture simboliche è decidibile.

2. La Proprietà del Modello Simbolico

Il lavoro stabilisce una proprietà del modello simbolico per specifici frammenti della FOL. Un frammento ammette questa proprietà se ogni formula soddisfacibile nel frammento ha una struttura simbolica soddisfacente su una teoria di base decidibile. Poiché il controllo dei modelli è decidibile per tali strutture, l'esistenza di questa proprietà implica la decidibilità del problema di soddisfacibilità del frammento.

3. La Famiglia dei Cicli di Auto-Connessione Ordinati (OSC)

Gli autori definiscono una famiglia di frammenti chiamata Cicli di Auto-Connessione Ordinati (OSC), parametrizzata da un'assiomatizzazione $\alpha$ di una relazione di ordine stretto $\prec$ su un tipo distinto $s_\infty$.

• Rilassamento di SF: OSC estende il frammento delle Formule Stratificate rilassando il requisito di aciclicità. Consente ai simboli di funzione di introdurre cicli di auto-connessione (cicli) sul tipo $s_\infty$, a condizione che il grafo di alternanza dei quantificatori non contenga altri cicli.
• Teorie di Base: Il lavoro utilizza due teorie di base principali:
  • Aritmetica Interale Lineare (LIA): Utilizzata per ordini totali.
  • Teoria Decidibile delle Stringhe (STR): Utilizzata per ordini di prefisso.

4. Costruzione della Dimostrazione

Le dimostrazioni di decidibilità seguono una "ricetta di dimostrazione" generica che costruisce un modello simbolico $S$ a partire da un modello arbitrario $M$ di una formula $\phi$. La costruzione comporta:

1. Partizionamento: Dividere il dominio di $M$ in classi di equivalenza basate sulle formule atomiche che soddisfano (atomi). Queste classi diventano i nodi della struttura simbolica.
2. Interpretazione: Definire le interpretazioni di costanti, relazioni unarie e dell'ordine $\prec$ per "osservare" gli atomi soddisfatti in $M$.
3. Gestione degli Atomi di Ordine Misto: La difficoltà principale risiede nel soddisfare gli atomi di ordine misto (ad esempio, $f(x) \prec g(x)$) e gli assiomi di ordine $\alpha$. Ciò è ottenuto definendo forme interne specifiche per i nodi (nodi di riepilogo) e i termini di funzione all'interno della teoria di base.
   • Per Ordini Totali (tot), i nodi di riepilogo sono modellati come linee infinite in entrambe le direzioni (interi), consentendo un'"incorporabilità universale finita" delle ordinazioni dei termini.
   • Per Ordini di Prefisso (pref), i nodi di riepilogo sono modellati come "alberi universali" (alberi infiniti in entrambe le direzioni con specifici fattori di diramazione) per adattarsi alla natura non lineare degli ordini di prefisso.

Contributi Chiave

1. Definizione Generale di Strutture Simboliche: Il lavoro fornisce una definizione parametrica di strutture simboliche su qualsiasi teoria di base con un modello standard, generalizzando lavori precedenti limitati alla LIA.
2. Introduzione della Famiglia OSC: Definisce la famiglia dei Cicli di Auto-Connessione Ordinati di frammenti, che estende le Formule Stratificate consentendo cicli di auto-connessione su un tipo ordinato sotto specifici assiomi.
3. Nuovi Risultati di Decidibilità: Gli autori dimostrano la decidibilità per diversi nuovi frammenti all'interno della famiglia OSC, in particolare:
   • OSC[pref]: Cicli di Auto-Connessione Ordinati per Prefisso, utilizzando la teoria delle stringhe. Questo frammento modella la raggiungibilità in strutture dati a forma di albero acicliche e liste collegate con condivisione.
   • Varianti con Successori/Predecessori: Frammenti che combinano ordini totali/di prefisso con assiomi che garantiscono l'esistenza di successori (prosucc) o predecessori (regpred).
4. Quadro di Dimostrazione Generico: Viene presentato una tecnica di dimostrazione unificata che costruisce modelli simbolici per questi frammenti, dimostrando che la soddisfacibilità si riduce alla validità delle formule nelle rispettive teorie di base decidibili (LIA o STR).
5. Implementazione: È stato implementato uno strumento di prova di concetto che estende la libreria open-source FEST per supportare strutture simboliche generiche, incluso il controllo dei modelli sulla teoria delle stringhe.

Risultati

Il lavoro stabilisce che il problema di soddisfacibilità è decidibile per i seguenti frammenti (dove $\alpha$ è l'assioma di ordine):

• $\alpha \in \{ \text{tot}, \text{tot} \land \text{prosucc}, \text{tot} \land \text{regpred}, \text{pref}, \text{pref} \land \text{prosucc}, \text{pref} \land \text{regpred} \}$.

Il risultato per tot riprende lavori precedenti [15], mentre i risultati per pref e le sue varianti sono nuovi. La decidibilità di OSC[pref] è particolarmente significativa in quanto gestisce strutture che non ammettono la proprietà del modello finito ma possono essere rappresentate simbolicamente utilizzando la teoria delle stringhe.

Significato e Affermazioni

Il lavoro afferma che questa offerta un nuovo approccio alla decidibilità che va oltre la proprietà del modello finito. Utilizzando strutture simboliche, consente la verifica di sistemi con domini illimitati che in precedenza erano intrattabili a causa della mancanza di contro-modelli finiti.

• Impatto Teorico: Colma il divario tra proprietà dei modelli finiti e rappresentazioni di modelli infiniti, mostrando che la decidibilità può essere raggiunta anche quando sono necessari modelli infiniti, a condizione che possano essere catturati da una teoria di base decidibile.
• Rilevanza Pratica: Il frammento OSC[pref] affronta direttamente scenari comuni di verifica che coinvolgono strutture dati a forma di albero e liste collegate con condivisione, che sono difficili da modellare in frammenti strettamente stratificati.
• Generalità: Il quadro è progettato per essere estendibile ad altre teorie di base e relazioni di ordine, suggerendo una via per scoprire ulteriori frammenti decidibili.

Gli autori notano che, sebbene la procedura decisionale riduca la soddisfacibilità alla validità delle formule nella teoria di base (che può essere non elementare per le teorie delle stringhe), il contributo principale è l'istituzione della decidibilità e la capacità di generare contro-modelli simbolici quando la verifica fallisce. L'implementazione funge da prova di concetto per la fattibilità di questo approccio.