Resumo Técnico: iSMC – Um Verificador de Modelos Simbólico Baseado em BDD com Certificação Interativa

1. Declaração do Problema

A verificação de modelos é uma técnica fundamental para verificar a correção de sistemas de hardware e software. No entanto, garantir a confiabilidade do próprio verificador de modelos é um desafio crítico. Os paradigmas tradicionais de certificação baseiam-se em protocolos não interativos: um provador (o verificador de modelos) gera um certificado (por exemplo, uma atribuição satisfatória ou uma prova de resolução), e um verificador o verifica independentemente.

O artigo identifica uma limitação teórica fundamental nessa abordagem: para muitos problemas, incluindo a verificação de modelos CTL geral, os certificados podem ter comprimento exponencial no pior caso em relação ao tamanho da instância. Consequentemente, o verificador requer tempo exponencial para verificá-los, tornando o processo de certificação impraticável para sistemas grandes, a menos que $NP = coNP$.

Os autores propõem a certificação interativa, um paradigma baseado em sistemas de prova interativa (IP), onde um provador e um verificador participam de um protocolo de múltiplas rodadas. O verificador faz perguntas de forma adaptativa, permitindo-lhe detectar erros com alta probabilidade em tempo polinomial, mesmo que o cálculo subjacente seja complexo. Embora as provas interativas para problemas PSPACE (como a verificação de modelos CTL) sejam teoricamente estabelecidas ($IP=PSPACE$ de Shamir), torná-las práticas para a verificação de modelos simbólica usando Diagramas de Decisão Binária (BDDs) permaneceu um desafio aberto.

2. Metodologia

O artigo apresenta o iSMC, o primeiro verificador de modelos auto-certificável que implementa certificação interativa para verificação de modelos CTL com requisitos de justiça. O sistema é construído sobre três módulos principais:

2.1 Arquitetura

• Solver: Um verificador de modelos simbólico baseado em BDD que calcula o conjunto de estados alcançáveis que satisfazem uma especificação CTL. Ele opera sobre modelos booleanos achatados (formato SMV) e utiliza a biblioteca BDD clic.
• Prover: Executa na mesma máquina que o Solver. Ele executa a instância de verificação de modelos e gera um rastro de execução consistindo na sequência de chamadas à biblioteca BDD e afirmações feitas durante o cálculo.
• Verificador: Um módulo leve que pode ser executado em um cliente com recursos limitados. Ele não reexecuta o algoritmo de verificação de modelos. Em vez disso, engaja-se em um protocolo interativo com o Prover para verificar o rastro de execução.

2.2 O Protocolo TraceCert

A inovação central é o TraceCert, um protocolo de prova interativa adaptado do trabalho de certificação QBF de Couillard et al. [11].

1. Rastro para Circuito: O rastro de execução é transformado em um Circuito Booleano Generalizado (GBC). Cada instrução no rastro torna-se uma porta, e as afirmações (por exemplo, "o conjunto de estados $C_1$ não é equivalente a $C_0$") tornam-se reivindicações de equivalência.
2. Aritmetização: Funções booleanas são codificadas como polinômios multivariados sobre um corpo finito $\mathbb{F}_p$. Isso permite que o verificador verifique propriedades do cálculo avaliando polinômios em pontos aleatórios, em vez de percorrer todo o circuito.
3. Redução de Grau: Para garantir que os polinômios tenham grau baixo (necessário para verificação em tempo polinomial), o protocolo introduz portas de redução de grau ($\delta_x$) que reduzem os expoentes para 1 sem alterar o valor da função em entradas booleanas.
4. Rodadas Interativas: O protocolo prossegue em rodadas, percorrendo o circuito. O Prover reivindica o valor de uma porta; o Verificador desafia o Prover com atribuições aleatórias às entradas da porta. O Prover deve fornecer polinômios consistentes com a reivindicação. Se o Prover mentir, a probabilidade de ser pego é limitada pelo lema de Schwartz-Zippel.

2.3 Melhorias Técnicas Chave sobre Trabalhos Anteriores

Os autores estendem a tecnologia de [11] (que focava em QBF) para atender às necessidades específicas da verificação de modelos CTL, abordando três grandes gargalos:

1. Renomeação e Equivalência Eficientes: O protocolo original (CPCertify) lidava com portas de equivalência e renomeação de forma ineficiente ($O(n^2)$ e $O(n^k)$). O TraceCert otimiza essas rodadas para $O(1)$ e $O(n)$, respectivamente.
2. Compatibilidade com Coleta de Lixo: Bibliotecas BDD padrão usam caches de computação globais e coleta de lixo. A abordagem anterior exigia que o Prover armazenasse todos os BDDs intermediários, impedindo a coleta de lixo. Os autores introduzem o TraceCertRev, uma variante de baixo para cima do protocolo que permite ao Prover descartar resultados intermediários (atuando como um oráculo) sem comprometer a solidez, desde que o Prover não conspira maliciosamente para lembrar desafios passados.
3. Cache de Computação Global: A implementação anterior (blic) não podia usar um cache global porque manipulava eBDDs estendidos de uma maneira incompatível com o cacheamento. Os autores introduzem uma representação imutável de eBDD inovadora usando campos de link para versionar nós, permitindo o uso de uma tabela única global e melhorando significativamente o desempenho.

3. Contribuições Principais

1. Sistema iSMC: A primeira implementação de um verificador de modelos auto-certificável com certificação interativa para propriedades CTL arbitrárias com requisitos de justiça.
2. Protocolo TraceCert: Um novo protocolo de prova interativa que lida eficientemente com renomeação de variáveis e afirmações de equivalência comuns em rastros de verificação de modelos, reduzindo a complexidade de rodadas de portas específicas.
3. Implementação Otimizada de eBDD: Um novo algoritmo (ApplyEBDD) e estrutura de dados que permitem o uso de caches de computação globais e coleta de lixo, superando as ineficiências da biblioteca blic anterior.
4. TraceCertRev: Uma variante do protocolo que permite a coleta de lixo durante a certificação, tornando o sistema viável para verificação de modelos em grande escala onde a memória é uma restrição.

4. Resultados Experimentais

Os autores avaliaram o iSMC em 53 benchmarks da trilha de vivacidade do HWMCC'25.

• Desempenho do Solver: Comparado à ferramenta madura NuSMV, o Solver do iSMC é, em média, 5,84 vezes mais lento. Os autores atribuem isso principalmente à falta de suporte para produtos relacionais (uma otimização de BDD) no protótipo atual, pois certificá-los interativamente permanece um problema aberto.
• Sobrecarga do Prover: O Prover executa em tempo $O(S)$, onde $S$ é o tempo do Solver. O fator constante é aproximadamente 2,00, o que significa que a sobrecarga de certificação é cerca de duas vezes o tempo de resolução.
• Eficiência do Verificador: O Verificador é altamente eficiente. Para um tempo limite de 15 minutos no Prover, o Verificador nunca levou mais de 3,6 segundos (aceleração média de 33,4x sobre o Prover). O tempo de execução do Verificador escala linearmente com o comprimento do rastro de execução, não com o tempo de computação.
• Impacto das Otimizações: As melhorias (TraceCert, biblioteca clic, cache global) resultaram em uma aceleração média de 2,26x no tempo de execução e uma redução de 16,12x no uso de memória em comparação com a implementação de base usando CPCertify e blic.

5. Significado e Alegações

O artigo afirma que o iSMC representa um passo significativo em direção à certificação interativa prática para verificação de modelos.

• Confiança em Servidores Não Confiáveis: O sistema permite um cenário onde um cliente com recursos limitados pode delegar a verificação de modelos a um servidor poderoso, mas não confiável. O servidor (Solver + Prover) realiza o cálculo pesado, enquanto o cliente (Verificador) certifica o resultado com alta probabilidade em tempo polinomial.
• Verificação Polinomial: Diferentemente dos métodos de certificação não interativa que requerem tempo exponencial para propriedades CTL gerais, o Verificador do iSMC executa em tempo polinomial em relação ao número de variáveis e ao comprimento do rastro.
• Escalabilidade: Os autores demonstram que, com suas otimizações, a sobrecarga da certificação interativa é gerenciável e a pegada de memória é significativamente reduzida, tornando a abordagem viável para benchmarks não triviais.

Os autores permanecem modestos, observando que o iSMC é um primeiro protótipo. Eles reconhecem que o Solver é atualmente mais lento do que ferramentas de última geração como o NuSMV devido a otimizações ausentes (produtos relacionais) e que a implementação atual visa CTL, embora o framework subjacente possa teoricamente se estender ao cálculo modal completo $\mu$.