Neste trabalho, apresentamos uma abordagem para o problema de verificação em `pi¦-calculus. Na nova 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. Durante este trabalho de pesquisa, a junção das duas técnicas foi implementada em um protótipo. Seções de testes e exemplos utilizando este protótipo são apresentadas

not available