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...
Na minha lista:
| Autor principal: | |
|---|---|
| Outros Autores: | |
| Formato: | Dissertação |
| Idioma: | por |
| Publicado em: |
Brasil
|
| Assuntos: | |
| Endereço do item: | https://repositorio.ufrn.br/jspui/handle/123456789/25529 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| Resumo: | 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. |
|---|