Back to Search Start Over

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

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

Authors :
Stéphane Julia
Franciny Medeiros Barreto
Source :
COMPUTING AND INFORMATICS; Vol. 40 No. 1 (2021): Computing and Informatics; 216–248
Publication Year :
2021
Publisher :
Institute of Informatics, Slovak Academy of Sciences, 2021.

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.

Details

Language :
English
ISSN :
13359150 and 25858807
Database :
OpenAIRE
Journal :
COMPUTING AND INFORMATICS
Accession number :
edsair.doi.dedup.....f8985581cd58cdd02a0cb8106eca6e43