Resumo Técnico: Complementação de Autômatos de Emerson-Lei do tipo Elevador

Declaração do Problema

A complementação de $\omega$-autômatos é uma operação fundamental em métodos formais, essencial para tarefas como análise de terminação de programas, model checking de lógicas temporais (ex: LTL, HyperLTL) e decisão de teorias lógicas (ex: S1S). No entanto, complementar $\omega$-autômatos genéricos é notoriamente difícil, resultando frequentemente em uma explosão do espaço de estados que torna a verificação prática inviável.

Embora restrições estruturais como "autômatos de elevador" (onde cada componente fortemente conexo é ou determinístico ou inerentemente fraco) tenham demonstrado permitir uma complementação mais eficiente para autômatos de Büchi padrão, essas otimizações não foram totalmente estendidas a autômatos com condições de aceitação mais ricas. Os autômatos de Emerson-Lei (ELAs), que suportam combinações booleanas arbitrárias de predicados Inf (infinitamente muitas vezes) e Fin (finitamente muitas vezes), oferecem maior concisão e flexibilidade, mas atualmente carecem de algoritmos de complementação eficientes que considerem a estrutura. Os algoritmos existentes para ELAs não restritos sofrem de alta complexidade assintótica, e há uma lacuna em métodos práticos para complementar ELAs que exibem a estrutura de "elevador" frequentemente encontrada em aplicações do mundo real.

Metodologia

O artigo introduz os Autômatos de Elevador de Emerson-Lei (ELEAs), uma generalização dos autômatos de elevador de Büchi para o framework de aceitação de Emerson-Lei. Os autores propõem um novo algoritmo de complementação que aproveita as propriedades estruturais dos ELEAs para alcançar limites de complexidade significativamente melhores do que a complementação de ELAs genéricos.

A metodologia procede em três estágios principais:

1. Autômatos Semi-Determinísticos (ELSAs) com Condições Específicas:
   Os autores abordam primeiro a complementação de Autômatos Semi-Determinísticos de Emerson-Lei (ELSAs), onde as execuções eventualmente entram em um componente determinístico. Eles desenvolvem construções para dois casos específicos:

   • Pares de Rabin Generalizados: O algoritmo combina a construção de Miyano-Hayashi (para condições Fin) e o algoritmo NCSB (para condições Inf). Ele utiliza uma estrutura de macroestado $(N, R, C, S_1, \dots, S_k, B)$ para rastrear execuções na parte não-determinística ($N$) e na parte determinística. A parte determinística é dividida em conjuntos que rastreiam violações de Fin ($R$) e violações de Inf ($C$ e conjuntos seguros $S_i$). Um conjunto de breakpoint global $B$ garante que todas as execuções sejam inspecionadas infinitamente muitas vezes.
   • Pares de Streett Generalizados: Como um dual ao caso de Rabin, esta construção utiliza um contador de escalonamento round-robin ($z$) para invalidar sequencialmente todas as condições no par de Streett. Ela reutiliza conjuntos entre uma instância de NCSB (para a condição Inf) e múltiplas instâncias de Miyano-Hayashi (para condições Fin).

2. Procedimento Indutivo para Condições de Emerson-Lei Arbitrárias:
   Para lidar com combinações booleanas arbitrárias de Inf e Fin, os autores introduzem uma abordagem de tree-macrostate (macroestado em árvore). A condição de aceitação negada $\psi = \neg Acc$ é representada como uma árvore que espelha sua estrutura sintática.

   • Modo de Amostragem (Sampling Mode): Execuções que entram no componente determinístico são atribuídas não-deterministicamente a subárvores correspondentes aos disjuntos de $\psi$.
   • Modo de Verificação (Checking Mode): O algoritmo verifica se as execuções satisfazem as subfórmulas atribuídas. Para condições Inf, utiliza conjuntos de breakpoint para garantir visitas infinitas; para condições Fin, garante que as execuções evitem cores específicas.
   • Otimizações: O artigo detalha várias otimizações para reduzir a explosão do espaço de estados:
     • Normalização de Tree-Macrostate: Fusão de rastreamento de execução redundante quando as execuções se fundem.
     • Otimização de Breakpoint Compartilhado: Uso de um único breakpoint compartilhado para múltiplos nós folha Inf via escalonamento round-robin.
     • Otimização OR-FIN: Propagação sequencial de estados violadores através de folhas Fin em disjunções para evitar ramificação exponencial.

3. Extensão para Autômatos de Elevador Completos e Não Restritos:
   As técnicas desenvolvidas para ELSAs são estendidas para ELEAs completos. Os autores observam que, na prática, muitos autômatos não-elevador são "quase elevadores" (contendo apenas alguns componentes fortemente conexos não-elevador). Sua conversão trata esses casos de forma eficiente, aproveitando o fato de que a maioria dos componentes fortemente conexos em autômatos práticos já são componentes de elevador.

Contribuições Principais e Resultados

• Definição de ELEAs: O artigo define formalmente os Autômatos de Elevador de Emerson-Lei, generalizando o conceito de autômatos de elevador para condições de aceitação ricas.
• Melhoria nos Limites de Complexidade: O algoritmo proposto alcança uma complexidade de espaço de estados assintótica significativamente menor para o complemento de um ELEA em comparação com os melhores algoritmos conhecidos para ELAs não restritos.
  • Para um par de Rabin generalizado com $k$ pares, o tamanho do complemento é limitado por $(k+3)n$ (ou $(5+k)n$ no caso geral apresentado na Seção 3), enquanto ELAs não restritos possuem limites como $O(n^{k}(0.76n)^{n})$.
  • A Tabela 1 no artigo fornece uma comparação abrangente, mostrando melhorias exponenciais ou polinomiais sobre os limites não restritos para várias condições (Büchi, Rabin, Streett, Paridade e Emerson-Lei).
• Implementação Prática e Avaliação: O algoritmo é implementado na ferramenta Kofola. Comparações experimentais com a ferramenta de estado da arte Spot demonstram que o Kofola frequentemente produz complementos muito menores em tamanho. Os benchmarks incluem ELAs da literatura, Autômatos de Rabin Generalizados gerados aleatoriamente e ELAs derivados de traduções de LTL.

Significância e Alegações

Os autores afirmam que este trabalho representa o primeiro passo em direção a algoritmos práticos para complementar, determinizar e testar universalidade e inclusão para autômatos de Emerson-Lei com condições de aceitação ricas.

A significância reside em preencher a lacuna entre a concisão teórica (fornecida pelos ELAs) e a eficiência de verificação prática. Ao explorar a prevalência estrutural de componentes de elevador em autômatos do mundo real (conforme observado em trabalhos anteriores [1]), os autores fornecem um método que reduz drasticamente o problema da explosão de estados inerente à complementação. O artigo posiciona isso como uma contribuição fundamental, permitindo fluxos de trabalho de verificação mais eficientes para sistemas modelados com condições de aceitação sofisticadas, sem inventar novas aplicações além das já estabelecidas no campo (model checking de LTL, verificação de hiperpropriedades).

O trabalho é modesto em seu escopo, focando estritamente no problema da complementação e suas implicações imediatas para determinização e teste de inclusão, ao mesmo tempo em que reconhece que trabalhos adicionais são necessários para realizar plenamente algoritmos práticos para todas as operações em ELEAs.