Robustness of Constraint Automata for Description Logics with Concrete Domains

Resumo Técnico: Robustez de Autômatos de Restrição para Lógicas de Descrição com Domínios Concretos

Definição do Problema
O artigo aborda o problema da consistência para Lógicas de Descrição (DLs) com domínios concretos, focando especificamente na lógica $\mathcal{ALCO}(\mathcal{D})$. Esta lógica estende $\mathcal{ALC}$ com nominais, papéis inversos (em extensões) e domínios concretos $\mathcal{D}$ que permitem o raciocínio sobre objetos concretos (por exemplo, números, intervalos) por meio de relações predefinidas. Embora a decidibilidade para tais lógicas tenha sido estabelecida usando métodos baseados em tableau ou eliminação de tipos (por exemplo, [LM07]), trabalhos recentes [BDK24, BBDK25] refinaram os limites de complexidade para $\text{ExpTime}$ para classes específicas de domínios concretos. No entanto, esses resultados frequentemente dependem de condições restritivas (por exemplo, conjuntos finitos de relações, condições JEPD) ou técnicas específicas que podem não se generalizar facilmente para adições de recursos complexos de DL, como papéis inversos ou asserções de restrição. Os autores visam investigar se uma abordagem baseada em autômatos pode alcançar limites superiores de $\text{ExpTime}$ ótimos, mantendo a robustez contra a adição de recursos complexos e relaxando certas restrições no domínio concreto.

Metodologia
Os autores propõem um procedimento de decisão baseado em autômatos que reduz o problema da consistência de $\mathcal{ALCO}(\mathcal{D})$ para o problema da não-vacuidade de Autômatos de Restrição de Árvore Global (TGCA).

1. Definição de Autômato de Restrição: O mecanismo central é um TGCA, que aceita árvores de dados infinitas onde os nós são rotulados com tuplas de valores do domínio concreto $\mathcal{D}$. As transições nesses autômatos são enriquecidas com restrições simbólicas (combinações booleanas de predicados) que relacionam os valores em um nó aos seus filhos.
2. Redução para Autômatos de Árvore Büchi (BTA): Para analisar a complexidade da não-vacuidade do TGCA, os autores constroem uma redução para Autômatos de Árvore Büchi padrão. Isso envolve:
   • Tipos Simbólicos: Abstrair valores concretos em "tipos simbólicos" (conjuntos de literais sobre registradores) que capturam todas as restrições atômicas relevantes.
   • Compatibilidade de Projeção: Garantir a coerência entre o tipo simbólico de um nó pai e seus filhos.
   • Propriedades de $\mathcal{D}$: A redução depende de propriedades específicas do domínio concreto $\mathcal{D}$, especificamente a propriedade de completude (ou alternativamente, a propriedade de amalgamação combinada com $\omega$-compactação de homomorfismo), aridade limitada de predicados e a decidibilidade do Problema de Satisfação de Restrições (CSP) para $\mathcal{D}$.
3. Tratamento de Ontologias: Os autores projetam um TGCA específico para modelar a consistência de uma ontologia (TBox e ABox). O autômato lida com:
   • Nominais: Através do uso de abstrações globais que persistem através da execução para rastrear a interpretação de nomes individuais.
   • Recursos Concretos: Utilizando registradores para armazenar valores de atributos e impor restrições entre eles.
   • Estruturas de Floresta: Codificando as estruturas de floresta típicas de DLs com ABoxes em uma única estrutura de árvore aceita pelo autômato.

Principais Contribuições

• Complexidade Ótima via Autômatos: O artigo estabelece que o problema da consistência para $\mathcal{ALCO}(\mathcal{D})$ está em $\text{ExpTime}$ (ou $k$-$\text{ExpTime}$ dependendo do CSP de $\mathcal{D}$) sob as condições (C1)–(C4). Isso corresponde aos limites ótimos alcançados anteriormente por métodos de eliminação de tipos, mas através de uma abordagem distinta baseada em autômatos.
• Robustez a Extensões: Uma contribuição primária é demonstrar a "robustez" da abordagem de autômatos de restrição. Os autores mostram que a tradução pode ser adaptada suavemente para incluir:
  • Papéis Inversos: Estendendo para $\mathcal{ALCI}(\mathcal{D})$ (sem nominais) ao introduzir "abstrações de pai" para lidar com arestas retroativas.
  • Nomes de Papéis Funcionais: Estendendo para $\mathcal{ALCOF}(\mathcal{D})$ ao modificar a função de rotulagem de ramificação para impor restrições funcionais.
  • Asserções de Restrição: Permitindo restrições arbitrárias entre atributos concretos de indivíduos nomeados na ABox.
• Condições Relaxadas para Domínios Concretos: O framework acomoda domínios concretos com conjuntos infinitos de relações (por exemplo, $(\mathbb{Q}, <, (=q)_{q \in \mathbb{Q}})$), desde que satisfaçam a propriedade de completude ou propriedades de amalgamação/compactação. Isso contrasta com trabalhos anteriores que frequentemente exigiam conjuntos de relações finitos ou condições JEPD (Conjuntamente Exaustivas e Parcialmente Disjuntas).
• Tratamento de Domínio Inteiro: O artigo aborda o domínio concreto dos inteiros $(\mathbb{Z}, <, =)$, que não satisfaz a propriedade de completude padrão. Aproveitando resultados de [DQ25] sobre TGCA sem restrições de irmãos, os autores mostram que $\mathcal{ALCO}(\mathbb{Z})$ também é $\text{ExpTime}$-completo.

Resultados

• Teorema 3.6: O problema da não-vacuidade para TGCA sobre um domínio $\mathcal{D}$ que satisfaz (C1), (C2) e (C3.1) está em $\text{ExpTime}$.
• Teorema 4.5: O problema da consistência para $\mathcal{ALCO}(\mathcal{D})$ está em $k$-$\text{ExpTime}$ se $\mathcal{D}$ satisfizer (C1)–(C4) e o CSP($\mathcal{D}$) estiver em $k$-$\text{ExpTime}$.
• Teoremas 5.1 & 5.5: Os problemas de consistência para $\mathcal{ALCOF}(\mathcal{D})$ e $\mathcal{ALCI}(\mathcal{D})$ (sem nominais) mantêm os mesmos limites de complexidade da lógica base.
• Teorema 5.6: O problema da consistência para $\mathcal{ALCO}(\mathbb{Z})$ é $\text{ExpTime}$-completo.

Significado e Alegações
Os autores alegam que seu trabalho fornece uma alternativa robusta e versátil aos métodos de tableau e eliminação de tipos para raciocinar sobre DLs com domínios concretos. Ao utilizar autômatos de restrição enriquecidos com restrições simbólicas, eles alcançam limites de complexidade ótimos enquanto lidam naturalmente com recursos que são frequentemente difíceis de integrar em outros frameworks, como papéis inversos e asserções de restrição.

O artigo enfatiza que a abordagem é "conceitualmente simples" em sua estratégia de redução, mesmo que as provas de correção exijam um trabalho técnico substancial. Ele destaca que o método permite uma análise de complexidade parametrizada, delineando claramente quais propriedades do domínio concreto (por exemplo, completude vs. amalgamação) são necessárias para a decidibilidade e complexidade. Os autores observam modestamente que, embora sua abordagem lide efetivamente com papéis inversos, a combinação de papéis inversos e nominais permanece um problema em aberto, particularmente quando restrições de CD estão envolvidas, pois isso pode levar a um ramificação infinita que as abstrações de estado finito atuais não conseguem capturar.

O trabalho serve como uma versão estendida de um artigo de conferência [DG26], oferecendo uma formalização abrangente da redução baseada em autômatos e suas extensões.