Repositório Digital

A- A A+

Identificação de nomes ativos em agentes-π baseada em tipos

.

Identificação de nomes ativos em agentes-π baseada em tipos

Mostrar registro completo

Estatísticas

Título Identificação de nomes ativos em agentes-π baseada em tipos
Autor Nascimento, Gleison Samuel do
Orientador Moreira, Alvaro Freitas
Co-orientador Lamb, Luis da Cunha
Data 2005
Nível Mestrado
Instituição Universidade Federal do Rio Grande do Sul. Instituto de Informática. Programa de Pós-Graduação em Computação.
Assunto Cálculo
Metodos formais
Teoria : Ciência : Computação
Resumo Na última década muitos esforços têm sido feitos em verificação formal de propriedades de agentes do cálculo-π. Uma dessas propriedades é a equivalência observacional, que serve para determinar se um processo é equivalente a sua especificação. Contudo, a verificação de equivalência observacional não é um problema trivial. A maioria dos algoritmos destinados a verificação de equivalência são baseados na construção de sistemas de transições rotuladas (π-autômatos). O principal problema com essa abordagem é o grande número de estados envolvidos podendo chegar a um número infinito. Montanari e Pistore mostram que é possível gerar π-autômatos finitos para agentes-π e é possível reduzir a quantidade de estados desses π-autômatos, através da identificação dos nomes ativos. Um nome é semanticamente ativo em um agente se ele pode ser executado de forma observável por ele. Este é um trabalho de análise estática, que tem por objetivo coletar os possíveis nomes ativos contidos em expressões-π, utilizando para isso um sistema de tipos. A vantagem da utilização de sistemas de tipos em relação a outras formas de análise estática é que sistemas de tipos são sistemas lógicos, logo as técnicas de prova da lógica podem ser aproveitadas no estudo de propriedades de sistemas de tipos. Além disso sistemas de tipos são definidos através da estrutura sintática de expressões, facilitando assim as provas por indução estrutural. Assim a principal contribuição deste trabalho é a elaboração do Active-Base-π, um sistema de tipos para a coleta de nomes ativos de expressões-π.
Tipo Dissertação
URI http://hdl.handle.net/10183/6219
Arquivos Descrição Formato
000482691.pdf (318.8Kb) Texto completo Adobe PDF Visualizar/abrir

Este item está licenciado na Creative Commons License

Este item aparece na(s) seguinte(s) coleção(ões)


Mostrar registro completo

Percorrer



  • O autor é titular dos direitos autorais dos documentos disponíveis neste repositório e é vedada, nos termos da lei, a comercialização de qualquer espécie sem sua autorização prévia.
    Projeto gráfico elaborado pelo Caixola - Clube de Criação Fabico/UFRGS Powered by DSpace software, Version 1.8.1.