Resumo Técnico: Kofola 1.0 – Uma Abordagem Modular para Complementação e Verificação de Inclusão ω-Regulares

Declaração do Problema

A verificação de inclusão de linguagens para autômatos de Büchi (ABs) é um problema fundamental na verificação baseada em teoria dos autômatos, com aplicações críticas em verificação de modelos, monitoramento e prova de teoremas. O problema é completo em PSpace e permanece computacionalmente exigente à medida que as especificações do sistema aumentam em tamanho e complexidade. Decidir se $L_1 \subseteq L_2$ reduz-se a verificar a vacuidade de $L_1 \cap \overline{L_2}$, onde $\overline{L_2}$ é o complemento de $L_2$. Esta redução apresenta dois desafios principais:

1. Complementação Compacta: Construir o autômato complemento $\overline{L_2}$ de forma eficiente sem causar uma explosão no espaço de estados.
2. Exploração Eficiente: Explorar o autômato produto de $L_1 \cap \overline{L_2}$, que frequentemente é enorme.

As ferramentas existentes dependem largamente de construções de complementação clássicas baseadas em Ramsey ou em determinização, datando de mais de três décadas. Embora existam avanços recentes em complementação, eles não foram totalmente integrados em verificadores de inclusão práticos.

Metodologia

O artigo apresenta o Kofola, uma ferramenta eficiente implementada em C++ que executa um framework de complementação modular de última geração. A metodologia baseia-se na decomposição do autômato de entrada em componentes fortemente conexos (CFCs) e na aplicação de algoritmos de complementação adaptados a cada componente com base em suas propriedades estruturais.

1. Decomposição Estrutural e Classificação de Componentes

O Kofola realiza uma análise estrutural de alta granularidade do autômato a ser complementado ($A_2$). Ele classifica seus CFCs maximais em quatro categorias distintas:

• Componentes não-aceitantes: Tratados via construção de subconjuntos tradicional.
• Componentes Aceitantes Intrinsecamente Fracos (IWACs): Componentes onde todos os ciclos aceitam.
• Componentes Aceitantes Determinísticos (DACs): Componentes com apenas transições determinísticas.
• Componentes Aceitantes Inicialmente Quase Determinísticos (IADACs): Um novo tipo de componente identificado neste artigo. São CFCs determinísticos alcançáveis a partir de estados iniciais via CFCs determinísticos, permitindo não-determinismo apenas em caminhos sem ciclos entre CFCs.
• Componentes Aceitantes Não-Determinísticos (NACs): Os CFCs aceitantes restantes.

2. Framework Modular de Complementação

Para cada tipo de componente, o Kofola aplica um algoritmo de complementação parcial dedicado:

• IWACs: Utiliza a construção clássica de Miyano-Hayashi, gerando uma condição de aceitação $Inf(1)$.
• DACs: Utiliza uma modificação do algoritmo NCSB, gerando uma condição de aceitação $Inf(2)$.
• NACs: Suporta duas abordagens dependendo da tarefa:
  • Complementação: Utiliza uma abordagem baseada em determinização (variante de Safra-Piterman) para produzir autômatos menores.
  • Verificação de Inclusão: Utiliza uma abordagem baseada em fatias (slice-based), mais adequada para testes de vacuidade de produto sob demanda (on-the-fly).
• IADACs: O artigo introduz um novo algoritmo parcial para estes componentes. Ele determiniza os IADACs usando uma construção de subconjuntos e emite uma marca de rejeição ($Fin(0)$) sempre que uma execução rastreada observa uma transição aceitadora. A correção baseia-se no fato de que as execuções em IADACs são limitadas devido ao seu não-determinismo restrito.

O algoritmo de nível superior sincroniza essas construções parciais. O autômato complemento resultante é um Autômato Rabin Generalizado Simples (SGRA) com uma única condição de aceitação da forma $Fin(0) \land Inf(1) \land \dots \land Inf(k-1)$.

3. Verificação de Vacuidade Sob Demanda (On-the-Fly)

Para abordar a explosão do espaço de estados na verificação de inclusão, o Kofola emprega um novo algoritmo de verificação de vacuidade sob demanda para o SGRA resultante.

• Construção Preguiçosa (Lazy): Diferentemente de ferramentas que exigem a construção explícita do autômato produto completo, o Kofola explora o espaço de estados de forma preguiçosa.
• Algoritmo: O algoritmo é uma variante do algoritmo de Couvreur estendida com um predicado $Fin$. Ele realiza uma busca em profundidade, gerenciando uma pilha de conjuntos de transições para detectar CFCs.
• Terminação: A busca termina assim que o espaço de estados explorado for suficiente para decidir o resultado (seja encontrando um ciclo aceitador ou provando a vacuidade). Isso minimiza a parte gerada do complemento, o que é crucial, pois a complementação é a principal fonte de explosão.

Principais Contribuições

1. Ferramenta Kofola: Uma ferramenta eficiente e modular para complementação de ABs e verificação de inclusão de linguagens.
2. Identificação de IADACs: A introdução e formalização de Componentes Aceitantes Inicialmente Quase Determinísticos (IADACs) como uma classe estrutural distinta.
3. Novo Algoritmo de Complementação: Um algoritmo parcial dedicado para IADACs que gera a condição $Fin(0)$, permitindo a construção de um único par Rabin generalizado.
4. Verificação de Vacuidade Preguiçosa: Um novo algoritmo sob demanda para SGRAs que evita a construção explícita do autômato completo, permitindo terminação antecipada.
5. Framework Modular: Uma arquitetura flexível que permite a combinação síncrona de diferentes algoritmos parciais com base na análise estrutural.

Resultados Experimentais

Os autores avaliaram o Kofola contra ferramentas de última geração: Spot, Ranker, Owl, Bait, Forklift e Rabit.

Benchmarks de Complementação

• Conjunto de Dados: 31.273 autômatos de diversas fontes (terminação de programas, lógica de palavras de Sturmian, hiperpropriedades, S1S, tradução de LTL e geração aleatória).
• Robustez: O Kofola foi a única ferramenta a complementar com sucesso todos os 31.273 autômatos de entrada. A próxima ferramenta mais robusta, o Spot, falhou em 2 instâncias devido a limites de memória.
• Tamanho: O Kofola produziu autômatos complemento significativamente menores em média (79,24 estados) em comparação com o Spot (115,38 estados) e o Ranker (45,80 estados, embora o Ranker tenha falhado em 443 instâncias).
• Desempenho: O Kofola resolveu o maior número de instâncias e frequentemente superou os concorrentes em várias ordens de magnitude no tempo de execução.

Benchmarks de Verificação de Inclusão

• Conjunto de Dados: 1.014 problemas de inclusão provenientes de terminação de programas, verificação de sistemas concorrentes, verificação de modelos de hiperpropriedades e prova de teoremas.
• Desempenho: O Kofola resolveu o maior número de instâncias (apenas 2 não resolvidas) e teve o menor tempo total de execução (141 segundos para problemas resolvidos).
• Comparação: O Kofola venceu estritamente o Spot(Det) em 263 instâncias e perdeu em apenas 0. Superou significativamente as ferramentas baseadas em Ramsey (Bait, Forklift, Rabit), que frequentemente exigiram uma ordem de magnitude mais de tempo.
• Observação: 98% dos autômatos no lado direito das consultas de inclusão (aqueles sendo complementados) eram autômatos de elevador (não contendo NACs), destacando a relevância prática de explorar propriedades estruturais.

Significado e Alegações

O artigo afirma que o Kofola estabelece um novo padrão de eficiência e robustez na complementação de ABs e na verificação de inclusão. Seu significado reside em:

• Praticidade: Traz técnicas modernas de complementação baseadas em decomposição para a verificação de inclusão prática, indo além das construções clássicas.
• Escalabilidade: Ao combinar decomposição estrutural com verificação de vacuidade preguiçosa sob demanda, mitiga efetivamente a explosão do espaço de estados, resolvendo instâncias que são intratáveis para ferramentas existentes.
• Extensibilidade: A arquitetura modular permite a integração de novos algoritmos de complementação parcial para tipos específicos de componentes.

Os autores posicionam o Kofola não meramente como uma melhoria incremental, mas como uma ferramenta altamente competitiva que frequentemente supera soluções de última geração em várias ordens de magnitude em benchmarks derivados de aplicações práticas.