Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words

Resumo Técnico: Scoped MSO, Autômatos de Registro e Expressões sobre Palavras de Dados

1. O Problema

A teoria clássica de linguagens regulares sobre alfabetos finitos é caracterizada por uma robusta "trindade" de equivalências: Autômatos Finitos Não Determinísticos (NFA), Expressões Regulares (RE) e Lógica Monádica de Segunda Ordem (MSO). No entanto, ao estender esse modelo para alfabetos infinitos (necessário para modelar identificadores de processos, chaves de banco de dados, ou valores em XML), essa robustez se quebra.

O modelo padrão para palavras de dados (sequências de pares $(label, dado)$) são os Autômatos de Registro Não Determinísticos com Adivinhação (NRAg). Embora os NRAg sejam uma base padrão para linguagens de dados, eles careciam de uma caracterização lógica e expressiva completa análoga ao teorema de Kleene.

• Desafios Específicos:
  • Adicionar fórmulas atômicas de dados à MSO padrão leva à indecidibilidade.
  • Restrições excessivas na lógica (ex: apenas duas variáveis) resultam em poder expressivo insuficiente.
  • A classe NRAg não é fechada sob complemento, o que impõe limitações na negação lógica.
  • Não existe uma única noção de "linguagem regular" para dados que unifique automatos, lógica e expressões de forma elegante.

2. Metodologia e Formalismos Propostos

O autor propõe dois novos formalismos para restaurar a equivalência tríplice para NRAg, focando em restrições sintáticas que limitam a comparação de dados para o que é fisicamente possível com um número finito de registros.

A. Expressões Regulares de Dados (Data-Regular Expressions - DRE)

• Conceito: Uma calculo de expressões minimalista construído sobre regiões livres de quantificadores de palavras de dados.
• Operação Chave: Introduz a concatenação $k$-contratante ($E \cdot_k F$).
  • Diferente da concatenação padrão, esta operação exige que as duas partes da palavra compartilhem uma "interface" de tamanho $k$ (onde $k$ é o número de registros do autômato).
  • Formalmente, $u \in K \cdot_k L$ se $u = vw$, onde existe uma sobreposição $v$ de tamanho $k$ tal que $v \in K$ (com o sufixo) e $v^R \in L$ (com o prefixo revertido).
  • Isso modela a capacidade finita do autômato de transportar dados através de uma "corte" na entrada.
• Iteração: Inclui uma estrela de Kleene parametrizada ($E^{k,*}$) que gera palíndromos de comprimento $2k$ como base para iterações.

B. Lógica MSO Escopada (Scoped MSO - MSOS)

• Conceito: Uma extensão da MSO sobre estruturas de palavras de dados com duas características principais:
  1. Modo de Escopo ($\mathcal{X}\varphi$): Um operador que avalia uma fórmula $\varphi$ em sub-intervalos definidos por um conjunto de posições de corte $X$. Isso permite recursão controlada sobre "intervalos de vida" de registros.
  2. Restrição de Bem-Formação (Well-formedness): Uma restrição sintática crucial em fórmulas atômicas de dados $R(x)$. Uma fórmula é bem-formada se cada átomo de dados contém no máximo uma variável de nível aninhado (nested variable).
     • Variáveis "top-level" são aquelas ligadas por quantificadores existenciais fora do escopo de negações.
     • Variáveis "nested" estão dentro do escopo de negações.
     • Essa restrição impede comparações arbitrárias de dados em posições não relacionadas sob negação, mantendo a lógica dentro da capacidade de registros finitos.

3. Resultados Principais

O artigo estabelece a seguinte equivalência fundamental para alfabetos finitos $\Sigma$ e átomos de dados $\mathcal{A}$:

$$\text{NRAg}[\Sigma, \mathcal{A}] \equiv \text{DRE}[\Sigma, \mathcal{A}] \equiv \text{MSOS}[\langle, \Sigma, \mathcal{A}]$$

Teoremas Chave:

1. Equivalência DRE $\leftrightarrow$ NRAg: A classe de linguagens reconhecidas por NRAg é exatamente a mesma definida por DRE. A prova envolve compilar expressões em autômatos (usando a adivinhação não determinística para a interface $k$) e vice-versa (separando o controle finito da consistência de dados).
2. Equivalência MSOS $\leftrightarrow$ NRAg: A lógica MSOS caracteriza exatamente as linguagens NRAg, sob a condição de que os átomos de dados admitam a eliminação de "adivinhação forte" (strong guessing).
   • Adivinhação Forte: Ocorre quando o autômato introduz um valor de dado fresco que nunca aparece na entrada e permanece em um registro por um intervalo de tempo sem nunca ser igualado a um valor de entrada.
   • Condição de Eliminação: Para átomos como igualdade ($\mathbb{N}, =$) e ordem densa ($\mathbb{Q}, <$), é possível transformar qualquer NRAg em um autômato de "adivinhação fraca" (onde todo valor em um registro aparece na entrada em algum momento).
   • Sob essa condição, a satisfatibilidade de MSOS é decidível se e somente se o problema de vacuidade (emptiness) de NRAg for decidível.

4. Detalhes Técnicos das Provas

• De DRE para NRAg: A construção usa indução estrutural. Para a concatenação $k$-contratante, o autômato adivinha não deterministicamente a palavra de sobreposição de tamanho $k$, armazena seus dados nos registros e depois "reproduz" essa sobreposição (invertida) para sincronizar com o segundo componente da expressão.
• De NRAg para MSOS:
  • O autômato é normalizado para uma forma "simples" (sem embaralhamento de registros).
  • A lógica "adivinha" um esqueleto de execução (rótulos de transição em cada posição).
  • O desafio é verificar as restrições de registros sem violar a bem-formação. A solução usa o operador de escopo $\mathcal{X}$ para dividir a palavra em "intervalos operacionais" baseados nos intervalos de vida dos registros.
  • Dentro de cada intervalo operacional, o autor escolhe existencialmente posições "testemunha" para os valores dos registros. Isso permite que as verificações de dados sejam feitas localmente, garantindo que apenas uma variável aninhada apareça por átomo.
• De MSOS para NRAg: A lógica é compilada para um autômato sobre um alfabeto expandido (multi-track). As variáveis de nível superior são tratadas como pistas auxiliares que carregam valores de testemunha. O operador de escopo é desdobrado em quantificação sobre sub-escopos definidos por MSO, reduzindo o problema a fórmulas localmente testáveis que podem ser reconhecidas por autômatos de 0 registros sobre o alfabeto expandido.

5. Significado e Implicações

• Teoria Descritiva Completa: O trabalho fornece a primeira caracterização lógica e expressiva completa e unificada para autômatos de registro não determinísticos com adivinhação, preenchendo uma lacuna fundamental na teoria de linguagens de dados.
• Decidibilidade: Estabelece condições claras (eliminação de adivinhação forte) sob as quais a satisfatibilidade da lógica MSOS é decidível, conectando diretamente a complexidade da lógica à do problema de vacuidade do autômato.
• Ferramenta para Problemas Abertos: A nova caracterização lógica oferece um novo conjunto de ferramentas para atacar problemas em aberto, como a conjectura de Colcombet sobre a separabilidade de linguagens NRAg por Autômatos de Registro Não Ambíguos.
• Generalização: Os resultados são estendidos para palavras infinitas ($\omega$-words) com condições de aceitação de Büchi, mantendo a equivalência.

Em suma, o artigo demonstra que, com as restrições sintáticas adequadas (escopos e limitação de variáveis aninhadas) e operacionais (interface de tamanho fixo), a rica teoria das linguagens regulares clássicas pode ser restaurada para o domínio de alfabetos infinitos, unificando automatos, lógica e expressões.