Contribuições ao controle supervisório utilizando técnicas de verificação formal e sistemas modelados por redes de Petri

Abstract

A resolução de diferentes problemas relacionados aos Sistemas a Eventos Discretos deu origem a duas classes de técnicas bem definidas. De um lado estão as técnicas de síntese automática de supervisores, cuja maior contribuição é a menor interação com o projetista durante o processo de cálculo. De outro lado, as técnicas de verificação formal, que permitem ao projetista verificar se uma dada especificação é válida para um sistema (controlado ou não). Dentro deste contexto, o presente trabalho contribui para a unificação destas técnicas, ao incorporar sistemas de equações escritas em µ-calculus ao processo de síntese de supervisores em sistemas modelados por redes de Petri. Após a etapa de determinação do comportamento minimamente restritivo, utiliza-se a Teoria das Regiões para implementar o supervisor por meio da adição de lugares de controle à rede de Petri que modela o comportamento do sistema em malha aberta. Para isto, utilizam-se alguns princípios das abordagens Ziller e Schneider e Ghaffari et al., em conjunto com alguns aspectos peculiares. O principal resultado é a proposta de uma nova metodologia tão flexível e computacionalmente eficiente quanto a abordagem Ramadge e Wonham, permitindo a resolução de alguns exemplos tratados na literatura. Ao herdar as boas características das abordagens anteriores, a metodologia proposta também pode ser generalizada, de forma que problemas não abordados diretamente pela abordagem Ramadge e Wonham possam ser tratados. Como principais ferramentas de apoio, foram utilizados os softwares Tina e MEC. Por último, são apresentadas perspectivas visando incorporar explicitamente aspectos temporais ao processo de síntese.