Resumo Técnico: Verificação de Modelos Simbólica usando Intervalos de Vetores

1. Definição do Problema

A verificação de modelos é uma técnica de verificação formal robusta para garantir que sistemas de software e hardware adiram a especificações. No entanto, ela é severamente dificultada pelo problema da explosão do espaço de estados, onde o número de estados e transições possíveis cresce exponencialmente com o tamanho do sistema. Este desafio é particularmente agudo na verificação de modelos global, onde o objetivo é identificar todos os estados que satisfazem uma fórmula de Lógica de Árvore de Computação (CTL), em vez de verificar uma única configuração.

Técnicas existentes, como Diagramas de Decisão (DDs), abstrações e redução de ordem parcial, mitigam esse problema, mas enfrentam limitações à medida que os modelos se tornam mais sofisticados. Especificamente, abordagens baseadas em intervalos padrão (por exemplo, Interval Decision Diagrams) codificam conjuntos de vetores como vetores de intervalos. Este artigo argumenta que uma abordagem mais eficaz para redes de Petri é codificar conjuntos de marcações usando intervalos generalizados de vetores (intervalos de vetores), em vez de vetores de intervalos. Esta distinção é crucial porque os espaços vetoriais frequentemente envolvem ordens parciais não totais, tornando definições simples de intervalos insuficientes.

2. Metodologia

Os autores propõem uma nova estrutura simbólica chamada Conjuntos de Vetores Simbólicos (SVS - Symbolic Vector Sets) para codificar conjuntos de marcações de redes de Petri. A metodologia é construída sobre três pilos fundamentais:

2.1. Vetores e Conjuntos Simbólicos

Um Vetor Simbólico é definido como um par $(a, b)$, onde $a$ e $b$ são conjuntos de vetores (marcações).

• Inclusão ($a$): Uma marcação $q$ pertence ao vetor simbólico se ela inclui todos os vetores em $a$ (sob uma ordem parcial não estrita $\subseteq_f$).
• Exclusão ($b$): Uma marcação $q$ pertence ao vetor simbólico se ela não inclui nenhum vetor em $b$.
• Generalização: Isso generaliza o intervalo de números naturais $[a, b]$ (onde $a \le x \le b$) para vetores. Como os vetores nem sempre são comparáveis, a estrutura requer um conjunto de limites inferiores ($a$) e um conjunto de limites superiores ($b$) em vez de limites únicos.

Um Conjunto de Vetores Simbólicos é uma coleção desses vetores simbólicos, representando a união de seus conjuntos subjacentes de marcações.

2.2. Forma Canônica e Operações

Para garantir a eficiência e evitar redundância, os autores definem uma forma canônica para vetores e conjuntos simbólicos. Propriedades principais incluem:

• Unicidade: Cada conjunto de marcações tem exatamente uma representação canônica.
• Operações Homomórficas: O artigo define operações homomórficas (união, interseção, diferença, negação) que operam diretamente nas estruturas simbólicas sem decodificá-las para marcações individuais.
• Mesclabilidade e Compartilhamento: Para manter a canonicidade, os autores introduzem relações para determinar quando dois vetores simbólicos podem ser fundidos ou quando existe um componente "compartilhável" entre eles. Isso envolve uma ordem total lexicográfica para resolver ambiguidades em ordens parciais não totais, garantindo o tratamento determinístico de restrições sobrepostas.

2.3. Verificação de Modelo CTL em Redes de Petri

O framework aplica essas estruturas a redes de Petri com capacidades finitas.

• Operação Pre: O núcleo da verificação de modelo global é a operação pre, que computa marcações predecessoras. Os autores definem uma operação pre simbólica que trabalha em conjuntos de vetores simbólicos, lidando com a reversibilidade de transições e restrições de capacidade.
• Avaliação de Ponto Fixo: Fórmulas CTL (ex: $EF$, $EG$, $EU$) são avaliadas usando computações de ponto fixo (menor e maior ponto fixo) sobre os conjuntos de vetores simbólicos. A satisfação de uma fórmula é determinada verificando se uma marcação pertence ao conjunto de vetores simbólicos resultante.

2.4. Otimizações

• Saturação: Para lidar com o "efeito de pico" onde soluções intermediárias em computações de ponto fixo crescem desnecessariamente, os autores implementam uma estratégia de saturação. Isso envolve iterar sobre limites de capacidade e alavancar resultados anteriores para computar passos subsequentes, reduzindo significamente o número de vetores simbólicos intermediários.
• Agrupamento (Clustering): O artigo menciona o agrupamento como uma otimização potencial para alcançabilidade, onde vetores menores são combinados, embora isso seja notado como um conceito para descrição formal futura.

3. Principais Contribuições

1. Codificação Inovadora: Introdução dos Conjuntos de Vetores Simbólicos, uma estrutura que generaliza intervalos para vetores, especificamente projetada para lidar com a ordem parcial não total das marcações de redes de Petri.
2. Canonicidade Formal: Uma definição rigorosa de uma forma canônica para vetores e conjuntos simbólicos, incluindo provas de unicidade e o desenvolvimento de operações homomórficas (união, interseção, diferença, negação) que preservam essa canonicidade.
3. Framework de Verificação de Modelo Global: Um formalismo completo para avaliar fórmulas CTL em redes de Petri usando essas estruturas simbólicas, incluindo a definição da operação pre simbólica.
4. Algoritmo de Saturação: Uma adaptação de princípios de saturação (derivados de outras técnicas simbólicas) ao contexto de conjuntos de vetores simbólicos para mitigar picos computacionais durante iterações de ponto fixo.
5. Implementação (SVSKit): Uma biblioteca Swift implementando a teoria, testada contra benchmarks do Model Checking Contest (MCC) 2022.

4. Resultados

Os autores avaliaram sua abordagem usando a ferramenta SVSKit em exemplos do MCC 2022, especificamente o modelo Circadian Clock.

• Escalabilidade com Saturação: Experimentos no modelo Circadian Clock (14 lugares, 16 transições) demonstraram que a saturação é crítica. Sem saturação, o tempo de computação cresceu exponencialmente com a capacidade do lugar (excedendo 5 horas para capacidade 6). Com saturação, o tempo permaneceu constante (aprox. 3,2s) para capacidades 2 e acima, e o número de vetores simbólicos permaneceu estável.
• Lidando com Grandes Espaços de Estados: A ferramenta lidou com sucesso com capacidades de até $N=100.000$, codificando aproximadamente $10^{84}$ marcações com um conjunto final de apenas 26 vetores simbólicos.
• Desempenho em Benchmarks: Na categoria de fireability de CTL do MCC 2022, ferramentas existentes (GreatSPN, ITS-Tools, Tapaal) falharam em responder a todas as 16 consultas dentro do limite de 60 minutos (Tapaal respondeu 9/16). A abordagem SVSKit resolveu todas as 16 consultas em aproximadamente 30 minutos.
• Limitações: Os autores reconhecem que a implementação atual enfrenta desafios de escalabilidade devido à complexidade de pior caso das operações canônicas ($O(n!)$). A eficiência depende fortemente da implementação dessas operações, e a ferramenta foi restrita a redes de Petri relativamente pequenas nos benchmarks devido a essas restrições.

5. Significância e Alegações

O artigo afirma oferecer uma alternativa promissora às técnicas existentes de verificação de modelos simbólica ao mudar de "vetores de intervalos" para "intervalos de vetores".

• Contribuição Teórica: Fornece um framework algébrico formal para manipular conjuntos de vetores sob ordens parciais, preenchendo uma lacuna na literatura onde tais estruturas estavam estagnadas (referenciando as "estruturas de predicados" originais de 30 anos atrás).
• Viabilidade Prática: Os resultados sugerem que esta abordagem pode lidar com espaços de estados infinitos ou muito grandes de forma mais eficiente do que a enumeração explícita e potencialmente superar ferramentas atuais em tarefas específicas de verificação de modelo global, particularmente aquelas envolvendo grandes capacidades.
• Direções Futuras: Os autores sugerem modestamente que a implementação atual requer refinamento, particularmente na otimização das operações canônicas. Eles propõem como trabalho futuro a verificação de modelo local, estendendo a abordagem para modelos além de redes de Petri, e a integração deste método com Diagramas de Decisão, postulando que as duas abordagens são ortogonais e podem se beneficiar da hibridização.

O artigo conclui que, embora a implementação atual possua limitações, a base teórica e os resultados experimentais iniciais validam o potencial dos conjuntos de vetores simbólicos para a verificação de modelos global.