Logo PUC-Rio Logo Maxwell
ETDs @PUC-Rio
Estatística
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.
Descrição: Arquivo:   
PDF    
COVER, ACKNOWLEDGEMENTS, RESUMO, ABSTRACT AND SUMMARY PDF    
CHAPTER 1 PDF    
CHAPTER 2 PDF    
CHAPTER 3 PDF    
CHAPTER 4 PDF    
CHAPTER 5 PDF    
CHAPTER 6 PDF    
CHAPTER 7 PDF    
APPENDICES PDF