💻 computer science

Termination analysis with interpolation-based transition invariant generation

Este artigo apresenta uma estrutura unificada de análise de terminação que aproveita a interpolação de Craig para gerar invariantes de transição bem fundados, permitindo assim a prova simultânea de terminação e não terminação para sistemas de estado infinito com desempenho comparável a ferramentas de última geração.

Autores originais: Konstantin Britikov, Martin Blicha, Grigory Fedyukovich, Natasha Sharygina

Publicado 2026-08-11

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Konstantin Britikov, Martin Blicha, Grigory Fedyukovich, Natasha Sharygina

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

A Grande Caça ao Tesouro do Escape Computacional

Imagine que você está observando um robô jogar um jogo de "siga o líder" dentro de um labirinto gigante e infinito. O robô começa em um ponto específico e segue um conjunto de regras para se mover de uma sala para a próxima. A grande questão que os cientistas da computação fazem é: este robô acabará se cansando e parará de se mover, ou correrá para sempre, preso em um loop infinito? Este é o problema da "análise de terminação". É um enigma fundamental no mundo dos métodos formais, um ramo da ciência da computação dedicado a provar que o software se comporta exatamente como esperamos.

Para entender o que está em jogo, pense nos dois resultados possíveis. Se o robô parar, significa que o programa é "seguro" e terminará seu trabalho. Se ele rodar para sempre, é "não-terminante", o que geralmente significa um erro que trava um sistema. Por muito tempo, os cientistas trataram esses dois resultados como mistérios completamente separados. Eles tinham um conjunto de ferramentas para provar que um robô pararia (como encontrar um cronômetro de contagem regressiva que sempre diminui) e um conjunto totalmente diferente de ferramentas para provar que ele não pararia (como encontrar uma sala onde o robô fica preso em um círculo). Mas, assim como um detetive precisa saber tanto como um crime aconteceu quanto como ele não aconteceu para resolver um caso, os cientistas da computação perceberam que entender por que um programa para e por que ele não para são dois lados da mesma moeda. O desafio era construir uma única agência de detetives que pudesse resolver ambos os mistérios de uma só vez.

A Grande Ideia do Artigo: Um Detetive com Dois Chapéus

Neste artigo, os autores — Konstantin Britikov, Martin Blicha, Grigory Fedyukovich e Natasha Sharygina — apresentam uma nova e inteligente maneira de resolver esse quebra-cabeça. Eles construíram uma estrutura unificada que permite que as ferramentas para provar "parada" e "não parada" conversem entre si e compartilhem pistas. A abordagem deles é como um detetive que não apenas procura pelo culpado, mas também estuda a cena do crime para entender como o crime não aconteceu, usando esse conhecimento para resolver o caso mais rapidamente.

O núcleo do método deles é algo chamado "geração de invariante de transição baseada em interpolação". Isso parece um nome complicado, então vamos decompor com uma história. Imagine que o robô deixa um rastro de pegadas enquanto se move pelo labirinto. Às vezes, o robô atinge um beco sem saída (um "estado de sumidouro") e para. O algoritmo dos autores analisa esses rastros de "becos sem saída". Em vez de apenas dizer: "Ok, ele parou aqui", eles usam um truque matemático chamado interpolação de Craig para generalizar a história. Eles perguntam: "Qual é o motivo de o robô ter parado? Foi porque a bateria acabou? Foi porque o chão estava escorregadio?"

Ao analisar as pegadas do robô que parou, o algoritmo constrói uma "regra de trânsito" (um invariante de transição) que explica por que o robô deve parar. É como perceber: "Ah, toda vez que o robô vira à esquerda, ele perde um passo de energia e, como ele começa com energia limitada, não pode correr para sempre". Esta regra é um "invariante de transição bem fundado", que é uma forma sofisticada de dizer uma garantia de que o robô está chegando mais perto da linha de chegada a cada movimento.

Mas aqui está a reviravolta mágica: o algoritmo não para por aí. Ele usa essa "regra de parada" para ajudar a caçar os casos de "não parada". Se o robô não para, significa que a "regra de parada" não cobre todos os caminhos possíveis que o robô poderia seguir. O algoritmo então foca sua atenção especificamente nas partes do labirinto que a regra esqueceu. Ele pergunta: "Ok, sabemos que o robô para se for para a esquerda, mas e se ele for para a direita?". Ele então executa uma verificação separada para ver se ir para a direita leva a um loop infinito. Se levar, o robô é não-terminante. Se não levar, o algoritmo adiciona este novo caminho à sua "regra de parada" e tenta novamente.

Este vai e vem é o principal avanço do artigo. Em vez de rodar dois programas separados — um para provar a parada e outro para provar o loop — eles rodam um programa inteligente que usa os resultados de um para guiar o outro. Se a prova de "parada" for fraca, a prova de "loop" entra em ação para encontrar as peças que faltam. Se a prova de "loop" encontrar um caminho seguro, a prova de "parada" usa isso para construir uma regra mais forte.

O Que Eles Descobriram e Quão Certos Estão

Os autores implementaram essa ideia em uma ferramenta chamada GOLEM e a testaram em uma coleção massiva de quebra-cabeças chamados de benchmarks da "Competição de Terminação". Estes são testes padrão usados por especialistas para ver quão boas são diferentes ferramentas ao resolver esses problemas de estado infinito.

Os resultados foram bastante promissores. A nova ferramenta, que eles chamam de ITPTIG+, conseguiu resolver 761 dos problemas de benchmark. Este é um avanço significativo em relação à sua versão anterior (SNA), que resolvia apenas 343. Mais importante ainda, o ITPTIG+ resolveu 240 problemas que nem suas ferramentas anteriores conseguiam resolver sozinhas. Isso sugere que combinar os dois tipos de análise realmente torna o trabalho de detetive mais eficiente.

Quando compararam sua ferramenta com os atuais campeões na área (ferramentas chamadas KOAT, LOAT e T2), o ITPTIG+ manteve o nível. Ele resolveu 8 problemas únicos que nenhuma das outras ferramentas de topo conseguiu resolver. Duas dessas soluções únicas foram problemas que nunca haviam sido resolvidos por qualquer ferramenta na história da Competição de Terminação. Os autores estão confiantes nesses resultados porque eles são baseados em provas matemáticas reais geradas pela ferramenta, não apenas em suposições ou simulações. Eles provaram que, se a ferramenta diz "Terminando", o sistema definitivamente para, e se diz "Não-terminante", o sistema definitivamente entra em loop para sempre.

No entanto, o artigo também admite onde o método encontra um limite. Ainda existem sistemas complexos onde a ferramenta retorna "DESCONHECIDO". Isso acontece quando o caminho do robô é tão complicado que a "regra de parada" que o algoritmo constrói não cobre todos os cenários possíveis, e a verificação de "loop" também não consegue encontrar um ciclo infinito claro. É como um detetive que tem uma ótima teoria sobre o crime, mas não consegue encontrar a peça final de evidência para encerrar o caso.

Em resumo, este artigo mostra que, ao deixar os detetives de "parada" e "não parada" trabalharem juntos, podemos resolver mais enigques de computador do que nunca. Não resolve todos os problemas do universo, mas prova que compartilhar pistas entre esses dois lados do problema é uma estratégia poderosa que nos aproxima de tornar nosso software mais seguro e confiável.

Resumo Técnico: Análise de Terminação com Geração de Invariantes de Transição Baseada em Interpolação

Declaração do Problema

A análise de terminação e de não-terminação de sistemas de estado infinito são problemas complementares que são tipicamente abordados por técnicas separadas. Enquanto a prova de terminação frequentemente depende de funções de ranking ou invariantes de transição disjuntivamente bem fundados, a análise de não-terminação foca predominantemente na detecção de conjuntos recorrentes (conjuntos de estados dos quais a execução não pode escapar). Métodos existentes, como a Análise de Não-Terminação Baseada em Segurança (SNA), tratam estes como problemas distintos. A SNA refina iterativamente problemas de segurança para provar a não-terminação ou retorna "UNKNOWN" se não conseguir concluir, mas carece de um mecanismo para provar a terminação quando falha em encontrar um conjunto recorrente. Este artigo aborda a necessidade de um framework unificado que conecte estas duas análises, permitindo que elas compartilhem resultados intermediários e guiem uma à outra.

Metodologia

Os autores propõem um framework unificado que estende a SNA para provar a terminação através da geração de invariantes de transição bem fundados usando interpolação de Craig. A metodologia central envolve os seguintes componentes:

1. Arquitetura do Framework Unificado

A abordagem integra a análise de terminação e de não-terminação em um único loop. Ela utiliza os traços de transição terminantes construídos pela SNA (quando uma verificação de segurança falha) como uma fonte de informação estrutural. Em vez de apenas bloquear estes traços para refinar o problema de segurança, o algoritmo os generaliza em invariantes de transição.

2. Geração de Invariante de Transição Baseada em Interpolação (TRINVGEN)

A inovação central é um procedimento, TRINVGEN, que gera um candidato a invariante de transição disjuntivamente bem fundado a partir de um traço terminante. O processo envolve cinco etapas:

Computação de $NT_n$ : O algoritmo computa uma fórmula que codifica estados dos quais estados não-sumidouro podem ser alcançados dentro de $n$ transições.
Interpolação: Um interpolante de Craig é computado entre a fórmula do traço e a negação de $NT_n$ (combinada com a negação de estados sumidouro). Este interpolante sobre-aproxima o traço e captura as razões estruturais para a terminação.
Sub-aproximação em DNF: O interpolante é convertido em uma fórmula em Forma Normal Disjuntiva (DNF). Para evitar a explosão exponencial, utiliza-se uma abordagem sob demanda onde os disjuntos são construídos com base em modelos de solver SMT.
Filtragem: Cada disjunto é verificado quanto à sua fundamentação (well-foundedness) através da síntese de uma função de ranking linear. Apenas os disjuntos que admitem uma função de ranking são preservados para formar o candidato a invariante de transição.
Síntese de Cobertura: O algoritmo computa uma fórmula de cobertura $C(X)$ , codificando o conjunto de estados para os quais o candidato a invariante de transição é válido.

3. Análise Iterativa e Autoguiamento

O loop principal de análise (Algoritmo 4 e sua extensão, Algoritmo 5) opera da seguinte forma:

Verificação de Segurança: O sistema realiza uma verificação de segurança no problema atual.
Caso Unsat (Traço Terminante Encontrado): Se um traço para um estado sumidouro for encontrado, o TRINVGEN produz um candidato a invariante de transição e uma fórmula de cobertura $C$ $C$ .
- O algoritmo então verifica se os estados não cobertos pelo invariante ( $\neg C$ ) são alcançáveis.
- Se $\neg C$ for inalcançável, o invariante cobre todos os estados alcançáveis, e o sistema é provado como terminante.
- Se $\neg C$ for alcançável, o algoritmo refina o problema bloqueando estados que levam deterministicamente à terminação (via BLOCKTERM) e envia novos subproblemas para analisar os estados não cobertos.
Caso Sat (Conjunto Recorrente Encontrado): Se a verificação de segurança retornar "SAFE" com um invariante indutivo, o algoritmo verifica se este invariante é um conjunto recorrente. Se sim, o sistema é não-terminante.
Extensão Baseada em Pilha (Algoritmo 5): Para lidar com casos complexos onde um único invariante não cobre todo o espaço de estados, o algoritmo estendido mantém uma pilha de problemas de segurança. Ele foca a análise em regiões específicas de estados alcançáveis ( $S_m$ ) onde o invariante atual é inválido, tentando estender o invariante ou provar a não-terminação para estas regiões específicas.

Principais Contribuições

O artigo apresenta três contribuições primárias:

Geração Inovadora Baseada em Interpolação: Um método para gerar invariantes de transição disjuntivamente bem fundados usando interpolação de Craig para capturar razões de terminação a partir de traços.
Procedimento de Análise Unificado: Um framework que unifica a análise de terminação e de não-terminação, utilizando resultados intermediários (traços e invariantes) para autoguiamento. Isso permite que a prova de terminação foque em estados não cobertos e que a prova de não-terminação beneficie-se dos insights estruturais dos traços de terminação.
Implementação e Avaliação: Implementação dentro do framework de verificação GOLEM e avaliação em benchmarks de Sistemas de Transição de Inteiros da Competição de Terminação.

Resultados Experimentais

Os autores avaliaram sua ferramenta, ITPTIG+, contra a SNA clássica, o ITPTIG intermediário e ferramentas de ponta (KOAT, LOAT, T2) em 1.200 benchmarks de Sistemas de Transição de Inteiros.

Desempenho vs. SNA Clássica: O ITPTIG+ resolveu 761 instâncias, superando significativamente a SNA (343 instâncias) e o ITPTIG (521 instâncias). Ele resolveu unicamente 240 instâncias que nem a SNA nem o ITPTIG conseguiram resolver.
Desempenho vs. Estado da Arte: Embora o T2 tenha resolvido o maior número de instâncias no total (1002), o ITPTIG+ foi competitivo e resolveu unicamente 8 instâncias que nenhuma outra ferramenta na comparação resolveu. Notavelmente, duas destas instâncias (juLinkedListCreateAddAll.jar-obl-11 e juLinkedListCreateAddAllAt.jar-obl-17) nunca haviam sido resolvidas por qualquer ferramenta da Competição de Terminação antes deste trabalho.
Não-terminação: A ferramenta demonstrou melhoria significativa na análise de não-terminação em comparação com a SNA clássica ao focar a detecção de conjuntos recorrentes em regiões específicas de estados não cobertos.

Significância e Alegações

O artigo alega que combinar o raciocínio de terminação e de não-terminação é benéfico, produzindo um desempenho comparável ao de ferramentas de ponta enquanto resolve instâncias únicas. A significância reside na unificação destes problemas anteriormente separados dentro de um único framework. Ao usar a interpolação de Craig para generalizar traços terminantes, a abordagem captura as razões estruturais para a terminação e as utiliza para guiar a análise de todo o sistema de transição. Os autores enfatizam que fundamentar a abordagem na verificação de segurança fornece uma base robusta, permitindo a verificação eficiente de ambas as propriedades via solvers de segurança existentes. O trabalho demonstra que resultados intermediários de um tipo de análise (por exemplo, traços de uma falha de verificação de segurança) podem efetivamente impulsionar o outro (por exemplo, geração de invariante para terminação), criando um efeito sinérgico que melhora as capacidades gerais de verificação.