[pt] Em métodos formais, uma das abordagens que vem obtendo sucesso nos últimos anos é a de verificação formal. Dentro desta, vem se destacando uma técnica chamada de verificação de modelos (model checking), na qual se verifica automaticamente a validade de propriedades em sistemas acerca do funcionamento de um sistema. Atualmente, a verificação de modelos é muito empregada em informática na verficação formal de software e hardware, mas tem sido utilizada em outra áreas, como em matemática e em economia. Esta dissertação visa aplicar verificação de modelos a problemas de economia. O tema da pesquisa seria delimitado à Teoria dos Jogos. Algumas inadequações foram observadas, fazendo-se necessário algumas novas definições: uma definição de qualitativa que se utiliza de uma linguagem lógica denominada de Game Analysis Logic (GAL); uma linguagem para descrever jogo denominada de RollGame (Romero - All Game); uma tradução de RollGame na linguagem de especificação de modelos; uma tradução da definição de jogo em estrutura de Kripke. Observou-se ainda que com a utilização de model checking em jogos consegue- se analisar estratégias de jogadores. Uma ferramenta para automatizar a tradução de RollGame em model checking foi desenvolvida, chamada de StratAn-RollGame (Strategy Analyzed using RollGame). Assim, a presente dissertação demonstrou que de fato é possível utilizar verificação de modelos em outras areas. / [en] In formal methods, one of the approaches that have been successful lately is Model Checking, which consists in a technique to achieve automatic verification about a system behavior. Nowadays, the model checking is very frequently employed in computer science to formal verification of software and hardware, but it is not used in other knowledge fields, such as mathematics and economics. The purpose of this research is to apply model checking in economics problems, using Game Theory. Some inadequacies have been observed. Therefore, it is necessary to create new definitions: a generic and qualitative definition of game that uses one logic language called Game Analysis Logic (GAL); a new language to describe game called RollGame (Romero + All Game); a translation from RollGame to a language of model specification; a translation from game definition to Kripke structure. It is also been observed that the use of model checking makes it possible to analyze players strategies. One tool, called StratAn-RollGame (Strategy Analyzed using RollGame), makes the translation from RollGame to model Checking automatic. Thus, the present research has demonstrated that is possible indeed to use model checking in other knowledge fields.

[pt] O Objetivo deste trabalho é prover os fundamentos necessários ao desenvolvimento de uma metodologia voltada para a análise e desenho das estratégias, regras e regulamentos associados ao setor elétrico, sob o contexto da teoria dos jogos evolutivos. A importância da escolha de estratégias eficientes, que formem perfis de estratégias com melhores payoffs traz a necessidade de uma abordagem que leve em conta as interações entre os agentes, submersos às incertezas regulatórias, hidrológicas e mercadológicas, existentes no setor elétrico, que geram superfícies de payoff descontínuas e ruidosas. É demonstrado como tais superfícies descontínuas podem ser desmembradas em um hiperespaço de estratégias mistas, onde órbitas regidas por dinâmicas baseadas em equações diferenciais convergirão para os perfis de equilíbrios atratores estáveis no sentido assintótico. Para a modelagem é sugerida a utilização de estratégias comportamentais, que possuem a propriedade de gerar perfis em equilíbrio mais robustos às constantes mudanças, assim como propiciar a análise entre os ambientes cooperativos e competitivos. / [en] The objective of this thesis is to provide the crucial points to the development of a methodology focused on the analysis of strategies, rules and regulations connected with the electrical sector, under the context of the evolutionary game theory. The importance of choosing efficient strategies responsible for profiles, with better payoffs, displays the approach regarding the interactions among agents under regulatory, hydrological and market uncertainties, which are present in the electrical sector, resulting in noncontinuous and noisy payoffs surfaces. It is demonstrated that the already mentioned non-continuous surfaces can be expanded in a hyper-space of mixed strategies, where orbits governed by the dynamics based on differential equations, will converge to profiles of stable attractive equilibrium, in an asymptotic meaning. In order to achieve the modeling, is suggested the employment of behavioral strategies, which possess the role of creating equilibrium profiles, immune to the frequently changes, as well as to propitiate the analysis in cooperative and competitive scenarios.

[pt] O principal objetivo deste trabalho é utilizar a teoria dos jogos para analisar as estratégias de um plano de recuperação judicial proposto por uma empresa. O princípio que envolve a recuperação está ligado à função social da empresa, que nada mais é do que toda função que ela possui para a sociedade do local onde se encontra. A teoria dos jogos é um ramo da matemática que também é conhecida como ciência da estratégia e, como o próprio nome diz, estuda as situações estratégicas onde os jogadores escolhem diferentes ações na tentativa de obter o melhor retorno possível nas suas escolhas. Para fazer essa análise tomamos o plano de recuperação judicial da empresa Oi S/A e detalhamos as estratégias de pagamento oferecidas por ela. Avaliando assim a melhor estratégia para a empresa e por consequência a melhor estratégia também para os credores envolvidos. Um jogo onde existe uma situação que é considerada ideal para ambas as partes é considerado um jogo que cada pessoa envolvida toma suas decisões para benefício próprio, mas em nossas análises podemos observar que nem sempre na recuperação judicial poderemos avaliar o jogo desta maneira, afinal se um credor optar por este tipo de jogo em um cenário mais racional, o prejuízo financeiro e social acabará sendo maior do que se optar por um jogo onde exista uma cooperação entre os jogadores e que trará um retorno positivo e onde a empresa obterá maiores prazos e condições de pagamento. / [en] The main objective of this work is to use game theory to analyze the strategies of a judicial recovery plan proposed by a company. The principle that involves recovery is linked to the social function of the company, which is nothing more than any function it has for society in the place where it is. Game theory is a branch of mathematics that is also known as the science of strategy and, as the name implies, studies the strategic situations in which players choose different actions in an attempt to obtain the best possible return on their choices. To do this analysis we take the legal recovery plan of the company Oi S / A and detail the payment strategies offered by it. Evaluating the best strategy for the company and consequently the best strategy also for the creditors involved. A game where there is a situation that is considered ideal for both parties is considered a game that each person involved makes their decisions for their own benefit, but in our analyzes we can observe that not always in judicial recovery we can evaluate the game in this way, a lender opts for this type of game in a more rational scenario, the financial and social loss will be greater than if you opt for a game where there is a cooperation between the players and that will bring a positive return and where the company will obtain longer deadlines and payment conditions.

[pt] O objetivo desta dissertação é demonstrar que mesmo em ambientes em que a decisão do individuo não segue a racionalidade, podemos obter uma estratégia ótima. Com o auxilio do equilíbrio evolucionariamente estável (ESS), conseguimos analisar casos diferentes da literatura usual de teoria dos jogos em que mesmo com escolhas sem racionalidade, encontramos a melhor estratégia, para tal usaremos a metodologia do jogo de opções, união entre a teoria dos jogos e a metodologia de opções reais, juntamente com o conceito de equilíbrio evolucionariamente estável (ESS). Isso é demonstrado através da modelagem de um mercado duopolista assimétrico, sujeito a incertezas. Neste trabalho as firmas são diferentes, existe um duopólio assimétrico. Aqui as empresas são não homogêneas porque uma empresa tem custo operacional mais baixo do que a outra para o mesmo investimento. Isto significa que uma empresa tem vantagem competitiva sobre a rival. Os resultados do modelo mostram que, dependendo do tipo de estratégia assumida pela empresa, é possível que a empresa de baixo custo se torne líder como na literatura usual e em alguns casos encontramos que diferente da expectativa usual é possível que a empresa de alto custo venha a se tornar líder e demonstra que a premissa de racionalidade não é necessária para a escolha inicial da empresa utilizando o conceito de ESS para definir o equilíbrio assim como foi feito no trabalho de Xiao e Yu (2006). / [en] The objective of this dissertation is show that even in environments where the decision of the individual not follow rationality, we can get a optimal strategy. with the help of evolutionarily stable strategy, we analyze different cases of the usual literature on game theory that even with choices without rationality, we find the best strategy, for that we will use the option game methodology, which is the union between gaming theory methodology and option game methodology, with the concept of evolutionarily stable strategy (ESS). This is demonstrated through modeling of a duopolistic market, with uncertainties, in this dissertation firms are different. Here companies has no-Homogeneous cost because a company has lower operating costs than the other for the same investment. This means that a company has competitive advantage over rival. The model results show that, depending on the strategy assumed by the company it is possible that the low-cost company to become leader as usual in the literature and in some cases also shows that is possible to the high cost company to become leader and demonstrates that the premise of rationality are not necessary for choosing initial strategy, the company can find equilibrium using the concept of ESS to set the balance as was done in the paper of Xiao and YU (2006).

[pt] Utilizando o instrumental da teoria dos jogos evolucionários, a proposta desta dissertação é analisar as interações entre emissores de dívida e agências de avaliação de risco de crédito em um ambiente com assimetria de informação. Enquanto os primeiros precisam das notas emitidas pelas agências para acessar fontes de financiamentos no mercado, as agências são remuneradas pela prestação desse serviço. Os resultados mostram que, de forma geral, quando o número de emissores grau de investimento é pequeno, incentiva-se a adoção de uma estratégia pouco transparente de divulgação de informação por parte do emissor, aumentando a assimetria de informação. A melhor resposta das agências é utilizar uma análise básica do perfil de crédito de seus clientes. O aumento do número de emissores grau de investimento na economia incentiva o aperfeiçoamento das políticas corporativas de transparência, enquanto as agências sofisticam sua análise com o objetivo de evitar os custos de reputação associados a erros de avaliação. Empiricamente, os resultados são condizentes com a evolução da economia colombiana nas últimas décadas. A melhoria do ambiente macroeconômico desse país atraiu emissores grau de investimento incentivando a atuação de agências que utilizam metodologia de análise sofisticada e emissores que adotam uma estratégia transparente de divulgação de suas informações. / [en] Using evolutionary game theory, this work aims to analyse the interactions between debt issuers and credit rating agencies in an asymmetric information environment. While the ratings grades are required by issuers to access funding sources for their investment projects, the agency s revenue is provided by this service. The results show that when the number of investment grade issuers is small, non-transparency strategy and basic methodology of analysis dominate, worsening the information asymmetry problem. The increase in the number of investment grade issuers encourages transparency policies while the agencies adopt a sophisticated analysis, avoiding the reputation costs associated with errors. Empirically, the results are consistent with the evolution of the Colombian economy in recent decades. The country s improvement in the macroeconomic environment attracted investment grade issuers encouraging the proliferation of sophisticated rating agencies and transparent issuers.

[pt] Este trabalho objetiva a definir as motivações, benefícios e limitações de atuação – e protagonismo – de empresas para a gestão dos recursos hídricos em nível de bacia hidrográfica. Aborda a bacia como espaço de conflito e cooperação, demonstrando como o conflito ante a escassez hídrica atual ou iminente é constantemente o resultado da (falta de) interação cooperativa entre os atores. Aprofunda, ainda, sobre a disputa pelo uso da água ante a lógica da interdependência água-energia-alimento e argumenta, a partir de uma análise da Teoria dos Jogos, que o conflito é consequência da falta de diálogo e de expectativas diferentes entre os atores. Por fim, demonstra como esses gaps podem ser, e já são, superados a partir da liderança de atores empresariais, enfatizando os ganhos potenciais da ação e gargalos para seu sucesso. / [en] The economic and population growth of the last two centuries presents a clear challenge to the management of water resources, easily explained by the relationship between supply and demand as well. Going beyond the usual categorization on the availability of fresh and salt water in the world, as important it is to mention the total amount of water on Earth. The water supply remains stable in absolute amounts on the planet, ranging just from where it can be captured and subsequent used, as well as its quality. Natural to say that water security is closely connected to food, energy, climate and, ultimately, to the classic sense of security of countries. It should be considered the tenuous balance between water availability and its multiple uses; agricultural production and the supply needs; generation by hydropower and growing energy demand; and changes of the hydrological cycle and changes in rainfall and flow. Globally, it is projected a growth of over 60 percent on water demand, driven mainly by rising industrial demand and power generation. (OECD, 2012) In Brazil, water management is largely decentralized since 1997 s Water Law. This means that the discussions, definitions, policies and actions with respect to water resources management in Brazil is made largely by local actors that are more affected. Institutionally, the Watershed Committees are the formal space for this dialogue. In this dynamic of Watershed Committees, given that participation is precisely from those who have the most interest in better use by availability and quality of water of the watershed, there is a great possibility that those users make choices that optimize the potential for multiple uses water, maximizing the possibility of continuity of their activities. This work analyzes the duality between conflict and cooperation in these scenarios, especially at the logic of the water-energy-food nexus. To this end, it uses concepts of Games Theory to demonstrate how rational actors tend to take collective decisions potentially bad for everyone precisely due their visions of maximization of their own gains. Finally, in the other hand, it presents the overcoming of these joint performance gaps in favor of the collective good from the institutionalization of a better-concerted action by the leadership of the business sector.

[pt] Este trabalho tem por objetivo analisar uma das formas de financiamento da República Federativa do Brasil: a venda de títulos da dívida pública. Para isso serão analisadas diversas informações oficiais dos órgãos competentes, relacionadas às regras que permeiam este tipo de negociação. Além disso, serão explorados trabalhos correlatos e suas principais contribuições. Por fim, o texto busca mostrar qual formato de leilão é, teoricamente, a mais vantajosa para o Tesouro Nacional negociar seus títulos de dívida. / [en] This work aims to analyze one of the forms of financing the Federative Republic of Brazil: the sale of government bonds. For this, varied information from official agencies related to the rules that govern this type of negotiation will be analyzed. In addition, related works and their main contributions will be explored. Finally, the text seeks to show which auction format is, theoretically, the most advantageous for the National Treasury to negotiate its debt securities.

[pt] A consideração dos custos de transmissão associados a cada projeto é fundamental para que as comparações econômicas dos custos totais de geração entre tecnologia sejam realizadas corretamente. Os custos de transmissão tendem a ser elevados para usinas distantes dos centros de carga; ou reduzidos para usinas próximas dos centros de carga. O custo de transmissão de cada agente é calculado a partir de uma tarifa, cujo valor depende do ponto de conexão e deveria refletir o sinal locacional da parcela da rede efetivamente utilizada. As metodologias existentes têm limitações que atenuam consideravelmente o sinal locacional, e, consequentemente, necessitam de fatores de ajuste conhecidos como selo, que podem ser bastante significativos quando comparados com a parcela locacional. Uma limitação importante das metodologias existentes é não considerar múltiplos cenários de despacho, sobretudo em países com forte presença de hidrelétricas, podendo influenciar bastante a alocação e criar um problema de recuperação de custos. Outro tema abordado é o cálculo da tarifa de transmissão diferenciada por patamar de carga, cujo benefício é possibilitar que os consumidores respondam ao sinal econômico da tarifa de transmissão, aumentando a eficiência econômica. Esta dissertação apresenta uma nova metodologia com base no esquema Aumann Shapley (AS) que incorpora o tema dos múltiplos cenários de despacho e cálculo da tarifa de transmissão diferenciada por patamar de carga. Para ilustrar a aplicação da metodologia proposta foi utilizado um sistema teste de 3 barras e o sistema elétrico da Bolívia. A metodologia proposta é comparada com as seguintes metodologias: (i) Participações Médias; (ii) Metodologia Nodal ou Custo Marginal de Longo Prazo (CMLP); e (iii) AS Original. Os resultados mostraram que a utilização da metodologia proposta melhorou significativamente o sinal locacional, reduzindo a necessidade complementação com a parcela selo da tarifa de transmissão. / [en] The consideration of transmission costs is essential for an isonomic economic valuation of generation projects due to the competition among different sources. The transmission costs tend to be greater for power plants located far from the load centers than for those that are closer. The transmission cost of each agent is calculated through a tariff, whose value depends on the point of connection and might reflect a locational signal of the transmission network s portion effectively used. The existing methodologies have limitations that greatly hinders the locational signal, therefore, is required a complementary charge known as postage stamp that can be quite significant when compared with the locational portion. The existing methodologies do not consider the multiple dispatch scenarios for allocation of the transmission costs, which is a very important issue and can greatly influence the allocation and create a cost recovery problem, especially in countries with a strong presence of hydroelectric plants. Another important issue to be considered in methodologies for allocation of transmission costs is the calculation of the transmission tariff varying in accordance with the load blocks, whose benefit is enable the consumers to respond to the transmission tariff s economic signal, increasing economic efficiency. This thesis presents a new methodology based on the AS scheme that incorporates the multiple dispatch scenarios and provides the calculation of the transmission tariff per load block. To illustrate the application of the proposed methodology, it was used a 3 bus test system and the Bolivian power system. The proposed methodology is compared with the following methods: (i) Average Participation Factors (APF); (ii) Long Run Marginal Cost (LRMC) and (iii) Original AS. The results showed that the use of the proposed methodology significantly improved the locational signal, reducing the need of the postage stamp portion of the transmission tariff.

[pt] No ramo imobiliário, a tomada de decisão deve ser rápida e precisa. São muitas as incertezas que podem afetar um projeto. Por isso, o Estudo de Viabilidade é fator determinante de sucesso ou fracasso de uma incorporação. Hoje o método de análise largamente utilizado é o do Fluxo de Caixa Descontado (FDC), onde o valor do projeto e seus parâmetros de resultado baseiam-se no Valor Presente Líquido (VPL) do fluxo. Porém, este método não considera as diferentes decisões gerenciais que podem ser tomadas durante a vida útil do empreendimento em função de novas informações adquiridas ao longo do tempo. A decisão gerencial pode atuar mudando o rumo do empreendimento de maneira a maximizar os resultados a serem obtidos e mensurar seu real valor. Este trabalho se propõe a, de forma simples, introduzir a ferramenta de análise pela Teoria de Opções Reais (TOR), abordada na literatura, mas ainda negligenciada pelo mercado imobiliário. Esta teoria utilizada isoladamente não é capaz de retratar o dia-a-dia do incorporador. No mercado, a TOR torna-se falha utilizada sem a abordagem da Teoria dos Jogos, por não considerar os efeitos nocivos da concorrência nos objetivos da empresa. Sendo assim, o objetivo foi não só auxiliar na melhor avaliação de projetos pela TOR, considerando incertezas das mudanças econômicas mundiais e flexibilidade de tomada de decisão na maximização do resultado, como também analisar pela Teoria dos Jogos, a influência dos concorrentes nos objetivos inerentes ao projeto. / [en] In Real Estate, the decision must be fast and accurate. There are many uncertainties that may affect projects. Therefore, the economic feasibility study is a critical factor of success or failure of an estate project. Currently the widely used analytical method is the discounted cash flow, in which the project s outcome and value are based on Net Present Value of the cash flow. However, this method does not consider the various management decisions that may be taken during the project life. The management decision may influence changing the course of estate development to maximize the financial results and measure their real value. This work aims to, in a simple way, introduce the analytical tool for Real Options Theory (ROT), discussed in the literature, but still neglected by the real estate market. This theory used in isolation isn t able to portray the developers daily. In the real estate market, the ROT becomes incorrect used without the Game Theory concepts, disregarding the competition effect s on the company s goals. Therefore, this work goes beyond a better project assessment through ROT, considering economic uncertainties and flexibility on decision making, but also considering the perspective of game theory, adding the influence of competitors actions on projects goals.

[pt] O termo jogo tem sido utilizado como uma metáfora, em várias áreas do conhecimento, para modelar e analisar situações onde agentes(jogadores) interagem em ambientes compartilhados para a realização de seus objetivos sejam eles individuais ou coletivos. Existem diversos modelos propostos para jogos por diferentes áreas do conhecimento, tais como matemática, ciência da computação, ciência política e social, entre outras. Dentre as diversas formas de modelar jogos examinamos a Teoria dos Jogos e as lógicas para jogos. Neste trabalho apresentamos uma lógica modal de primeira-ordem baseada na lógica CTL, chamada de Game Analysis nalysis Logic, para raciocinar sobre jogos. Relacionamos os principais modelos da Teoria dos Jogos (jogo estratégico, extensivo, e de coalizão) e seus principais conceitos de soluções(equilíbrio de Nash, equilíbrio de subjogo perfeito,e core) aos modelos de GAL e às fórmulas de GAL, respectivamente. Além disso, estudamos as alternativas de quantificação De Re e De Dicto no contexto dos jogos extensivos, caracterizando o conceito de equilíbrio de Nash e equilíbrio de subjogo perfeito de acordo com as alternativas de quantificação. Relacionamos as lógicas Alternating-time lternating-Tempomporal Logic (A ATL) TL) e Coalitional Game Logic (CGL) com a lógica GAL, demonstrando que ambas as lógicas são fragmentos da lógica GAL. Outro resultado deste trabalho é caracterizar uma classe de sistemas multi- agentes,que é baseada na arquitetura de agentes Belief-Desir Desire- Intention(BDI), para a qual existem jogos extensivos e vice-v versa. Como conseqüência, os critérios de racionalidade da Teoria dos Jogos podem ser aplicados diretamente para agentes BDI e vice-versa. Assim, a abordagem deste trabalho pode ser utilizada para analisar sistemas multi-agentes. Do ponto de vista prático, apresentamos um verificador de modelos para a lógica GAL. Diversos estudos de casos são realizados utilizando o verificador de modelos. / [en] Games are abstract models of decision-making in which decision-makers(players)interact in a shared environment to accomplish their goals. Several models have been proposed to analyze a wide variety of applications in many disciplines such as mathematics, computer science and even political and social sciences among others. In this work, we focus on Game Theory and Game Logics. We present a first-order modal logic based on CTL, namely Game Analysis Logic (GAL), to model and reason about out games. The standard models of Game Theory (strategic games, extensiv games and coalition games) as well as their solution concepts (Nash equilibrium, subgame perfect equilibrium and co re),respectively, are express as models dels of GAL and formulas of GAL. Moreover, we study the alternatives of De Re and De Dicto quantification in the context of extensive games. We also show that two of the most representative game logics, namely Alternating-time lternating-Temp empor oral Logic (A ATL) TL) and Coalitional Game Logic (CGL), are fragments of GAL. We also characterize haracterize a class of multi-agent systems, which is based on the architecture Belief-Desire- Intention (BDI), for which there is a somehow equivalent class of games and vice-versa. As a consequence, criteria of rationality for agents can be directly applied to players and vice-versa. Game analysis formal tools can be applied to MAS as well. From a practical poin of view, we provide and develop a model-checker for GAL. In addition, we perform case studies using our prototype.