[en] ANALYSIS OF STRATEGIES USING MODEL CHECKING

• Ano de defesa: 2003
• Autor(a) principal: DAVI ROMERO DE VASCONCELOS
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: MAXWELL
• Palavras-chave em Português: [pt] TEORIA DOS JOGOS; [pt] ROLLGAME; [pt] ESTRUTURAS DE KRIPKE; [pt] TRADUCAO; [pt] VERIFICACAO DE MODELOS; [en] GAME THEORY; [en] ROLLGAME; [en] KRIPKE STRUCTURE; [en] TRANSLATION; [en] MODEL CHECKING
• Link de acesso: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4336&idi=1; https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4336&idi=2; http://doi.org/10.17771/PUCRio.acad.4336

[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.