Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2017. / Submitted by Fernanda Percia França (fernandafranca@bce.unb.br) on 2017-04-26T14:09:10Z No. of bitstreams: 1 2017_ThiagoMendonçaFerreiraRamos.pdf: 615472 bytes, checksum: 07c6f1995d15d71ca3dce6b9186c1bb8 (MD5) / Approved for entry into archive by Raquel Viana(raquelviana@bce.unb.br) on 2017-04-27T22:18:25Z (GMT) No. of bitstreams: 1 2017_ThiagoMendonçaFerreiraRamos.pdf: 615472 bytes, checksum: 07c6f1995d15d71ca3dce6b9186c1bb8 (MD5) / Made available in DSpace on 2017-04-27T22:18:25Z (GMT). No. of bitstreams: 1 2017_ThiagoMendonçaFerreiraRamos.pdf: 615472 bytes, checksum: 07c6f1995d15d71ca3dce6b9186c1bb8 (MD5) / Terminação é uma propriedade crítica para formalização de correção de programas. Verificar automaticamente terminação de um programa é conhecido como Problema da Parada e Turing provou que é um problema indecidível. Apesar disso, é possível construir algoritmos de semi decisão para verificar terminação, que respondem ‘sim’ se pode provar que o algoritmo para e ‘não sei’ caso contrário. Para construir esses algoritmos de semi decisão é necessário considerar diferentes noções de terminação, provando que são equivalentes. Neste trabalho, noções de terminação são formalizadas equivalentes para uma linguagem funcional de primeira ordem chamada PVS0 usando o assistente de prova Prototype Verification System. Essas noções são: as funções produzem uma saída, a árvore de derivação de chamados recursivos de funções tem tamanho finito (ambas as noções são chamadas terminação semântica), e os argumentos das funções decrescem para cada chamado recursivo (essa noção é chamada ranking function). As contribuições desse trabalho incluem a formalização de alguns lemas necessários para demonstrar equivalência entre noções de terminação semântica e ranking function, e como resultado principal a formalizações de indecidibilidade do Problema da Parada e Turing-Completude de PVS0. / Termination is a critical property for the formalization of programs correctness. Verifing automatically termination of a program for an input is known as Halting Problem and Turing proved that this is undecidable. However, it is possible to build semi decision algorithms for the verification of termination, that answer ‘yes’ if it is possible to prove that the algorithm halts, and ‘do not know’ otherwise. To construct these semi decision algorithms it is necessary to consider different notions of termination, proving that they are equivalent. In this work, notions of termination were formalized equivalent for a minimal functional first order language called PVS0 using the proof assistant Prototype Verification System. These notions are: the functions produces an output, the derivation tree of recursive calls of functions has a finite size (both these notions are called semantic termination), and the arguments of functions decreases for each recursive call (this notion is called ranking function). The contributions of this work includes formalization of lemma related with the equivalence between notions of semantic and ranking function termination, and the main results are the formalization of indecidability of Halting Problem and Turing-Completeness of PVS0.

Dissertação (mestrado)—Universidade de Brasília, Departamento de Economia, 2011. / Submitted by Shayane Marques Zica (marquacizh@uol.com.br) on 2011-09-28T21:01:15Z No. of bitstreams: 1 2011_JoseBorgesdaSilvaNeto.pdf: 916247 bytes, checksum: afee5ac041d27d9a8e3f3dcf43ffa6f9 (MD5) / Approved for entry into archive by LUCIANA SETUBAL MARQUES DA SILVA(lucianasetubal@bce.unb.br) on 2011-10-03T16:28:20Z (GMT) No. of bitstreams: 1 2011_JoseBorgesdaSilvaNeto.pdf: 916247 bytes, checksum: afee5ac041d27d9a8e3f3dcf43ffa6f9 (MD5) / Made available in DSpace on 2011-10-03T16:28:20Z (GMT). No. of bitstreams: 1 2011_JoseBorgesdaSilvaNeto.pdf: 916247 bytes, checksum: afee5ac041d27d9a8e3f3dcf43ffa6f9 (MD5) / A telefonia móvel tem sido apresentada como um resultado de grande sucesso do novo modelo de organização das telecomunicações do Brasil instituído no final da década de 1990. De fato, hoje a telefonia móvel é o mais popular serviço de telecomunicação. No entanto, o problema de acesso é um aspecto estrutural que existe em todas as redes de telecomunicações. Diante desse fato, a probabilidade de exercício de práticas anticompetitivas associadas à terminação móvel é alta. A principal evidência disso é a definição de excessivos preços de terminação móvel no regime de Calling Party Pays (CPP). Assim, esse estudo investiga os estímulos anticompetitivos presentes na terminação móvel no Brasil. Como se verifica nos conflitos de definição dos preços de terminação móvel, os sinais de poder de mercado na terminação móvel são incontroversos. De forma mais grave, há sérias suspeitas de estrangulamento de margens. Essa conduta está ancorada na discriminação entre os preços on-net e os preços off-net pelas operadoras móveis, viabilizada pelos elevados preços de terminação móvel. Por meio de um teste de estrangulamento de margens, os resultados indicam fortes evidências de estrangulamento de margens. _______________________________________________________________________________ ABSTRACT / Mobile telephony has been presented as a result of the highly successful new model of telecommunications in Brazil established in the late 1990s. In fact, today mobile telephony is the most popular telecommunication service. However, the access problem is a structural feature that exists in all telecommunications networks. Given this fact, the probability of exercise of anticompetitive practices associated with the mobile termination is high. The main evidence is the excessive mobile termination rates in the regime of Calling Party Pays (CPP). Thus, this study investigates anticompetitive stimuli present in the mobile termination in Brazil. As shown in the pricing conflicts of mobile termination, signs of market power in mobile termination are incontrovertible. More severe, there are serious suspicions of price squeeze. This approach is anchored in price discrimination between on-net and off-net prices by mobile operators, made possible by high mobile termination rates. By means of a price squeeze test, the results indicate strong evidence of a price squeeze.