Robustness of Constraint Automata for Description Logics with Concrete Domains

Sintesi Tecnica: Robustezza degli Automi di Vincolo per i Logiche di Descrizione con Domini Concreti

Problematica
Il documento affronta il problema della coerenza per le Logiche di Descrizione (DL) con domini concreti, concentrandosi specificamente sulla logica $\mathcal{ALCO}(\mathcal{D})$. Questa logica estende $\mathcal{ALC}$ con nominali, ruoli inversi (in estensioni) e domini concreti $\mathcal{D}$ che permettono di ragionare su oggetti concreti (ad esempio, numeri, intervalli) tramite relazioni predefinite. Sebbene la decidibilità per tali logiche sia stata stabilita utilizzando metodi basati su tableau o eliminazione dei tipi (ad esempio, [LM07]), lavori recenti [BDK24, BBDK25] hanno raffinato i limiti di complessità a $\text{ExpTime}$ per classi specifiche di domini concreti. Tuttavia, questi risultati spesso dipendono da condizioni restrittive (ad esempio, insiemi finiti di relazioni, condizioni JEPD) o tecniche specifiche che potrebbero non generalizzarsi facilmente ad ulteriori caratteristiche delle DL come i ruoli inversi o le asserzioni di vincolo. Gli autori mirano a investigare se un approccio basato su automi possa raggiungere limiti superiori ottimali di $\text{ExpTime}$ mantenendo al contempo la robustezza rispetto all'aggiunta di caratteristiche complesse e rilassando determinati vincoli sul dominio concreto.

Metodologia
Gli autori propongono una procedura decisionale basata su automi che riduce il problema della coerenza di $\mathcal{ALCO}(\mathcal{D})$ al problema della non-vacuità di Tree Global Constraint Automata (TGCA).

1. Definizione di Automa di Vincolo: Il meccanismo centrale è un TGCA, che accetta alberi di dati infiniti dove i nodi sono etichettati con tuple di valori dal dominio concreto $\mathcal{D}$. Le transizioni in questi automi sono arricchite con vincoli simbolici (combinazioni booleane di predicati) che mettono in relazione i valori in un nodo con quelli dei suoi figli.
2. Riduzione a Büchi Tree Automata (BTA): Per analizzare la complessità della non-vacuità dei TGCA, gli autori costruiscono una riduzione ai classici Büchi Tree Automata. Ciò comporta:
   • Tipi Simbolici: Astrazione dei valori concreti in "tipi simbolici" (insiemi di letterali su registri) che catturano tutti i vincoli atomici rilevanti.
   • Compatibilità di Proiezione: Garantire la coerenza tra il tipo simbolico di un nodo genitore e quello dei suoi figli.
   • Proprietà di $\mathcal{D}$: La riduzione si basa su proprietà specifiche del dominio concreto $\mathcal{D}$, nello specifico la proprietà di completamento (o alternativamente, la proprietà di amalgamazione combinata con l'$\omega$-compattezza dell'omomorfismo), l'arità limitata dei predicati e la decidibilità del Problema di Soddisfacimento dei Vincoli (CSP) per $\mathcal{D}$.
3. Gestione delle Ontologie: Gli autori progettano un TGCA specifico per modellare la coerenza di un'ontologia (TBox e ABox). L'automa gestisce:
   • Nominali: Utilizzando astrazioni globali che persistono attraverso l'esecuzione per tracciare l'interpretazione dei nomi individuali.
   • Caratteristiche Concrete: Utilizzando registri per memorizzare i valori delle feature e imponendo vincoli tra di esse.
   • Strutture a Foresta: Codifica delle strutture a foresta tipiche delle DL con ABox in un singolo albero accettato dall'automa.

Contributi Chiave

• Complessità Ottimale tramite Automa: Il documento stabilisce che il problema della coerenza per $\mathcal{ALCO}(\mathcal{D})$ è in $\text{ExpTime}$ (o $k$-$\text{ExpTime}$ a seconda della complessità CSP di $\mathcal{D}$) sotto le condizioni (C1)–(C4). Ciò eguaglia i limiti ottimali precedentemente raggiunti dai metodi di eliminazione dei tipi, ma tramite un approccio distinto basato sugli automi.
• Robustezza alle Estensioni: Un contributo primario è la dimostrazione della "robustezza" dell'approccio degli automi di vincolo. Gli autori mostrano che la traduzione può essere adattata fluidamente per includere:
  • Ruoli Inversi: Estensione a $\mathcal{ALCI}(\mathcal{D})$ (senza nominali) introducendo "astrazioni del genitore" per gestire gli archi retroattivi.
  • Nomi di Ruolo Funzionali: Estensione a $\mathcal{ALCOF}(\mathcal{D})$ modificando la funzione di etichettatura del branching per imporre vincoli funzionali.
  • Asserzioni di Vincolo: Permettere vincoli arbitrari tra le feature concrete di individui nominati nell'ABox.
• Condizioni Rilassate sui Domini Concreti: Il framework accoglie domini concreti con insiemi infiniti di relazioni (ad esempio, $(\mathbb{Q}, <, (=q)_{q \in \mathbb{Q}})$), purché soddisfino la proprietà di completamento o le proprietà di amalgamazione/compattezza. Questo contrasta con i lavori precedenti che spesso richiedevano insiemi di relazioni finiti o condizioni JEPD (Jointly Exhaustive Pairwise Disjoint).
• Gestione del Dominio degli Interi: Il documento affronta il dominio concreto degli interi $(\mathbb{Z}, <, =)$, che non soddisfa la standard proprietà di completamento. Sfruttando i risultati di [DQ25] riguardanti i TGCA senza vincoli tra fratelli (sibling constraints), gli autori dimostrano che anche $\mathcal{ALCO}(\mathbb{Z})$ è $\text{ExpTime}$-completo.

Risultati

• Teorema 3.6: Il problema della non-vacuità per i TGCA su un dominio $\mathcal{D}$ che soddisfa (C1), (C2) e (C3.1) è in $\text{ExpTime}$.
• Teorema 4.5: Il problema della coerenza per $\mathcal{ALCO}(\mathcal{D})$ è in $k$-$\text{ExpTime}$ se $\mathcal{D}$ soddisfa (C1)–(C4) e CSP($\mathcal{D}$) è in $k$-$\text{ExpTime}$.
• Teorema 5.1 & 5.5: I problemi di coerenza per $\mathcal{ALCOF}(\mathcal{D})$ e $\mathcal{ALCI}(\mathcal{D})$ (senza nominali) mantengono gli stessi limiti di complessità della logica di base.
• Teorema 5.6: Il problema della coerenza per $\mathcal{ALCO}(\mathbb{Z})$ è $\text{ExpTime}$-completo.

Significato e Rivendicazioni
Gli autori sostengono che il loro lavoro fornisce un'alternativa robusta e versatile ai metodi basati su tableau e di eliminazione dei tipi per il ragionamento sulle DL con domini concreti. Utilizzando automi di vincolo arricchiti con vincoli simbolici, raggiungono limiti di complessità ottimali gestendo naturalmente caratteristiche che sono spesso difficili da integrare in altri framework, come i ruoli inversi e le asserzioni di vincolo.

Il documento sottolinea che l'approccio è "concettualmente semplice" nella sua strategia di riduzione, anche se le prove di correttezza richiedono un lavoro tecnico sostanziale. Evidenzia come il metodo permetta un'analisi della complessità parametrizzata, delineando chiaramente quali proprietà del dominio concreto (ad esempio, completamento vs. amalgamazione) siano necessarie per la decidibilità e la complessità. Gli autori notano con modestia che, sebbene il loro approccio gestisca efficacementamente i ruoli inversi, la combinazione di ruoli inversi e nominali rimane un problema aperto, in particolare quando sono coinvolte restrizioni del dominio concreto (CD-restrictions), poiché ciò può portare a un branching infinito che le attuali astrazioni a stati finiti non possono catturare.

Il lavoro serve come versione estesa di un articolo di conferenza [DG26], offrendo una formalizzazione completa della riduzione basata su automi e delle sue estensioni.