Vega, Carlos Alberto OlarteSilva, Washington Cavalcante da2018-07-092018-07-092018-05-28SILVA, 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/25529Linear 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.Acesso AbertoLógica linearFocusingSistemas de transiçãoProtocolos de votaçãomasterThesisCNPQ::CIENCIAS EXATAS E DA TERRA::MATEMATICA APLICADA E ESTATÍSTICA