"Busquei, primeiro, o amor, porque ele produz um êxtase - um êxtase tão grande que, não raro, eu sacrificava todo o resto da minha vida por umas poucas horas dessa alegria". Bertrand Russel.
Davi Romero de Vasconcelos
M.Sc., D.Sc. in Computer Science, PUC-Rio
Professor at UFC (Universidade Federal do Ceará)
Email: <daviromero AT SPAMFREE ufc DOT br>
Currículo Lattes (CNPq, in Portuguese)
2. Publications (under construction)
3. Research in Progress
Towards an Implementation Theory via a Game Logic Approach Abstract
4. Game Analysis Logic (GAL)
Game Analysis Logic is a logic to reason about games in which a game is a model of the logic and a formula is an analysis that we would like to check if it is true in the model. GAL is a many-sorted modal first-order logic language based on the standard Computation Tree Logic. We have a prototype of a model-cheker that was written in Java. The GAL Model-Checker is available for Windows and Linux. A jar-file is also available. If you need some help please send an email to <daviromero AT ufc DOT br>
A preliminary version of the GAL Model-Checker Manual (in Portuguese)
RollGame is a meta-language to describe games. This language can be automatically translated into the SMV language from the available code below. After that one can perform formal analysis using SMV model checker. It is necessary to download Txl Programming Language (available at http://www.txl.ca/) and SMV (available at http://www.cs.cmu.edu/~modelcheck/).
Use the following command line to translate your code.
rtxl -s 100 %1 jogo_main.txl >%2
For example, the tictactoe game can be translated as follow.
rtxl -s 100 jogoSemEstr.ins jogo_main.txl > tictactoe.smv