Formal Approach Based on Petri Nets for Modeling and Verification of Video Games

Authors

  • Franciny M. Barreto Federal University of Jataí, Department of Computer Science, Jataí – GO, Brazil
  • Stéphane Julia Federal University of Uberlândia, Faculty of Computation, Uberlândia – MG, Brazil

DOI:

https://doi.org/10.31577/cai_2021_1_216

Keywords:

Petri nets, video games, WorkFlow net, state graph, soundness verification, simulation, CPN tools

Abstract

Video games are complex systems that combine technical and artistic processes. The specification of this type of system is not a trivial task, making it necessary to use diagrams and charts to visually specify sets of requirements. Therefore, the underlying proposal of this work is to present an approach based on the formalism of Petri nets for aiding in the design process of video games. The activities of the game are represented by a specific type of Petri net called WorkFlow net. The definition of a topological map can be represented by state graphs. Using Colored Petri nets, it is possible to define formal communication mechanisms between the model of activity and the model of the map. The simulation of the timed models allows then to produce an estimated time that corresponds to the effective duration a player will need to complete a level of a game. Furthermore, a kind of Soundness property related to gameplay in a game Quest can be verified through state space analysis. For a better understanding of the approach, the video game Silent Hill II is used.

Downloads

Download data is not yet available.

Downloads

Published

2021-08-03

How to Cite

Barreto, F. M., & Julia, S. (2021). Formal Approach Based on Petri Nets for Modeling and Verification of Video Games. COMPUTING AND INFORMATICS, 40(1), 216–248. https://doi.org/10.31577/cai_2021_1_216

Most read articles by the same author(s)