Robustness of Constraint Automata for Description Logics with Concrete Domains

Resumen Técnico: Robustez de los Autómatas de Restricciones para Lógicas de Descripción con Dominios Concretos

Planteamiento del Problema
El artículo aborda el problema de la consistencia para las Lógicas de Descripción (DL) con dominios concretos, centrándose específicamente en la lógica $\mathcal{ALCO}(\mathcal{D})$. Esta lógica extiende $\mathcal{ALC}$ con nominales, roles inversos (en extensiones) y dominios concretos $\mathcal{D}$ que permiten el razonamiento sobre objetos concretos (por ejemplo, números, intervalos) mediante relaciones predefinidas. Si bien la decidibilidad para tales lógicas ha sido establecida utilizando métodos basados en el tableau o de eliminación de tipos (por ejemplo, [LM07]), trabajos recientes [BDK24, BBDK25] han refinado los límites de complejidad a $\text{ExpTime}$ para clases específicas de dominios concretos. Sin embargo, estos resultados a menudo dependen de condiciones restrictivas (por ejemplo, conjuntos finitos de relaciones, condiciones JEPD) o técnicas específicas que pueden no generalizarse fácilmente a características adicionales de DL como los roles inversos o las aserciones de restricciones. Los autores investigan si un enfoque basado en autómatas puede lograr límites superiores óptimos de $\text{ExpTime}$ manteniendo la robustez frente a la adición de características complejas y relajando ciertas restricciones sobre el dominio concreto.

Metodología
Los autores proponen un procedimiento de decisión basado en autómatas que reduce el problema de la consistencia de $\mathcal{ALCO}(\mathcal{D})$ al problema de la no vaciedad de los Autómatas de Restricciones Globales de Árbol (TGCA).

1. Definición de Autómatas de Restricciones: El mecanismo central es un TGCA, que acepta árboles de datos infinitos donde los nodos están etiquetados con tuplas de valores del dominio concreto $\mathcal{D}$. Las transiciones en estos autómatas están enriquecidas con restricciones simbólicas (combinaciones booleanas de predicados) que relacionan los valores en un nodo con los de sus hijos.
2. Reducción a Autómatas de Árbol Büchi (BTA): Para analizar la complejidad de la no vaciedad de los TGCA, los autores construyen una reducción a los estándares Autómatas de Árbol Büchi. Esto implica:
   • Tipos Simbólicos: Abstraer los valores concretos en "tipos simbólicos" (conjuntos de literales sobre registros) que capturan todas las restricciones atómicas relevantes.
   • Compatibilidad de Proyección: Asegurar la coherencia entre el tipo simbólico de un nodo padre y sus hijos.
   • Propiedades de $\mathcal{D}$: La reducción depende de propiedades específicas del dominio concreto $\mathcal{D}$, específicamente la propiedad de completitud (o alternativamente, la propiedad de amalgamación combinada con la $\omega$-compacidad de homomorfismo), la aridad acotada de los predicados y la decidibilidad del Problema de Satisfacción de Restricciones (CSP) para $\mathcal{D}$.
3. Manejo de Ontologías: Los autores diseñan un TGCA específico para modelar la consistencia de una ontología (TBox y ABox). El autómata gestiona:
   • Nominales: Mediante el uso de abstracciones globales que persisten a lo largo de la ejecución para rastrear la interpretación de nombres individuales.
   • Características Concretas: Utilizando registros para almacenar valores de características y aplicar restricciones entre ellos.
   • Estructuras de Bosque: Codificando las estructuras de bosque típicas de las DL con ABoxes en una única estructura de árbol aceptada por el autómata.

Contribuciones Clave

• Complejidad Óptima vía Autómatas: El artículo establece que el problema de la consistencia para $\mathcal{ALCO}(\mathcal{D})$ está en $\text{ExpTime}$ (o $k\text{-}\text{ExpTime}$ dependiendo de la complejidad del CSP de $\mathcal{D}$) bajo las condiciones (C1)–(C4). Esto coincide con los límites óptimos alcanzados previamente por métodos de eliminación de tipos, pero a través de un enfoque distinto basado en la teoría de autómatas.
• Robustez ante Extensiones: Una contribución primaria es demostrar la "robustez" del enfoque de autómatas de restricciones. Los autores muestran que la traducción puede adaptarse suavemente para incluir:
  • Roles Inversos: Extensión a $\mathcal{ALCI}(\mathcal{D})$ (sin nominales) mediante la introducción de "abstracciones de padre" para manejar las aristas hacia atrás.
  • Nombres de Roles Funcionales: Extensión a $\mathcal{ALCOF}(\mathcal{D})$ modificando la función de etiquetado de ramificación para imponer restricciones funcionales.
  • Aserciones de Restricciones: Permitir restricciones arbitrarias entre características concretas de individuos nombrados en la ABox.
• Condiciones Relajadas en Dominios Concretos: El marco acomoda dominios concretos con conjuntos infinitos de relaciones (por ejemplo, $(\mathbb{Q}, <, (=q)_{q \in \mathbb{Q}})$), siempre que satisfagan la propiedad de completitud o las propiedades de amalgamación/compacidad. Esto contrasta con trabajos previos que a menudo requerían conjuntos de relaciones finitos o condiciones JEPD (Conjuntamente Exhaustivas y Parejamente Disjuntas).
• Manejo de Dominios Enteros: El artículo aborda el dominio concreto de los enteros $(\mathbb{Z}, <, =)$, el cual no satisface la propiedad de completitud estándar. Aprovechando los resultados de [DQ25] respecto a los TGCA sin restricciones de hermanos, los autores demuestran que $\mathcal{ALCO}(\mathbb{Z})$ también es $\text{ExpTime}$-completo.

Resultados

• Teorema 3.6: El problema de la no vaciedad para TGCA sobre un dominio $\mathcal{D}$ que satisface (C1), (C2) y (C3.1) está en $\text{ExpTime}$.
• Teorema 4.5: El problema de la consistencia para $\mathcal{ALCO}(\mathcal{D})$ está en $k\text{-}\text{ExpTime}$ si $\mathcal{D}$ satisface (C1)–(C4) y el CSP($\mathcal{D}$) está en $k\text{-}\text{ExpTime}$.
• Teoremas 5.1 y 5.5: Los problemas de consistencia para $\mathcal{ALCOF}(\mathcal{D})$ y $\mathcal{ALCI}(\mathcal{D})$ (sin nominales) mantienen los mismos límites de complejidad que la lógica base.
• Teorema 5.6: El problema de la consistencia para $\mathcal{ALCO}(\mathbb{Z})$ es $\text{ExpTime}$-completo.

Significado y Reivindicaciones
Los autores afirman que su trabajo proporciona una alternativa robusta y versátil a los métodos basados en el tableau y de eliminación de tipos para el razonamiento sobre DL con dominios concretos. Al utilizar autómatas de restricciones enriquecidos con restricciones simbólicas, logran límites de complejidad óptimos mientras manejan naturalmente características que suelen ser difíciles de integrar en otros marcos, como los roles inversos y las aserciones de restricciones.

El artículo enfatiza que el enfoque es "conceptualmente simple" en su estrategia de reducción, incluso si las pruebas de corrección requieren un trabajo técnico sustancial. Destaca que el método permite un análisis de complejidad parametrizado, delineando claramente qué propiedades del dominio concreto (por ejemplo, completitud vs. amalgamación) son necesarias para la decidibilidad y la complejidad. Los autores señalan modestamente que, aunque su enfoque maneja los roles inversos eficazmente, la combinación de roles inversos y nominales sigue siendo un problema abierto, particularmente cuando se involucran restricciones de CD, ya que esto puede conducir a una ramificación infinita que las abstracciones de estado finito actuales no pueden capturar.

El trabajo sirve como una versión extendida de un artículo de conferencia [DG26], ofreciendo una formalización exhaustiva de la reducción basada en autómatas y sus extensiones.