[en] ANALYSIS OF STRATEGIES USING MODEL CHECKING

DAVI ROMERO DE VASCONCELOS

[pt] ANÁLISE DE ESTRATÉGIAS UTILIZANDO VERIFICAÇÃO FORMAL DE MODELOS

dc.contributor	EDWARD HERMANN HAEUSLER
dc.creator	DAVI ROMERO DE VASCONCELOS
dc.date	2003-12-29
dc.date.accessioned	2022-09-21T21:42:11Z
dc.date.available	2022-09-21T21:42:11Z
dc.identifier	https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4336@1
dc.identifier	https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4336@2
dc.identifier	http://doi.org/10.17771/PUCRio.acad.4336
dc.identifier.uri	https://hdl.handle.net/20.500.12032/42439
dc.description	[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.
dc.description	[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.
dc.language	pt
dc.publisher	MAXWELL
dc.subject	[pt] TEORIA DOS JOGOS
dc.subject	[pt] ROLLGAME
dc.subject	[pt] ESTRUTURAS DE KRIPKE
dc.subject	[pt] TRADUCAO
dc.subject	[pt] VERIFICACAO DE MODELOS
dc.subject	[en] GAME THEORY
dc.subject	[en] ROLLGAME
dc.subject	[en] KRIPKE STRUCTURE
dc.subject	[en] TRANSLATION
dc.subject	[en] MODEL CHECKING
dc.title	[en] ANALYSIS OF STRATEGIES USING MODEL CHECKING
dc.title	[pt] ANÁLISE DE ESTRATÉGIAS UTILIZANDO VERIFICAÇÃO FORMAL DE MODELOS
dc.type	TEXTO

Files in this item

Files	Size	Format	View
There are no files associated with this item.

This item appears in the following Collection(s)

Documentos - PUC-RIO

Show simple item record