A Forward-Only Construction of Semilinear Inductive Invariants for VAS

Resumo Técnico: Uma Construção Unidirecional de Invariantes Indutivos Semilineares para VAS

Enunciado do Problema
O problema da alcançabilidade para Sistemas de Adição de Vetores (VAS), também conhecidos como redes de Petri, é um problema de decisão central na teoria dos sistemas de estado infinito. Embora a decidibilidade tenha sido estabelecida na década de 1980 por Kosaraju e Mayr, a complexidade computacional permaneceu em aberto por décadas até ser recentemente demonstrada como sendo de completude de Ackermann. Uma alternativa significativa à decidibilidade, introduzida por Leroux, caracteriza a não-alcançabilidade via invariantes indutivos semilineares. Este método baseia-se em um esquema de "ida e volta" (back-and-forth) que expande simultaneamente uma sobre-aproximação direta a partir da origem e uma sobre-aproximação inversa a partir do alvo.

No entanto, esta abordagem existente possui duas limitações primárias:

1. Dependência de Simetria: A construção baseia-se na simetria dos VAS, onde as execuções podem ser revertidas. Essa simetria quebra-se em modelos assimétricos como o VAS de Ramificação (BVAS), onde as execuções são em forma de árvore em vez de sequências lineares, tornando a extensão do método de Leroux para BVAS difícil.
2. Falta de Canonicidade: O invariante resultante depende igualmente da origem e do alvo. Em muitos cenários de verificação, a origem é fixa enquanto o alvo varia; um método que produz invariantes que mudam drasticamente com o alvo é menos canônico e mais difícil de relacionar com a estrutura intrínseca do sistema. Além disso, para subclasses específicas como o VAS periódico, o método de Leroux não garante que os invariantes resultantes sejam periódicos.

Metodologia
Os autores propõem uma nova construção unidirecional (forward-only) de invariantes indutivos semilineares. Diferente da abordagem de ida e volta, este método constrói invariantes puramente a partir do conjunto de configurações iniciais ($C_0$), sem a necessidade de raciocínio inverso a partir do alvo.

Os ingredientes técnicos centrais incluem:

• VAS Periódico: Os autores definem uma classe de VAS onde o conjunto de alcançabilidade é periódico (fechado sob adição e contendo o vetor zero). Eles provam que o problema da alcançabilidade para VAS gerais pode ser reduzido ao problema da alcançabilidade para VAS periódicos através da adição de um único contador.
• Conjuntos Quase Semilineares e Linearização: O método utiliza a caracterização geométrica dos conjuntos de alcançabilidade de VAS como conjuntos "quase semilineares". Estes são decompostos em conjuntos "quase lineares" ($b + P$), que são então sobre-aproximados por conjuntos lineares através de um processo chamado linearização ($lin(L)$).
• Vetores Interiores: Um conceito inovador introduzido neste trabalho é o de "vetores interiores" de um conjunto periódico. Esses vetores permitem que o algoritmo refine as aproximações, empurrando vetores para dentro do conjunto original, garantindo que o invariante construído permaneça disjunto do conjunto alvo enquanto mantém a periodicidade.
• Construção Algorítmica: O artigo apresenta um algoritmo (Algoritmo 1) que refina iterativamente um conjunto periódico semilinear $Inv$. Em cada iteração, ele identifica a diferença entre a alcançabilidade direta do conjunto atual e o próprio conjunto, decompõe essa diferença em componentes quase lineares e adiciona linearizações traduzidas específicas a $Inv$. O algoritmo é provado como terminável porque a "dimensão espacial" do conjunto de diferença diminui estritamente a cada iteração.

Principais Contribuições

1. Construção Unidirecional (Forward-Only): Os autores introduzem um método para construir invariantes indutivos semilineares que dependem primordialmente das configurações alcançáveis a partir da origem. Isso resulta em invariantes que são mais canônicos e melhor alinhados com a estrutura do sistema.
2. Invariantes Periódicos para VAS Periódicos: O artigo prova que, para VAS periódicos, se o conjunto de alcançabilidade é disjunto de um conjunto semilinear alvo, existe um invariante indutivo semilinear periódico que também é disjunto do alvo. Isso contrasta com métodos anteriores que poderiam produzir invariantes não periódicos mesmo para sistemas periódicos.
3. Redução para VAS Periódico: Os autores fornecem uma caracterização efetiva de VAS periódicos e demonstram que o problema da alcançabilidade para VAS comuns reduz-se ao de VAS periódicos. Consequentemente, invariantes semilineares para VAS gerais podem ser derivados dos invariantes periódicos construídos para o sistema reduzido.
4. Prova de Existência via Oráculo: A construção é apresentada como um algoritmo com chamadas de oráculo (para linearização e seleção de vetores). O artigo estabelece a existência dos vetores necessários e a terminação do processo, fornecendo uma prova construtiva da existência de invariantes indutivos semilineares periódicos.

Resultados

• Teorema 4.5: O conjunto de alcançabilidade de um VAS periódico $(A, C_0)$ tem uma interseção vazia com um conjunto semilinear $C_{bad}$ se, e somente se, existe um invariante indutivo semilinear periódico $I$ de $(A, C_0)$ tal que $I \cap C_{bad}$ seja vazio.
• Terminação e Correção: O algoritmo proposto termina e retorna um invariante indutivo semilinear periódico disjunto do conjunto alvo, desde que as chamadas de oráculo possam ser satisfeitas. A terminação é garantida pela diminuição estrita da dimensão espacial do conjunto $Post^*_A(Inv) \setminus Inv$ em cada etapa.
• Exemplos: O artigo ilustra o método com exemplos onde a construção unidirecional produz invariantes que são independentes da configuração específica do alvo (ao contrário do método de ida e volta) e, no caso de VAS periódicos, produz invariantes periódicos onde o método de ida e volta falha em fazê-lo.

Significância e Alegações
Os autores alegam que esta abordagem unidirecional representa um passo em direção à extensão de técnicas baseadas em invariantes para VAS de Ramificação (BVAS). Dado que os BVAS carecem da simetria necessária para o raciocínio inverso (as configurações iniciais estão nas folhas e os alvos na raiz das árvores de execução), o método de ida e volta, dependente de simetria, é difícil de generalizar. Ao construir invariantes puramente a partir da origem, os autores sugerem que seu método é mais adequado para abordar o problema aberto da alcançabilidade para BVAS.

O artigo também discute a propriedade de "invariante indutivo semilinear" no contexto de GVAS (Grammar VAS), conjecturando que propriedades semelhantes podem ser válidas, embora isso permaneça uma área aberta para investigações futuras. O trabalho é estruturado como um avanço teórico na compreensão estrutural da alcançabilidade de VAS, oferecendo uma ferramenta mais canônica para verificação que respeita a assimetria de certos modelos de sistema.