|
|
| RESUMO |
| ADOLFO GUSTAVO SERRA SÊCA NETO.
Usando Lógica para Concorrência - Um Estudo Crítico.
01/12/1996 |
| 1v.
225p.
Mestrado.
UNIVERSIDADE FEDERAL DE PERNAMBUCO -
CIÊNCIA DA COMPUTAÇÃO |
| Orientador(es): RUY JOSÉ GUERRA BARRETO DE QUEIROZ |
| Biblioteca Depositaria:
BIBLIOTECA CENTRAL/UFPE |
|
|
|
| Palavras - chave: |
| Concorrência, lógica, lógica linear |
|
|
|
|
| Banca examinadora: |
|
|
|
|
| RUY JOSÉ GUERRA BARRETO DE QUEIROZ |
|
|
| Linha(s) de pesquisa: |
| LÓGICA E SISTEMAS DEDUTIVOS
Trata-se de subárea de Teoria da Computação em que se estuda, através da lógica matemática, modelos e semântica da computação, fundamentos da dedução automática, teoria dos modelos, computabilidade, teoria da prova, semântica e sistemas dedutivos. |
|
|
| Agência(s) financiadora(s) do discente ou autor tese/dissertação: |
|
|
|
|
|
| Dependência administrativa |
|
|
|
| Resumo tese/dissertação: |
| Concorrência - o estudo da teoria e da prática de sistemas concorrentes - é um assunto muito importante em computação atualmente. Sistemas concorrentes são utilizados em diversas aplicações, por exemplo, no projeto de protocolos de redesde computadores e na modelagem de transações em bancos de dados. Apesar dos avanços ocorridos nesta área nos últimos anos, com o desenvolvimento de vários novos modelos de concorrência (ex. CCS, CSP, PI-cálculo, mi-cálculo), pode-se dizer que ainda existem alguns problemas em aberto nesta área. Por exemplo, a inexistência de bons cálculos básicos tipados para formalização e raciocínio sobre propriedades de processos concorrentes. Alguns trabalhos recentes tentaram relacionar sistemas lógicos a modelos matemáticos de concorrência com o intuito de fornecer uma base lógica para a teoria de concorrência e prover meios para a resolução de problemas através de métodos formais. Os trabalhos neste sentido que apresentam melhores resultados foram aqueles que relacionaram a lógica linear (desenvolvida por Jean-Yves Girard em 1987) ao pi-cálculo, um modelo algébrico de concorrência desenvolvido por Robin Milner.
Nesta dissertação analisamos as principais abordagens para a obtenção de uma base lógica para concorrência. Em primeiro lugar, discutimos em detalhes lógica linear a fim de entender os trabalhos que a utilizam para explicar concorrência. Em seguida, estudamos os modelos algébricos de processos concorrentes (com destaque para CCS e pi-cálculo) e algumas de suas principais características. Vimos então como os trabalhos que utilizam lógica linear se enquadram no contexto dequeles que relacionam lógica e concorrência. Os trabalhos com lógica linear baseiam-se no paradigma "provas como processos" de Samson Abramsky, uma variação do paradigma já bastante estebelecido "proposições como tipos" para o mundo da concorrência. O paradgma "proposições como tipos" por sua vez, é a base da bem-sucedida Interpretação Funcional de Curry-Howard (que fornece uma base lógica e um sistema de tipos para programação funcional, relacionando-a à lógica intuicionista). Apesar de não ter sido completamente bem sucedido com relação aos objetivos propostos por Abramsky, o trabalho de Gianluigi Bellin e Phil Scott sobre a correspondência entre a lógica linear e o pi-cálculo obteve resultados significativos e serve como base para futuros trabalhos relacionando lógica e concorrência.
Por fim, discutimos sucintamente a possibilidade de utilizar os Sistemas Dedutivos Rotulados de Dov Gabbay com o objetivo semelhante de fornecer uma base lógica para concorrência baseada na Interpretação Funcional de Curry-Howard. |
|
|
|
|
|
| Para alterar os dados da tese, digite o CPF: |
|
|
|
|
| As informações constantes desta base de dados são fornecidas diretamente à CAPES pelos programas de pós-graduação mantidos por universidades e instituições de pesquisa brasileiras e são de sua inteira responsabilidade. O uso da base de dados e de seus registros está sujeito a todas as leis de direitos autorais aplicáveis. |
|
|
|
|
|
