Methods for Efficient Unfolding of Colored Petri Nets

Título: Métodos para Desdobramento Eficiente de Redes de Petri Coloridas

1. Problema

As Redes de Petri (P/T - Lugares/Transições) são uma formalização poderosa para modelagem e verificação de sistemas distribuídos. No entanto, modelos P/T podem tornar-se excessivamente grandes e complexos para a compreensão humana. Para mitigar isso, as Redes de Petri Coloridas (CPN) foram introduzidas, permitindo que os tokens tenham "cores" (valores) e que as transições possuam guardas e expressões de arcos que manipulam esses valores.

O desafio central reside na verificação automática: a maioria das ferramentas de verificação de modelos (como verificação de alcançabilidade ou lógica temporal) opera nativamente sobre redes P/T. Para analisar uma CPN, ela deve ser "desdobrada" (unfolding) em uma rede P/T equivalente.

• O Obstáculo: O desdobramento ingênuo cria uma nova transição e um novo lugar para cada combinação possível de cores e ligações de variáveis. Isso resulta em uma explosão exponencial no tamanho da rede desdobrada, tornando a verificação inviável em tempo e memória para muitos modelos do mundo real (como os benchmarks do Model Checking Contest).
• Limitação Atual: Mesmo com otimizações existentes (análise de guardas, lugares estáveis, simetria de variáveis), certos modelos complexos ainda não podem ser desdobrados pelas ferramentas atuais.

2. Metodologia

Os autores propõem duas técnicas complementares de análise estática para reduzir o tamanho das redes desdobradas antes ou durante o processo de conversão para P/T. Ambas as técnicas são implementadas na ferramenta de verificação TAPAAL.

A. Quocientação de Cores (Color Quotienting)

• Conceito: Identifica cores que se comportam de maneira indistinguível (bisimilares) dentro da rede. Se diferentes cores geram o mesmo comportamento de transição e marcação, elas podem ser agrupadas em uma única classe de equivalência.
• Mecanismo:
  1. Define-se uma partição $\delta$ sobre o domínio de cores de cada lugar.
  2. O algoritmo busca uma partição estável, onde a relação de equivalência induzida pela partição é uma relação de bisimulação. Isso garante que, se dois estados são equivalentes sob a partição, suas transições futuras também o serão.
  3. A rede original é transformada em uma rede quociente onde as cores são substituídas por suas classes de equivalência.
  4. Algoritmo: Utiliza um processo de refinamento iterativo (similar a algoritmos de minimização de autômatos) que começa com uma partição grosseira e a divide dinamicamente até que a estabilidade seja alcançada, considerando apenas marcações limitadas (bounded markings) para garantir a terminação.

B. Aproximação de Cores (Color Approximation)

• Conceito: Calcula um superconjunto (overapproximation) seguro das cores que podem aparecer em cada lugar durante a execução da rede. Cores que nunca podem estar presentes em um lugar específico são excluídas do desdobramento.
• Mecanismo:
  1. Define-se uma função de expansão $E$ que itera sobre os lugares e transições, acumulando as cores possíveis baseadas nas marcações iniciais e nas expressões dos arcos.
  2. Calcula-se o ponto fixo mínimo dessa função.
  3. O resultado é um conjunto de cores aproximado para cada lugar. Se uma cor não estiver no conjunto aproximado de um lugar, ela é removida do domínio de cores desse lugar na rede desdobrada.
  4. Isso também invalida ligações (bindings) de transições que dependem de cores inalcançáveis, reduzindo o número de transições geradas.
• Implementação: Para CPNs inteiras (usadas no concurso), as cores são representadas compactamente como intervalos de inteiros (ranges), permitindo uma análise eficiente sem listar cada cor individualmente.

3. Contribuições Principais

1. Novos Algoritmos de Otimização: Introdução de duas técnicas estáticas (Quocientação e Aproximação) que atuam diretamente na estrutura da CPN para reduzir a complexidade do desdobramento.
2. Correção Formal: Provas matemáticas de que a rede quociente (via Quocientação) e a rede com domínio de cores reduzido (via Aproximação) preservam a bisimilaridade com a rede original, garantindo que as propriedades verificadas na rede desdobrada sejam válidas para a rede colorida original.
3. Implementação Eficiente: Integração robusta dessas técnicas no motor de verificação verifypn da ferramenta TAPAAL, utilizando representações compactas (intervalos) para lidar com grandes domínios de cores.
4. Avaliação Comparativa Abrangente: Testes extensivos contra os principais desdobradores do estado da arte (MCC, Spike, ITS-Tools) utilizando o conjunto completo de benchmarks do Model Checking Contest de 2021.

4. Resultados Experimentais

Os experimentos foram realizados em um cluster com limites de 15 GB de memória e 5 minutos de tempo por modelo.

• Capacidade de Desdobramento:
  • A combinação das duas técnicas (Método A+B) conseguiu desdobrar 203 redes, enquanto o MCC desdobrou 200, ITS-Tools 193 e Spike 170.
  • O método A+B foi o único capaz de desdobrar 3 instâncias críticas (FamilyReunion e DrinkVendingMachine) que nenhuma outra ferramenta conseguiu.
• Tamanho das Redes Desdobradas:
  • O método A+B produziu redes significativamente menores. Para 144 das 213 redes testadas, o tamanho foi estritamente menor que o dos concorrentes.
  • Em 45 casos, a redução foi de pelo menos uma ordem de magnitude (10x menor).
• Tempo de Execução:
  • A análise estática adiciona um custo computacional, mas o tempo total de desdobramento foi competitivo. O método A+B foi significativamente mais rápido que ITS-Tools e MCC em redes maiores, demonstrando que a redução de tamanho compensa o custo da análise.
• Verificação de Consultas (Model Checking):
  • Ao usar as redes desdobradas menores, a ferramenta TAPAAL conseguiu responder a mais consultas de verificação.
  • Em consultas totais (Reachability, CTL, LTL), o método A+B respondeu a 77,9% das consultas, superando o MCC (73,9%) e o ITS-Tools (72,0%). Isso representa um ganho de cerca de 4 pontos percentuais sobre o segundo colocado.

5. Significado e Conclusão

O artigo demonstra que a aplicação de análise estática avançada no nível da rede colorida (antes do desdobramento) é uma estratégia superior à simples otimização pós-desdobramento ou à análise de simetria de variáveis isolada.

• Impacto Prático: Permite a verificação de modelos complexos que anteriormente eram intratáveis devido à explosão de estado.
• Eficiência: A abordagem não apenas reduz o tamanho da rede (economizando memória), mas também acelera o processo de verificação subsequente, mantendo o tempo de desdobramento competitivo.
• Futuro: Os autores planejam combinar essas técnicas com reduções estruturais aplicadas diretamente nas redes coloridas para obter ganhos ainda maiores.

Em resumo, este trabalho estabelece um novo padrão para o desdobramento de Redes de Petri Coloridas, provando que a inteligência na fase de pré-processamento é crucial para a escalabilidade da verificação de modelos.