Resumo Técnico: Resultados de Decidibilidade para Fragmentos da Lógica de Primeira Ordem via Propriedade de Modelo Simbólico

Declaração do Problema

A lógica de primeira ordem (LPO) é um formalismo poderoso para especificar condições de verificação para sistemas com domínios ilimitados, como aqueles envolvendo listas encadeadas ou estruturas de dados em forma de árvore. No entanto, a LPO é geralmente indecidível. Embora a propriedade de modelo finito (onde toda fórmula satisfatível possui um modelo finito) implique decidibilidade, muitos fragmentos úteis da LPO não possuem essa propriedade; eles podem admitir apenas modelos infinitos. Consequentemente, ferramentas de verificação baseadas em LPO podem falhar ao encontrar contra-modelos para fórmulas inválidas, deixando os usuários sem feedback acionável.

Fragmentos decidíveis existentes, como o fragmento de Fórmulas Estratificadas (SF) (uma variante de muitas ordens de EPR), impõem restrições estritas de aciclicidade em grafos de alternância de quantificadores para garantir a propriedade de modelo finito. Essas restrições são frequentemente excessivamente limitantes para modelar sistemas complexos, exigindo esforço significativo do usuário para adaptar especificações. Este artigo aborda o desafio de estabelecer a decidibilidade para fragmentos de LPO que não desfrutam de uma propriedade de modelo finito, especificamente aqueles que permitem ciclos próprios no grafo de alternância de quantificadores sobre uma ordem específica, desde que certas restrições de teoria da ordem sejam atendidas.

Metodologia

Os autores propõem uma generalização de estruturas simbólicas, originalmente introduzidas em [15] usando Aritmética Linear Inteira (LIA), para teorias base arbitrárias que admitem um modelo padrão.

1. Estruturas Simbólicas Generalizadas

Uma estrutura simbólica é uma representação finita de uma estrutura de primeira ordem potencialmente infinita. Ela consiste em:

• Nós: Um conjunto finito de nós representando subconjuntos do domínio de um modelo padrão de uma teoria base $T$.
• Fórmulas Limitadoras: Cada nó está associado a uma fórmula na linguagem de $T$ que define o conjunto de elementos que ele representa.
• Interpretações Simbólicas: Interpretações de constantes, funções e relações são definidas simbolicamente usando termos e fórmulas de $T$.

A propriedade chave das estruturas simbólicas é que a verificação de modelo (determinar se uma estrutura satisfaz uma fórmula) reduz-se à validade de uma fórmula na teoria base $T$. Se $T$ for decidível, a verificação de modelo para estruturas simbólicas é decidível.

2. A Propriedade de Modelo Simbólico

O artigo estabelece uma propriedade de modelo simbólico para fragmentos específicos da LPO. Um fragmento admite essa propriedade se toda fórmula satisfatível no fragmento tiver uma estrutura simbólica satisfatória sobre uma teoria base decidível. Como a verificação de modelo é decidível para tais estruturas, a existência dessa propriedade implica a decidibilidade do problema de satisfatibilidade do fragmento.

3. A Família de Ciclos Próprios Ordenados (OSC)

Os autores definem uma família de fragmentos chamada Ciclos Próprios Ordenados (OSC), parametrizada por uma axiomatização $\alpha$ de uma relação de ordem estrita $\prec$ sobre uma ordem distinta $s_\infty$.

• Relaxação de SF: O OSC estende o fragmento de Fórmulas Estratificadas ao relaxar o requisito de aciclicidade. Ele permite que símbolos de função introduzam ciclos próprios (laços) sobre a ordem $s_\infty$, desde que o grafo de alternância de quantificadores não contenha outros ciclos.
• Teorias Base: O artigo utiliza duas teorias base primárias:
  • Aritmética Linear Inteira (LIA): Usada para ordens totais.
  • Teoria Decidível de Strings (STR): Usada para ordens de prefixo.

4. Construção da Prova

As provas de decidibilidade seguem uma "receita de prova" genérica que constrói um modelo simbólico $S$ a partir de um modelo arbitrário $M$ de uma fórmula $\phi$. A construção envolve:

1. Particionamento: Dividir o domínio de $M$ em classes de equivalência com base nas fórmulas atômicas que elas satisfazem (átomos). Essas classes tornam-se os nós da estrutura simbólica.
2. Interpretação: Definir as interpretações de constantes, relações unárias e a ordem $\prec$ para "observar" os átomos satisfeitos em $M$.
3. Tratamento de Átomos de Ordem Mista: A dificuldade central reside em satisfazer átomos de ordem mista (por exemplo, $f(x) \prec g(x)$) e os axiomas de ordem $\alpha$. Isso é alcançado definindo formas internas específicas para os nós (nós de resumo) e termos de função dentro da teoria base.
   • Para Ordens Totais (tot), os nós de resumo são modelados como linhas infinitas bidirecionais (inteiros), permitindo "embebidabilidade finita universal" de ordenações de termos.
   • Para Ordens de Prefixo (pref), os nós de resumo são modelados como "árvores universais" (árvores infinitas bidirecionais com fatores de ramificação específicos) para acomodar a natureza não linear das ordens de prefixo.

Contribuições Principais

1. Definição Geral de Estruturas Simbólicas: O artigo fornece uma definição paramétrica de estruturas simbólicas sobre qualquer teoria base com um modelo padrão, generalizando trabalhos anteriores limitados à LIA.
2. Introdução da Família OSC: Define a família de fragmentos Ciclos Próprios Ordenados, que estende as Fórmulas Estratificadas ao permitir ciclos próprios sobre uma ordem ordenada sob axiomas específicos.
3. Novos Resultados de Decidibilidade: Os autores provam a decidibilidade para vários fragmentos novos dentro da família OSC, especificamente:
   • OSC[pref]: Ciclo Próprio Ordenado por Prefixo, usando a teoria de strings. Este fragmento modela alcançabilidade em estruturas de dados em forma de árvore acíclicas e listas encadeadas com compartilhamento.
   • Variantes com Sucessores/Predecessores: Fragmentos combinando ordens totais/prefixo com axiomas garantindo a existência de sucessores (prosucc) ou predecessores (regpred).
4. Framework de Prova Genérico: Apresenta-se uma técnica de prova unificada que constrói modelos simbólicos para esses fragmentos, demonstrando que a satisfatibilidade reduz-se à validade de fórmulas nas respectivas teorias base decidíveis (LIA ou STR).
5. Implementação: Uma ferramenta de prova de conceito que estende a biblioteca de código aberto FEST é implementada para suportar estruturas simbólicas genéricas, incluindo verificação de modelo sobre a teoria de strings.

Resultados

O artigo estabelece que o problema de satisfatibilidade é decidível para os seguintes fragmentos (onde $\alpha$ é o axioma de ordem):

• $\alpha \in \{ \text{tot}, \text{tot} \land \text{prosucc}, \text{tot} \land \text{regpred}, \text{pref}, \text{pref} \land \text{prosucc}, \text{pref} \land \text{regpred} \}$.

O resultado para tot reafirma trabalhos anteriores [15], enquanto os resultados para pref e suas variantes são novos. A decidibilidade de OSC[pref] é particularmente significativa, pois lida com estruturas que não admitem uma propriedade de modelo finito, mas podem ser representadas simbolicamente usando a teoria de strings.

Significado e Alegações

O artigo alega que este trabalho oferece uma nova abordagem para a decidibilidade que vai além da propriedade de modelo finito. Ao utilizar estruturas simbólicas, permite a verificação de sistemas com domínios ilimitados que anteriormente eram intratáveis devido à falta de contra-modelos finitos.

• Impacto Teórico: Preenche a lacuna entre propriedades de modelo finito e representações de modelo infinito, mostrando que a decidibilidade pode ser alcançada mesmo quando modelos infinitos são necessários, desde que possam ser capturados por uma teoria base decidível.
• Relevância Prática: O fragmento OSC[pref] aborda diretamente cenários comuns de verificação envolvendo estruturas de dados em forma de árvore e listas encadeadas com compartilhamento, que são difíceis de modelar em fragmentos estritamente estratificados.
• Generalidade: O framework é projetado para ser extensível a outras teorias base e relações de ordem, sugerindo um caminho para a descoberta de futuros fragmentos decidíveis.

Os autores observam que, embora o procedimento de decisão reduza a satisfatibilidade à validade de fórmulas na teoria base (que pode ser não elementar para teorias de strings), a contribuição principal é o estabelecimento da decidibilidade e a capacidade de gerar contra-modelos simbólicos quando a verificação falha. A implementação serve como uma prova de conceito para a viabilidade dessa abordagem.