Resumo Técnico: Um Procedimento de Decisão para uma Teoria de Conjuntos Finitos com Intervalos Inteiros Finitos

Declaração do Problema

No contexto da verificação e análise formais, ferramentas de raciocínio automatizado são essenciais para descarregar condições de verificação. Embora as ferramentas existentes baseadas na teoria dos conjuntos (por exemplo, B, ProB) sejam eficazes, elas frequentemente carecem de procedimentos de decisão para fragmentos específicos da teoria dos conjuntos que combinam conjuntos finitos com intervalos inteiros. Especificamente, a álgebra booleana de conjuntos finitos estendida com restrições de cardinalidade (denotada como $L|\cdot|$) é decidível, mas não pode expressar ou raciocinar nativamente sobre intervalos inteiros finitos (intervalos) onde os limites podem ser variáveis ilimitadas. Esta limitação impede a verificação automática de propriedades envolvendo operações de conjuntos, como encontrar o mínimo ou máximo de um conjunto, particionar conjuntos com base em limiares inteiros ou raciocinar sobre domínios de arrays definidos por intervalos. O problema central abordado é a decidibilidade de uma teoria que integra conjuntos finitos, restrições de cardinalidade e intervalos inteiros finitos (denotada como $L[\ ]$) dentro de uma lógica livre de quantificadores.

Metodologia

Os autores propõem um procedimento de decisão, SAT $[\ ]$, que estende o solucionador existente SAT $|\cdot|$ (para $L|\cdot|$) para lidar com intervalos inteiros. A metodologia baseia-se numa teoria base de conjuntos finitos hereditários implementada na linguagem de Programação Lógica com Restrições (CLP) CLP($SET$) e na ferramenta {log}.

Componentes Técnicos Chave:

1. Extensão da Linguagem ($L[\ ]$):

   • A linguagem é estendida para incluir termos de conjunto da forma $[k, m]$, representando o conjunto $\{p \in \mathbb{Z} \mid k \le p \le m\}$.
   • Os limites do intervalo ($k, m$) podem ser termos lineares inteiros, incluindo variáveis.
   • A lógica permanece livre de quantificadores, utilizando conjunções e disjunções de restrições envolvendo pertinência a conjuntos, união, disjunção, cardinalidade e pertinência a intervalos.

2. Identidade Central e Estratégia de Redução:

   • A principal insight teórica é a identidade: $k \le m \implies (A = [k, m] \iff A \subseteq [k, m] \land |A| = m - k + 1)$.
   • Esta identidade permite que o procedimento transforme restrições envolvendo igualdade com um intervalo em restrições envolvendo relações de subconjunto e cardinalidade.
   • O solucionador reescreve fórmulas numa conjunção de uma fórmula padrão $L|\cdot|$ ($\Phi_{|\cdot|}$) e um conjunto de restrições de subconjunto envolvendo intervalos ($\Phi_{\subseteq[\ ]}$), tipicamente da forma $X \subseteq [p, q]$ onde $X$ é uma variável.

3. O Algoritmo SAT $[\ ]$:

   • Regras de Reescrita: O solucionador emprega um conjunto de regras de reescrita (STEPS$[\ ]$) que reduzem a complexidade sintática. Estas regras lidam com igualdade, pertinência, união, disjunção e restrições de cardinalidade envolvendo intervalos.
   • Redução para Aritmética Inteira: Muitas regras reescrevem restrições de conjuntos envolvendo intervalos diretamente em restrições de aritmética linear inteira (LIA).
   • Verificação da Solução Mínima: Quando restrições irredutíveis da forma $X \subseteq [p, q]$ permanecem, o procedimento não falha simplesmente. Em vez disso, aproveita a propriedade de que, se uma fórmula é satisfatível, deve ter uma "solução mínima" (uma solução onde os conjuntos têm a cardinalidade possível mínima).
     • O solucionador calcula a solução mínima para a parte $L|\cdot|$ ($\Phi_{|\cdot|}$).
     • Em seguida, verifica se esta solução mínima satisfaz as restrições de intervalo ($\Phi_{\subseteq[\ ]}$).
     • Os autores provam que, se nenhuma solução mínima satisfizer a fórmula completa, então nenhuma solução maior também o fará, tornando a fórmula insatisfatível.

4. Implementação em {log}:

   • O procedimento é implementado em {log} (setlog), uma ferramenta baseada em Prolog.
   • A implementação inclui um esquema de memorização para rastrear substituições de variáveis para intervalos, prevenindo reescrita redundante e melhorando a eficiência.
   • Restrições derivadas (por exemplo, interseção, diferença) são definidas em termos de restrições primitivas para manter a consistência.

Contribuições Chave

1. Prova de Decidibilidade: O artigo fornece a primeira prova de que a álgebra booleana de conjuntos finitos estendida com restrições de cardinalidade e intervalos inteiros finitos ($L[\ ]$) é decidível.
2. Procedimento de Decisão (SAT $[\ ]$): É apresentado um algoritmo completo que decide a satisfatibilidade de fórmulas $L[\ ]$. O procedimento é provado ser correto, completo e terminante.
3. Integração de Intervalos e Conjuntos: Ao contrário de abordagens que tratam intervalos como um domínio separado ou exigem limites constantes, este trabalho integra perfeitamente intervalos inteiros com limites variáveis na teoria dos conjuntos, permitindo a expressão de operadores não triviais (por exemplo, o $i$-ésimo elemento menor, particionamento por um limiar) numa lógica livre de quantificadores.
4. Implementação e Ferramentas: O procedimento de decisão é implementado como uma extensão da ferramenta {log}, fornecendo uma capacidade dual como linguagem de programação lógica com restrições e solucionador de satisfatibilidade.

Resultados e Avaliação

O artigo apresenta evidências empíricas e um estudo de caso para demonstrar a utilidade prática da abordagem:

• Avaliação de Benchmarks: Um conjunto de 60 fórmulas $L[\ ]$, representando propriedades de operadores definidos no artigo (por exemplo, mínimo, máximo, $i$-ésimo elemento), foi resolvido. O {log} resolveu todos os problemas numa média de 0,51 segundos por problema, com apenas um levando mais de 5 segundos.
• Estudo de Caso (Algoritmo de Elevador): Os autores modelaram um sistema de controle de elevador onde o elevador deve atender a pedidos numa direção específica. O modelo utilizou intervalos inteiros para definir pisos e pedidos.
  • O sistema incluiu 7 operações (por exemplo, adicionar pedidos, atender ao próximo pedido).
  • O {log} foi utilizado para descarregar automaticamente 49 lemas de invariância (provando que as operações de estado preservam 7 invariantes de estado) e 7 verificações de estado inicial.
  • Todas as provas foram concluídas em aproximadamente 0,5 segundos num laptop padrão.
  • A ferramenta gerou com sucesso contraexemplos quando os invariantes foram intencionalmente enfraquecidos, demonstrando as suas capacidades de depuração.

Significado e Alegações

Os autores afirmam que este trabalho representa um passo significativo para a frente no raciocínio automatizado para verificação formal. Ao estender o fragmento decidível da teoria dos conjuntos para incluir intervalos inteiros finitos com limites variáveis, a abordagem permite a verificação automática de propriedades que anteriormente eram difíceis ou impossíveis de expressar sem quantificadores.

O artigo enfatiza que a abordagem está enraizada na teoria dos conjuntos, distinguindo-a de outras ferramentas de raciocínio sobre intervalos (como aquelas baseadas na álgebra de intervalos de Allen ou reticulados de análise estática) que frequentemente carecem da capacidade de combinar intervalos com operações gerais de conjuntos. A integração do raciocínio sobre intervalos no framework {log} permite aos utilizadores escrever programas e provar as suas propriedades utilizando o mesmo código e ferramenta, aproveitando a dualidade entre fórmula e programa. Os autores notam modestamente que, embora a abordagem seja geral e coerente, pode incorrer em custos de eficiência em comparação com solucionadores especializados para problemas específicos apenas de intervalos, mas o compromisso é a capacidade de raciocinar sobre estruturas híbridas complexas de conjuntos-intervalos.