Verificação de conflito na supervisão de sistemas concorrentes usando abstrações

Abstract

A explosão do espaço de estados associada ao teste para detecção do conflito é um dos principais problemas que impedem a aplicação da Teoria de Controle Supervisório de Sistemas a Eventos Discretos a sistemas industriais reais. O conflito é uma propriedade global dos sistemas concorrentes sendo que, para sua detecção, deve-se verificar não-bloqueio da composição dos subsistemas que estão sendo verificados. Esta tese trata do problema de detecção de conflito de forma eficiente. Neste trabalho, propõe-se um novo teste de não-conflito baseado em abstrações dos supervisores, obtidas pela operação de projeção natural. Apresentam-se dois conjuntos de condições sobre as abstrações para os quais o teste de não-conflito pode ser aplicado, com resultado equivalente àquele do teste sobre os supervisores originais. No primeiro conjunto de condições os eventos compartilhados são mantidos nas abstrações e a projeção deve possuir a propriedade do observador. O segundo conjunto de condições sobre as abstrações leva em conta propriedades estruturais dos supervisores originais para derivar o conjunto de eventos a serem mantidos nas abstrações, além da propriedade do observador sobre a projeção obtida. As duas abordagens podem ser utilizadas em conjunto para obter abstrações possivelmente melhores, de forma a obter maior redução do espaço de estados na verificação de não-conflito. Apresenta-se ainda um algoritmo para verificação da propriedade do observador. Esta propriedade é utilizada exaustivamente nos resultados apresentados e sua verificação torna-se de grande interesse para a aplicação dos resultados obtidos.