Resumen Técnico: La Complejidad de Definir y Separar Fórmulas de Punto Fijo en la Lógica Modal

1. Planteamiento del Problema

El artículo investiga el problema de la separabilidad modal del cálculo $\mu$-modal ($\mu$ML) con respecto a la lógica modal proposicional (ML). Dada dos fórmulas inconsistentes de $\mu$ML, $\phi$ y $\phi'$, el problema consiste en determinar si existe una fórmula de ML $\psi$ (un "separador") tal que $\phi \models \psi$ y $\psi \models \neg \phi'$.

Este problema generaliza la definibilidad modal: determinar si una fórmula específica de $\mu$ML es equivalente a una fórmula de ML. La definibilidad es el caso especial donde $\phi' = \neg \phi$. El estudio se lleva a cabo sobre diversas clases de modelos relevantes para la informática:

• Modelos arbitrarios (grado de salida sin restricciones).
• Palabras (modelos de grado de salida $\le 1$, denotados como $T_1$).
• Árboles binarios (grado de salida $\le 2$, denotados como $T_2$).
• Árboles de grado de salida acotado $d \ge 3$ (denotados como $T_d$).
• Modelos finitos y palabras infinitas.

Los autores también investigan el problema de existencia del interpolante de Craig (un caso especial de separabilidad donde el separador debe utilizar únicamente los símbolos comunes a $\phi$ y $\phi'$) y la construcción efectiva de los separadores.

2. Metodología

Los autores emplean una combinación de caracterizaciones model-teóricas y técnicas de teoría de autómatas:

• Caracterizaciones Model-Teóricas: El núcleo del procedimiento de decisión se basa en la consistencia conjunta. Dos fórmulas no son separables si y solo si son "conjuntamente consistentes" con respecto a relaciones de bisimilitud específicas. Específicamente, $\phi$ y $\phi'$ no son ML-separables sobre una clase $\mathcal{C}$ si son conjuntamente consistentes con respecto a $(\sigma, n)$-bisimilitudes para todo $n$.

  • Para palabras ($T_1$) y árboles binarios ($T_2$), los autores aprovechan el hecho de que la bisimilitud implica isomorfismo (o puede reducirse a ello) para equiparar la consistencia de la bisimilitud conjunta con la consistencia de isomorfismo conjunta.
  • Para $d \ge 3$, esta equivalencia falla, lo que requiere un análisis más complejo involucrando cocientes de bisimilitud.

• Teoría de Autómatas: El artículo utiliza la conocida correspondencia entre $\mu$ML y Autómatas de Árbol de Paridad No Deterministas (NPTA).

  • Las fórmulas de $\mu$ML se traducen en NPTAs.
  • El problema de verificar la consistencia conjunta se reduce a verificar la intersección de los lenguajes aceptados por estos autómatas.
  • Una herramienta técnica clave es la construcción de autómatas que reconocen cocientes de bisimilitud de los lenguajes aceptados por los autómatas originales. Esto permite a los autores decidir la separabilidad sobre árboles de grado de salida acotado reduciéndolo a la verificación de isomorfismo de estos cocientes.

• Construcción de Separadores: Cuando se establece la separabilidad, los autores proporcionan algoritmos para construir la fórmula separadora. Estas construcciones a menudo implican la generación de consecuencias ML-uniformes de las fórmulas de entrada, que son disyunciones de tipos consistentes con la entrada.

3. Contribuciones Clave y Resultados

3.1. Complejidad de la Separabilidad y la Definibilidad

El artículo establece un panorama de complejidad preciso para la ML-separabilidad y la ML-definibilidad de las fórmulas de $\mu$ML, resumido en la Tabla 1 del documento:

Clase de Modelo	ML-Definibilidad	ML-Separabilidad	Tamaño de Construcción del Separador
Palabras ($T_1$)	PSpace-completo	PSpace-completo	Exponencial simple
Árboles Binarios ($T_2$)	ExpTime-completo	ExpTime-completo	Doble exponencial
Modelos Sin Restricciones	ExpTime-completo	ExpTime-completo	Doble exponencial
Árboles ($T_d, d \ge 3$)	ExpTime-completo	2-ExpTime-completo	Triple exponencial

• Palabras ($T_1$): La separabilidad es PSpace-completa. Este es el caso más sencillo, coincidiendo con la complejidad de la satisfacibilidad de $\mu$ML sobre palabras.
• Árboles Binarios ($T_2$) y Sin Restricciones: La separabilidad es ExpTime-completa. Los autores muestran que las propiedades estructurales de los árboles binarios (donde la bisimilitud implica isomorfismo) permiten un tratamiento algorítmico común con los modelos sin restricciones.
• Árboles con $d \ge 3$: Este es el hallazgo más significativo. Mientras que la ML-definibilidad sigue siendo ExpTime-completa, la ML-separabilidad salta a 2-ExpTime-completo.
  • Los autores demuestran que este aumento en la complejidad no se debe meramente a la codificación de grados de salida superiores en árboles binarios (lo cual preservaría la complejidad).
  • La dificultad surge porque la ML carece de la Propiedad de Interpolación de Craig (CIP) sobre $T_d$ para $d \ge 3$.

3.2. Interpolación de Craig e Existencia de Interpolantes

• Fallo de la CIP: El artículo demuestra que la ML goza de la Propiedad de Interpolación de Craig sobre todos los modelos, palabras y árboles binarios, pero falla sobre árboles de grado de salida $d \ge 3$.
• Existencia de Interpolante: Motivado por el fallo de la CIP, los autores estudian el problema de existencia del interpolante de Craig (¿existe un separador usando solo los símbolos comunes?) para ML sobre $T_d$ ($d \ge 3$). Muestran que este problema es coNExpTime-completo, lo cual es estrictamente más difícil que el problema de validez para ML (que es PSpace-completo sobre estas clases).

3.3. Construcción Efectiva

El artículo proporciona algoritmos para construir separadores cuando existen:

• Palabras: La construcción es posible en tiempo exponencial (óptimo, dado que $\mu$ML es exponencialmente más sucinta que ML sobre palabras).
• Binarios/Sin Restricciones: La construcción es posible en tiempo doble exponencial.
• $d \ge 3$: La construcción es posible en tiempo triple exponencial.
• Los autores señalan que para $d \ge 3$, los separadores construidos se conjeturan como óptimos en tamaño, aunque una cota inferior formal para el tamaño de la construcción permanece abierta.

3.4. Modalidades Graduadas (Estudio de Caso)

Los autores extienden sus resultados a la Lógica Modal Graduada (grML) y al Cálculo $\mu$-Graduado (gr$\mu$ML), que incluyen modalidades que cuentan el número de sucesores (por ejemplo, "al menos $k$ hijos satisfacen...").

• Con Grados en el Separador: Tanto la definibilidad como la separabilidad siguen siendo ExpTime-completo.
• Sin Grados en el Separador:
  • Definibilidad: La ML-definibilidad de las fórmulas de gr$\mu$ML es ExpTime-completo.
  • Separabilidad: La ML-separabilidad de las fórmulas de gr$\mu$ML es 2-ExpTime-completo.
  • Los autores atribuyen la mayor complejidad de la separabilidad (comparada con la definibilidad) al hecho de que los árboles de aridad acotada son definibles en gr$\mu$ML, permitiendo la reducción del caso general $d \ge 3$ al entorno graduado.

4. Significado y Reivindicaciones

El artículo afirma proporcionar una "imagen bastante completa e interesante" de la complejidad de la definibilidad y la separabilidad para las lógicas de punto fijo. Su principal significación radica en:

1. Identificar una Brecha de Complejidad: Es el primer caso conocido en el área de la lógica donde la separabilidad es demostrablemente más difícil que la definibilidad (específicamente, 2-ExpTime vs. ExpTime) para una lógica natural sobre una clase estándar de modelos. Esto contrasta con resultados previos donde la separabilidad era igual o más fácil que la definibilidad.
2. Conectar la Interpolación y la Complejidad: El trabajo establece un vínculo directo entre el fallo de la Propiedad de Interpolación de Craig y el aumento en la complejidad computacional del problema de la separabilidad. Se demuestra que la falta de CIP sobre árboles $d \ge 3$ es la causa raíz de la dificultad 2-ExpTime.
3. Refinar el Panorama de la Lógica Modal: Los resultados aclaran que la complejidad del razonamiento modal no es uniforme a través de las estructuras de árboles; la transición de árboles binarios a ternarios altera fundamentalmente las propiedades lógicas (específicamente la interpolación) y el coste computacional de las tareas de razonamiento como la separabilidad.
4. Resultados Constructivos: Más allá de los procedimientos de decisión, el artículo ofrece construcciones efectivas para los separadores, proporcionando límites sobre el tamaño de estos (por ejemplo, doble exponencial para árboles binarios, triple exponencial para $d \ge 3$).

Los autores concluyen que sus hallazgos resaltan la sutil interacción entre las propiedades estructurales de los modelos (grado de salida), las propiedades lógicas del lenguaje (interpolación) y la complejidad computacional de los problemas de razonamiento. Dejan abiertas las preguntas sobre la optimalidad de los tamaños de los separadores para $d \ge 3$ y la extensión de estos resultados a otros fragmentos u operadores.