Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

Riepilogo Tecnico: Automi di Insiemi e Limiti della Decidibilità della Logica a Due Variabili su Parole di Dati

Enunciato del Problema
Il lavoro affronta la decidibilità del problema di soddisfacibilità per estensioni della logica del primo ordine a due variabili ($FO_2$) su parole di dati. Una parola di dati è una sequenza finita di coppie $(a_i, d_i)$ dove $a_i$ proviene da un alfabeto finito $\Sigma$ e $d_i$ da un dominio infinito $D$, con l'uguaglianza come unica proprietà verificabile su $D$. Mentre la logica $FO_2$ standard su parole di dati (con ordine, successore e uguaglianza sui dati) è nota per essere decidibile (nello specifico, $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1]$), gli autori investigano i limiti della decidibilità quando si estende questa logica con predicati regolari protetti.

Questi predicati, indicati con $eL(x, y)$, sono veri se le posizioni $x$ e $y$ appartengono alla stessa classe di dati (cioè $x \sim y$) e il fattore della stringa strettamente compreso tra esse appartiene a un linguaggio regolare $L$. La domanda centrale è: per quali classi di monoidi (o semigruppi) $M$ che riconoscono la famiglia di linguaggi regolari utilizzati in questi predicati il problema di soddisfacibilità è decidibile?

Metodologia
Gli autori impiegano una combinazione di teoria degli automi e teoria algebrica dei semigruppi per caratterizzare la frontiera della decidibilità.

1. Automi di Insiemi: Gli autori introducono un nuovo formalismo di automi chiamato automi di insiemi. Questi sono automi a stati finiti dotati di un numero fisso di insiemi che possono memorizzare valori di dati. Le transizioni permettono:

   • Aggiornamenti locali: Aggiungere o rimuovere il valore di dati corrente da insiemi specifici.
   • Aggiornamenti globali: Applicare una relazione (o trasformazione) ai contenuti di tutti gli insiemi simultaneamente (ad esempio, spostare dati dall'insieme $X_i$ all'insieme $X_j$).
     Gli autori stabiliscono che gli automi di insiemi sono espressivamente equivalenti agli automi di classi (introdotti da Bojańczyk e Lasota), un modello noto per avere un problema di vuoto indecidibile.

2. Sottoclassi e Decidibilità: Per recuperare la decidibilità, gli autori definiscono una sottoclasse chiamata automi di insiemi ordinati quasi-normali.

   • Quasi-normali: Garantisce che i valori di dati siano presenti in al più un insieme tra un sottoinsieme specifico di insiemi "non stabili".
   • Ordinati: Impone un ordine lineare sugli insiemi non stabili tale che gli aggiornamenti globali svuotino i contenuti di un prefisso di tali insiemi e li spostino verso insiemi più alti nell'ordine.
     Il problema di vuoto per gli automi di insiemi ordinati quasi-normali risulta decidibile riducendolo al problema di vuoto degli automi a più contatori ordinati, un problema noto come decidibile.

3. Traduzione Logica-Automata: Il lavoro fornisce traduzioni tra le formule logiche e gli automi:

   • Ogni automa di insiemi può essere espresso come una formula $EMSO_2$ con predicati regolari protetti.
   • Viceversa, le formule che utilizzano predicati riconosciuti da un monoide $M$ possono essere tradotte in automi di insiemi con memorizzazione di suffissi (un tipo specifico di automa quasi-normale).

4. Caratterizzazione Algebrica: Gli autori analizzano la struttura algebrica dei monoidi $M$. Definiscono bande lineari come monoidi idempotenti in cui gli ideali bilateri sono ordinati linearmente (cioè, per qualsiasi due ideali $I, J$, oppure $I \subseteq J$ oppure $J \subseteq I$).

Contributi e Risultati Chiave

• Teorema Principale (Teorema 6): La soddisfacibilità delle formule $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1, \tilde{F}_M]$ su parole di dati è decidibile se e solo se il monoide $M$ è una banda lineare.

  • Direzione della Decidibilità: Se $M$ è una banda lineare, gli autori costruiscono un automa di insiemi ordinato quasi-normale equivalente. Poiché il vuoto di tali automi è decidibile, la logica è decidibile.
  • Direzione dell'Indecidibilità: Se $M$ non è una banda lineare, deve contenere una sottostruttura isomorfa a $U_1^2$ (il prodotto diretto di due monoidi a due elementi con zero) oppure a $N_2$ (un specifico monoide nullo). Gli autori dimostrano che i predicati regolari protetti riconosciuti da questi specifici monoidi permettono la codifica del problema della fermata delle macchine a due contatori, rendendo la logica indecidibile.

• Equivalenza Espressiva: Il lavoro dimostra che gli automi di insiemi sono espressivamente equivalenti alla $EMSO_2$ con predicati regolari protetti. Inoltre, mostra che qualsiasi formula con predicati regolari riconosciuti da un monoide $M$ può essere riscritta in modo equivalente utilizzando predicati regolari protetti riconosciuti da un altro monoide $M'$ (nello specifico, il monoide dell'insieme delle parti $P(M)$).

• Estensione Stretta: Il frammento decidibile identificato è un'estensione stretta della logica $FO_2$ originale da [4]. Ad esempio, il linguaggio $L_2$ (che richiede nessun test di zero tra incrementi e decrementi della stessa classe), che non è definibile nella $FO_2$ standard o negli automi di dati, diventa definibile in questa logica estesa quando il monoide sottostante è una banda lineare.

Significato e Affermazioni
Il lavoro afferma di fornire una caratterizzazione precisa della frontiera della decidibilità per la logica a due variabili su parole di dati estesa con predicati regolari protetti. Collegando la decidibilità logica alla proprietà algebrica del monoide riconoscitore di essere una "banda lineare", il lavoro colma il divario tra espressività logica e struttura algebrica.

Gli autori notano che, mentre la decidibilità per le bande lineari è stabilita, la caratterizzazione per i semigruppi generali rimane aperta. Sottolineano inoltre che la classe dei linguaggi regolari riconosciuti dalle bande lineari non è stata ampiamente studiata nella letteratura, suggerendo la necessità di un'ulteriore esplorazione in quel dominio algebrico. La complessità delle procedure decisionali rimane non elementare, ereditata dai risultati sottostanti su $FO_2$ e automi di dati.

Il lavoro si distingue dalle logiche temporali (come freeze-LTL) offrendo un'estensione decidibile della logica del primo ordine che cattura proprietà regolari specifiche all'interno di classi di dati, che precedentemente erano indecidibili o richiedevano diversi framework logici.