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

Resumo Técnico: Autômatos de Conjuntos e Limites da Decidibilidade da Lógica de Duas Variáveis em Palavras de Dados

Enunciado do Problema
O artigo aborda a decidibilidade do problema de satisfatibilidade para extensões da lógica de primeira ordem de duas variáveis ($FO_2$) em palavras de dados. Uma palavra de dados é uma sequência finita de pares $(a_i, d_i)$, onde $a_i$ pertence a um alfabeto finito $\Sigma$ e $d_i$ a um domínio infinito $D$, sendo a igualdade a única propriedade testável em $D$. Embora a lógica $FO_2$ padrão em palavras de dados (com ordem, sucessor e igualdade de dados) seja conhecida por ser decidível (especificamente, $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1]$), os autores investigam os limites da decidibilidade ao estender essa lógica com predicados regulares guardados.

Esses predicados, denotados $eL(x, y)$, são verdadeiros se as posições $x$ e $y$ pertencem à mesma classe de dados (ou seja, $x \sim y$) e o fator da cadeia estritamente entre elas pertence a uma linguagem regular $L$. A questão central é: para quais classes de monoides (ou semigrupos) $M$ que reconhecem a família de linguagens regulares usadas nesses predicados o problema de satisfatibilidade é decidível?

Metodologia
Os autores empregam uma combinação de teoria dos autômatos e teoria algébrica de semigrupos para caracterizar a fronteira da decidibilidade.

1. Autômatos de Conjuntos: Os autores introduzem um novo formalismo de autômatos chamado autômatos de conjuntos. Estes são autômatos de estado finito equipados com um número fixo de conjuntos que podem armazenar valores de dados. As transições permitem:

   • Atualizações locais: Adicionar ou remover o valor de dados atual de conjuntos específicos.
   • Atualizações globais: Aplicar uma relação (ou transformação) ao conteúdo de todos os conjuntos simultaneamente (por exemplo, mover dados do conjunto $X_i$ para $X_j$).
     Os autores estabelecem que os autômatos de conjuntos são expressivamente equivalentes aos autômatos de classe (introduzidos por Bojańczyk e Lasota), um modelo conhecido por ter um problema de vazio indecidível.

2. Subclasses e Decidibilidade: Para recuperar a decidibilidade, os autores definem uma subclasse chamada autômatos de conjuntos quasi-normais ordenados.

   • Quasi-normal: Garante que os valores de dados estejam presentes em, no máximo, um conjunto entre um subconjunto específico de conjuntos "não estáveis".
   • Ordenado: Impõe uma ordem linear nos conjuntos não estáveis, de modo que as atualizações globais esvaziem o conteúdo de um prefixo desses conjuntos e os movam para conjuntos mais altos na ordem.
     O problema de vazio para autômatos de conjuntos quasi-normais ordenados é mostrado como decidível através da redução ao problema de vazio de autômatos de múltiplos contadores ordenados, um problema conhecido por ser decidível.

3. Tradução Lógica para Autômatos: O artigo fornece traduções entre as fórmulas lógicas e os autômatos:

   • Todo autômato de conjuntos pode ser expresso como uma fórmula $EMSO_2$ com predicados regulares guardados.
   • Inversamente, fórmulas usando predicados reconhecidos por um monoide $M$ podem ser traduzidas em autômatos de conjuntos de armazenamento de sufixo (um tipo específico de autômato quasi-normal).

4. Caracterização Algébrica: Os autores analisam a estrutura algébrica dos monoides $M$. Eles definem bandas lineares como monoides idempotentes onde os ideais bilaterais estão linearmente ordenados (ou seja, para quaisquer dois ideais $I, J$, ou $I \subseteq J$ ou $J \subseteq I$).

Principais Contribuições e Resultados

• Teorema Principal (Teorema 6): A satisfatibilidade de fórmulas $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1, \tilde{F}_M]$ sobre palavras de dados é decidível se e somente se o monoide $M$ for uma banda linear.

  • Direção da Decidibilidade: Se $M$ for uma banda linear, os autores constroem um autômato de conjuntos quasi-normal ordenado equivalente. Como o vazio de tais autômatos é decidível, a lógica é decidível.
  • Direção da Indecidibilidade: Se $M$ não for uma banda linear, ele deve conter uma subestrutura isomórfica a $U_1^2$ (o produto direto de dois monoides de dois elementos com zero) ou $N_2$ (um monoide nulo específico). Os autores mostram que predicados regulares guardados reconhecidos por esses monoides específicos permitem a codificação do problema da parada de máquinas de dois contadores, tornando a lógica indecidível.

• Equivalência Expressiva: O artigo prova que os autômatos de conjuntos são expressivamente equivalentes à $EMSO_2$ com predicados regulares guardados. Além disso, mostra que qualquer fórmula com predicados regulares reconhecidos por um monoide $M$ pode ser equivalentemente reescrita usando predicados regulares guardados reconhecidos por outro monoide $M'$ (especificamente, o monoide do conjunto das partes $P(M)$).

• Extensão Estrita: O fragmento decidível identificado é uma extensão estrita da lógica original $FO_2$ de [4]. Por exemplo, a linguagem $L_2$ (que exige nenhum teste de zero entre incrementos e decrementos da mesma classe), que não é definível em $FO_2$ padrão ou em autômatos de dados, torna-se definível nesta lógica estendida quando o monoide subjacente é uma banda linear.

Significado e Alegações
O artigo alega fornecer uma caracterização precisa da fronteira da decidibilidade para a lógica de duas variáveis em palavras de dados estendida com predicados regulares guardados. Ao vincular a decidibilidade lógica à propriedade algébrica do monoide reconhecedor ser uma "banda linear", o trabalho preenche a lacuna entre a expressividade lógica e a estrutura algébrica.

Os autores observam que, embora a decidibilidade para bandas lineares esteja estabelecida, a caracterização para semigrupos gerais permanece aberta. Eles também destacam que a classe de linguagens regulares reconhecidas por bandas lineares não foi extensivamente estudada na literatura, sugerindo a necessidade de maior exploração nesse domínio algébrico. A complexidade dos procedimentos de decisão permanece não elementar, herdada dos resultados subjacentes de $FO_2$ e autômatos de dados.

O trabalho distingue-se das lógicas temporais (como freeze-LTL) ao oferecer uma extensão decidível da lógica de primeira ordem que captura propriedades regulares específicas dentro de classes de dados, que anteriormente eram indecidíveis ou exigiam diferentes frameworks lógicos.