[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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:4336 |
| Date | 29 December 2003 |
| Creators | DAVI ROMERO DE VASCONCELOS |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | English |
| Type | TEXTO |
Page generated in 0.7349 seconds