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.