Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-02T21:58:30Z
No. of bitstreams: 1
WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-09T12:29:25Z (GMT) No. of bitstreams: 1
WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5) / Made available in DSpace on 2018-07-09T12:29:25Z (GMT). No. of bitstreams: 1
WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5)
Previous issue date: 2018-05-28 / 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. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/25529 |
| Date | 28 May 2018 |
| Creators | Silva, Washington Cavalcante da |
| Contributors | 70600793435, Pimentel, Elaine Gouvea, 84151781668, Reis, Giselle Machado Nogueira, 06651142658, Vega, Carlos Alberto Olarte |
| Publisher | PROGRAMA DE PÓS-GRADUAÇÃO EM MATEMÁTICA APLICADA E ESTATÍSTICA, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0019 seconds