Resumo de Token Variation Vector and Analysis of some Properties of Petri Nets - Eduard M. M. Costa; José B. Medeiros; Eliane Pozzebon; Anderson L.F. Perez; José V. S. Filho

As redes de Petri têm sido muito utilizadas em muitas estratégias de modelagem e controle de sistemas, especialmente os sistemas a eventos discretos (SEDs). As redes de Petri foram definidas com o especial intuito de modelagem de sistemas concorrentes, em que suas propriedades se aplicam de modo conveniente nas aplicações definidas na área de automação da manufatura, sistemas de comunicações, sistemas híbridos, entre outros. Na área de automação, várias são as perspectivas, o que inclui algoritmos de conversão de modelos para diagramas ladder, desde que através do modelo é possível se analisar e gerar sua verificação e validação, bem como aplicação de estratégias de controle através de simulação. Com a necessidade de inserção de características específicas para melhor representar os sistemas, a teoria das redes de Petri avançou, como a inclusão de características em arcos, transições e lugares para ampliar as suas aplicações, como a temporização, cores ou características específicas nas fichas, redes contínuas, funções de transições, multiplexação de arcos, entre outras, seja na perspectiva de formas de análise de suas propriedades. Devido as grandes aplicações das redes de Petri ao mundo atual, a necessidade de geração de modelos corretos para aplicação à controle de sistemas, exige estratégias de suas verificações e validações, para garantir o correto funcionamento do sistema. Entretanto, este problema de verificação e validação de sistemas modelados por redes de Petri, é uma questão complexa do ponto de vista computacional, desde que a complexidade e custo computacionais crescem exponencialmente com o número de lugares que representam as partes do sistema, bem como, da definição da marcação inicial em alguns casos e de transições específicas, como as transições fontes, sorvedouros ou auto-laços. Em especial, a maior parte destas formas de análises dos modelos de sistemas em redes de Petri ainda se baseia na construção da árvore de alcançabilidade ou no seu respectivo grafo. Neste caso, devido a isso, quanto maior o número de lugares e marcações alcançadas na rede a partir de sua marcação inicial em alguns modelos, a árvore de alcançabilidade tende a apresentar uma explosão de estados, que aumenta consideravelmente o problema da verificação do modelo. Mesmo para avaliações básicas sobre o modelo gerado, como análise de comportamento em termos de propriedades como cobertura, crescimento indefinido de fichas nos lugares, variação de número de fichas nos lugares, bloqueios em transições, entre outros, a utilização deste método ainda é comum, o que determina altos custos computacionais para simples análises. Sendo assim, baseado em análises sobre o comportamento e a estrutura das redes de Petri, tomando como princípio os seus fundamentos matriciais, como as matrizes pre e post, concebe-se uma estratégia de verificação de alguns comportamentos básicos das redes, eliminando a utilização da árvore de alcançabilidade. Essa estratégia se baseia na variação do número de fichas na rede de Petri, gerado pelo disparo de cada uma das transições habilitadas. Tal estratégia é definida a partir da estrutura da rede, que permite avaliar algumas situações comuns de forma simples, reduzindo aplicações de algoritmos como o da árvore de alcançabilidade. Além do mais, deve-se observar que, nesse contexto, o presente trabalho também não é formulado através de cálculos de invariantes.

Resumos Relacionados