Formal modelling and performance evaluation of puzzle type computer game using colored petri net

Detection and removal of existing faults in system during design process is one way of preventing failure and a solution for minimizing cost of production in different systems. Since it is not possible to study and analyze all systems directly, formal methods provide a chance for indirect examining of systems through modeling and a way to ensure the existence of answer and deadlock-freeness in different systems. Colored petri net is one of several formal methods that can be used as a powerful tool for modeling and performance evaluation of concurrent systems and computer games. In this paper, Sokoban game is modeled as a case study for n boxes using colored petri net. We introduce a method for modeling and analyzing automatic state space of computer puzzle games in order to compute their complexity and prove their behavioral properties through colored petri nets. According to this analysis, there is no real deadlock in this model which indicates that the proposed model is correct. This method can be applied for modeling similar games