Título: Uma técnica de verificação para pi-calculus baseada em bi-simulações
up-to e algoritmos de particionamento

Palestrante: Marcelo M. Amorim

Resumo:

Neste seminário será apresentada uma abordagem para o problema de
verificação em pi-calculus. Nessa abordagem são estudadas as vantagens e
desvantagens em aplicar sistemas de normalização e técnicas de prova por
bi-simulações up- to em algoritmos de verificação baseados na construção de
autômatos de transição e no refinamento de partições (partition refinement
algorithm). O objetivo é tentar juntar dois trabalhos propostos na
literatura de verificação em pi-calculus de maneira a obter vantagens
durante o processo. Essa junção consiste em gerarmos os desdobramentos das
transições do processo durante a construção do autômato realizando uma
verificação sintática entre os estados já atingidos durante o desdobramento.
A intenção é de minimizar o número de estados do autômato. Além do possível
ganho em compactação do autômato, conseguimos, em alguns casos, reduzir um
passo necessário na construção do autômato, no qual se faz necessário
encontrar os nomes ativos de um processo.