Game modeling using WorkFlow nets

The objective of this article is to present an approach based on WorkFlow net and Linear Logic for the design process of video games. The main idea consists of representing the scenarios existing at a quest level by a particular type of Petri net called WorkFlow net. A kind of qualitative analysis based on the proof trees of linear logic can then be performed in order to prove the correctness of the soundness property which corresponds to a consistent quest from the point of view of the game. An extended version of theWorkFlow nets which allows the inclusion of discrete resources permits representing in a formal way, the different items that the player can find and use during the quests of the game.