Análise Formal de Gameplay com Redes de Petri Coloridas
Resumo
Introdução: o gameplay define as ações e interações do jogador perante desafios do jogo. Sua análise é útil para entender o comportamento do jogo, evitar erros do projeto ainda nas fases de design. Objetivo: apresentar uma abordagem formal para analisar o gameplay durante o game e level design, utilizando Redes de Petri Coloridas. Metodologia: o jogo é modelado em CPNs, onde atividades viram transições, estados viram lugares e o jogador é representado por uma ficha composta com seu progresso. A verificação formal exige definir propriedades-chave, como fluxo de eventos e ausência de impasses. Depois, executa-se a simulação do modelo e a análise de propriedades, baseando-se na validação da propriedade soundness, para calcular todas as marcações alcançáveis. Resultados: a verificação permite identificar automaticamente falhas de design e simular múltiplos cenários. A eficácia da abordagem foi comprovada com exemplos do jogo Detroit: Become Human.
Palavras-chave:
Gameplay, Redes de Petri Coloridas, Análise formal, Detroit: Become Human, Método formal
Referências
Adams, E. (2009). Fundamentals of Game Design. New Riders Publishing, USA, 2nd edition.
Araújo, M. e Roque, L. (2009). Modeling games with petri nets. In Proceedings of the 2009 DiGRA International Conference: Breaking New Ground: Innovation in Games, Play, Practice and Theory (DiGRA 2009), London, UK. DiGRA.
Barreto, F. M., de Freitas, J. C. J., Soares, M. S., e Julia, S. (2014). A straightforward introduction to formal methods using coloured petri nets. In International Conference on Enterprise Information Systems, volume 2, pages 145–152. SCITEPRESS.
Barreto, F. M. e Julia, S. (2021). Formal approach based on petri nets for modeling and verification of video games. Computing and Informatics, 40(1):216–248.
Bergonse, R. (2017). Fifty years on, what exactly is a videogame? an essentialistic definitional approach. The Computer Games Journal, 6(4):239–255.
Blow, J. (2004). Game development: Harder than you think: Ten or twenty years ago it was all fun and games. now it’s blood, sweat, and code. Queue, 1(10):28–37.
Cardoso, J. e Valette, R. (1997). Redes de petri. Editora da UFSC, Florianópolis, SC.
Guardiola, E. (2019). Gameplay definition: A game design perspective. Proceeding of the Game On 19 conference, pages 5–10.
Horrocks, I. (1999). Constructing the User Interface with Statecharts. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1st edition.
Jensen, K. (1996). An introduction to the practical use of coloured petri nets. Advanced Course on Petri Nets, 1(1):237–292.
Jensen, K. e Kristensen, L. M. (2009). Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, Berlin, Heidelberg, 1 edition.
Lankoski, P. e Björk, S. (2015). Formal analysis of gameplay. In Lankoski, P. e Björk, S., editors, Game Research Methods: An Overview, pages 23–35. ETC Press, Pittsburgh, PA.
Liu, Y. e Wu, W. (2013). Petri net modeling analysis of processes at clutch time in nba games. In 2013 IEEE International Conference of IEEE Region 10 (TENCON 2013), pages 1–4, Piscataway, NJ. IEEE.
Montero-Reyno, E. e Carsí-Cubel, J. Á. (2009). A platform-independent model for videogame gameplay specification. In Proceedings of DiGRA 2009 Conference: Breaking New Ground: Innovation in Games, Play, Practice and Theory, New York, NY, USA. Association for Computing Machinery.
Murata, T. (1989). Petri nets: Properties, analysis and applications. vol, 77:541–580.
Novak, J. (2012). Game Development Essentials: An Introduction. Delmar, Cengage Learning, Boston, Massachusetts, EUA, 3 edition.
Reuter, C., Göbel, S., e Steinmetz, R. (2015). Detecting structural errors in scene-based multiplayer games using automatically generated petri nets. In Proceedings of the 10th International Conference on the Foundations of Digital Games (FDG 2015), pages 1– 9, Pacific Grove, CA, USA. Society for the Advancement of the Science of Digital Games. Conference held June 22-25, 2015. Copyright held by author(s).
Rouse III, R. (2004). Game Design Theory and Practice. Wordware Publishing Inc., Plano, TX, USA, 2 edition.
Taghinezhad-Niar, A. e Pashazadeh, S. (2024). State-space analysis and complexity assessment of puzzle games using colored petri nets. International Journal of Web Research, 7(4):13–27.
van der Aalst, W. e Stahl, C. (2011). Modeling Business Processes: A Petri Net-Oriented Approach. The MIT Press, Cambridge, MA.
van der Aalst, W. M. P. e ter Hofstede, A. H. M. (2000). Verification of workflow task structures: A petri-net-based approach. Information Systems, 25(1):43–69.
Zhou, M. e Zurawski, R. (1995). Introduction to Petri Nets in Flexible and Agile Automation. Petri Nets in Flexible and Agile Automation. Kluwer Academic Publishers, Amsterdam, Netherlands.
Araújo, M. e Roque, L. (2009). Modeling games with petri nets. In Proceedings of the 2009 DiGRA International Conference: Breaking New Ground: Innovation in Games, Play, Practice and Theory (DiGRA 2009), London, UK. DiGRA.
Barreto, F. M., de Freitas, J. C. J., Soares, M. S., e Julia, S. (2014). A straightforward introduction to formal methods using coloured petri nets. In International Conference on Enterprise Information Systems, volume 2, pages 145–152. SCITEPRESS.
Barreto, F. M. e Julia, S. (2021). Formal approach based on petri nets for modeling and verification of video games. Computing and Informatics, 40(1):216–248.
Bergonse, R. (2017). Fifty years on, what exactly is a videogame? an essentialistic definitional approach. The Computer Games Journal, 6(4):239–255.
Blow, J. (2004). Game development: Harder than you think: Ten or twenty years ago it was all fun and games. now it’s blood, sweat, and code. Queue, 1(10):28–37.
Cardoso, J. e Valette, R. (1997). Redes de petri. Editora da UFSC, Florianópolis, SC.
Guardiola, E. (2019). Gameplay definition: A game design perspective. Proceeding of the Game On 19 conference, pages 5–10.
Horrocks, I. (1999). Constructing the User Interface with Statecharts. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1st edition.
Jensen, K. (1996). An introduction to the practical use of coloured petri nets. Advanced Course on Petri Nets, 1(1):237–292.
Jensen, K. e Kristensen, L. M. (2009). Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, Berlin, Heidelberg, 1 edition.
Lankoski, P. e Björk, S. (2015). Formal analysis of gameplay. In Lankoski, P. e Björk, S., editors, Game Research Methods: An Overview, pages 23–35. ETC Press, Pittsburgh, PA.
Liu, Y. e Wu, W. (2013). Petri net modeling analysis of processes at clutch time in nba games. In 2013 IEEE International Conference of IEEE Region 10 (TENCON 2013), pages 1–4, Piscataway, NJ. IEEE.
Montero-Reyno, E. e Carsí-Cubel, J. Á. (2009). A platform-independent model for videogame gameplay specification. In Proceedings of DiGRA 2009 Conference: Breaking New Ground: Innovation in Games, Play, Practice and Theory, New York, NY, USA. Association for Computing Machinery.
Murata, T. (1989). Petri nets: Properties, analysis and applications. vol, 77:541–580.
Novak, J. (2012). Game Development Essentials: An Introduction. Delmar, Cengage Learning, Boston, Massachusetts, EUA, 3 edition.
Reuter, C., Göbel, S., e Steinmetz, R. (2015). Detecting structural errors in scene-based multiplayer games using automatically generated petri nets. In Proceedings of the 10th International Conference on the Foundations of Digital Games (FDG 2015), pages 1– 9, Pacific Grove, CA, USA. Society for the Advancement of the Science of Digital Games. Conference held June 22-25, 2015. Copyright held by author(s).
Rouse III, R. (2004). Game Design Theory and Practice. Wordware Publishing Inc., Plano, TX, USA, 2 edition.
Taghinezhad-Niar, A. e Pashazadeh, S. (2024). State-space analysis and complexity assessment of puzzle games using colored petri nets. International Journal of Web Research, 7(4):13–27.
van der Aalst, W. e Stahl, C. (2011). Modeling Business Processes: A Petri Net-Oriented Approach. The MIT Press, Cambridge, MA.
van der Aalst, W. M. P. e ter Hofstede, A. H. M. (2000). Verification of workflow task structures: A petri-net-based approach. Information Systems, 25(1):43–69.
Zhou, M. e Zurawski, R. (1995). Introduction to Petri Nets in Flexible and Agile Automation. Petri Nets in Flexible and Agile Automation. Kluwer Academic Publishers, Amsterdam, Netherlands.
Publicado
29/09/2026
Como Citar
BORGES, Hugo Gabriel Batista; RAMOS, Lucas Emerenciano; FREITAS, Joslaine Cristina Jeske de; REZENDE, Críscilla Maia Costa; BARRETO, Franciny Medeiros.
Análise Formal de Gameplay com Redes de Petri Coloridas. In: SIMPÓSIO BRASILEIRO DE JOGOS E ENTRETENIMENTO DIGITAL (SBGAMES), 25. , 2026, Goiânia/GO.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 294-305.
DOI: https://doi.org/10.5753/sbgames.2026.25677.
