Título: | ANALYSIS OF STRATEGIES USING MODEL CHECKING | ||||||||||||||||||||||||||||||||||||||||||||||||
Autor: |
DAVI ROMERO DE VASCONCELOS |
||||||||||||||||||||||||||||||||||||||||||||||||
Colaborador(es): |
EDWARD HERMANN HAEUSLER - Orientador |
||||||||||||||||||||||||||||||||||||||||||||||||
Catalogação: | 29/DEZ/2003 | Língua(s): | PORTUGUESE - BRAZIL |
||||||||||||||||||||||||||||||||||||||||||||||
Tipo: | TEXT | Subtipo: | THESIS | ||||||||||||||||||||||||||||||||||||||||||||||
Notas: |
[pt] Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio. [en] All data contained in the documents are the sole responsibility of the authors. The data used in the descriptions of the documents are in conformity with the systems of the administration of PUC-Rio. |
||||||||||||||||||||||||||||||||||||||||||||||||
Referência(s): |
[pt] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=4336&idi=1 [en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=4336&idi=2 |
||||||||||||||||||||||||||||||||||||||||||||||||
DOI: | https://doi.org/10.17771/PUCRio.acad.4336 | ||||||||||||||||||||||||||||||||||||||||||||||||
Resumo: | |||||||||||||||||||||||||||||||||||||||||||||||||
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.
|
|||||||||||||||||||||||||||||||||||||||||||||||||
|