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

Resumen Técnico: Autómatas de Conjuntos y Límites de la Decidibilidad de la Lógica de Dos Variables en Palabras de Datos

Planteamiento del Problema
El artículo aborda la decidibilidad del problema de satisfacibilidad para extensiones de la lógica de primer orden de dos variables ($FO_2$) en palabras de datos. Una palabra de datos es una secuencia finita de pares $(a_i, d_i)$ donde $a_i$ proviene de un alfabeto finito $\Sigma$ y $d_i$ de un dominio infinito $D$, siendo la igualdad la única propiedad comprobable en $D$. Si bien la lógica $FO_2$ estándar en palabras de datos (con orden, sucesor y igualdad de datos) es conocida por ser decidible (específicamente, $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1]$), los autores investigan los límites de la decidibilidad al extender esta lógica con predicados regulares acotados.

Estos predicados, denotados $eL(x, y)$, son verdaderos si las posiciones $x$ e $y$ pertenecen a la misma clase de datos (es decir, $x \sim y$) y el factor de la cadena estrictamente entre ellas pertenece a un lenguaje regular $L$. La pregunta central es: ¿para qué clases de monoides (o semigrupos) $M$ que reconocen la familia de lenguajes regulares utilizados en estos predicados es decidible el problema de satisfacibilidad?

Metodología
Los autores emplean una combinación de la teoría de autómatas y la teoría algebraica de semigrupos para caracterizar la frontera de la decidibilidad.

1. Autómatas de Conjuntos: Los autores introducen un nuevo formalismo de autómatas llamado autómatas de conjuntos. Estos son autómatas de estado finito equipados con un número fijo de conjuntos que pueden almacenar valores de datos. Las transiciones permiten:

   • Actualizaciones locales: Añadir o eliminar el valor de datos actual de conjuntos específicos.
   • Actualizaciones globales: Aplicar una relación (o transformación) al contenido de todos los conjuntos simultáneamente (por ejemplo, mover datos del conjunto $X_i$ al $X_j$).
     Los autores establecen que los autómatas de conjuntos son expresivamente equivalentes a los autómatas de clases (introducidos por Bojańczyk y Lasota), un modelo conocido por tener un problema de vacuidad indecidible.

2. Subclases y Decidibilidad: Para recuperar la decidibilidad, los autores definen una subclase llamada autómatas de conjuntos ordenados cuasi-normales.

   • Casi-normales: Garantiza que los valores de datos estén presentes en como máximo un conjunto entre un subconjunto específico de conjuntos "no estables".
   • Ordenados: Impone un orden lineal sobre los conjuntos no estables tal que las actualizaciones globales vacían el contenido de un prefijo de estos conjuntos y los mueven a conjuntos superiores en el orden.
     El problema de vacuidad para autómatas de conjuntos ordenados cuasi-normales se demuestra decidible reduciéndolo al problema de vacuidad de los autómatas de múltiples contadores ordenados, un problema conocido como decidible.

3. Traducción Lógica-Automática: El artículo proporciona traducciones entre las fórmulas lógicas y los autómatas:

   • Cada autómata de conjuntos puede expresarse como una fórmula $EMSO_2$ con predicados regulares acotados.
   • Inversamente, las fórmulas que utilizan predicados reconocidos por un monoide $M$ pueden traducirse a autómatas de conjuntos de almacenamiento de sufijos (un tipo específico de autómata cuasi-normal).

4. Caracterización Algebraica: Los autores analizan la estructura algebraica de los monoides $M$. Definen bandas lineales como monoides idempotentes donde los ideales bilaterales están ordenados linealmente (es decir, para cualesquiera dos ideales $I, J$, o bien $I \subseteq J$ o bien $J \subseteq I$).

Contribuciones y Resultados Clave

• Teorema Principal (Teorema 6): La satisfacibilidad de fórmulas $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1, \tilde{F}_M]$ sobre palabras de datos es decidible si y solo si el monoide $M$ es una banda lineal.

  • Dirección de Decidibilidad: Si $M$ es una banda lineal, los autores construyen un autómata de conjuntos ordenado cuasi-normal equivalente. Dado que la vacuidad de tales autómatas es decidible, la lógica es decidible.
  • Dirección de Indecidibilidad: Si $M$ no es una banda lineal, debe contener una subestructura isomorfa a $U_1^2$ (el producto directo de dos monoides de dos elementos con cero) o a $N_2$ (un monoide nulo específico). Los autores demuestran que los predicados regulares acotados reconocidos por estos monoides específicos permiten la codificación del problema de la parada de máquinas de dos contadores, haciendo que la lógica sea indecidible.

• Equivalencia Expresiva: El artículo demuestra que los autómatas de conjuntos son expresivamente equivalentes a $EMSO_2$ con predicados regulares acotados. Además, muestra que cualquier fórmula con predicados regulares reconocidos por un monoide $M$ puede reescribirse de manera equivalente utilizando predicados regulares acotados reconocidos por otro monoide $M'$ (específicamente, el monoide de conjuntos de partes $P(M)$).

• Extensión Estricta: El fragmento decidible identificado es una extensión estricta de la lógica original $FO_2$ de [4]. Por ejemplo, el lenguaje $L_2$ (que requiere ninguna prueba de cero entre incrementos y decrementos de la misma clase), que no es definible en $FO_2$ estándar ni en autómatas de datos, se vuelve definible en esta lógica extendida cuando el monoide subyacente es una banda lineal.

Significado y Afirmaciones
El artículo afirma proporcionar una caracterización precisa de la frontera de la decidibilidad para la lógica de dos variables en palabras de datos extendida con predicados regulares acotados. Al vincular la decidibilidad lógica con la propiedad algebraica de que el monoide reconocedor sea una "banda lineal", el trabajo cierra la brecha entre la expresividad lógica y la estructura algebraica.

Los autores señalan que, si bien la decidibilidad para bandas lineales está establecida, la caracterización para semigrupos generales permanece abierta. También destacan que la clase de lenguajes regulares reconocidos por bandas lineales no ha sido estudiada extensamente en la literatura, sugiriendo la necesidad de una mayor exploración en ese dominio algebraico. La complejidad de los procedimientos de decisión sigue siendo no elemental, heredada de los resultados subyacentes de $FO_2$ y autómatas de datos.

El trabajo se distingue de las lógicas temporales (como freeze-LTL) al ofrecer una extensión decidible de la lógica de primer orden que captura propiedades regulares específicas dentro de las clases de datos, las cuales anteriormente eran indecidibles o requerían marcos lógicos diferentes.