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
- 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.
- Subjects :
- Soundness
WorkFlow net
CPN tools
Theoretical computer science
Computer science
General Engineering
ComputingMilieux_PERSONALCOMPUTING
Petri nets
video games
Petri net
simulation
68-M99
CPN Tools
state graph
State space
soundness verification
State (computer science)
Topological map
Engineering design process
Video game
Subjects
Details
- Language :
- English
- ISSN :
- 13359150 and 25858807
- Database :
- OpenAIRE
- Journal :
- COMPUTING AND INFORMATICS
- Accession number :
- edsair.doi.dedup.....f8985581cd58cdd02a0cb8106eca6e43