Especificação e verificação de protocolos de votação em lógica linear com focusing

Linear logic (LL) has been consolidated as a good framework for specifying computational systems, since formulas can be interpreted as resources that can be consumed and / or produced during a proof. From the point of view of Proof Theory, LL reconciles the constructive aspect of intuitionistic l...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Silva, Washington Cavalcante da
Outros Autores: Vega, Carlos Alberto Olarte
Formato: Dissertação
Idioma:por
Publicado em: Brasil
Assuntos:
Lógica linear
Focusing
Sistemas de transição
Protocolos de votação
CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA APLICADA E ESTATÍSTICA
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/25529
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-25529
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language por
topic Lógica linear
Focusing
Sistemas de transição
Protocolos de votação
CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA APLICADA E ESTATÍSTICA
spellingShingle Lógica linear
Focusing
Sistemas de transição
Protocolos de votação
CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA APLICADA E ESTATÍSTICA
Silva, Washington Cavalcante da
Especificação e verificação de protocolos de votação em lógica linear com focusing
description Linear logic (LL) has been consolidated as a good framework for specifying computational systems, since formulas can be interpreted as resources that can be consumed and / or produced during a proof. From the point of view of Proof Theory, LL reconciles the constructive aspect of intuitionistic logic with the symmetry of rules in classical logic. Hence, LL offers a more flexible way to model states of a system as well as transitions among those states. We note that the proof search procedure is inherently non-deterministic since there are different ways of proving the same proposition. In order to tame this problem, focused systems have been proposed aiming at reducing the number of choices during the proof search procedure. Roughly, a focused system considers normal form proofs, thus eliminating the occurrences of nonessential proofs that are syntactically different but equivalent. In this work, we present the proof of the completeness of a focused system for LL as well as some other essential properties of this system. In addition, we use the focused system for specifying and verifying voting protocols. Such systems define how a candidate is chosen by tallying votes and computing the final result of an election. We formally specify two voting protocols using transition systems, which naturally model the states and behavior of such protocols. For each system, an encoding in LL is defined and we show that our specification is correct: a focused step corresponds exactly to a transition in the modeled system. Finally, we verify important properties of the voting protocols such as the fact that the system ensures that the election result reflects the voters’ desire.
author2 Vega, Carlos Alberto Olarte
author_facet Vega, Carlos Alberto Olarte
Silva, Washington Cavalcante da
format masterThesis
author Silva, Washington Cavalcante da
author_sort Silva, Washington Cavalcante da
title Especificação e verificação de protocolos de votação em lógica linear com focusing
title_short Especificação e verificação de protocolos de votação em lógica linear com focusing
title_full Especificação e verificação de protocolos de votação em lógica linear com focusing
title_fullStr Especificação e verificação de protocolos de votação em lógica linear com focusing
title_full_unstemmed Especificação e verificação de protocolos de votação em lógica linear com focusing
title_sort especificação e verificação de protocolos de votação em lógica linear com focusing
publisher Brasil
publishDate 2018
url https://repositorio.ufrn.br/jspui/handle/123456789/25529
work_keys_str_mv AT silvawashingtoncavalcanteda especificacaoeverificacaodeprotocolosdevotacaoemlogicalinearcomfocusing
AT silvawashingtoncavalcanteda specificationandverificationofvotingprotocolsinfocusedlinearlogic
_version_ 1773966257053237248
spelling ri-123456789-255292019-01-30T04:34:12Z Especificação e verificação de protocolos de votação em lógica linear com focusing Specification and verification of voting protocols in focused linear logic Silva, Washington Cavalcante da Vega, Carlos Alberto Olarte Pimentel, Elaine Gouvea Reis, Giselle Machado Nogueira Lógica linear Focusing Sistemas de transição Protocolos de votação CNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA APLICADA E ESTATÍSTICA Linear logic (LL) has been consolidated as a good framework for specifying computational systems, since formulas can be interpreted as resources that can be consumed and / or produced during a proof. From the point of view of Proof Theory, LL reconciles the constructive aspect of intuitionistic logic with the symmetry of rules in classical logic. Hence, LL offers a more flexible way to model states of a system as well as transitions among those states. We note that the proof search procedure is inherently non-deterministic since there are different ways of proving the same proposition. In order to tame this problem, focused systems have been proposed aiming at reducing the number of choices during the proof search procedure. Roughly, a focused system considers normal form proofs, thus eliminating the occurrences of nonessential proofs that are syntactically different but equivalent. In this work, we present the proof of the completeness of a focused system for LL as well as some other essential properties of this system. In addition, we use the focused system for specifying and verifying voting protocols. Such systems define how a candidate is chosen by tallying votes and computing the final result of an election. We formally specify two voting protocols using transition systems, which naturally model the states and behavior of such protocols. For each system, an encoding in LL is defined and we show that our specification is correct: a focused step corresponds exactly to a transition in the modeled system. Finally, we verify important properties of the voting protocols such as the fact that the system ensures that the election result reflects the voters’ desire. A lógica linear (LL) tem se consolidado como um bom arcabouço para especificar sistemas computacionais, uma vez que fórmulas podem ser interpretadas como recursos que podem ser consumidos e/ou produzidos. Além disso, do ponto de vista da Teoria da Prova, a LL reconcilia o aspecto construtivo da lógica intuicionista com a simetria da lógica clássica. Desta maneira, é possível, de uma forma mais flexível, modelar estados de um sistema como fórmulas lógicas, e as transições entre esses estados como etapas na construção de uma prova. No entanto, a busca por provas, em geral, não é determinística, pois existem diferentes maneiras de se provar a mesma proposição. Visando reduzir esse problema, um sistema de provas focado pode ser utilizado nesse processo de busca. A grosso modo, um sistema focado considera provas em forma normal, reduzindo assim as ocorrências de provas não essenciais que são sintaticamente diferentes, mas equivalentes no final do processo. Neste trabalho, é apresentada a prova da completude de um sistema focado para a LL, bem como outras propriedades essenciais desse sistema. Além disso, o sistema focado será utilizado para especificar e verificar protocolos de votação, que definem como deve ser escolhido um candidato, feita uma contagem de votos, e divulgado o resultado de uma eleição. Para que isso seja possível, dois protocolos de votação serão especificados formalmente utilizando sistemas de transição de estados, que modelam de forma natural os estados e comportamento de tais protocolos. Junto a isso, para cada sistema, uma especificação em LL será definida e demonstrada que é correta, ou seja, que um passo focado representa uma determinada transição no sistema de estados modelado. Por fim, propriedades inerentes aos protocolos de votação, como a garantia de que o resultado da eleição reflete o desejo dos eleitores, serão apresentadas e demonstradas através de derivações no sistema focado. 2018-07-09T12:29:25Z 2018-07-09T12:29:25Z 2018-05-28 masterThesis SILVA, Washington Cavalcante da. Especificação e verificação de protocolos de votação em lógica linear com focusing. 2018. 111f. Dissertação (Mestrado em Matemática Aplicada e Estatística) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2018. https://repositorio.ufrn.br/jspui/handle/123456789/25529 por Acesso Aberto application/pdf Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM MATEMÁTICA APLICADA E ESTATÍSTICA

Registros relacionados