Resumo Técnico: A Complexidade de Definir e Separar Fórmulas de Ponto Fixo em Lógica Modal

1. Enunciado do Problema

O artigo investiga o problema da separabilidade modal para o cálculo-$\mu$ modal ($\mu$ML) em relação à lógica modal proposicional (ML). Dada duas fórmulas inconsistentes de $\mu$ML $\phi$ e $\phi'$, o problema questiona se existe uma fórmula de ML $\psi$ (um "separador") tal que $\phi \models \psi$ e $\psi \models \neg \phi'$.

Este problema generaliza a definibilidade modal: determinar se uma fórmula específica de $\mu$ML é equivalente a uma fórmula de ML. A definibilidade é o caso especial onde $\phi' = \neg \phi$. O estudo é conduzido sobre várias classes de modelos relevantes para a ciência da computação:

• Modelos arbitrários (grau de saída irrestrito).
• Palavras (modelos de grau de saída $\le 1$, denotados por $T_1$).
• Árvores binárias (grau de saída $\le 2$, denotadas por $T_2$).
• Árvores de grau de saída limitado $d \ge 3$ (denotadas por $T_d$).
• Modelos finitos e palavras infinitas.

Os autores também investigam o problema da existência do interpolante de Craig (um caso especial de separabilidade onde o separador deve usar apenas os símbolos comuns a $\phi$ e $\phi'$) e a construção efetiva de separadores.

2. Metodologia

Os autores empregam uma combinação de caracterizações de modelos e técnicas de teoria de autómatos:

• Caracterizações de Modelos: O núcleo do procedimento de decisão baseia-se na consistência conjunta. Duas fórmulas não são separáveis se, e somente se, são "conjuntamente consistentes" em relação a relações de bisimilação específicas. Especificamente, $\phi$ e $\phi'$ não são ML-separáveis sobre uma classe $\mathcal{C}$ se forem conjuntamente consistentes em relação a $(\sigma, n)$-bisimulações para todo $n$.

  • Para palavras ($T_1$) e árvores binárias ($T_2$), os autores aproveitam o fato de que a bisimilaridade implica isomorfismo (ou pode ser reduzida a isso) para equiparar a consistência de bisimulação conjunta com a consistência de isomorfismo conjunto.
  • Para $d \ge 3$, essa equivalência falha, exigindo uma análise mais complexa envolvendo quotientes de bisimulação.

• Teoria de Autómatos: O artigo utiliza a conhecida correspondência entre $\mu$ML e Autómatos de Árvore de Paridade Não-Determinísticos (NPTA).

  • Fórmulas de $\mu$ML são traduzidas em NPTAs.
  • O problema de verificar a consistência conjunta é reduzido à verificação da interseção das linguagens aceitas por esses autómatos.
  • Uma ferramenta técnica fundamental é a construção de autómatos que reconhecem quotientes de bisimulação das linguagens aceitas pelos autómatos originais. Isso permite que os autores decidam a separabilidade sobre árvores de grau de saída limitado, reduzindo-a à verificação de isomorfismo desses quotientes.

• Construção de Separadores: Quando a separabilidade é estabelecida, os autores fornecem algoritmos para construir a fórmula separadora. Essas construções frequentemente envolvem a geração de consequências ML-uniformes das fórmulas de entrada, que são disjunções de tipos consistentes com a entrada.

3. Contribuições e Resultados Principais

3.1. Complexidade de Separabilidade e Definibilidade

O artigo estabelece um panorama preciso de complexidade para a ML-separabilidade e ML-definibilidade de fórmulas de $\mu$ML, resumido na Tabela 1 do artigo:

Classe de Modelo	ML-Definibilidade	ML-Separabilidade	Tamanho da Construção do Separador
Palavras ($T_1$)	PSpace-completo	PSpace-completo	Exponencial simples
Árvores Binárias ($T_2$)	ExpTime-completo	ExpTime-completo	Duplo exponencial
Modelos Irrestritos	ExpTime-completo	ExpTime-completo	Duplo exponencial
Árvores ($T_d, d \ge 3$)	ExpTime-completo	2-ExpTime-completo	Triplo exponencial

• Palavras ($T_1$): A separabilidade é PSpace-completa. Este é o caso mais fácil, correspondendo à complexidade da satisfatibilidade de $\mu$ML sobre palavras.
• Árvores Binárias ($T_2$) e Irrestritos: A separabilidade é ExpTime-completa. Os autores mostram que as propriedades estruturais das árvores binárias (onde a bisimilaridade implica isomorfismo) permitem um tratamento algorítmico comum com modelos irrestritos.
• Árvores com $d \ge 3$: Esta é a descoberta mais significativa. Enquanto a ML-definibilidade permanece ExpTime-completa, a ML-separabilidade salta para 2-ExpTime-completo.
  • Os autores demonstram que este aumento de complexidade não se deve meramente ao codificar graus de saída mais altos em árvores binárias (o que preservaria a complexidade).
  • A dificuldade surge porque a ML carece da Propriedade de Interpolação de Craig (CIP) sobre $T_d$ para $d \ge 3$.

3.2. Interpolação de Craig e Existência de Interpolante

• Falha da CIP: O artigo prova que a ML desfruta da Propriedade de Interpolação de Craig sobre todos os modelos, palavras e árvores binárias, mas falha sobre árvores de grau de saída $d \ge 3$.
• Existência de Interpolante: Motivado pela falha da CIP, os autores estudam o problema da existência do interpolante de Craig (existe um separador usando apenas os símbolos comuns?) para ML sobre $T_d$ ($d \ge 3$). Eles mostram que este problema é coNExpTime-completo, o que é estritamente mais difícil que o problema da validade para ML (que é PSpace-completo sobre estas classes).

3.3. Construção Efetiva

O artigo fornece algoritmos para construir separadores quando estes existem:

• Palavras: A construção é possível em tempo exponencial (ótimo, dado que o $\mu$ML é exponencialmente mais sucinto que o ML sobre palavras).
• Binárias/Irrestritos: A construção é possível em tempo duplo exponencial.
• $d \ge 3$: A construção é possível em tempo triplo exponencial.
• Os autores observam que, para $d \ge 3$, os separadores construídos são conjecturados como sendo ótimos em tamanho, embora um limite inferior formal para o tamanho da construção permaneça em aberto.

3.4. Modalidades Graduadas (Estudo de Caso)

Os autores estendem os seus resultados para a Lógica Modal Graduada (grML) e o Cálculo-$\mu$ Graduado (gr$\mu$ML), que incluem modalidades que contam o número de sucessores (ex: "pelo menos $k$ filhos satisfazem...").

• Com Graus no Separador: Tanto a definibilidade quanto a separabilidade permanecem ExpTime-completo.
• Sem Graus no Separador:
  • Definibilidade: A ML-definibilidade de fórmulas de gr$\mu$ML é ExpTime-completo.
  • Separabilidade: A ML-separabilidade de fórmulas de gr$\mu$ML é 2-ExpTime-completo.
  • Os autores atribuem a maior complexidade da separabilidade (comparada à definibilidade) ao fato de que árvores de aridade limitada são definíveis em gr$\mu$ML, permitindo a redução do caso geral $d \ge 3$ para o cenário graduado.

4. Significância e Alegações

O artigo afirma fornecer um "quadro bastante completo e interessante" da complexidade de definibilidade e separabilidade para lógicas de ponto fixo. A sua principal significância reside em:

1. Identificar um Hiato de Complexidade: É o primeiro caso conhecido na área da lógica onde a separabilidade é provadamente mais difícil que a definibilidade (especificamente, 2-ExpTime vs. ExpTime) para uma lógica natural sobre uma classe padrão de modelos. Isto contrasta com resultados anteriores onde a separabilidade era igual ou mais fácil que a definibilidade.
2. Conectar Interpolação e Complexidade: O trabalho estabelece uma ligação direta entre a falha da Propriedade de Interpolação de Craig e o aumento da complexidade computacional do problema de separabilidade. A falta de CIP sobre árvores $d \ge 3$ é mostrada como a causa raiz da dureza 2-ExpTime.
3. Refinar o Panorama da Lógica Modal: Os resultados esclarecem que a complexidade do raciocínio modal não é uniforme através de estruturas de árvores; a transição de árvores binárias para ternárias altera fundamentalmente as propriedades lógicas (especificamente, a interpolação) e o custo computacional de tarefas de raciocínio como a separabilidade.
4. Resultados Construtivos: Além dos procedimentos de decisão, o artigo oferece construções efetivas para separadores, fornecendo limites para o tamanho desses separadores (ex: duplo exponencial para árvores binárias, triplo exponencial para $d \ge 3$).

Os autores concluem que as suas descobertas destacam a interação subtil entre as propriedades estruturais dos modelos (grau de saída), as propriedades lógicas da linguagem (interpolação) e a complexidade computacional dos problemas de raciocínio. Eles deixam em aberto questões relativas à otimalidade do tamanho dos separadores para $d \ge 3$ e a extensão destes resultados para outros fragmentos ou operadores.